Remove (almost!) all external use of _≤″_ beyond Data.Nat.* (#2262)

* additional proofs and patterns in `Data.Nat.Properties`

* added two projections; refactored `pad*` operations

* `CHANGELOG`

* removed one more use

* removed final uses of `<″-offset` outside `Data.Nat.Base|Properties`

* rename `≤-proof` to `m≤n⇒∃[o]m+o≡n`

* removed new pattern synonyms

* interim commit: deprecate everything!

* add guarded monus; make arguments more irrelevant

* fixed up `CHANGELOG`

* propagate use of irrelevance

* tidy up deprecations; reinstate `s<″s⁻¹` for `Data.Fin.Properties`

* tightened up the deprecation story

* paragraph on use of `pattern` synonyms

* removed `import`

* Update CHANGELOG.md

Fix refs to Algebra.Definitions.RawMagma

* Update Base.agda

Fix refs. to Algebra.Definitions.RawMagma

* inlined guarded monus definition in property

* remove comment about guarded monus

CHANGELOG.md

@@ -99,6 +99,15 @@ Deprecated names
   map-compose  ↦  map-∘
   ```
 
+* In `Data.Nat.Base`: the following pattern synonyms and definitions are all
+  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
+  pattern <″-offset k = k , refl
+  s≤″s⁻¹
+ ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -663,12 +672,16 @@ Additions to existing modules
 
 * Added new proofs in `Data.Nat.Properties`:
   ```agda
-  m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
-  m<n+o⇒m∸n<o : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
-  pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
-  pred-cancel-< : pred m < pred n → m < n
+  m≤n+o⇒m∸n≤o    : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
+  m<n+o⇒m∸n<o    : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
+  pred-cancel-≤  : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
+  pred-cancel-<  : pred m < pred n → m < n
   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
+  pred-cancel-≡  : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
+
+  <⇒<″          : _<_ ⇒ _<″_
+  m≤n⇒∃[o]m+o≡n : .(m ≤ n) → ∃ λ k → m + k ≡ n
+  guarded-∸≗∸   : .(m≤n : m ≤ n) → let k , _ = m≤n⇒∃[o]m+o≡n m≤n in k ≡ n ∸ m
   ```
 
 * Added new proofs to `Data.Nat.Primality`:
@@ -769,6 +782,12 @@ Additions to existing modules
   Stable : Pred A ℓ → Set _
   ```
 
+* 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.
 

doc/style-guide.md

@@ -657,6 +657,14 @@ Type formers:
 
 #### 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

src/Data/Fin/Properties.agda

@@ -247,9 +247,9 @@ fromℕ<-injective (suc _) (suc _) {o = suc _} m<n n<o r
 
 fromℕ<≡fromℕ<″ : ∀ (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                  fromℕ< m<n ≡ fromℕ<″ m m<″n
-fromℕ<≡fromℕ<″ {m = zero}  m<n (ℕ.<″-offset _) = refl
-fromℕ<≡fromℕ<″ {m = suc m} m<n (ℕ.<″-offset _)
-  = cong suc (fromℕ<≡fromℕ<″ (ℕ.s<s⁻¹ m<n) (ℕ.<″-offset _))
+fromℕ<≡fromℕ<″ {m = zero}  {n = suc _} _ _ = refl
+fromℕ<≡fromℕ<″ {m = suc m} {n = suc _} m<n m<″n
+  = cong suc (fromℕ<≡fromℕ<″ (ℕ.s<s⁻¹ m<n) (ℕ.s<″s⁻¹ m<″n))
 
 toℕ-fromℕ<″ : ∀ (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<n = begin

src/Data/Nat/Base.agda

@@ -363,8 +363,6 @@ infix 4 _≤″_ _<″_ _≥″_ _>″_
 _≤″_ : (m n : ℕ)  → Set
 _≤″_ = _∣ˡ_ +-rawMagma
 
-pattern less-than-or-equal {k} proof = k , proof
-
 _<″_ : Rel ℕ 0ℓ
 m <″ n = suc m ≤″ n
 
@@ -374,18 +372,10 @@ m ≥″ n = n ≤″ 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
+-- Smart destructor of _<″_
 
 s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
-s<″s⁻¹ (<″-offset k) = <″-offset k
+s<″s⁻¹ (k , refl) = k , refl
 
 -- _≤‴_: this definition is useful for induction with an upper bound.
 
@@ -429,5 +419,26 @@ 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 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.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.Definitions.RawMagma._∣ˡ_ 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) from Algebra.Definitions.RawMagma._∣ˡ_ instead. "
+#-}

src/Data/Nat/DivMod.agda

@@ -17,6 +17,7 @@ open import Data.Nat.DivMod.Core
 open import Data.Nat.Divisibility.Core
 open import Data.Nat.Induction
 open import Data.Nat.Properties
+open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_)
 open import Relation.Binary.PropositionalEquality.Core
@@ -105,7 +106,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 k , refl ← m≤n⇒∃[o]m+o≡n m≤n
   = a≤n⇒a[modₕ]n≡a 0 (m + k) m k
 
 m<n⇒m%n≡m : .{{_ : NonZero n}} → m < n → m % n ≡ m

src/Data/Nat/Properties.agda

@@ -14,6 +14,7 @@ module Data.Nat.Properties where
 open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP)
 open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup;
   CommutativeMonoid; Monoid; Semiring; CommutativeSemiring; CommutativeSemiringWithoutOne)
+open import Algebra.Definitions.RawMagma using (_,_)
 open import Algebra.Morphism
 open import Algebra.Consequences.Propositional
   using (comm+cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ)
@@ -41,7 +42,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)
 
@@ -2106,31 +2107,46 @@ n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
 -- Properties of _≤″_ and _<″_
 ------------------------------------------------------------------------
 
-m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
-m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)
+-- equivalence of  _≤″_ to _≤_
 
-m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
-m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
+≤⇒≤″ : _≤_ ⇒ _≤″_
+≤⇒≤″ = (_ ,_) ∘ m+[n∸m]≡n
 
-<ᵇ⇒<″ : T (m <ᵇ n) → m <″ n
-<ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))
+<⇒<″ : _<_ ⇒ _<″_
+<⇒<″ = ≤⇒≤″
 
-<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
-<″⇒<ᵇ {m} (<″-offset k) = <⇒<ᵇ (m≤m+n (suc m) k)
+≤″⇒≤ : _≤″_ ⇒ _≤_
+≤″⇒≤ (k , refl) = m≤m+n _ k
 
 -- equivalence to the old definition of _≤″_
 
-≤″-proof : ∀ {m n} (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
 
--- equivalence to _≤_
+-- yielding analogous proof for _≤_
 
-≤″⇒≤ : _≤″_ ⇒ _≤_
-≤″⇒≤ {zero}  (≤″-offset k) = z≤n {k}
-≤″⇒≤ {suc m} (≤″-offset k) = s≤s (≤″⇒≤ (≤″-offset k))
+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)
 
-≤⇒≤″ : _≤_ ⇒ _≤″_
-≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n
+-- whose witness is equal to monus
+
+guarded-∸≗∸ : ∀ {m n} → .(m≤n : m ≤ n) →
+              let k , _ = m≤n⇒∃[o]m+o≡n m≤n in k ≡ n ∸ m
+guarded-∸≗∸ m≤n = refl
+
+-- equivalence of _<″_ to _<ᵇ_
+
+m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
+m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)
+
+m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
+m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
+
+<ᵇ⇒<″ : T (m <ᵇ n) → m <″ n
+<ᵇ⇒<″ {m} {n} = <⇒<″ ∘ (<ᵇ⇒< m n)
+
+<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
+<″⇒<ᵇ {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`.
@@ -2144,7 +2160,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 _≥″_
@@ -2154,10 +2170,9 @@ _>″?_ : 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
@@ -2173,8 +2188,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})
@@ -2397,4 +2412,3 @@ open Data.Nat.Base public
 {-# WARNING_ON_USAGE <-transˡ
 "Warning: <-transˡ was deprecated in v2.0. Please use <-≤-trans instead. "
 #-}
-

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

src/Data/Vec/Bounded/Base.agda

@@ -21,7 +21,7 @@ open import Data.These.Base as These using (These)
 open import Function.Base using (_∘_; id; _$_)
 open import Level using (Level)
 open import Relation.Nullary.Decidable.Core using (recompute)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 
@@ -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 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 ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n)
+  with k , refl ← ℕ.m≤n⇒∃[o]m+o≡n 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 k , refl ← ℕ.m≤n⇒∃[o]m+o≡n 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