From e4da88b2be765de5c260a43803fa536b69cce3ab Mon Sep 17 00:00:00 2001
From: Felix Klein <felix@qbaylogic.com>
Date: Fri, 8 May 2026 14:22:52 +0200
Subject: [PATCH] Add more Data.Rational.Properties

---
 CHANGELOG.md                      |  11 +++
 src/Data/Rational/Properties.agda | 139 +++++++++++++++++++++++++++++-
 2 files changed, 149 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 05c7eeeccd..531338c986 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -450,6 +450,17 @@ Additions to existing modules
   p*q≡0⇒p≡0∨q≡0 : p * q ≡ 0ℚ → p ≡ 0ℚ ⊎ q ≡ 0ℚ
   p*q≢0⇒p≢0     : p * q ≢ 0ℚ → p ≢ 0ℚ
   p*q≢0⇒q≢0     : p * q ≢ 0ℚ → q ≢ 0ℚ
+  ↥[i/1]≡i  : (i : ℤ) → ↥ (i / 1) ≡ i
+  ↧ₙ[i/1]≡1 : (i : ℤ) → ↧ₙ (i / 1) ≡ 1
+  n/n≡1 : ∀ (n : ℕ) .{{_ : ℕ.NonZero n}} → + n / n ≡ 1ℚ
+  -i/n≡-[i/n] : ∀ (i : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n}} →
+                ℤ.- i / n ≡ - (i / n)
+  *-cancelˡ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (p ℕ.* r)}} →
+                (+ p ℤ.* q) / (p ℕ.* r) ≡ q / r
+  *-cancelʳ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (r ℕ.* p)}} →
+                (q ℤ.* + p) / (r ℕ.* p) ≡ q / r
+  i/n+j/n≡[i+j]/n : ∀ (i j : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n }} →
+                    i / n + j / n ≡ (i ℤ.+ j) / n
   ```
 
 * In `Data.Rational.Show`:
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 519caf712b..70ee39a53b 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -31,7 +31,7 @@ open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_)
 open import Data.Integer.Coprimality using (coprime-divisor)
 import Data.Integer.Properties as ℤ
-open import Data.Integer.GCD using (gcd; gcd[i,j]≡0⇒i≡0; gcd[i,j]≡0⇒j≡0)
+open import Data.Integer.GCD using (gcd; gcd[i,j]≡0⇒i≡0; gcd[i,j]≡0⇒j≡0; gcd-zeroʳ)
 open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕ
@@ -394,12 +394,51 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
 ↥p/↧p≡p (mkℚ (+ n)    d-1 prf) = normalize-coprime prf
 ↥p/↧p≡p (mkℚ -[1+ n ] d-1 prf) = cong (-_) (normalize-coprime prf)
 
+↥[i/1]≡i : (i : ℤ) → ↥ (i / 1) ≡ i
+↥[i/1]≡i i = begin
+    (↥ (i / 1))              ≡⟨ sym $ ℤ.*-identityʳ (↥ (i / 1)) ⟩
+    (↥ (i / 1)) ℤ.* 1ℤ       ≡⟨ cong (↥ (i / 1) ℤ.*_) $ sym $ gcd-zeroʳ i ⟩
+    (↥ (i / 1)) ℤ.* gcd i 1ℤ ≡⟨ ↥-/ i 1 ⟩
+    i                        ∎
+  where open ≡-Reasoning
+
+↧ₙ[i/1]≡1 : (i : ℤ) → ↧ₙ (i / 1) ≡ 1
+↧ₙ[i/1]≡1 i = ℤ.+-injective $ begin
+    ↧ (i / 1)               ≡⟨ sym $ ℤ.*-identityʳ (↧ (i / 1)) ⟩
+    ↧ (i / 1) ℤ.* 1ℤ        ≡⟨ cong (↧ (i / 1) ℤ.*_) $ sym $ gcd-zeroʳ i ⟩
+    ↧ (i / 1) ℤ.* gcd i 1ℤ  ≡⟨ ↧-/ i 1 ⟩
+    1ℤ                      ∎
+  where open ≡-Reasoning
+
 0/n≡0 : ∀ n .{{_ : ℕ.NonZero n}} → 0ℤ / n ≡ 0ℚ
 0/n≡0 n@(suc n-1) {{n≢0}} = mkℚ+-cong {{n/n≢0}} {c₂ = 0-cop-1} (ℕ.0/n≡0 (ℕ.gcd 0 n)) (ℕ.n/n≡1 n)
   where
   0-cop-1 = C.sym (C.1-coprimeTo 0)
   n/n≢0   = ℕ.>-nonZero (subst (ℕ._> 0) (sym (ℕ.n/n≡1 n)) (ℕ.z<s))
 
+n/n≡1 : ∀ (n : ℕ) .{{_ : ℕ.NonZero n}} → + n / n ≡ 1ℚ
+n/n≡1 n {{nz}} = mkℚ+-cong n/gcd[n,n]≡1 n/gcd[n,n]≡1
+  where
+  instance g≢0   = ℕ.≢-nonZero (ℕ.gcd[m,n]≢0 n n (inj₂ (ℕ.≢-nonZero⁻¹ n)))
+           n/g≢0 = ℕ.≢-nonZero (ℕ.n/gcd[m,n]≢0 n n {{gcd≢0 = g≢0}})
+
+  gcd[n,n]≡n : ∀ n → ℕ.gcd n n ≡ n
+  gcd[n,n]≡n n rewrite sym (ℕ.*-identityʳ n)
+    = sym (ℕ.c*gcd[m,n]≡gcd[cm,cn] n 1 1)
+
+  n/gcd[n,n]≡1
+    = trans (ℕ./-congʳ {ℕ.gcd n n} (gcd[n,n]≡n n)) (ℕ.n/n≡1 n {{nz}})
+
+-i/n≡-[i/n] : ∀ (i : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n}} →
+              ℤ.- i / n ≡ - (i / n)
+-i/n≡-[i/n] +0       n = trans (0/n≡0 n) (cong -_ (sym (0/n≡0 n)))
+-i/n≡-[i/n] +[1+ m ] n = refl
+-i/n≡-[i/n] -[1+ m ] n
+  with +[1+ m ] / n
+... | mkℚ -[1+ a ] d prf = refl
+... | mkℚ +0       d prf = refl
+... | mkℚ +[1+ a ] d prf = refl
+
 /-cong : ∀ {p₁ q₁ p₂ q₂} .{{_ : ℕ.NonZero q₁}} .{{_ : ℕ.NonZero q₂}} →
          p₁ ≡ p₂ → q₁ ≡ q₂ → p₁ / q₁ ≡ p₂ / q₂
 /-cong {+ n}       refl = normalize-cong {n} refl
@@ -1361,6 +1400,40 @@ module _ where
   heytingField : HeytingField 0ℓ 0ℓ 0ℓ
   heytingField = record { isHeytingField = isHeytingField }
 
+------------------------------------------------------------------------
+-- Properties of _*_ and _/_
+
+*-cancelˡ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (p ℕ.* r)}} →
+              (+ p ℤ.* q) / (p ℕ.* r) ≡ q / r
+*-cancelˡ-/ p {q} {r} = proof q
+  where
+  *-cancelˡ-/-helper : ∀ qₙ → normalize (p ℕ.* qₙ) (p ℕ.* r) ≡ + qₙ / r
+  *-cancelˡ-/-helper qₙ = mkℚ+-cong (lemma qₙ) (lemma r)
+    where
+    instance
+      p≢0    = ℕ.m*n≢0⇒m≢0 p
+      g≢0    = ℕ.≢-nonZero $ ℕ.gcd[m,n]≢0 (p ℕ.* qₙ) (p ℕ.* r) $ inj₂
+                           $ ℕ.≢-nonZero⁻¹ $ p ℕ.* r
+      n/g≢0  = ℕ.≢-nonZero $ ℕ.n/gcd[m,n]≢0 (p ℕ.* qₙ) (p ℕ.* r) {{gcd≢0 = g≢0}}
+      g≢0'   = ℕ.≢-nonZero $ ℕ.gcd[m,n]≢0 qₙ r $ inj₂ $ ℕ.≢-nonZero⁻¹ r
+      n/g≢0' = ℕ.≢-nonZero $ ℕ.n/gcd[m,n]≢0 qₙ r {{gcd≢0 = g≢0'}}
+      p*g≢0  = ℕ.m*n≢0 p (ℕ.gcd qₙ r)
+
+    lemma : ∀ n → (p ℕ.* n) ℕ./ ℕ.gcd (p ℕ.* qₙ) (p ℕ.* r) ≡ n ℕ./ ℕ.gcd qₙ r
+    lemma n = trans (ℕ./-congʳ $ sym $ ℕ.c*gcd[m,n]≡gcd[cm,cn] p qₙ r)
+                    (ℕ.m*n/m*o≡n/o p n $ ℕ.gcd qₙ r)
+
+  proof : ∀ q → (+ p ℤ.* q) / (p ℕ.* r) ≡ q / r
+  proof (+ qₙ)    rewrite sym (ℤ.pos-* p qₙ) = *-cancelˡ-/-helper qₙ
+  proof -[1+ qₙ ] rewrite sym (ℤ.neg-distribʳ-* (+ p) +[1+ qₙ ])
+                           | sym (ℤ.pos-* p (suc qₙ))
+                           = trans (-i/n≡-[i/n] (+ (p ℕ.* suc qₙ)) (p ℕ.* r))
+                               (cong (-_) $ *-cancelˡ-/-helper $ suc qₙ)
+
+*-cancelʳ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (r ℕ.* p)}} →
+              (q ℤ.* + p) / (r ℕ.* p) ≡ q / r
+*-cancelʳ-/ p {q} {r}
+  rewrite ℕ.*-comm r p | ℤ.*-comm q (ℤ.+ p) = *-cancelˡ-/ p
 
 ------------------------------------------------------------------------
 -- Properties of _*_ and _≤_
@@ -1844,6 +1917,70 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
 ∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
 
+------------------------------------------------------------------------
+-- Other properties of _+_
+------------------------------------------------------------------------
+
+i/n+j/n≡[i+j]/n : ∀ (i j : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n }} →
+                  i / n + j / n ≡ (i ℤ.+ j) / n
+i/n+j/n≡[i+j]/n i j n = proof
+  where
+  pᵢ = i / n
+  qⱼ = j / n
+  gcd[i,n]ₙ = ℕ.gcd ℤ.∣ i ∣ n
+  gcd[i,n]  = + gcd[i,n]ₙ
+  gcd[j,n]ₙ = ℕ.gcd ℤ.∣ j ∣ n
+  gcd[j,n]  = + gcd[j,n]ₙ
+
+  instance
+   _ = ℕ.≢-nonZero $ ℕ.gcd[m,n]≢0 ℤ.∣ i ∣ n $ inj₂ $ ℕ.≢-nonZero⁻¹ n
+   _ = ℕ.≢-nonZero $ ℕ.gcd[m,n]≢0 ℤ.∣ j ∣ n $ inj₂ $ ℕ.≢-nonZero⁻¹ n
+   _ = ℕ.m*n≢0 (↧ₙ pᵢ ℕ.* ↧ₙ qⱼ) gcd[j,n]ₙ
+   _ = ℕ.m*n≢0 (↧ₙ pᵢ ℕ.* ↧ₙ qⱼ ℕ.* gcd[j,n]ₙ) gcd[i,n]ₙ
+   _ = ℕ.m*n≢0 n n
+
+  +-def : pᵢ + qⱼ ≡ (↥ pᵢ ℤ.* ↧ qⱼ ℤ.+ ↥ qⱼ ℤ.* ↧ pᵢ) / (↧ₙ pᵢ ℕ.* ↧ₙ qⱼ)
+  +-def with record{} ← pᵢ with record{} ← qⱼ = refl
+
+  ↥≡ : (↥ pᵢ ℤ.* ↧ qⱼ ℤ.+ ↥ qⱼ ℤ.* ↧ pᵢ) ℤ.* gcd[j,n] ℤ.* gcd[i,n]
+     ≡ (i ℤ.+ j) ℤ.* + n
+  ↥≡ rewrite ℤ.*-distribʳ-+ gcd[j,n] (↥ pᵢ ℤ.* ↧ qⱼ) (↥ qⱼ ℤ.* ↧ pᵢ)
+           | ℤ.*-distribʳ-+ gcd[i,n] (↥ pᵢ ℤ.* ↧ qⱼ ℤ.* gcd[j,n])
+                                     (↥ qⱼ ℤ.* ↧ pᵢ ℤ.* gcd[j,n])
+           | ℤ.*-assoc (↥ pᵢ) (↧ qⱼ) gcd[j,n]
+           | cong (↥ pᵢ ℤ.*_) (↧-/ j n)
+           | ℤ.*-assoc (↥ qⱼ) (↧ pᵢ) gcd[j,n]
+           | ℤ.*-comm (↧ pᵢ) gcd[j,n]
+           | sym (ℤ.*-assoc (↥ qⱼ) gcd[j,n] (↧ pᵢ))
+           | cong (ℤ._* ↧ pᵢ) (↥-/ j n)
+           | ℤ.*-assoc j (↧ pᵢ) gcd[i,n]
+           | cong (j ℤ.*_) (↧-/ i n)
+           | ℤ.*-comm (↥ pᵢ) (+ n)
+           | ℤ.*-assoc (+ n) (↥ pᵢ) gcd[i,n]
+           | cong (+ n ℤ.*_) (↥-/ i n)
+           | ℤ.*-comm (+ n) i
+           | sym (ℤ.*-distribʳ-+ (+ n) i j)
+           = refl
+
+  ↧≡ : ↧ₙ pᵢ ℕ.* ↧ₙ qⱼ ℕ.* gcd[j,n]ₙ ℕ.* gcd[i,n]ₙ ≡ n ℕ.* n
+  ↧≡ rewrite ℕ.*-assoc (↧ₙ pᵢ) (↧ₙ qⱼ) gcd[j,n]ₙ
+           | sym (ℤ.abs-* (↧ qⱼ) (gcd j (+ n)))
+           | cong ℤ.∣_∣ (↧-/ j n)
+           | ℕ.*-comm (↧ₙ pᵢ) n
+           | ℕ.*-assoc n (↧ₙ pᵢ) gcd[i,n]ₙ
+           | sym (ℤ.abs-* (↧ pᵢ) (gcd i (+ n)))
+           | cong ℤ.∣_∣ (↧-/ i n)
+           = refl
+
+  proof : i / n + j / n ≡ (i ℤ.+ j) / n
+  proof rewrite +-def
+              | sym (*-cancelʳ-/ gcd[j,n]ₙ
+                  {↥ pᵢ ℤ.* ↧ qⱼ ℤ.+ ↥ qⱼ ℤ.* ↧ pᵢ} { ↧ₙ pᵢ ℕ.* ↧ₙ qⱼ })
+              | sym (*-cancelʳ-/ gcd[i,n]ₙ
+                  { (↥ pᵢ ℤ.* ↧ qⱼ ℤ.+ ↥ qⱼ ℤ.* ↧ pᵢ) ℤ.* gcd[j,n] }
+                  { ↧ₙ pᵢ ℕ.* ↧ₙ qⱼ ℕ.* gcd[j,n]ₙ })
+              | sym (*-cancelʳ-/ n {i ℤ.+ j} {n})
+              = /-cong ↥≡ ↧≡
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES