[ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}}

CHANGELOG.md

@@ -319,6 +319,21 @@ Additions to existing modules
   n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o
   ```
 
+* In `Data.Nat.DivMod`:
+  ```agda
+  infix 4 _≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
+  m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
+  m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
+
+  infix 4 _≡[_]%_ : ∀ m o .{{_ : NonZero o}} n → Set _
+  m ≡[ o ]% n = m % o ≡ n % o
+
+  ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡[ o ]%_
+  ≡%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≡[ o ]%_
+  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≡%[o] : .{{_ : NonZero o}} → _≡[ o ]%_ ⇒ _≡%[ o ]_
+  ```
+
 * In `Data.Nat.Logarithm`
   ```agda
   2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
@@ -481,6 +496,14 @@ Additions to existing modules
   ≤⁺-resp-≈⁺ : _≤_ Respects₂ _≈_ → _≤⁺_ Respects₂ _≈⁺_
   ```
 
+* In `Relation.Binary.Construct.Closure.Symmetric`:
+  ```
+  hmap : ∀ (g : C → A) (f : C → B) → (R on g) ⇒ (S on f) →
+         ((SymClosure R) on g) ⇒ ((SymClosure S) on f)
+  on-commutesˡ : ((SymClosure R) on g) ⇒ SymClosure (R on g)
+  on-commutesʳ : SymClosure (R on g) ⇒ ((SymClosure R) on g)
+  ```
+
 * In `Data.Vec.Relation.Binary.Pointwise.Inductive`
   ```agda
   irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m})

src/Data/Nat/DivMod.agda

@@ -17,9 +17,12 @@ 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.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Function.Base using (_$_; _∘_)
+open import Function.Base using (id; _$_; _∘_; _on_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Construct.Closure.Symmetric
+  as SymClosure using (SymClosure; fwd; bwd)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; cong; cong₂; refl; trans; _≢_; sym)
 open import Relation.Nullary.Negation using (contradiction)
@@ -463,6 +466,86 @@ m%n*o≡m*o%[n*o] m n o = begin-equality
     p-1 * n + n ≡⟨ +-comm (p-1 * n) n ⟩
     pn          ∎
 
+-- Lemmas characterising `m ≡ n (mod o)`
+
+-- Definition of an asymmetric version of that notion
+-- NB. `Relation.Binary.Construct.Closure.Symmetric`
+-- gives us the relation we're after.
+
+infix 4 _≲%[_]_ _≡%[_]_
+_≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
+
+m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
+m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
+
+infix 4 _≡[_]%_
+_≡[_]%_ : ∀ m o .{{_ : NonZero o}} n → Set _
+m ≡[ o ]% n = m % o ≡ n % o
+
+-- Equivalence between _≡%[_]_ and _≡[_]%_
+
+module _ .{{_ : NonZero o}} where
+
+  ≲%[o]⇒≡[o]% : _≲%[ o ]_ ⇒ _≡[ o ]%_
+  ≲%[o]⇒≡[o]% {x = m} {y = n} (k , eq) = begin-equality
+    m % o           ≡⟨ [m+kn]%n≡m%n m k o ⟨
+    (m + k * o) % o ≡⟨ cong (_% o) eq ⟨
+    n % o ∎
+
+  ≡%[o]⇒≡[o]% : _≡%[ o ]_ ⇒ _≡[ o ]%_
+  ≡%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
+
+  ≡[o]%⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
+    n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩
+    n % o + n / o * o           ≡⟨ cong (_+ n / o * o) eq ⟨
+    m % o + n / o * o           ≡⟨ cong ((m % o +_) ∘ (_* o)) (m+[n∸m]≡n (/-monoˡ-≤ o m≤n)) ⟨
+    m % o + (m / o + k) * o     ≡⟨ cong (m % o +_) (*-distribʳ-+ o (m / o) k) ⟩
+    m % o + (m / o * o + k * o) ≡⟨ +-assoc (m % o) _ _ ⟨
+    (m % o + m / o * o) + k * o ≡⟨ cong (_+ k * o) (m≡m%n+[m/n]*n m o) ⟨
+    m + k * o                   ∎)
+    where k = n / o ∸ m / o
+
+  ≡[o]%⇒≡%[o] : _≡[ o ]%_ ⇒ _≡%[ o ]_
+  ≡[o]%⇒≡%[o] {x = m} {y = n} eq with ≤-total m n
+  ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] eq m≤n)
+  ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m)
+
+
+private
+
+  -- Example application, a result sought by Jacques Carette, taken from
+  -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
+
+  CarettesLemma : ∀ o .{{_ : NonZero o}} → Set _
+  CarettesLemma o = (_≡[ o ]%_ on suc) ⇒ _≡[ o ]%_
+
+  carettesLemma : .{{_ : NonZero o}} → CarettesLemma o
+  carettesLemma {o = o} = ≡%[o]⇒≡[o]% ∘ lemma-≡% ∘ ≡[o]%⇒≡%[o]
+    where
+    lemma-≲% : (_≲%[ o ]_ on suc) ⇒ _≲%[ o ]_
+    lemma-≲% (k , eq) = k , cong pred eq
+
+    lemma-≡% : (_≡%[ o ]_ on suc) ⇒ _≡%[ o ]_
+    lemma-≡% = SymClosure.hmap suc id lemma-≲%
+
+  -- Alex Rice's optimised proof
+  carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o
+  carettesLemma′ {o = o@(suc d)} {x = m} {y = n} eq = begin-equality
+    m % o                   ≡⟨ lemma m ⟩
+    (suc m % o + d % o) % o ≡⟨ cong (λ a → (a + d % o) % o) eq ⟩
+    (suc n % o + d % o) % o ≡⟨ lemma n ⟨
+    n % o ∎
+    where
+    lemma : ∀ n → n % o ≡ (suc n % o + d % o) % o
+    lemma n = begin-equality
+      n % o                   ≡⟨ [m+n]%n≡m%n n o ⟨
+      (n + o) % o             ≡⟨⟩
+      (n + suc d) % o         ≡⟨ %-congˡ (+-suc n d) ⟩
+      (suc n + d) % o         ≡⟨ %-distribˡ-+ (suc n) d o ⟩
+      (suc n % o + d % o) % o ∎
+
+
 ------------------------------------------------------------------------
 --  A specification of integer division.
 

src/Relation/Binary/Construct/Closure/Symmetric.agda

@@ -17,7 +17,7 @@ import Relation.Binary.Construct.On as On
 private
   variable
     a ℓ ℓ₁ ℓ₂ : Level
-    A B : Set a
+    A B C : Set a
     R S : Rel A ℓ
 
 ------------------------------------------------------------------------
@@ -38,10 +38,22 @@ symmetric _ (bwd bRa) = fwd bRa
 ------------------------------------------------------------------------
 -- Operations
 
--- A generalised variant of `map` which allows the index type to change.
+-- A generalised variant of `map` where *both* index types can change.
+hmap : ∀ (g : C → A) (f : C → B) → (R on g) ⇒ (S on f) →
+       ((SymClosure R) on g) ⇒ ((SymClosure S) on f)
+hmap _ _ g*R⇒f*S (fwd aRb) = fwd (g*R⇒f*S aRb)
+hmap _ _ g*R⇒f*S (bwd bRa) = bwd (g*R⇒f*S bRa)
+
+-- Hence SymClosure commutes with `on`
+on-commutesˡ : (g : B → A) → ((SymClosure R) on g) ⇒ SymClosure (R on g)
+on-commutesˡ g = hmap g id id
+
+on-commutesʳ : (g : B → A) → SymClosure (R on g) ⇒ ((SymClosure R) on g)
+on-commutesʳ g = hmap id g id
+
+-- And: the 'usual' generalised variant of `map`
 gmap : (f : A → B) → R =[ f ]⇒ S → SymClosure R =[ f ]⇒ SymClosure S
-gmap _ g (fwd aRb) = fwd (g aRb)
-gmap _ g (bwd bRa) = bwd (g bRa)
+gmap = hmap id
 
 map : R ⇒ S → SymClosure R ⇒ SymClosure S
 map = gmap id