From 132c710cbe6e7987d6662775fc4be0acb4f194b1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 24 Oct 2022 22:01:04 +0100 Subject: [PATCH 1/8] =?UTF-8?q?deprecating=20=5F=E2=89=BA=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Fin/Base.agda | 17 ++++++++++++++--- src/Data/Fin/Properties.agda | 17 +++++++++++++---- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 06c4581337..ac5d0e5b89 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -290,9 +290,6 @@ _>_ : IRel Fin 0ℓ i > j = toℕ i ℕ.> toℕ j -data _≺_ : ℕ → ℕ → Set where - _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n - ------------------------------------------------------------------------ -- An ordering view. @@ -335,3 +332,17 @@ NB argument order has been flipped: the left-hand argument is the Fin m the right-hand is the Nat index increment." #-} +data _≺_ : ℕ → ℕ → Set where + _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n +{- +≺toFin : ∀ {m n} → m ≺ n → Fin n +≺toFin (n ≻toℕ i) = i +-} +{-# WARNING_ON_USAGE _≺_ +"Warning: _≺_ was deprecated in v2.0. +Please use equivalent relation _<_ instead." +#-} +{-# WARNING_ON_USAGE _≻toℕ_ +"Warning: _≻toℕ_ was deprecated in v2.0. +Please use toℕ Date: Mon, 24 Oct 2022 22:09:56 +0100 Subject: [PATCH 2/8] factorise the to-be-deprecated properties --- src/Data/Fin/Base.agda | 5 +--- src/Data/Fin/Properties.agda | 46 ++++++++++++++++++++---------------- 2 files changed, 26 insertions(+), 25 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index ac5d0e5b89..8b210c837e 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -334,10 +334,7 @@ the right-hand is the Nat index increment." #-} data _≺_ : ℕ → ℕ → Set where _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n -{- -≺toFin : ∀ {m n} → m ≺ n → Fin n -≺toFin (n ≻toℕ i) = i --} + {-# WARNING_ON_USAGE _≺_ "Warning: _≺_ was deprecated in v2.0. Please use equivalent relation _<_ instead." diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 6ec56635a5..2285452035 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -758,27 +758,6 @@ lift-injective f inj (suc k) {zero} {zero} eq = refl lift-injective f inj (suc k) {suc _} {suc _} eq = cong suc (lift-injective f inj k (suc-injective eq)) ------------------------------------------------------------------------- --- _≺_ ------------------------------------------------------------------------- - -private - - ≺⇒< : _≺_ ⇒ ℕ._<_ - ≺⇒< (n ≻toℕ i) = toℕ Date: Mon, 24 Oct 2022 22:27:52 +0100 Subject: [PATCH 3/8] now deprecate those properties --- src/Data/Fin/Base.agda | 24 ++++++++++++++++++++++++ src/Data/Fin/Properties.agda | 9 ++------- 2 files changed, 26 insertions(+), 7 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 8b210c837e..b93941f949 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -332,9 +332,33 @@ NB argument order has been flipped: the left-hand argument is the Fin m the right-hand is the Nat index increment." #-} + +------------------------------------------------------------------------ +-- _≺_ data _≺_ : ℕ → ℕ → Set where _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n +------------------------------------------------------------------------ +-- properties of _≺_ +-- introduce new proofs, actually simplified compared to original +-- so that Data.Fin.Properties doesn't mention the constructor + +private + + z≺s : ∀ {n} → zero ≺ suc n + z≺s = _ ≻toℕ zero + + s≺s : ∀ {m n} → m ≺ n → suc m ≺ suc n + s≺s (n ≻toℕ i) = (suc n) ≻toℕ (suc i) + +-- new lemma, nowhere else used except to define deprecated property later + +<⇒≺ : ℕ._<_ ⇒ _≺_ +<⇒≺ {zero} {n@(suc _)} z Date: Mon, 24 Oct 2022 23:10:33 +0100 Subject: [PATCH 4/8] spacing plus further simplification, but warnings remain --- src/Data/Fin/Base.agda | 6 +++--- src/Data/Fin/Properties.agda | 3 ++- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index b93941f949..1c4ffd38b9 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -335,6 +335,7 @@ the right-hand is the Nat index increment." ------------------------------------------------------------------------ -- _≺_ + data _≺_ : ℕ → ℕ → Set where _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n @@ -354,11 +355,10 @@ private -- new lemma, nowhere else used except to define deprecated property later <⇒≺ : ℕ._<_ ⇒ _≺_ -<⇒≺ {zero} {n@(suc _)} z Date: Tue, 25 Oct 2022 18:23:56 +0100 Subject: [PATCH 5/8] [fix] issue #1726 --- CHANGELOG.md | 8 ++++++++ src/Data/Fin/Base.agda | 20 -------------------- src/Data/Fin/Properties.agda | 14 ++++++++++++++ 3 files changed, 22 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 58ca827765..95e68a384c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -866,6 +866,11 @@ Deprecated names raise ↦ _↑ʳ_ ``` + Issue #1726: the relation `_≺_` and its single constructor `_≻toℕ_` + have been deprecated in favour of their extensional equivalent `_<_` + but omitting the inversion principle which pattern matching on `_≻toℕ_` + would achieve; this instead is proxied by the property `Data.Fin.Properties.toℕ<`. + * In `Data.Fin.Properties`: ``` toℕ-raise ↦ toℕ-↑ʳ @@ -876,6 +881,9 @@ Deprecated names eq? ↦ inj⇒≟ ``` + Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated + in favour of their proxy counterparts `<⇒<′` and `<′⇒<`. + * In `Data.Fin.Permutation.Components`: ``` reverse ↦ Data.Fin.Base.opposite diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 1c4ffd38b9..6f943ac1aa 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -332,32 +332,12 @@ NB argument order has been flipped: the left-hand argument is the Fin m the right-hand is the Nat index increment." #-} - ------------------------------------------------------------------------ -- _≺_ data _≺_ : ℕ → ℕ → Set where _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n ------------------------------------------------------------------------- --- properties of _≺_ --- introduce new proofs, actually simplified compared to original --- so that Data.Fin.Properties doesn't mention the constructor - -private - - z≺s : ∀ {n} → zero ≺ suc n - z≺s = _ ≻toℕ zero - - s≺s : ∀ {m n} → m ≺ n → suc m ≺ suc n - s≺s (n ≻toℕ i) = (suc n) ≻toℕ (suc i) - --- new lemma, nowhere else used except to define deprecated property later - -<⇒≺ : ℕ._<_ ⇒ _≺_ -<⇒≺ {zero} z Date: Tue, 25 Oct 2022 18:41:02 +0100 Subject: [PATCH 6/8] overlooked import; warning suppressed --- src/Data/Fin/Induction.agda | 62 ++++++++++++++++++++++++++----------- 1 file changed, 44 insertions(+), 18 deletions(-) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index 401c95b38a..a5b0fac2b8 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -5,6 +5,7 @@ ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --warn=noUserWarning #-} -- for issue #1726 open import Data.Fin.Base open import Data.Fin.Properties @@ -94,24 +95,6 @@ private ... | no n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁) where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i))))) ------------------------------------------------------------------------- --- Induction over _≺_ - -≺-Rec : RecStruct ℕ ℓ ℓ -≺-Rec = WfRec _≺_ - -≺-wellFounded : WellFounded _≺_ -≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded - -module _ {ℓ} where - open WF.All ≺-wellFounded ℓ public - renaming - ( wfRecBuilder to ≺-recBuilder - ; wfRec to ≺-rec - ) - hiding (wfRec-builder) - - ------------------------------------------------------------------------ -- Well-foundedness of other (strict) partial orders on Fin @@ -159,3 +142,46 @@ module _ {_≈_ : Rel (Fin n) ℓ} where WellFounded (flip (ToStrict._<_ _≈_ _⊑_)) po-noetherian isPO = spo-noetherian (ToStrict.<-isStrictPartialOrder _≈_ _ isPO) + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +------------------------------------------------------------------------ +-- Induction over _≺_ + +≺-Rec : RecStruct ℕ ℓ ℓ +≺-Rec = WfRec _≺_ + +≺-wellFounded : WellFounded _≺_ +≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded + +module _ {ℓ} where + open WF.All ≺-wellFounded ℓ public + renaming + ( wfRecBuilder to ≺-recBuilder + ; wfRec to ≺-rec + ) + hiding (wfRec-builder) + +{-# WARNING_ON_USAGE ≺-Rec +"Warning: ≺-Rec was deprecated in v2.0. +Please use <-Rec instead." +#-} +{-# WARNING_ON_USAGE ≺-wellFounded +"Warning: ≺-wellFounded was deprecated in v2.0. +Please use <-wellFounded instead." +#-} +{-# WARNING_ON_USAGE ≺-recBuilder +"Warning: ≺-recBuilder was deprecated in v2.0. +Please use <-recBuilder instead." +#-} +{-# WARNING_ON_USAGE ≺-rec +"Warning: ≺-rec was deprecated in v2.0. +Please use <-rec instead." +#-} + From cbd1ef25f5943feb6516a602e69f4fd9802c929e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 26 Oct 2022 10:29:04 +0100 Subject: [PATCH 7/8] resolved conversations --- src/Data/Fin/Base.agda | 3 --- src/Data/Fin/Induction.agda | 8 +++----- src/Data/Fin/Properties.agda | 6 +----- 3 files changed, 4 insertions(+), 13 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 6f943ac1aa..93ea438156 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -332,13 +332,10 @@ NB argument order has been flipped: the left-hand argument is the Fin m the right-hand is the Nat index increment." #-} ------------------------------------------------------------------------- --- _≺_ data _≺_ : ℕ → ℕ → Set where _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n --- now do the deprecation! {-# WARNING_ON_USAGE _≺_ "Warning: _≺_ was deprecated in v2.0. Please use equivalent relation _<_ instead." diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index a5b0fac2b8..954aac6f48 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -5,7 +5,7 @@ ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -{-# OPTIONS --warn=noUserWarning #-} -- for issue #1726 +{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726) open import Data.Fin.Base open import Data.Fin.Properties @@ -21,7 +21,8 @@ open import Function.Base using (flip; _$_) open import Induction open import Induction.WellFounded as WF open import Level using (Level) -open import Relation.Binary using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder) +open import Relation.Binary + using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder) import Relation.Binary.Construct.Converse as Converse import Relation.Binary.Construct.Flip as Flip import Relation.Binary.Construct.NonStrictToStrict as ToStrict @@ -151,9 +152,6 @@ module _ {_≈_ : Rel (Fin n) ℓ} where -- Version 2.0 ------------------------------------------------------------------------- --- Induction over _≺_ - ≺-Rec : RecStruct ℕ ℓ ℓ ≺-Rec = WfRec _≺_ diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 38b702f166..07c7ae982b 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -6,7 +6,7 @@ ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -{-# OPTIONS --warn=noUserWarning #-} -- for issue #1726 +{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726) module Data.Fin.Properties where @@ -1122,10 +1122,6 @@ eq? = inj⇒≟ "Warning: eq? was deprecated in v2.0. Please use inj⇒≟ instead." #-} ------------------------------------------------------------------------- --- deprecated properties of deprecated _≺_ --- introduce new proofs, actually simplified compared to original --- so that Data.Fin.Properties doesn't mention the constructor private From f03006273c123063f0ac95482d264c30a98654d5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 28 Oct 2022 12:09:43 +0100 Subject: [PATCH 8/8] resolved conversation re `CHANGELOG`? --- CHANGELOG.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f47d33f40d..80ce0dda32 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -893,6 +893,19 @@ Deprecated names but omitting the inversion principle which pattern matching on `_≻toℕ_` would achieve; this instead is proxied by the property `Data.Fin.Properties.toℕ<`. +* In `Data.Fin.Induction`: + ``` + ≺-Rec + ≺-wellFounded + ≺-recBuilder + ≺-rec + ``` + + As with Issue #1726 above: the deprecation of relation `_≺_` means that these definitions + associated with wf-recursion are deprecated in favour of their `_<_` counterparts. + But it's not quite sensible to say that these definiton should be *renamed* to *anything*, + least of all those counterparts... the type confusion would be intolerable. + * In `Data.Fin.Properties`: ``` toℕ-raise ↦ toℕ-↑ʳ