From 1f1a90a7bea6a2a8bcb5e875dccca7378fd68c8d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 21 Jan 2024 09:25:10 +0000 Subject: [PATCH 01/19] additional proofs and patterns in `Data.Nat.Properties` --- CHANGELOG.md | 8 ++++++- src/Data/Nat/Properties.agda | 42 +++++++++++++++++++++++------------- 2 files changed, 34 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c690740a1e..5a32b1f715 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -75,7 +75,7 @@ Additions to existing modules nonZeroDivisor : DivMod dividend divisor → NonZero divisor ``` -* Added new proofs in `Data.Nat.Properties`: +* Added new proofs and pattern synonyms in `Data.Nat.Properties`: ```agda m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o m Date: Sun, 21 Jan 2024 10:03:46 +0000 Subject: [PATCH 02/19] added two projections; refactored `pad*` operations --- src/Data/Vec/Bounded/Base.agda | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda index 7476afb2d4..9b010abbfd 100644 --- a/src/Data/Vec/Bounded/Base.agda +++ b/src/Data/Vec/Bounded/Base.agda @@ -43,20 +43,27 @@ record Vec≤ (A : Set a) (n : ℕ) : Set a where vec : Vec A length .bound : length ≤ n +-- projection to recompute irrelevant field +isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n +isBounded as@(_ , m≤n) = recompute (_ ℕ.≤? _) m≤n + ------------------------------------------------------------------------ -- Conversion functions +toVec : (as : Vec≤ A n) → Vec A (Vec≤.length as) +toVec as@(vs , _) = vs + fromVec : Vec A n → Vec≤ A n fromVec v = v , ℕ.≤-refl padRight : A → Vec≤ A n → Vec A n -padRight a (vs , m≤n) - with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n) +padRight a as@(vs , m≤n) + with ℕ.≤-offset k ← ℕ.≤-proof (isBounded as) = vs Vec.++ Vec.replicate k a padLeft : A → Vec≤ A n → Vec A n padLeft a record { length = m ; vec = vs ; bound = m≤n } - with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n) + with ℕ.≤-offset k ← ℕ.≤-proof (recompute (_ ℕ.≤? _) m≤n) rewrite ℕ.+-comm m k = Vec.replicate k a Vec.++ vs @@ -72,7 +79,7 @@ private padBoth : A → A → Vec≤ A n → Vec A n padBoth aₗ aᵣ record { length = m ; vec = vs ; bound = m≤n } - with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n) + with ℕ.≤-offset k ← ℕ.≤-proof (recompute (_ ℕ.≤? _) m≤n) rewrite split m k = Vec.replicate ⌊ k /2⌋ aₗ Vec.++ vs @@ -83,7 +90,7 @@ fromList : (as : List A) → Vec≤ A (List.length as) fromList = fromVec ∘ Vec.fromList toList : Vec≤ A n → List A -toList = Vec.toList ∘ Vec≤.vec +toList = Vec.toList ∘ toVec ------------------------------------------------------------------------ -- Creating new Vec≤ vectors From b03b0a6c309a69b5bd968f7ea20f14f37d41bb48 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 21 Jan 2024 10:10:30 +0000 Subject: [PATCH 03/19] `CHANGELOG` --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5a32b1f715..5bde490536 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -96,5 +96,11 @@ Additions to existing modules map : (Char → Char) → String → String ``` +* Added new functions in `Data.Vec.Bounded.Base`: + ```agda + isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n + toVec : (as : Vec≤ A n) → Vec A (Vec≤.length as) + ``` + * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can be used infix. From 2c06c98e9038c85ef4a7c184879d32dbc4e1274a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 5 Feb 2024 09:13:11 +0000 Subject: [PATCH 04/19] removed one more use --- src/Data/Nat/DivMod.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index 5ff23e4c72..7fbd1abf59 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -104,7 +104,7 @@ m%n≤m : ∀ m n .{{_ : NonZero n}} → m % n ≤ m m%n≤m m (suc n-1) = a[modₕ]n≤a 0 m n-1 m≤n⇒m%n≡m : m ≤ n → m % suc n ≡ m -m≤n⇒m%n≡m {m = m} m≤n with ≤″-offset k ← ≤⇒≤″ m≤n +m≤n⇒m%n≡m {m = m} m≤n with ≤-offset k ← ≤-proof m≤n = a≤n⇒a[modₕ]n≡a 0 (m + k) m k m Date: Mon, 5 Feb 2024 09:36:43 +0000 Subject: [PATCH 05/19] =?UTF-8?q?removed=20final=20uses=20of=20`<=E2=80=B3?= =?UTF-8?q?-offset`=20outside=20`Data.Nat.Base|Properties`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Fin/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 303cf64905..e6b2f5e8aa 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -246,9 +246,9 @@ fromℕ<-injective (suc _) (suc _) {o = suc _} m Date: Sun, 24 Mar 2024 09:35:41 +0000 Subject: [PATCH 06/19] =?UTF-8?q?rename=20`=E2=89=A4-proof`=20to=20`m?= =?UTF-8?q?=E2=89=A4n=E2=87=92=E2=88=83[o]m+o=E2=89=A1n`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 4 ++-- src/Data/Nat/DivMod.agda | 2 +- src/Data/Nat/Properties.agda | 4 ++-- src/Data/Vec/Bounded/Base.agda | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5bde490536..44420d5a87 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -84,8 +84,8 @@ Additions to existing modules pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n - <⇒<″ : _<_ ⇒ _<″_ - ≤-proof : m ≤ n → ∃ λ k → m + k ≡ n + <⇒<″ : _<_ ⇒ _<″_ + m≤n⇒∃[o]m+o≡n : m ≤ n → ∃ λ k → m + k ≡ n pattern ≤-offset k = k , refl pattern <-offset k = ≤-offset k diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index 7fbd1abf59..5c8aa7029f 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -104,7 +104,7 @@ m%n≤m : ∀ m n .{{_ : NonZero n}} → m % n ≤ m m%n≤m m (suc n-1) = a[modₕ]n≤a 0 m n-1 m≤n⇒m%n≡m : m ≤ n → m % suc n ≡ m -m≤n⇒m%n≡m {m = m} m≤n with ≤-offset k ← ≤-proof m≤n +m≤n⇒m%n≡m {m = m} m≤n with ≤-offset k ← m≤n⇒∃[o]m+o≡n m≤n = a≤n⇒a[modₕ]n≡a 0 (m + k) m k m Date: Sun, 24 Mar 2024 09:50:24 +0000 Subject: [PATCH 07/19] removed new pattern synonyms --- CHANGELOG.md | 7 ++----- src/Data/Nat/DivMod.agda | 3 ++- src/Data/Nat/Properties.agda | 5 +---- src/Data/Vec/Bounded/Base.agda | 8 ++++---- 4 files changed, 9 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 44420d5a87..9796b017a8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -75,7 +75,7 @@ Additions to existing modules nonZeroDivisor : DivMod dividend divisor → NonZero divisor ``` -* Added new proofs and pattern synonyms in `Data.Nat.Properties`: +* Added new proofs in `Data.Nat.Properties`: ```agda m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o m Date: Sun, 24 Mar 2024 15:08:07 +0000 Subject: [PATCH 08/19] interim commit: deprecate everything! --- src/Data/Fin/Base.agda | 7 +++++- src/Data/Nat/Base.agda | 44 ++++++++++++++++++++++++------------ src/Data/Nat/Properties.agda | 40 +++++++++++++++++++------------- src/Data/Nat/WithK.agda | 3 ++- 4 files changed, 62 insertions(+), 32 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index d762e10007..e01f47c9c3 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -11,6 +11,7 @@ module Data.Fin.Base where +open import Algebra.Definitions.RawMagma using (_,_) open import Data.Bool.Base using (Bool; T) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂) @@ -75,7 +76,11 @@ fromℕ< {suc m} {suc _} m″_ : Rel ℕ 0ℓ m >″ n = n <″ m --- Smart constructors of _≤″_ and _<″_ - -pattern ≤″-offset k = less-than-or-equal {k = k} refl -pattern <″-offset k = ≤″-offset k - --- Smart destructors of _<″_ - -s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n -s≤″s⁻¹ (≤″-offset k) = ≤″-offset k - -s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n -s<″s⁻¹ (<″-offset k) = <″-offset k - -- _≤‴_: this definition is useful for induction with an upper bound. data _≤‴_ : ℕ → ℕ → Set where @@ -429,5 +416,34 @@ compare (suc m) (suc n) with compare m n -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 2.0 +-- Version 2.1 + +-- Smart constructors of _≤″_ and _<″_ +pattern less-than-or-equal {k} eq = k , eq +{-# WARNING_ON_USAGE less-than-or-equal +"Warning: less-than-or-equal was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_,_) instead. " +#-} +pattern ≤″-offset k = k , refl +{-# WARNING_ON_USAGE ≤″-offset +"Warning: ≤″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +#-} +pattern <″-offset k = k , refl +{-# WARNING_ON_USAGE <″-offset +"Warning: <″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +#-} + +-- Smart destructors of _<″_ + +s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n +s≤″s⁻¹ (k , refl) = k , refl +{-# WARNING_ON_USAGE s≤″s⁻¹ +"Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +#-} + +s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n +s<″s⁻¹ (k , refl) = k , refl +{-# WARNING_ON_USAGE s<″s⁻¹ +"Warning: s<″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +#-} + diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 6be03a3c4c..23671a5d11 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -13,6 +13,7 @@ module Data.Nat.Properties where open import Axiom.UniquenessOfIdentityProofs open import Algebra.Bundles +open import Algebra.Definitions.RawMagma using (_,_) open import Algebra.Morphism open import Algebra.Consequences.Propositional open import Algebra.Construct.NaturalChoice.Base @@ -36,7 +37,7 @@ open import Relation.Binary open import Relation.Binary.Consequences using (flip-Connex) open import Relation.Binary.PropositionalEquality open import Relation.Nullary hiding (Irrelevant) -open import Relation.Nullary.Decidable using (True; via-injection; map′) +open import Relation.Nullary.Decidable using (True; via-injection; map′; recompute) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (fromEquivalence) @@ -2104,23 +2105,31 @@ n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n) -- equivalence of _≤″_ to _≤_ ≤⇒≤″ : _≤_ ⇒ _≤″_ -≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n +≤⇒≤″ = (_ ,_) ∘ m+[n∸m]≡n <⇒<″ : _<_ ⇒ _<″_ <⇒<″ = ≤⇒≤″ ≤″⇒≤ : _≤″_ ⇒ _≤_ -≤″⇒≤ (≤″-offset k) = m≤m+n _ k +≤″⇒≤ (k , refl) = m≤m+n _ k -- equivalence to the old definition of _≤″_ -≤″-proof : (le : m ≤″ n) → let less-than-or-equal {k} _ = le in m + k ≡ n -≤″-proof (less-than-or-equal prf) = prf +≤″-proof : (le : m ≤″ n) → let k , _ = le in m + k ≡ n +≤″-proof (_ , prf) = prf --- yielding corresponding proof _≤″_ +-- yielding analogous proof for _≤_ -m≤n⇒∃[o]m+o≡n : m ≤ n → ∃ λ k → m + k ≡ n -m≤n⇒∃[o]m+o≡n le with less-than-or-equal {k} refl ← ≤⇒≤″ le = k , refl +m≤n⇒∃[o]m+o≡n : .(m ≤ n) → ∃ λ k → m + k ≡ n +m≤n⇒∃[o]m+o≡n m≤n = _ , m+[n∸m]≡n (recompute (_ ≤? _) m≤n) + +-- and a 'guarded' version of monus + +guarded-∸ : ∀ n m → .(m ≤ n) → ℕ +guarded-∸ n m m≤n = let k , _ = m≤n⇒∃[o]m+o≡n (recompute (m ≤? n) m≤n) in k + +guarded-∸≗∸ : ∀ {m n} → .(m≤n : m ≤ n) → guarded-∸ n m m≤n ≡ n ∸ m +guarded-∸≗∸ m≤n = refl -- equivalence of _<″_ to _<ᵇ_ @@ -2134,7 +2143,7 @@ m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _) <ᵇ⇒<″ {m} {n} = <⇒<″ ∘ (<ᵇ⇒< m n) <″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n) -<″⇒<ᵇ {m} (<″-offset k) = <⇒<ᵇ (m≤m+n (suc m) k) +<″⇒<ᵇ {m} (k , refl) = <⇒<ᵇ (m≤m+n (suc m) k) -- NB: we use the builtin function `_<ᵇ_ : (m n : ℕ) → Bool` here so -- that the function quickly decides whether to return `yes` or `no`. @@ -2148,7 +2157,7 @@ _<″?_ : Decidable _<″_ m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n)) _≤″?_ : Decidable _≤″_ -zero ≤″? n = yes (≤″-offset n) +zero ≤″? n = yes (n , refl) suc m ≤″? n = m <″? n _≥″?_ : Decidable _≥″_ @@ -2158,10 +2167,10 @@ _>″?_ : Decidable _>″_ _>″?_ = flip _<″?_ ≤″-irrelevant : Irrelevant _≤″_ -≤″-irrelevant {m} (less-than-or-equal eq₁) - (less-than-or-equal eq₂) +≤″-irrelevant {m} (_ , eq₁) + (_ , eq₂) with refl ← +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂)) - = cong less-than-or-equal (≡-irrelevant eq₁ eq₂) + = cong (_ ,_) (≡-irrelevant eq₁ eq₂) <″-irrelevant : Irrelevant _<″_ <″-irrelevant = ≤″-irrelevant @@ -2177,8 +2186,8 @@ _>″?_ = flip _<″?_ ------------------------------------------------------------------------ ≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n -≤‴⇒≤″ {m = m} ≤‴-refl = less-than-or-equal {k = 0} (+-identityʳ m) -≤‴⇒≤″ {m = m} (≤‴-step m≤n) = less-than-or-equal (trans (+-suc m _) (≤″-proof (≤‴⇒≤″ m≤n))) +≤‴⇒≤″ {m = m} ≤‴-refl = 0 , (+-identityʳ m) +≤‴⇒≤″ {m = m} (≤‴-step m≤n) = _ , trans (+-suc m _) (≤″-proof (≤‴⇒≤″ m≤n)) m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m}) @@ -2401,4 +2410,3 @@ open Data.Nat.Base public {-# WARNING_ON_USAGE <-transˡ "Warning: <-transˡ was deprecated in v2.0. Please use <-≤-trans instead. " #-} - diff --git a/src/Data/Nat/WithK.agda b/src/Data/Nat/WithK.agda index 49966a93f0..bb6a97a7aa 100644 --- a/src/Data/Nat/WithK.agda +++ b/src/Data/Nat/WithK.agda @@ -8,8 +8,9 @@ module Data.Nat.WithK where +open import Algebra.Definitions.RawMagma using (_,_) open import Data.Nat.Base open import Relation.Binary.PropositionalEquality.WithK ≤″-erase : ∀ {m n} → m ≤″ n → m ≤″ n -≤″-erase (less-than-or-equal eq) = less-than-or-equal (≡-erase eq) +≤″-erase (_ , eq) = _ , ≡-erase eq From 5091a4e74a5ac715401263adcb66d77eaac4d424 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 24 Mar 2024 17:58:16 +0000 Subject: [PATCH 09/19] add guarded monus; make arguments more irrelevant --- src/Data/Nat/Properties.agda | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 23671a5d11..61650f2207 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -2126,7 +2126,7 @@ m≤n⇒∃[o]m+o≡n m≤n = _ , m+[n∸m]≡n (recompute (_ ≤? _) m≤n) -- and a 'guarded' version of monus guarded-∸ : ∀ n m → .(m ≤ n) → ℕ -guarded-∸ n m m≤n = let k , _ = m≤n⇒∃[o]m+o≡n (recompute (m ≤? n) m≤n) in k +guarded-∸ n m m≤n = let k , _ = m≤n⇒∃[o]m+o≡n m≤n in k guarded-∸≗∸ : ∀ {m n} → .(m≤n : m ≤ n) → guarded-∸ n m m≤n ≡ n ∸ m guarded-∸≗∸ m≤n = refl @@ -2167,8 +2167,7 @@ _>″?_ : Decidable _>″_ _>″?_ = flip _<″?_ ≤″-irrelevant : Irrelevant _≤″_ -≤″-irrelevant {m} (_ , eq₁) - (_ , eq₂) +≤″-irrelevant {m} (_ , eq₁) (_ , eq₂) with refl ← +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂)) = cong (_ ,_) (≡-irrelevant eq₁ eq₂) @@ -2186,7 +2185,7 @@ _>″?_ = flip _<″?_ ------------------------------------------------------------------------ ≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n -≤‴⇒≤″ {m = m} ≤‴-refl = 0 , (+-identityʳ m) +≤‴⇒≤″ {m = m} ≤‴-refl = 0 , +-identityʳ m ≤‴⇒≤″ {m = m} (≤‴-step m≤n) = _ , trans (+-suc m _) (≤″-proof (≤‴⇒≤″ m≤n)) m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n From 59986ffd85326800926207dafb553a431483f130 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 24 Mar 2024 17:58:40 +0000 Subject: [PATCH 10/19] fixed up `CHANGELOG` --- CHANGELOG.md | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9796b017a8..8d4a5ce245 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,17 @@ Deprecated modules Deprecated names ---------------- +* In `Data.Nat.Base`: the following pattern synonyms and definitions are all + deprecated in favour of direct pattern matching on (_,_) + ```agda + pattern less-than-or-equal {k} eq = k , eq + pattern ≤″-offset k = k , refl + pattern <″-offset k = k , refl + + s≤″s⁻¹ + s<″s⁻¹ + ``` + * In `Data.Nat.Divisibility.Core`: ```agda *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ @@ -75,7 +86,7 @@ Additions to existing modules nonZeroDivisor : DivMod dividend divisor → NonZero divisor ``` -* Added new proofs in `Data.Nat.Properties`: +* Added new proofs and 'guarded' version of `_∸_` in `Data.Nat.Properties`: ```agda m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o m Date: Sun, 24 Mar 2024 18:02:58 +0000 Subject: [PATCH 11/19] propagate use of irrelevance --- src/Data/Vec/Bounded/Base.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda index 1552fa4eaa..fa7eb758ed 100644 --- a/src/Data/Vec/Bounded/Base.agda +++ b/src/Data/Vec/Bounded/Base.agda @@ -58,12 +58,12 @@ fromVec v = v , ℕ.≤-refl padRight : A → Vec≤ A n → Vec A n padRight a as@(vs , m≤n) - with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n (isBounded as) + with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n m≤n = vs Vec.++ Vec.replicate k a padLeft : A → Vec≤ A n → Vec A n padLeft a record { length = m ; vec = vs ; bound = m≤n } - with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n (recompute (_ ℕ.≤? _) m≤n) + with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n m≤n rewrite ℕ.+-comm m k = Vec.replicate k a Vec.++ vs @@ -79,7 +79,7 @@ private padBoth : A → A → Vec≤ A n → Vec A n padBoth aₗ aᵣ record { length = m ; vec = vs ; bound = m≤n } - with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n (recompute (_ ℕ.≤? _) m≤n) + with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n m≤n rewrite split m k = Vec.replicate ⌊ k /2⌋ aₗ Vec.++ vs From a9e9a2e37acab8ddd11ca901057d7522f2f92caa Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 24 Mar 2024 18:18:36 +0000 Subject: [PATCH 12/19] =?UTF-8?q?tidy=20up=20deprecations;=20reinstate=20`?= =?UTF-8?q?s<=E2=80=B3s=E2=81=BB=C2=B9`=20for=20`Data.Fin.Properties`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Fin/Base.agda | 6 +----- src/Data/Nat/Base.agda | 15 +++++---------- 2 files changed, 6 insertions(+), 15 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index e01f47c9c3..46ea5b8a7b 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -76,11 +76,7 @@ fromℕ< {suc m} {suc _} m″_ _≤″_ : (m n : ℕ) → Set _≤″_ = _∣ˡ_ +-rawMagma -pattern less-than-or-equal {k} proof = k , proof - _<″_ : Rel ℕ 0ℓ m <″ n = suc m ≤″ n @@ -374,6 +372,11 @@ m ≥″ n = n ≤″ m _>″_ : Rel ℕ 0ℓ m >″ n = n <″ m +-- Smart destructor of _<″_ + +s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n +s<″s⁻¹ (k , refl) = k , refl + -- _≤‴_: this definition is useful for induction with an upper bound. data _≤‴_ : ℕ → ℕ → Set where @@ -439,11 +442,3 @@ s≤″s⁻¹ (k , refl) = k , refl {-# WARNING_ON_USAGE s≤″s⁻¹ "Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " #-} - -s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n -s<″s⁻¹ (k , refl) = k , refl -{-# WARNING_ON_USAGE s<″s⁻¹ -"Warning: s<″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " -#-} - - From a78538a3816c82c76cd9c1421e37582a3fb28adc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 25 Mar 2024 12:22:27 +0000 Subject: [PATCH 13/19] tightened up the deprecation story --- CHANGELOG.md | 4 +--- src/Data/Nat/Base.agda | 8 ++++---- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 66e179f8dd..4c72105c6e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -50,14 +50,12 @@ Deprecated names ``` * In `Data.Nat.Base`: the following pattern synonyms and definitions are all - deprecated in favour of direct pattern matching on (_,_) + deprecated in favour of direct pattern matching on `Algebra.RawMagma._∣ˡ_._,_` ```agda pattern less-than-or-equal {k} eq = k , eq pattern ≤″-offset k = k , refl pattern <″-offset k = k , refl - s≤″s⁻¹ - s<″s⁻¹ ``` * In `Data.Nat.Divisibility.Core`: diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index a5c03839f0..178106a978 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -424,15 +424,15 @@ compare (suc m) (suc n) with compare m n -- Smart constructors of _≤″_ and _<″_ pattern less-than-or-equal {k} eq = k , eq {-# WARNING_ON_USAGE less-than-or-equal -"Warning: less-than-or-equal was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_,_) instead. " +"Warning: less-than-or-equal was deprecated in v2.1. Please match directly on proofs of ≤″ using constructor Algebra.RawMagma._∣ˡ_._,_ instead. " #-} pattern ≤″-offset k = k , refl {-# WARNING_ON_USAGE ≤″-offset -"Warning: ≤″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +"Warning: ≤″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.RawMagma._∣ˡ_ instead. " #-} pattern <″-offset k = k , refl {-# WARNING_ON_USAGE <″-offset -"Warning: <″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +"Warning: <″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.RawMagma._∣ˡ_ instead. " #-} -- Smart destructors of _<″_ @@ -440,5 +440,5 @@ pattern <″-offset k = k , refl s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n s≤″s⁻¹ (k , refl) = k , refl {-# WARNING_ON_USAGE s≤″s⁻¹ -"Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) instead. " +"Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.RawMagma._∣ˡ_ instead. " #-} From ca44eb0bc2100b1a59b766d124d89948af2df244 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 25 Mar 2024 13:46:43 +0000 Subject: [PATCH 14/19] paragraph on use of `pattern` synonyms --- doc/style-guide.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/doc/style-guide.md b/doc/style-guide.md index 254a7ec071..1bc6960a58 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -569,6 +569,14 @@ word within a compound word is capitalized except for the first word. #### Specific pragmatics/idiomatic patterns +## Use of `pattern` synonyms + +In general, these are intended to be used to provide specialised +constructors for `Data` types (and sometimes, inductive +families/binary relations such as `Data.Nat.Divisibility._∣_`), and as +such, their use should be restricted to `Base` or `Core` modules, and +not pollute the namespaces of `Properties` or other modules. + ## Use of `with` notation Thinking on this has changed since the early days of the library, with From f58442fa44fa755342d1aeb97590270b3c516675 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 25 Mar 2024 14:19:30 +0000 Subject: [PATCH 15/19] removed `import` --- src/Data/Fin/Base.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 46ea5b8a7b..d762e10007 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -11,7 +11,6 @@ module Data.Fin.Base where -open import Algebra.Definitions.RawMagma using (_,_) open import Data.Bool.Base using (Bool; T) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂) From bdd91ee71b944f5233071dbf49fbeacef7a922b9 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Wed, 5 Jun 2024 16:41:04 +0100 Subject: [PATCH 16/19] Update CHANGELOG.md Fix refs to Algebra.Definitions.RawMagma --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d29d56d9ab..b4cf487aeb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -90,7 +90,7 @@ Deprecated names ``` * In `Data.Nat.Base`: the following pattern synonyms and definitions are all - deprecated in favour of direct pattern matching on `Algebra.RawMagma._∣ˡ_._,_` + deprecated in favour of direct pattern matching on `Algebra.Definitions.RawMagma._∣ˡ_._,_` ```agda pattern less-than-or-equal {k} eq = k , eq pattern ≤″-offset k = k , refl From 561502d2e0730be2e3ebbfabe21001cc814fcd90 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Wed, 5 Jun 2024 16:44:23 +0100 Subject: [PATCH 17/19] Update Base.agda Fix refs. to Algebra.Definitions.RawMagma --- src/Data/Nat/Base.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 178106a978..db46274f24 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -424,15 +424,15 @@ compare (suc m) (suc n) with compare m n -- Smart constructors of _≤″_ and _<″_ pattern less-than-or-equal {k} eq = k , eq {-# WARNING_ON_USAGE less-than-or-equal -"Warning: less-than-or-equal was deprecated in v2.1. Please match directly on proofs of ≤″ using constructor Algebra.RawMagma._∣ˡ_._,_ instead. " +"Warning: less-than-or-equal was deprecated in v2.1. Please match directly on proofs of ≤″ using constructor Algebra.Definitions.RawMagma._∣ˡ_._,_ instead. " #-} pattern ≤″-offset k = k , refl {-# WARNING_ON_USAGE ≤″-offset -"Warning: ≤″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.RawMagma._∣ˡ_ instead. " +"Warning: ≤″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.Definitions.RawMagma._∣ˡ_ instead. " #-} pattern <″-offset k = k , refl {-# WARNING_ON_USAGE <″-offset -"Warning: <″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.RawMagma._∣ˡ_ instead. " +"Warning: <″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.Definitions.RawMagma._∣ˡ_ instead. " #-} -- Smart destructors of _<″_ @@ -440,5 +440,5 @@ pattern <″-offset k = k , refl s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n s≤″s⁻¹ (k , refl) = k , refl {-# WARNING_ON_USAGE s≤″s⁻¹ -"Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.RawMagma._∣ˡ_ instead. " +"Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.Definitions.RawMagma._∣ˡ_ instead. " #-} From bdb1306f8924c8ce26a28efb301d6c50366b6b58 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Jun 2024 17:16:01 +0100 Subject: [PATCH 18/19] inlined guarded monus definition in property --- CHANGELOG.md | 15 +++++++-------- src/Data/Nat/Properties.agda | 8 +++----- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b4cf487aeb..dce0bc31e1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -554,17 +554,16 @@ Additions to existing modules * Added new proofs and 'guarded' version of `_∸_` in `Data.Nat.Properties`: ```agda - m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o - m Date: Sat, 8 Jun 2024 03:57:46 +0100 Subject: [PATCH 19/19] remove comment about guarded monus --- CHANGELOG.md | 2 +- src/Data/Nat/Properties.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index dce0bc31e1..551b243969 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -552,7 +552,7 @@ Additions to existing modules nonZeroDivisor : DivMod dividend divisor → NonZero divisor ``` -* Added new proofs and 'guarded' version of `_∸_` in `Data.Nat.Properties`: +* Added new proofs in `Data.Nat.Properties`: ```agda m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o m