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

* [ add ] proof of Carette's Lemma

* refactor: remove simple lemmas

* add: one half of the equivalence

* refactor: in terms of `_on_` and `_⇒_`; introduce name for equality mod `o`

* add: new lemmas relating `SymClosure` and `on`

* use: new lemmas

* rename: according to review comments

* change notation, following review comments

* chnage comment text to reflect the analysis better

* refactor: in terms of `wlog`

* refactor: export Jacques' lemma; leave Alex' proof `private`

* refactor: comment out the `wlog` proof; tidy up the presentation

* removed `wlog` proof

* refactor: appeal to `Sum` elimination, rather than `with`

* Remove Zulip reference

---------

Co-authored-by: Matthew Daggitt <matthewdaggitt@gmail.com>

Author: jamesmckinna

CHANGELOG.md

@@ -344,6 +344,23 @@ 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 .{{_ : NonZero o}} n → Set _
+  m ≡%[ o ] n = m % o ≡ n % o
+
+  infix 4 _≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
+  m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
+  m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n
+
+  ≲%[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 ]_
+
+  ≡%-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
+  ```
+
 * In `Data.Nat.Logarithm`
   ```agda
   2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
@@ -608,6 +625,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⁺  : ((SymClosure R) on g) ⇒ SymClosure (R on g)
+  on⁻  : 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,13 @@ 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 Data.Product.Base using (_,_; ∃)
+open import Data.Sum.Base as Sum using (inj₁; inj₂)
+open import Function.Base using (id; _$_; _∘_; _on_)
+open import Function.Definitions using (Injective)
+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 +467,78 @@ m%n*o≡m*o%[n*o] m n o = begin-equality
     p-1 * n + n ≡⟨ +-comm (p-1 * n) n ⟩
     pn          ∎
 
+------------------------------------------------------------------------
+-- Lemmas characterising the relation `m ≡ n (mod o)`
+
+infix 4 _≡%[_]_
+_≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
+m ≡%[ o ] n = m % o ≡ n % o
+
+-- Definition of an alternative, *asymmetric* version of that relation
+-- whose `Relation.Binary.Construct.Closure.Symmetric` is equivalent.
+
+infix 4 _≲%[_]_ _≅%[_]_
+_≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
+
+m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
+m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n
+
+-- 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 =
+    Sum.[ fwd ∘ ≡[o]%⇒≲%[o] eq , bwd ∘ ≡[o]%⇒≲%[o] (sym eq) ]′ (≤-total m n)
+
+  ≡%-suc-injective : Injective _≡%[ o ]_ _≡%[ o ]_ suc
+  ≡%-suc-injective = ≅%[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-≲%
+
+private
+
+  -- Alex Rice's optimised direct proof of the above
+  ≡%[o]-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
+  ≡%[o]-suc-injective {o = so@(suc o)} {x = m} {y = n} eq = begin-equality
+    m % so                     ≡⟨ lemma m ⟩
+    (suc m % so + o % so) % so ≡⟨ cong (λ a → (a + o % so) % so) eq ⟩
+    (suc n % so + o % so) % so ≡⟨ lemma n ⟨
+    n % so ∎
+    where
+    lemma : ∀ n → n % so ≡ (suc n % so + o % so) % so
+    lemma n = begin-equality
+      n % so                     ≡⟨ [m+n]%n≡m%n n so ⟨
+      (n + so) % so              ≡⟨⟩
+      (n + suc o) % so           ≡⟨ %-congˡ (+-suc n o) ⟩
+      (suc n + o) % so           ≡⟨ %-distribˡ-+ (suc n) o so ⟩
+      (suc n % so + o % so) % so ∎
+
+
 ------------------------------------------------------------------------
 --  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⁺ : (g : B → A) → ((SymClosure R) on g) ⇒ SymClosure (R on g)
+on⁺ g = hmap g id id
+
+on⁻ : (g : B → A) → SymClosure (R on g) ⇒ ((SymClosure R) on g)
+on⁻ 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