From 6fe6a4acda22232f655426c0ee41159854aa1687 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Thu, 19 Feb 2026 15:48:58 -0500 Subject: [PATCH 01/27] floor upper bound, ceil lower bound --- .../Rational/Unnormalised/Properties.agda | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index e084ab7776..b3c7926fd3 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -33,6 +33,7 @@ import Data.Nat.Properties as ℕ using (≤-refl; +-comm; +-identityʳ; +-assoc ; *-identityʳ; *-comm; *-assoc; *-suc) open import Data.Integer.Base as ℤ using (ℤ; +0; +[1+_]; -[1+_]; 0ℤ; 1ℤ; -1ℤ) +open import Data.Integer.DivMod using ([n/d]*d≤n) open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver) import Data.Integer.Properties as ℤ open import Data.Rational.Unnormalised.Base @@ -1923,6 +1924,24 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ∣-∣-nonNeg (mkℚᵘ +0 _) = _ ∣-∣-nonNeg (mkℚᵘ -[1+ _ ] _) = _ +------------------------------------------------------------------------ +-- Rounding functions + +floor[q]≤q : ∀ q → (floor q) / 1 ≤ q +floor[q]≤q q@record{} = *≤* (begin + floor q ℤ.* (↧ q) ≡⟨⟩ + (↥ q ℤ./ ↧ q) ℤ.* (↧ q) ≤⟨ [n/d]*d≤n _ (↧ q) ⟩ + (↥ q) ≡⟨ sym (ℤ.*-identityʳ (↥ q)) ⟩ + (↥ q) ℤ.* (↧ (floor q / 1)) ∎) + where + open ℤ.≤-Reasoning + +ceiling[q]≥q : ∀ q → (ceiling q) / 1 ≥ q +ceiling[q]≥q q@record{} = subst + (λ h → lhs ≥ h) + (neg-involutive-≡ q) + (neg-mono-≤ (floor[q]≤q (- q))) + where lhs = - (floor (- q) / 1) ------------------------------------------------------------------------ -- DEPRECATED NAMES From c900d0b9dac9b938678fef8d8fa17c0039f10af0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Sat, 21 Feb 2026 17:11:18 -0500 Subject: [PATCH 02/27] Add bounds for floor and ceil --- CHANGELOG.md | 4 ++ .../Rational/Unnormalised/Properties.agda | 46 +++++++++++++------ 2 files changed, 37 insertions(+), 13 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d270255bb6..5a4ef5013a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -318,6 +318,10 @@ 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ℚᵘ + ⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q + q<⌊q⌋+1 : ∀ q → q < ℤ.suc ⌊ q ⌋ / 1 + q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1 + ⌈q⌉-1 Date: Mon, 23 Feb 2026 21:30:23 -0500 Subject: [PATCH 03/27] add introduction of absolute value via inequalities --- CHANGELOG.md | 1 + src/Data/Rational/Unnormalised/Properties.agda | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5a4ef5013a..20c61f17e7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -318,6 +318,7 @@ 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ℚᵘ + -q≤p≤q⇒|p|≤q : ∀ p q → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q ⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q q<⌊q⌋+1 : ∀ q → q < ℤ.suc ⌊ q ⌋ / 1 q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1 diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 9d9b2bae30..3b8299f6ed 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1924,6 +1924,13 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ∣-∣-nonNeg (mkℚᵘ +0 _) = _ ∣-∣-nonNeg (mkℚᵘ -[1+ _ ] _) = _ +-q≤p≤q⇒|p|≤q : ∀ p q → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q +-q≤p≤q⇒|p|≤q p q -q≤p p≤q = + [ (λ ∣p∣≡p → subst (λ h → h ≤ q) (sym ∣p∣≡p) p≤q) + , (λ ∣p∣≡-p → subst (λ h → h ≤ q) (sym ∣p∣≡-p) + (subst (λ h → _ ≤ h) (neg-involutive-≡ q) (neg-mono-≤ -q≤p))) ]′ + (∣p∣≡p∨∣p∣≡-p p) + ------------------------------------------------------------------------ -- Properties of ⌊_⌋ and ⌈_⌉ From 1a25ede5d9eb41cefeb9a84c6d404d99649f360c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Wed, 25 Feb 2026 09:20:13 -0500 Subject: [PATCH 04/27] Add rounding error for floor, ceil, and round --- CHANGELOG.md | 19 +-- .../Rational/Unnormalised/Properties.agda | 133 ++++++++++++++---- 2 files changed, 117 insertions(+), 35 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 20c61f17e7..fbd6c00638 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -315,14 +315,17 @@ Additions to existing modules * In `Data.Rational.Unnormalised.Properties`: ```agda - 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ℚᵘ - -q≤p≤q⇒|p|≤q : ∀ p q → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q - ⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q - q<⌊q⌋+1 : ∀ q → q < ℤ.suc ⌊ q ⌋ / 1 - q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1 - ⌈q⌉-1 Date: Wed, 25 Feb 2026 12:59:36 -0500 Subject: [PATCH 05/27] Apply suggestions from code review Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Rational/Unnormalised/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 88c84bb4ba..7fb0550561 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -33,7 +33,7 @@ import Data.Nat.Properties as ℕ using (≤-refl; +-comm; +-identityʳ; +-assoc ; *-identityʳ; *-comm; *-assoc; *-suc) open import Data.Integer.Base as ℤ using (ℤ; +0; +[1+_]; -[1+_]; 0ℤ; 1ℤ; -1ℤ) -open import Data.Integer.DivMod as ℤ using () +import Data.Integer.DivMod as ℤ open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver) import Data.Integer.Properties as ℤ open import Data.Rational.Unnormalised.Base @@ -1936,9 +1936,9 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) -q≤p≤q⇒∣p∣≤q : ∀ p q → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q -q≤p≤q⇒∣p∣≤q p q -q≤p p≤q = - [ (λ ∣p∣≡p → subst (λ h → h ≤ q) (sym ∣p∣≡p) p≤q) - , (λ ∣p∣≡-p → subst (λ h → h ≤ q) (sym ∣p∣≡-p) - (subst (λ h → _ ≤ h) (neg-involutive-≡ q) (neg-mono-≤ -q≤p))) ]′ + [ (λ ∣p∣≡p → subst (_≤ q) (sym ∣p∣≡p) p≤q) + , (λ ∣p∣≡-p → subst (_≤ q) (sym ∣p∣≡-p) + (subst (_ ≤_) (neg-involutive-≡ q) (neg-mono-≤ -q≤p))) ]′ (∣p∣≡p∨∣p∣≡-p p) ------------------------------------------------------------------------ From 585f6f72dee8064ccb01a5e6c9114085cd1a8192 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Wed, 25 Feb 2026 13:03:04 -0500 Subject: [PATCH 06/27] Remove unnecessary lambda notation --- src/Data/Rational/Unnormalised/Properties.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 7fb0550561..15e8a0b843 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1970,7 +1970,7 @@ q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1 q≤⌈q⌉ q@record{} = subst - (λ h → h ≤ - (⌊ - q ⌋ / 1)) + (_≤ - (⌊ - q ⌋ / 1)) (neg-involutive-≡ q) (neg-mono-≤ (⌊q⌋≤q (- q))) @@ -2004,7 +2004,7 @@ q≤⌈q⌉ q@record{} = subst ∣ q - ⌈ q ⌉ / 1 ∣ ≡⟨⟩ ∣ q - (- ⌊-q⌋) ∣ ≡⟨ cong (λ h → ∣ q + h ∣) (neg-involutive-≡ ⌊-q⌋) ⟩ ∣ q + ⌊-q⌋ ∣ ≡⟨ sym (∣-p∣≡∣p∣ (q + ⌊-q⌋)) ⟩ - ∣ - (q + ⌊-q⌋) ∣ ≡⟨ cong (λ h → ∣ h ∣) (neg-distrib-+ q ⌊-q⌋) ⟩ + ∣ - (q + ⌊-q⌋) ∣ ≡⟨ cong ∣_∣ (neg-distrib-+ q ⌊-q⌋) ⟩ ∣ - q - ⌊-q⌋ ∣ ≤⟨ ∣q-⌊q⌋∣≤1 (- q) ⟩ 1ℚᵘ ∎ where open ≤-Reasoning @@ -2014,7 +2014,7 @@ private - ½ ≃⟨ ≃-sym (+-identityˡ _) ⟩ 0ℚᵘ - ½ ≃⟨ +-congˡ (- ½) (≃-sym (+-inverseʳ q)) ⟩ q - q - ½ ≃⟨ +-assoc q _ _ ⟩ - q + (- q - ½) ≡⟨ cong (λ h → q + h) (sym (neg-distrib-+ q ½)) ⟩ + q + (- q - ½) ≡⟨ cong (q +_) (sym (neg-distrib-+ q ½)) ⟩ q - (q + ½) ≤⟨ +-monoʳ-≤ q (neg-mono-≤ (⌊q⌋≤q (q + ½))) ⟩ q - ⌊ q + ½ ⌋ / 1 ∎ where open ≤-Reasoning @@ -2040,7 +2040,7 @@ private q-⌈q-½⌉≤½ : ∀ q → q - ⌈ q - ½ ⌉ / 1 ≤ ½ q-⌈q-½⌉≤½ q = let ⌊-q+½⌋ = ⌊ - q + ½ ⌋ / 1 in begin q - ⌈ q - ½ ⌉ / 1 ≡⟨ cong (λ h → q - h / 1) (ceil-to-floor q) ⟩ - q - (- ⌊-q+½⌋) ≡⟨ cong (λ h → h - (- ⌊-q+½⌋)) (sym (neg-involutive-≡ q)) ⟩ + q - (- ⌊-q+½⌋) ≡⟨ cong (_- (- ⌊-q+½⌋)) (sym (neg-involutive-≡ q)) ⟩ - (- q) - (- ⌊-q+½⌋) ≡⟨ sym (neg-distrib-+ (- q) _) ⟩ - (- q - ⌊-q+½⌋) ≤⟨ neg-mono-≤ (-½≤q-⌊q+½⌋ (- q)) ⟩ - (- ½) ≡⟨ neg-involutive-≡ ½ ⟩ @@ -2050,7 +2050,7 @@ private -½≤q-⌈q-½⌉ q = let ⌊-q+½⌋ = ⌊ - q + ½ ⌋ / 1 in begin - ½ ≤⟨ neg-mono-≤ (q-⌊q+½⌋≤½ (- q)) ⟩ - (- q - ⌊-q+½⌋) ≡⟨ neg-distrib-+ (- q) (- ⌊-q+½⌋) ⟩ - - (- q) - (- ⌊-q+½⌋) ≡⟨ cong (λ h → h - (- ⌊-q+½⌋)) (neg-involutive-≡ q) ⟩ + - (- q) - (- ⌊-q+½⌋) ≡⟨ cong (_- (- ⌊-q+½⌋)) (neg-involutive-≡ q) ⟩ q - (- ⌊-q+½⌋) ≡⟨ cong (λ h → q - h / 1) (sym (ceil-to-floor q)) ⟩ q - ⌈ q - ½ ⌉ / 1 ∎ where open ≤-Reasoning From 3a2ee47c474c5bb9c973b96462db468b36f4009e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Thu, 26 Feb 2026 10:28:03 -0500 Subject: [PATCH 07/27] Switch syntax of sym on equalities --- src/Data/Rational/Unnormalised/Properties.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 15e8a0b843..af81d977ba 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1949,7 +1949,7 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q ⌊q⌋≤q q@record{} = *≤* (begin ⌊ q ⌋ ℤ.* (↧ q) ≤⟨ ℤ.[n/d]*d≤n (↥ q) (↧ q) ⟩ - (↥ q) ≡⟨ sym (ℤ.*-identityʳ (↥ q)) ⟩ + (↥ q) ≡⟨ ℤ.*-identityʳ (↥ q) ⟨ (↥ q) ℤ.* (↧ (⌊ q ⌋ / 1)) ∎) where open ℤ.≤-Reasoning q<⌊q⌋+1 : ∀ q → q < ⌊ q ⌋ / 1 + 1ℚᵘ @@ -1961,7 +1961,7 @@ q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict d ℤ.+ ⌊ q ⌋ ℤ.* d ≡⟨ cong (λ h → h ℤ.+ ⌊ q ⌋ ℤ.* d) (sym (ℤ.*-identityˡ d)) ⟩ (1ℤ ℤ.* d) ℤ.+ ⌊ q ⌋ ℤ.* d - ≡⟨ sym (ℤ.*-distribʳ-+ d 1ℤ (n ℤ./ d)) ⟩ + ≡⟨ ℤ.*-distribʳ-+ d 1ℤ (n ℤ./ d) ⟨ (1ℤ ℤ.+ ⌊ q ⌋) ℤ.* d ≡⟨ cong (λ h → h ℤ.* d) (ℤ.+-comm 1ℤ ⌊ q ⌋) ⟩ (⌊ q ⌋ ℤ.+ 1ℤ) ℤ.* d @@ -1987,7 +1987,7 @@ q≤⌈q⌉ q@record{} = subst ∣q-⌊q⌋∣≤1 q = let ⌊q⌋ = ⌊ q ⌋ / 1 in -q≤p≤q⇒∣p∣≤q (q - ⌊ q ⌋ / 1) 1ℚᵘ (begin - 1ℚᵘ ≤⟨ *≤* ℤ.-≤+ ⟩ - 0ℚᵘ ≃⟨ ≃-sym (+-inverseʳ ⌊q⌋) ⟩ + 0ℚᵘ ≃⟨ +-inverseʳ ⌊q⌋ ⟨ ⌊q⌋ - ⌊q⌋ ≤⟨ +-monoˡ-≤ _ (⌊q⌋≤q q) ⟩ q - ⌊q⌋ ∎) (begin @@ -2003,7 +2003,7 @@ q≤⌈q⌉ q@record{} = subst ∣q-⌈q⌉∣≤1 q@record{} = let ⌊-q⌋ = ⌊ - q ⌋ / 1 in begin ∣ q - ⌈ q ⌉ / 1 ∣ ≡⟨⟩ ∣ q - (- ⌊-q⌋) ∣ ≡⟨ cong (λ h → ∣ q + h ∣) (neg-involutive-≡ ⌊-q⌋) ⟩ - ∣ q + ⌊-q⌋ ∣ ≡⟨ sym (∣-p∣≡∣p∣ (q + ⌊-q⌋)) ⟩ + ∣ q + ⌊-q⌋ ∣ ≡⟨ ∣-p∣≡∣p∣ (q + ⌊-q⌋) ⟨ ∣ - (q + ⌊-q⌋) ∣ ≡⟨ cong ∣_∣ (neg-distrib-+ q ⌊-q⌋) ⟩ ∣ - q - ⌊-q⌋ ∣ ≤⟨ ∣q-⌊q⌋∣≤1 (- q) ⟩ 1ℚᵘ ∎ where open ≤-Reasoning @@ -2011,7 +2011,7 @@ q≤⌈q⌉ q@record{} = subst private -½≤q-⌊q+½⌋ : ∀ q → - ½ ≤ q - ⌊ q + ½ ⌋ / 1 -½≤q-⌊q+½⌋ q = begin - - ½ ≃⟨ ≃-sym (+-identityˡ _) ⟩ + - ½ ≃⟨ +-identityˡ _ ⟨ 0ℚᵘ - ½ ≃⟨ +-congˡ (- ½) (≃-sym (+-inverseʳ q)) ⟩ q - q - ½ ≃⟨ +-assoc q _ _ ⟩ q + (- q - ½) ≡⟨ cong (q +_) (sym (neg-distrib-+ q ½)) ⟩ @@ -2041,7 +2041,7 @@ private q-⌈q-½⌉≤½ q = let ⌊-q+½⌋ = ⌊ - q + ½ ⌋ / 1 in begin q - ⌈ q - ½ ⌉ / 1 ≡⟨ cong (λ h → q - h / 1) (ceil-to-floor q) ⟩ q - (- ⌊-q+½⌋) ≡⟨ cong (_- (- ⌊-q+½⌋)) (sym (neg-involutive-≡ q)) ⟩ - - (- q) - (- ⌊-q+½⌋) ≡⟨ sym (neg-distrib-+ (- q) _) ⟩ + - (- q) - (- ⌊-q+½⌋) ≡⟨ neg-distrib-+ (- q) _ ⟨ - (- q - ⌊-q+½⌋) ≤⟨ neg-mono-≤ (-½≤q-⌊q+½⌋ (- q)) ⟩ - (- ½) ≡⟨ neg-involutive-≡ ½ ⟩ ½ ∎ where open ≤-Reasoning From 9d2818cac8f4c6ab45523e3712ee9b6837f999da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Thu, 26 Feb 2026 18:59:31 -0500 Subject: [PATCH 08/27] Apply suggestions from code review --- .../Rational/Unnormalised/Properties.agda | 59 ++++++++++--------- 1 file changed, 32 insertions(+), 27 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index af81d977ba..98b1deb185 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1934,12 +1934,11 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ∣-∣-nonNeg (mkℚᵘ +0 _) = _ ∣-∣-nonNeg (mkℚᵘ -[1+ _ ] _) = _ --q≤p≤q⇒∣p∣≤q : ∀ p q → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q --q≤p≤q⇒∣p∣≤q p q -q≤p p≤q = - [ (λ ∣p∣≡p → subst (_≤ q) (sym ∣p∣≡p) p≤q) - , (λ ∣p∣≡-p → subst (_≤ q) (sym ∣p∣≡-p) - (subst (_ ≤_) (neg-involutive-≡ q) (neg-mono-≤ -q≤p))) ]′ - (∣p∣≡p∨∣p∣≡-p p) +-q≤p≤q⇒∣p∣≤q : ∀ {p q} → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q +-q≤p≤q⇒∣p∣≤q {p} {q} -q≤p p≤q with ∣p∣≡p∨∣p∣≡-p p +... | inj₁ ∣p∣≡p rewrite ∣p∣≡p = p≤q +... | inj₂ ∣p∣≡-p rewrite ∣p∣≡-p = + subst (_ ≤_) (neg-involutive-≡ q) (neg-mono-≤ -q≤p) ------------------------------------------------------------------------ -- Properties of Rounding functions @@ -1954,8 +1953,10 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) q<⌊q⌋+1 : ∀ q → q < ⌊ q ⌋ / 1 + 1ℚᵘ q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict - n ℤ.* 1ℤ ≡⟨ ℤ.*-identityʳ n ⟩ - n ≡⟨ ℤ.a≡a%n+[a/n]*n n d ⟩ + n ℤ.* 1ℤ + ≡⟨ ℤ.*-identityʳ n ⟩ + n + ≡⟨ ℤ.a≡a%n+[a/n]*n n d ⟩ ℤ.+ (n ℤ.% d) ℤ.+ ⌊ q ⌋ ℤ.* d <⟨ ℤ.+-monoˡ-< (⌊ q ⌋ ℤ.* d) (ℤ.+<+ (ℤ.n%d Date: Thu, 26 Feb 2026 21:12:46 -0500 Subject: [PATCH 09/27] Simplify proofs using group properties --- .../Rational/Unnormalised/Properties.agda | 37 +++++++++---------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 98b1deb185..1d50bf9385 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1994,12 +1994,12 @@ private q-⌊q⌋≤1 : ∀ q → q - ⌊ q ⌋ / 1 ≤ 1ℚᵘ q-⌊q⌋≤1 q = let ⌊q⌋ = ⌊ q ⌋ / 1 in begin - q - ⌊q⌋ ≤⟨ <⇒≤ (+-monoˡ-< _ (q<⌊q⌋+1 q)) ⟩ - ⌊q⌋ + 1ℚᵘ - ⌊q⌋ ≃⟨ +-congˡ (- ⌊q⌋) (+-comm ⌊q⌋ 1ℚᵘ) ⟩ - 1ℚᵘ + ⌊q⌋ - ⌊q⌋ ≃⟨ +-assoc 1ℚᵘ ⌊q⌋ (- ⌊q⌋) ⟩ - 1ℚᵘ + (⌊q⌋ - ⌊q⌋) ≃⟨ +-congʳ 1ℚᵘ (+-inverseʳ ⌊q⌋) ⟩ - 1ℚᵘ + 0ℚᵘ ≃⟨ +-identityʳ _ ⟩ - 1ℚᵘ ∎ where open ≤-Reasoning + q - ⌊q⌋ ≤⟨ <⇒≤ (+-monoˡ-< _ (q<⌊q⌋+1 q)) ⟩ + ⌊q⌋ + 1ℚᵘ - ⌊q⌋ ≃⟨ xyx⁻¹≈y ⌊q⌋ 1ℚᵘ ⟩ + 1ℚᵘ ∎ + where + open ≤-Reasoning + open import Algebra.Properties.AbelianGroup +-0-abelianGroup ∣q-⌊q⌋∣≤1 : ∀ q → ∣ q - ⌊ q ⌋ / 1 ∣ ≤ 1ℚᵘ ∣q-⌊q⌋∣≤1 q = -q≤p≤q⇒∣p∣≤q (-1≤q-⌊q⌋ q) (q-⌊q⌋≤1 q) @@ -2016,25 +2016,24 @@ private private -½≤q-⌊q+½⌋ : ∀ q → - ½ ≤ q - ⌊ q + ½ ⌋ / 1 -½≤q-⌊q+½⌋ q = begin - - ½ ≃⟨ +-identityˡ _ ⟨ - 0ℚᵘ - ½ ≃⟨ +-congˡ (- ½) (≃-sym (+-inverseʳ q)) ⟩ - q - q - ½ ≃⟨ +-assoc q _ _ ⟩ + - ½ ≃⟨ \\-leftDividesˡ q (- ½) ⟨ q + (- q - ½) ≡⟨ cong (q +_) (sym (neg-distrib-+ q ½)) ⟩ q - (q + ½) ≤⟨ +-monoʳ-≤ q (neg-mono-≤ (⌊q⌋≤q (q + ½))) ⟩ - q - ⌊ q + ½ ⌋ / 1 ∎ where open ≤-Reasoning + q - ⌊ q + ½ ⌋ / 1 ∎ + where + open ≤-Reasoning + open import Algebra.Properties.Group +-0-group q-⌊q+½⌋≤½ : ∀ q → q - ⌊ q + ½ ⌋ / 1 ≤ ½ q-⌊q+½⌋≤½ q = let ⌊q+½⌋ = ⌊ q + ½ ⌋ / 1 in begin - q - ⌊q+½⌋ ≃⟨ +-congˡ _ (≃-sym (+-identityʳ q)) ⟩ - q + 0ℚᵘ - ⌊q+½⌋ ≃⟨ +-congˡ _ (+-congʳ q (≃-sym (+-inverseʳ ½))) ⟩ - q + (½ - ½) - ⌊q+½⌋ ≃⟨ +-congˡ _ (≃-sym (+-assoc q ½ (- ½))) ⟩ - q + ½ - ½ - ⌊q+½⌋ <⟨ +-monoˡ-< _ (+-monoˡ-< (- ½) (q<⌊q⌋+1 (q + ½))) ⟩ + q - ⌊q+½⌋ ≃⟨ +-congˡ _ (≃-sym (//-rightDividesʳ ½ q)) ⟩ + q + ½ - ½ - ⌊q+½⌋ <⟨ +-monoˡ-< _ (+-monoˡ-< _ (q<⌊q⌋+1 (q + ½))) ⟩ ⌊q+½⌋ + 1ℚᵘ - ½ - ⌊q+½⌋ ≃⟨ +-congˡ (- ⌊q+½⌋) (+-assoc ⌊q+½⌋ 1ℚᵘ (- ½)) ⟩ - ⌊q+½⌋ + ½ - ⌊q+½⌋ ≃⟨ +-congˡ (- ⌊q+½⌋) (+-comm ⌊q+½⌋ ½) ⟩ - ½ + ⌊q+½⌋ - ⌊q+½⌋ ≃⟨ +-assoc ½ ⌊q+½⌋ (- ⌊q+½⌋) ⟩ - ½ + (⌊q+½⌋ - ⌊q+½⌋) ≃⟨ +-congʳ ½ (+-inverseʳ ⌊q+½⌋) ⟩ - ½ + 0ℚᵘ ≃⟨ +-identityʳ ½ ⟩ - ½ ∎ where open ≤-Reasoning + ⌊q+½⌋ + ½ - ⌊q+½⌋ ≃⟨ xyx⁻¹≈y ⌊q+½⌋ ½ ⟩ + ½ ∎ + where + open ≤-Reasoning + open import Algebra.Properties.AbelianGroup +-0-abelianGroup ceil-to-floor : ∀ q → ⌈ q - ½ ⌉ ≡ ℤ.- ⌊ - q + ½ ⌋ ceil-to-floor q@record{} = begin From baf6c2c58302f72a79ba506ce2970d8760e4736c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Thu, 26 Feb 2026 22:36:29 -0500 Subject: [PATCH 10/27] change use of subst in favour of equational reasoning --- src/Data/Rational/Unnormalised/Properties.agda | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 1d50bf9385..44335196aa 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1970,16 +1970,17 @@ q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict (↥ (⌊ q ⌋ / 1 + 1ℚᵘ)) ℤ.* d ∎) where open ℤ.≤-Reasoning q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1 -q≤⌈q⌉ q@record{} = subst - (_≤ - (⌊ - q ⌋ / 1)) - (neg-involutive-≡ q) - (neg-mono-≤ (⌊q⌋≤q (- q))) +q≤⌈q⌉ q@record{} = begin + q ≡⟨ neg-involutive-≡ q ⟨ + - (- q) ≤⟨ neg-mono-≤ (⌊q⌋≤q (- q)) ⟩ + ⌈ q ⌉ / 1 ∎ where open ≤-Reasoning ⌈q⌉-1 Date: Fri, 27 Feb 2026 20:16:56 -0500 Subject: [PATCH 11/27] remove subst and rewrite from proof --- src/Data/Rational/Unnormalised/Properties.agda | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 44335196aa..87c4318206 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1936,9 +1936,12 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) -q≤p≤q⇒∣p∣≤q : ∀ {p q} → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q -q≤p≤q⇒∣p∣≤q {p} {q} -q≤p p≤q with ∣p∣≡p∨∣p∣≡-p p -... | inj₁ ∣p∣≡p rewrite ∣p∣≡p = p≤q -... | inj₂ ∣p∣≡-p rewrite ∣p∣≡-p = - subst (_ ≤_) (neg-involutive-≡ q) (neg-mono-≤ -q≤p) +... | inj₁ ∣p∣≡p = ≤-respˡ-≃ (≃-reflexive (sym ∣p∣≡p)) p≤q +... | inj₂ ∣p∣≡-p = begin + ∣ p ∣ ≡⟨ ∣p∣≡-p ⟩ + - p ≤⟨ neg-mono-≤ -q≤p ⟩ + - (- q) ≡⟨ neg-involutive-≡ q ⟩ + q ∎ where open ≤-Reasoning ------------------------------------------------------------------------ -- Properties of Rounding functions From 5fa00018bb7dae696ae2c6eb5e50760d3a353326 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Fri, 27 Feb 2026 21:12:36 -0500 Subject: [PATCH 12/27] prove ceil <= floor + 1 --- .../Rational/Unnormalised/Properties.agda | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 87c4318206..010c54f6fe 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1985,6 +1985,65 @@ q≤⌈q⌉ q@record{} = begin - (- (⌊ - q ⌋ / 1 + 1ℚᵘ)) ≡⟨ cong -_ (neg-distrib-+ (⌊ - q ⌋ / 1) 1ℚᵘ) ⟩ - (⌈ q ⌉ / 1 - 1ℚᵘ) ∎) where open ≤-Reasoning +private + -[n/d]*d≡-n+n%d : ∀ (n d : ℤ) .{{_ : ℤ.NonZero d}} + → ℤ.- (n ℤ./ d) ℤ.* d ≡ ℤ.- n ℤ.+ (ℤ.+ (n ℤ.% d)) + -[n/d]*d≡-n+n%d n d = + let [n/d]*d = (n ℤ./ d) ℤ.* d; n%d = ℤ.+ (n ℤ.% d) in begin + ℤ.- (n ℤ./ d) ℤ.* d + ≡⟨ ℤ.neg-distribˡ-* (n ℤ./ d) d ⟨ + ℤ.- [n/d]*d + ≡⟨ cong ℤ.-_ (sym (\\-leftDividesʳ n%d [n/d]*d)) ⟩ + ℤ.- (ℤ.- n%d ℤ.+ (n%d ℤ.+ [n/d]*d)) + ≡⟨ cong (λ h → ℤ.- (ℤ.- n%d ℤ.+ h)) (sym (ℤ.a≡a%n+[a/n]*n n d)) ⟩ + ℤ.- (ℤ.- n%d ℤ.+ n) + ≡⟨ ⁻¹-anti-homo-\\ n%d n ⟩ + ℤ.- n ℤ.+ n%d ∎ + where + open ≡-Reasoning + open import Algebra.Properties.AbelianGroup ℤ.+-0-abelianGroup + + ⌈q⌉-⌊q⌋≤1 : ∀ q → ⌈ q ⌉ ℤ.- ⌊ q ⌋ ℤ.≤ 1ℤ + ⌈q⌉-⌊q⌋≤1 q = ℤ.i Date: Fri, 27 Feb 2026 22:05:24 -0500 Subject: [PATCH 13/27] Replace lambda notation and sym use --- .../Rational/Unnormalised/Properties.agda | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 010c54f6fe..2ea54ee22c 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1963,13 +1963,13 @@ q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict ℤ.+ (n ℤ.% d) ℤ.+ ⌊ q ⌋ ℤ.* d <⟨ ℤ.+-monoˡ-< (⌊ q ⌋ ℤ.* d) (ℤ.+<+ (ℤ.n%d Date: Sun, 1 Mar 2026 19:46:24 -0500 Subject: [PATCH 14/27] clean ceil <= floor + 1 proof --- .../Rational/Unnormalised/Properties.agda | 82 +++++++++++-------- 1 file changed, 46 insertions(+), 36 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 2ea54ee22c..fec69a1e7d 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1986,23 +1986,27 @@ q≤⌈q⌉ q@record{} = begin - (⌈ q ⌉ / 1 - 1ℚᵘ) ∎) where open ≤-Reasoning private - -[n/d]*d≡-n+n%d : ∀ (n d : ℤ) .{{_ : ℤ.NonZero d}} - → ℤ.- (n ℤ./ d) ℤ.* d ≡ ℤ.- n ℤ.+ (ℤ.+ (n ℤ.% d)) - -[n/d]*d≡-n+n%d n d = - let [n/d]*d = (n ℤ./ d) ℤ.* d; n%d = ℤ.+ (n ℤ.% d) in begin - ℤ.- (n ℤ./ d) ℤ.* d - ≡⟨ ℤ.neg-distribˡ-* (n ℤ./ d) d ⟨ - ℤ.- [n/d]*d - ≡⟨ cong ℤ.-_ (\\-leftDividesʳ n%d [n/d]*d) ⟨ - ℤ.- (ℤ.- n%d ℤ.+ (n%d ℤ.+ [n/d]*d)) - ≡⟨ cong (λ h → ℤ.- (ℤ.- n%d ℤ.+ h)) (ℤ.a≡a%n+[a/n]*n n d) ⟨ - ℤ.- (ℤ.- n%d ℤ.+ n) - ≡⟨ ⁻¹-anti-homo-\\ n%d n ⟩ - ℤ.- n ℤ.+ n%d ∎ + a≡b+c⇒c≡a-b : ∀ a b c → a ≡ b ℤ.+ c → c ≡ a ℤ.- b + a≡b+c⇒c≡a-b a b c a≡b+c = sym (begin + a ℤ.- b ≡⟨ cong (ℤ._- b) a≡b+c ⟩ + b ℤ.+ c ℤ.- b ≡⟨ xyx⁻¹≈y b c ⟩ + c ∎) where open ≡-Reasoning open import Algebra.Properties.AbelianGroup ℤ.+-0-abelianGroup + -[-n-m]≡n+m : ∀ n m → ℤ.- (ℤ.- n ℤ.- m) ≡ n ℤ.+ m + -[-n-m]≡n+m n m = begin + ℤ.- (ℤ.- n ℤ.- m) ≡⟨ cong (ℤ.-_) (ℤ.neg-distrib-+ n m) ⟨ + ℤ.- (ℤ.- (n ℤ.+ m)) ≡⟨ ℤ.neg-involutive (n ℤ.+ m) ⟩ + n ℤ.+ m ∎ where open ≡-Reasoning + + n+n≡2n : ∀ n → n ℤ.+ n ≡ (ℤ.+ 2) ℤ.* n + n+n≡2n n = begin + n ℤ.+ n ≡⟨ cong (λ x → x ℤ.+ x) (ℤ.*-identityˡ n) ⟨ + 1ℤ ℤ.* n ℤ.+ 1ℤ ℤ.* n ≡⟨ ℤ.*-distribʳ-+ n 1ℤ 1ℤ ⟨ + (ℤ.+ 2) ℤ.* n ∎ where open ≡-Reasoning + ⌈q⌉-⌊q⌋≤1 : ∀ q → ⌈ q ⌉ ℤ.- ⌊ q ⌋ ℤ.≤ 1ℤ ⌈q⌉-⌊q⌋≤1 q = ℤ.i Date: Sun, 1 Mar 2026 20:29:10 -0500 Subject: [PATCH 15/27] floor and ceil of integers --- src/Data/Integer/DivMod.agda | 12 ++++++++++-- src/Data/Rational/Unnormalised/Properties.agda | 6 ++++++ 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda index 4f4572d2eb..f5a4a46491 100644 --- a/src/Data/Integer/DivMod.agda +++ b/src/Data/Integer/DivMod.agda @@ -14,10 +14,10 @@ open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣; open import Data.Integer.Properties open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z Date: Wed, 18 Mar 2026 09:40:40 -0500 Subject: [PATCH 16/27] Remove unnecessary lemma --- .../Rational/Unnormalised/Properties.agda | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 9a86cf6872..eda30b94a6 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1986,15 +1986,6 @@ q≤⌈q⌉ q@record{} = begin - (⌈ q ⌉ / 1 - 1ℚᵘ) ∎) where open ≤-Reasoning private - a≡b+c⇒c≡a-b : ∀ a b c → a ≡ b ℤ.+ c → c ≡ a ℤ.- b - a≡b+c⇒c≡a-b a b c a≡b+c = sym (begin - a ℤ.- b ≡⟨ cong (ℤ._- b) a≡b+c ⟩ - b ℤ.+ c ℤ.- b ≡⟨ xyx⁻¹≈y b c ⟩ - c ∎) - where - open ≡-Reasoning - open import Algebra.Properties.AbelianGroup ℤ.+-0-abelianGroup - -[-n-m]≡n+m : ∀ n m → ℤ.- (ℤ.- n ℤ.- m) ≡ n ℤ.+ m -[-n-m]≡n+m n m = begin ℤ.- (ℤ.- n ℤ.- m) ≡⟨ cong (ℤ.-_) (ℤ.neg-distrib-+ n m) ⟨ @@ -2025,12 +2016,10 @@ private ≡⟨ ℤ.neg-distrib-+ [-n/d]*d [n/d]*d ⟨ ℤ.- ([-n/d]*d ℤ.+ [n/d]*d) ≡⟨ cong₂ (λ x y → ℤ.- (x ℤ.+ y)) - (a≡b+c⇒c≡a-b -n -n%d [-n/d]*d - (ℤ.a≡a%n+[a/n]*n -n d)) - (a≡b+c⇒c≡a-b n n%d [n/d]*d - (ℤ.a≡a%n+[a/n]*n n d)) ⟩ - ℤ.- ((-n ℤ.- -n%d) ℤ.+ (n ℤ.- n%d)) - ≡⟨ cong (λ x → ℤ.- (x ℤ.+ (n ℤ.- n%d))) (ℤ.+-comm -n _) ⟩ + (y≈x\\z -n%d [-n/d]*d -n (sym (ℤ.a≡a%n+[a/n]*n -n d))) + (y≈x\\z n%d [n/d]*d n (sym (ℤ.a≡a%n+[a/n]*n n d))) ⟩ + ℤ.- ( (ℤ.- -n%d ℤ.+ -n) ℤ.+ (ℤ.- n%d ℤ.+ n)) + ≡⟨ cong (λ x → ℤ.- ((ℤ.- -n%d ℤ.+ -n) ℤ.+ x)) (ℤ.+-comm _ n) ⟩ ℤ.- ((ℤ.- -n%d ℤ.+ -n) ℤ.+ (n ℤ.- n%d)) ≡⟨ cong (ℤ.-_) (ℤ.+-minus-telescope (ℤ.- -n%d) n n%d) ⟩ ℤ.- (ℤ.- -n%d ℤ.- n%d) From cabc7f478765a43ee49c76fae15e2676567a0a19 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Sun, 2 Aug 2026 17:54:50 -0500 Subject: [PATCH 17/27] =?UTF-8?q?prettier=20proof=20of=20=E2=8C=88q?= =?UTF-8?q?=E2=8C=89=E2=89=A4=E2=8C=8Aq=E2=8C=8B+1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Rational/Unnormalised/Properties.agda | 81 +++++++------------ 1 file changed, 29 insertions(+), 52 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 6e9ef612fc..ea349190b2 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1571,6 +1571,23 @@ p>1⇒1/p<1 {p} p>1 = lemma′ p (p>1⇒p≢0 p>1) p>1 1/q≥0 : NonNegative 1/q 1/q≥0 = pos⇒nonNeg 1/q {{1/pos⇒pos q}} +------------------------------------------------------------------------ +-- Properties of _/_ + +/-cancelʳ-< : ∀ {i} {j} d .{{_ : ℕ.NonZero d}} → i / d < j / d → i ℤ.< j +/-cancelʳ-< {i} {j} d@(suc _) (*<* i*d Date: Sun, 2 Aug 2026 18:42:52 -0500 Subject: [PATCH 18/27] floor and ceil are optimal --- .../Rational/Unnormalised/Properties.agda | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index ea349190b2..67b1e04d08 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -2025,6 +2025,36 @@ q≤⌈q⌉ q@record{} = begin (ℤ.*-identityʳ 1ℤ) ⟩ ⌊ q ⌋ ℤ.+ 1ℤ ∎ +i/1≤q⇒i≤⌊q⌋ : ∀ i q → i / 1 ≤ q → i ℤ.≤ ⌊ q ⌋ +i/1≤q⇒i≤⌊q⌋ i q i/1≤q = begin + i ≤⟨ ℤ.i Date: Sun, 2 Aug 2026 20:14:02 -0500 Subject: [PATCH 19/27] relate floor and ceil and reduce their error --- .../Rational/Unnormalised/Properties.agda | 41 +++++++++++++------ 1 file changed, 28 insertions(+), 13 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 67b1e04d08..0013001184 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1965,8 +1965,24 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) - (- q) ≡⟨ neg-involutive-≡ q ⟩ q ∎ where open ≤-Reasoning +-q Date: Sat, 8 Aug 2026 19:13:16 -0500 Subject: [PATCH 20/27] *-cancel-/ for Integers --- src/Data/Integer/DivMod.agda | 118 +++++++++++++++++++++++++++++-- src/Data/Integer/Properties.agda | 26 ++++++- src/Data/Nat/DivMod.agda | 5 ++ src/Data/Nat/Properties.agda | 3 + 4 files changed, 144 insertions(+), 8 deletions(-) diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda index f5a4a46491..731c494b0a 100644 --- a/src/Data/Integer/DivMod.agda +++ b/src/Data/Integer/DivMod.agda @@ -8,16 +8,17 @@ module Data.Integer.DivMod where -open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣; - _%ℕ_; _/ℕ_; _+_; _*_; -_; _-_; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _<_; +≤+; suc; - +<+) +open import Data.Integer.Base open import Data.Integer.Properties open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z0∧j<0⇒i*j<0 (+ m) i + helper : (+ m * i) /ℕ (m ℕ.* n) ≡ i /ℕ n + helper with ∣ + m * i ∣ ℕ.% (m ℕ.* n) in ∣m*i∣%[m*n] + ... | ℕ.zero = begin-equality + (+ m * i) /ℕ (m ℕ.* n) + ≡⟨ neg[i]∧∣i∣%d≡0⇒i/ℕd (+ m * i) ∣m*i∣%[m*n] ⟩ + - (+ (∣ + m * i ∣ ℕ./ (m ℕ.* n))) + ≡⟨ cong (-_ ∘′ +_ ∘′ (ℕ._/ _)) (∣i*j∣≡∣i∣*∣j∣ (+ m) i) ⟩ + - (+ ((m ℕ.* ∣ i ∣) ℕ./ (m ℕ.* n))) + ≡⟨ cong (-_ ∘′ +_) (ℕ.m*n/m*o≡n/o m ∣ i ∣ n) ⟩ + - (+ (∣ i ∣ ℕ./ n)) ≡⟨ neg[i]∧∣i∣%d≡0⇒i/ℕd i ∣i∣%m≡0 ⟨ + i /ℕ n ∎ + where + m*[∣i∣%n]≡0 : m ℕ.* (∣ i ∣ ℕ.% n) ≡ 0 + m*[∣i∣%n]≡0 rewrite m*[∣i∣%n]≡∣m*i∣%[m*n] | ∣m*i∣%[m*n] = refl + ∣i∣%m≡0 : ∣ i ∣ ℕ.% n ≡ 0 + ∣i∣%m≡0 = ℕ.m*n≡0⇒n≡0 m _ m*[∣i∣%n]≡0 + ... | ℕ.suc _ = begin-equality + (+ m * i) /ℕ (m ℕ.* n) + ≡⟨ neg[i]∧∣i∣%d≢0⇒i/ℕd (+ m * i) (m ℕ.* n) ⟩ + -[1+ ∣ + m * i ∣ ℕ./ (m ℕ.* n) ] + ≡⟨ cong (-[1+_] ∘′ (ℕ._/ (m ℕ.* n))) (∣i*j∣≡∣i∣*∣j∣ (+ m) i) ⟩ + -[1+ (m ℕ.* ∣ i ∣) ℕ./ (m ℕ.* n) ] + ≡⟨ cong -[1+_] (ℕ.m*n/m*o≡n/o m ∣ i ∣ n) ⟩ + -[1+ ∣ i ∣ ℕ./ n ] ≡⟨ neg[i]∧∣i∣%d≢0⇒i/ℕd i n ⟨ + i /ℕ n ∎ + where instance + ∣m*i∣%[m*n]≢0 : ℕ.NonZero (∣ + m * i ∣ ℕ.% (m ℕ.* n)) + ∣m*i∣%[m*n]≢0 rewrite ∣m*i∣%[m*n] = _ + m*[∣i∣%n]≢0 : ℕ.NonZero (m ℕ.* (∣ i ∣ ℕ.% n)) + m*[∣i∣%n]≢0 rewrite m*[∣i∣%n]≡∣m*i∣%[m*n] | ∣m*i∣%[m*n] = _ + ∣i∣%n≢0 : ℕ.NonZero (∣ i ∣ ℕ.% n) + ∣i∣%n≢0 = ℕ.m*n≢0⇒n≢0 m + +*-cancelʳ-/ℕ : ∀ i m n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (n ℕ.* m)}} → + (i * + m) /ℕ (n ℕ.* m) ≡ i /ℕ n +*-cancelʳ-/ℕ i m n rewrite *-comm i (+ m) | ℕ.*-comm n m = *-cancelˡ-/ℕ m i n + +*-cancelˡ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (i * k)}} → + {{_ : NonNegative i}} → (i * j) / (i * k) ≡ j / k +*-cancelˡ-/ (+ i) j k = begin-equality + (sign (+ i * k) ◃ 1) * ((+ i * j) /ℕ ∣ + i * k ∣) + ≡⟨ cong (λ x → (x ◃ 1) * ((+ i * j) /ℕ _)) (sign-* (+ i) k)⟩ + (sign k ◃ 1) * ((+ i * j) /ℕ ∣ + i * k ∣) + ≡⟨ cong ((sign k ◃ 1) *_) (/ℕ-congʳ (+ i * j) (∣i*j∣≡∣i∣*∣j∣ (+ i) k)) ⟩ + (sign k ◃ 1) * ((+ i * j) /ℕ (∣ + i ∣ ℕ.* ∣ k ∣)) + ≡⟨ cong ((sign k ◃ 1) *_) (*-cancelˡ-/ℕ i j ∣ k ∣) ⟩ + j / k ∎ + where + instance + _ : NonZero (+ i) + _ = i*j≢0⇒i≢0 (+ i) + _ : ℕ.NonZero (∣ + i ∣ ℕ.* ∣ k ∣) + _ = ℕ.m*n≢0 ∣ + i ∣ ∣ k ∣ + +*-cancelʳ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (k * j)}} → + {{_ : NonNegative j}} → (i * j) / (k * j) ≡ i / k +*-cancelʳ-/ i j k rewrite *-comm i j | *-comm k j = *-cancelˡ-/ j i k + ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 78b58585c5..da7d96ce91 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -36,12 +36,12 @@ open import Relation.Binary.Structures open import Relation.Binary.Definitions using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri<; tri>) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; cong; cong₂; sym; _≢_; subst; subst₂; resp₂; trans) + using (_≡_; refl; cong; cong₂; sym; _≢_; ≢-sym; subst; subst₂; resp₂; trans) open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning; setoid; decSetoid; isEquivalence) open import Relation.Nullary.Decidable.Core using (yes; no) import Relation.Nullary.Reflects as Reflects -open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Negation.Core using (¬_; contradiction; contraposition) import Relation.Nullary.Decidable as Dec open import Algebra.Definitions {A = ℤ} _≡_ @@ -407,9 +407,16 @@ nonPositive⁻¹ -[1+ n ] = -≤+ nonNegative⁻¹ : ∀ i → .{{NonNegative i}} → i ≥ 0ℤ nonNegative⁻¹ (+ n) = +≤+ z≤n +nonZero⁻¹ : ∀ i → .{{NonZero i}} → i ≢ 0ℤ +nonZero⁻¹ (+ n) = contraposition +-injective (ℕ.≢-nonZero⁻¹ n) +nonZero⁻¹ -[1+ n ] () + negative j *-cancelʳ-<-neg {i} {j} n = *-cancelʳ-<-nonPos -[1+ n ] +------------------------------------------------------------------------ +-- Properties of _*_ and Positive/NonPositive/Negative/NonNegative + +i≥0∧j≥0⇒i*j≥0 : ∀ i j → .{{NonNegative i}} → .{{NonNegative j}} → NonNegative (i * j) +i≥0∧j≥0⇒i*j≥0 i j = nonNegative (*-monoʳ-≤-nonNeg j (nonNegative⁻¹ i)) + +i>0∧j<0⇒i*j<0 : ∀ i j → .{{Positive i}} → .{{Negative j}} → Negative (i * j) +i>0∧j<0⇒i*j<0 i j = negative (*-monoʳ-<-neg j (positive⁻¹ i)) + ------------------------------------------------------------------------ -- Properties of _*_ and ∣_∣ diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index 86bc8d3168..eaf94f05aa 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -440,6 +440,11 @@ m%n*o≡m*o%[n*o] m n o = begin-equality m * o ∸ m * o / (n * o) * (n * o) ≡⟨ m%n≡m∸m/n*n (m * o) (n * o) ⟨ m * o % (n * o) ∎ +m*n%o≡m*n%[m*o] : ∀ m n o .{{_ : NonZero o}} .{{_ : NonZero (m * o)}} → + m * (n % o) ≡ (m * n) % (m * o) +m*n%o≡m*n%[m*o] m n o rewrite *-comm m (n % o) | *-comm m n | *-comm m o + = m%n*o≡m*o%[n*o] n o m + [m*n+o]%[p*n]≡[m*n]%[p*n]+o : ∀ m {n o} p .{{_ : NonZero (p * n)}} → o < n → (m * n + o) % (p * n) ≡ (m * n) % (p * n) + o [m*n+o]%[p*n]≡[m*n]%[p*n]+o m {n} {o} p@(suc p-1) o Date: Sat, 8 Aug 2026 19:32:11 -0500 Subject: [PATCH 21/27] congruence for floor, ceil, round in Unnormalized Rational --- src/Data/Bool/Properties.agda | 12 +++++ .../Rational/Unnormalised/Properties.agda | 52 +++++++++++++++++-- src/Relation/Nullary/Reflects.agda | 14 +++++ 3 files changed, 75 insertions(+), 3 deletions(-) diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index 53b4a1f4a7..fc6c372653 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -839,10 +839,22 @@ T-≡ : ∀ {x} → T x ⇔ x ≡ true T-≡ {false} = mk⇔ (λ ()) (λ ()) T-≡ {true} = mk⇔ (const refl) (const _) +T-to-≡ : ∀ {x} → T x → x ≡ true +T-to-≡ = Equivalence.to T-≡ + +≡-to-T : ∀ {x} → x ≡ true → T x +≡-to-T = Equivalence.from T-≡ + T-not-≡ : ∀ {x} → T (not x) ⇔ x ≡ false T-not-≡ {false} = mk⇔ (const refl) (const _) T-not-≡ {true} = mk⇔ (λ ()) (λ ()) +T-not-to-≡ : ∀ {x} → T (not x) → x ≡ false +T-not-to-≡ = Equivalence.to T-not-≡ + +≡-to-T-not : ∀ {x} → x ≡ false → T (not x) +≡-to-T-not = Equivalence.from T-not-≡ + T-∧ : ∀ {x y} → T (x ∧ y) ⇔ (T x × T y) T-∧ {true} {true} = mk⇔ (const (_ , _)) (const _) T-∧ {true} {false} = mk⇔ (λ ()) proj₂ diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 0013001184..d1654fb9b4 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -27,7 +27,8 @@ open import Algebra.Construct.NaturalChoice.Base using (MaxOperator; MinOperator) import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp -open import Data.Bool.Base using (T; true; false) +open import Data.Bool.Base using (T; true; false; not) +open import Data.Bool.Properties using (if-cong; T-to-≡; ≡-to-T; T-not-to-≡; ≡-to-T-not) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Base as ℕ using (suc; pred) import Data.Nat.Properties as ℕ @@ -43,8 +44,6 @@ open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂) import Data.Sign as Sign open import Function.Base using (_on_; _$_; _∘_; flip) open import Level using (0ℓ) -open import Relation.Nullary.Decidable.Core as Dec using (yes; no) -open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder @@ -63,6 +62,10 @@ open import Relation.Binary.PropositionalEquality import Relation.Binary.Properties.Poset as PosetProperties import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Reasoning.Syntax +open import Relation.Nullary.Decidable.Core as Dec using (yes; no) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Reflects + using (Reflects; fromEquivalence; reflects-false; reflects-refute) open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup @@ -407,6 +410,15 @@ antimono⇒cong = BC.antimono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antis ≤⇒≤ᵇ : p ≤ q → T (p ≤ᵇ q) ≤⇒≤ᵇ = ℤ.≤⇒≤ᵇ ∘ drop-*≤* +≤ᵇ-reflects-≤ : ∀ p q → Reflects (p ≤ q) (p ≤ᵇ q) +≤ᵇ-reflects-≤ p q = fromEquivalence ≤ᵇ⇒≤ ≤⇒≤ᵇ + +≰ᵇ⇒≰ : T (not (p ≤ᵇ q)) → p ≰ q +≰ᵇ⇒≰ {p} {q} p≰ᵇq = reflects-false (≤ᵇ-reflects-≤ p q) (T-not-to-≡ p≰ᵇq) + +≰⇒≰ᵇ : p ≰ q → T (not (p ≤ᵇ q)) +≰⇒≰ᵇ {p} {q} p≰q = ≡-to-T-not (reflects-refute (≤ᵇ-reflects-≤ p q) p≰q) + ------------------------------------------------------------------------ -- Properties of _<_ ------------------------------------------------------------------------ @@ -1977,6 +1989,40 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ------------------------------------------------------------------------ -- Properties of Rounding functions +floor-cong : ∀ {p} {q} → p ≃ q → ⌊ p ⌋ ≡ ⌊ q ⌋ +floor-cong {p@record{}} {q@record{}} (*≡* ↥p↧q≡↥q↧p) = begin + ↥ p ℤ./ ↧ p ≡⟨ ℤ.*-cancelʳ-/ (↥ p) (↧ q) (↧ p) ⟨ + (↥ p ℤ.* ↧ q) ℤ./ (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._/ (↧ p ℤ.* ↧ q)) ↥p↧q≡↥q↧p ⟩ + (↥ q ℤ.* ↧ p) ℤ./ (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._/ (↧ p ℤ.* ↧ q)) (ℤ.*-comm (↥ q) _)⟩ + (↧ p ℤ.* ↥ q) ℤ./ (↧ p ℤ.* ↧ q) ≡⟨ ℤ.*-cancelˡ-/ (↧ p) (↥ q) (↧ q) ⟩ + ↥ q ℤ./ ↧ q ∎ where open ≡-Reasoning + +ceiling-cong : ∀ {p} {q} → p ≃ q → ⌈ p ⌉ ≡ ⌈ q ⌉ +ceiling-cong {p@record{}} {q@record{}} eq = cong ℤ.-_ (floor-cong (-‿cong eq)) + +round-cong : ∀ {p} {q} → p ≃ q → round p ≡ round q +round-cong {p@record{}} {q@record{}} eq with p ≤ᵇ 0ℚᵘ in leq +... | false = begin + ⌊ p + ½ ⌋ ≡⟨ floor-cong (+-congˡ ½ eq) ⟩ + ⌊ q + ½ ⌋ ≡⟨ if-cong q≤ᵇ0≡false ⟨ + round q ∎ + where + open ≡-Reasoning + 0 ∘ ≰ᵇ⇒≰ ∘ ≡-to-T-not) leq) + q≤ᵇ0≡false : (q ≤ᵇ 0ℚᵘ) ≡ false + q≤ᵇ0≡false = T-not-to-≡ (≰⇒≰ᵇ (<⇒≱ 0 Date: Sat, 8 Aug 2026 19:39:02 -0500 Subject: [PATCH 22/27] round(-q) = round(q) for Unnormalized Rational --- .../Rational/Unnormalised/Properties.agda | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index d1654fb9b4..f68233f8ba 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -2029,6 +2029,34 @@ round-cong {p@record{}} {q@record{}} eq with p ≤ᵇ 0ℚᵘ in leq ⌈-q⌉≡-⌊q⌋ : ∀ q → ⌈ - q ⌉ ≡ ℤ.- ⌊ q ⌋ ⌈-q⌉≡-⌊q⌋ q@record{} = cong (λ x → ℤ.- ⌊ x ⌋) (neg-involutive-≡ q) +private + q>0⇒round[-q]≡round[q] : ∀ {q} → q > 0ℚᵘ → round (- q) ≡ ℤ.- round q + q>0⇒round[-q]≡round[q] {q} q>0 = begin + round (- q) ≡⟨ if-cong -q≤0 ⟩ + ⌈ - q - ½ ⌉ ≡⟨ cong ceiling (neg-distrib-+ q ½) ⟨ + ⌈ - (q + ½) ⌉ ≡⟨ ⌈-q⌉≡-⌊q⌋ (q + ½) ⟩ + ℤ.- ⌊ q + ½ ⌋ ≡⟨ cong ℤ.-_ (if-cong q≥0) ⟨ + ℤ.- round q ∎ + where + open ≡-Reasoning + -q≤0 : (- q ≤ᵇ 0ℚᵘ) ≡ true + -q≤0 = T-to-≡ (≤⇒≤ᵇ (<⇒≤ (neg-mono-< q>0))) + q≥0 : (q ≤ᵇ 0ℚᵘ) ≡ false + q≥0 = T-not-to-≡ (≰⇒≰ᵇ (<⇒≱ q>0)) + +round[-q]≡round[q] : ∀ q → round (- q) ≡ ℤ.- (round q) +round[-q]≡round[q] q@record{} with <-cmp q 0ℚᵘ +... | tri< a ¬b ¬c = begin + round (- q) ≡⟨ ℤ.neg-involutive (round (- q)) ⟨ + ℤ.- (ℤ.- round (- q)) ≡⟨ cong ℤ.-_ (q>0⇒round[-q]≡round[q] (neg-mono-< a)) ⟨ + ℤ.- round (- (- q)) ≡⟨ cong (ℤ.-_ ∘ round) (neg-involutive-≡ q) ⟩ + ℤ.- round q ∎ where open ≡-Reasoning +... | tri≈ ¬a b ¬c = begin + round (- q) ≡⟨ round-cong (-‿cong b) ⟩ + ℤ.- 0ℤ ≡⟨ cong ℤ.-_ (round-cong b) ⟨ + ℤ.- round q ∎ where open ≡-Reasoning +... | tri> ¬a ¬b c = q>0⇒round[-q]≡round[q] c + ------------------------------------------------------------------------ -- Bounds of ⌊_⌋ and ⌈_⌉ From b798e8b1e408c30c630ce5889f9361aff09576b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Sat, 8 Aug 2026 20:15:29 -0500 Subject: [PATCH 23/27] tweak proof of error of floor and round --- .../Rational/Unnormalised/Properties.agda | 102 +++++++----------- 1 file changed, 41 insertions(+), 61 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index f68233f8ba..1614d2e9fc 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -2044,8 +2044,8 @@ private q≥0 : (q ≤ᵇ 0ℚᵘ) ≡ false q≥0 = T-not-to-≡ (≰⇒≰ᵇ (<⇒≱ q>0)) -round[-q]≡round[q] : ∀ q → round (- q) ≡ ℤ.- (round q) -round[-q]≡round[q] q@record{} with <-cmp q 0ℚᵘ +round[-q]≡-round[q] : ∀ q → round (- q) ≡ ℤ.- (round q) +round[-q]≡-round[q] q@record{} with <-cmp q 0ℚᵘ ... | tri< a ¬b ¬c = begin round (- q) ≡⟨ ℤ.neg-involutive (round (- q)) ⟨ ℤ.- (ℤ.- round (- q)) ≡⟨ cong ℤ.-_ (q>0⇒round[-q]≡round[q] (neg-mono-< a)) ⟨ @@ -2148,25 +2148,23 @@ q≤i/1⇒⌈q⌉≤i i q q≤i/1 = begin ------------------------------------------------------------------------ -- Approximation errors of ⌊_⌋ ⌈_⌉ and round(_) -private - -1 Date: Sun, 9 Aug 2026 22:52:44 -0500 Subject: [PATCH 24/27] round is optimal --- src/Data/Integer/Base.agda | 13 ++++ src/Data/Integer/Properties.agda | 3 + .../Rational/Unnormalised/Properties.agda | 67 +++++++++++++++++-- 3 files changed, 77 insertions(+), 6 deletions(-) diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda index db856b355f..48bc9fc72f 100644 --- a/src/Data/Integer/Base.agda +++ b/src/Data/Integer/Base.agda @@ -103,6 +103,19 @@ data _<_ : ℤ → ℤ → Set where -<+ : ∀ {m n} → -[1+ m ] < + n +<+ : ∀ {m n} → (m Date: Sun, 9 Aug 2026 23:28:14 -0500 Subject: [PATCH 25/27] remove unnecessary rewrites, change n to i for integer --- src/Data/Integer/DivMod.agda | 21 +++++++++---------- .../Rational/Unnormalised/Properties.agda | 2 +- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda index 731c494b0a..7f403f38e8 100644 --- a/src/Data/Integer/DivMod.agda +++ b/src/Data/Integer/DivMod.agda @@ -17,7 +17,7 @@ import Data.Nat.Properties as ℕ using (m∸n≤m; m*n≢0; m*n≢0⇒m≢0; m* m*n≡0⇒n≡0; *-comm) open import Function.Base using (_∘′_) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; _≢_; refl; cong; sym; subst; trans) + using (_≡_; _≢_; refl; cong; sym; subst; trans; respʳ) open import Relation.Nullary.Negation using (contradiction) open ≤-Reasoning @@ -91,9 +91,7 @@ div-neg-is-neg-/ℕ n (ℕ.suc d) = -1*i≡-i (n /ℕ ℕ.suc d) 0≤n⇒0≤n/ℕd (+ n) d (+≤+ m≤n) = +≤+ z≤n 0≤n⇒0≤n/d : ∀ n d .{{_ : NonZero d}} → 0ℤ ≤ n → 0ℤ ≤ d → 0ℤ ≤ (n / d) -0≤n⇒0≤n/d n (+ d) {{d≢0}} 0≤n (+≤+ 0≤d) - rewrite div-pos-is-/ℕ n d {{d≢0}} - = 0≤n⇒0≤n/ℕd n d 0≤n +0≤n⇒0≤n/d n (+ d) 0≤n _ = respʳ _≤_ (sym (div-pos-is-/ℕ n d)) (0≤n⇒0≤n/ℕd n d 0≤n) [n/d]*d≤n : ∀ n d .{{_ : NonZero d}} → (n / d) * d ≤ n [n/d]*d≤n n (+ d) = begin @@ -130,13 +128,13 @@ a≡a%n+[a/n]*n n d@(-[1+ _ ]) = begin-equality + r + - q * d ≡⟨ cong (_+_ (+ r) ∘′ (_* d)) (sym (-1*i≡-i q)) ⟩ + r + n / d * d ∎ -n/ℕ1≡n : ∀ n → n /ℕ 1 ≡ n -n/ℕ1≡n (+ n) = cong +_ (ℕ.n/1≡n n) -n/ℕ1≡n -[1+ n ] with ℕ.suc n ℕ.% 1 | ℕ.n%1≡0 (ℕ.suc n) +i/ℕ1≡i : ∀ i → i /ℕ 1 ≡ i +i/ℕ1≡i (+ n) = cong +_ (ℕ.n/1≡n n) +i/ℕ1≡i -[1+ n ] with ℕ.suc n ℕ.% 1 | ℕ.n%1≡0 (ℕ.suc n) ... | ℕ.zero | suc[n]%1≡0 = cong (λ x → - (+ x)) (ℕ.n/1≡n (ℕ.suc n)) -n/1≡n : ∀ n → n / + 1 ≡ n -n/1≡n n = trans (div-pos-is-/ℕ n 1) (n/ℕ1≡n n) +i/1≡i : ∀ i → i / + 1 ≡ i +i/1≡i i = trans (div-pos-is-/ℕ i 1) (i/ℕ1≡i i) /ℕ-congʳ : ∀ i {m} {n} .{{_ : ℕ.NonZero m}} → .{{_ : ℕ.NonZero n}} → m ≡ n → i /ℕ m ≡ i /ℕ n @@ -177,7 +175,8 @@ neg[i]∧∣i∣%d≢0⇒i/ℕd -[1+ n ] d {{_}} {{_}} {{mod}} with ℕ.suc n *-cancelˡ-/ℕ m i@(-[1+ _ ]) n = helper where m*[∣i∣%n]≡∣m*i∣%[m*n] : m ℕ.* (∣ i ∣ ℕ.% n) ≡ ∣ + m * i ∣ ℕ.% (m ℕ.* n) - m*[∣i∣%n]≡∣m*i∣%[m*n] rewrite ∣i*j∣≡∣i∣*∣j∣ (+ m) i = ℕ.m*n%o≡m*n%[m*o] m ∣ i ∣ n + m*[∣i∣%n]≡∣m*i∣%[m*n] = trans (ℕ.m*n%o≡m*n%[m*o] m ∣ i ∣ n) + (cong (ℕ._% (m ℕ.* n)) (sym (∣i*j∣≡∣i∣*∣j∣ (+ m) i))) instance _ : ℕ.NonZero m _ = ℕ.m*n≢0⇒m≢0 m @@ -198,7 +197,7 @@ neg[i]∧∣i∣%d≢0⇒i/ℕd -[1+ n ] d {{_}} {{_}} {{mod}} with ℕ.suc n i /ℕ n ∎ where m*[∣i∣%n]≡0 : m ℕ.* (∣ i ∣ ℕ.% n) ≡ 0 - m*[∣i∣%n]≡0 rewrite m*[∣i∣%n]≡∣m*i∣%[m*n] | ∣m*i∣%[m*n] = refl + m*[∣i∣%n]≡0 = trans m*[∣i∣%n]≡∣m*i∣%[m*n] ∣m*i∣%[m*n] ∣i∣%m≡0 : ∣ i ∣ ℕ.% n ≡ 0 ∣i∣%m≡0 = ℕ.m*n≡0⇒n≡0 m _ m*[∣i∣%n]≡0 ... | ℕ.suc _ = begin-equality diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index bedab303fa..7bacd664de 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -2233,7 +2233,7 @@ q≤i/1⇒⌈q⌉≤i i q q≤i/1 = begin q + ℤ.- round q / 1 ∎ ⌊i/1⌋≡i : ∀ i → ⌊ i / 1 ⌋ ≡ i -⌊i/1⌋≡i i = ℤ.n/1≡n i +⌊i/1⌋≡i i = ℤ.i/1≡i i ⌈i/1⌉≡i : ∀ i → ⌈ i / 1 ⌉ ≡ i ⌈i/1⌉≡i i = trans (cong ℤ.-_ (⌊i/1⌋≡i (ℤ.- i))) (ℤ.neg-involutive i) From d8193fd6075d6eafa1f478a349cdac58cfe9f710 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Ortega?= Date: Mon, 10 Aug 2026 00:10:02 -0500 Subject: [PATCH 26/27] =?UTF-8?q?extract=20lemma=20from=20q<=E2=8C=8Aq?= =?UTF-8?q?=E2=8C=8B+1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Rational/Unnormalised/Properties.agda | 99 +++++++++---------- 1 file changed, 48 insertions(+), 51 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 7bacd664de..5f1255f86f 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -2049,6 +2049,12 @@ round-cong {p@record{}} {q@record{}} eq with p ≤ᵇ 0ℚᵘ in leq q≤ᵇ0≡true : (q ≤ᵇ 0ℚᵘ) ≡ true q≤ᵇ0≡true = T-to-≡ (≤⇒≤ᵇ q≤0) +⌊i/1⌋≡i : ∀ i → ⌊ i / 1 ⌋ ≡ i +⌊i/1⌋≡i i = ℤ.i/1≡i i + +⌈i/1⌉≡i : ∀ i → ⌈ i / 1 ⌉ ≡ i +⌈i/1⌉≡i i = trans (cong ℤ.-_ (⌊i/1⌋≡i (ℤ.- i))) (ℤ.neg-involutive i) + ⌊-q⌋≡-⌈q⌉ : ∀ q → ⌊ - q ⌋ ≡ ℤ.- ⌈ q ⌉ ⌊-q⌋≡-⌈q⌉ q@record{} = sym (ℤ.neg-involutive ⌊ - q ⌋) @@ -2094,21 +2100,19 @@ round[-q]≡-round[q] q@record{} with <-cmp q 0ℚᵘ q<⌊q⌋+1 : ∀ q → q < ⌊ q ⌋ / 1 + 1ℚᵘ q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict - n ℤ.* 1ℤ - ≡⟨ ℤ.*-identityʳ n ⟩ - n - ≡⟨ ℤ.a≡a%n+[a/n]*n n d ⟩ - ℤ.+ (n ℤ.% d) ℤ.+ ⌊ q ⌋ ℤ.* d - <⟨ ℤ.+-monoˡ-< (⌊ q ⌋ ℤ.* d) (ℤ.+<+ (ℤ.n%d Date: Mon, 10 Aug 2026 01:07:17 -0500 Subject: [PATCH 27/27] Update CHANGELOG.md --- CHANGELOG.md | 108 ++++++++++++++++++++++++++++++----- src/Data/Integer/DivMod.agda | 12 ++-- 2 files changed, 102 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 16a3c48095..82ca5eeab7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -252,6 +252,14 @@ Additions to existing modules ``` NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`. +* In `Data.Bool.Properties`: + ```agda + T-to-≡ : ∀ {x} → T x → x ≡ true + ≡-to-T : ∀ {x} → x ≡ true → T x + T-not-to-≡ : ∀ {x} → T (not x) → x ≡ false + ≡-to-T-not : ∀ {x} → x ≡ false → T (not x) + ``` + * In `Data.Fin.Permutation.Components`: ```agda transpose[i,i,j]≡j : (i j : Fin n) → transpose i i j ≡ j @@ -282,12 +290,47 @@ Additions to existing modules * In `Data.Integer.Base`: ``` _<ᵇ_ : ℤ → ℤ → Bool + -≤-⁻¹ : ∀ {m} {n} → -[1+ m ] ≤ -[1+ n ] → n ℕ.≤ m + +≤+⁻¹ : ∀ {m} {n} → + m ≤ + n → m ℕ.≤ n + -<-⁻¹ : ∀ {m} {n} → -[1+ m ] < -[1+ n ] → n ℕ.< m + +<+⁻¹ : ∀ {m} {n} → + m < + n → m ℕ.< n + ``` + +* In `Data.Integer.DivMod`: + ```agda + i/ℕ1≡i : ∀ i → i /ℕ 1 ≡ i + i/1≡i : ∀ i → i / + 1 ≡ i + /ℕ-congʳ : ∀ i {m} {n} .{{_ : ℕ.NonZero m}} → .{{_ : ℕ.NonZero n}} → + m ≡ n → i /ℕ m ≡ i /ℕ n + nonNeg[i]⇒i/ℕd : ∀ i d .{{_ : ℕ.NonZero d}} .{{_ : NonNegative i}} → + i /ℕ d ≡ + (∣ i ∣ ℕ./ d) + neg[i]∧∣i∣%d≡0⇒i/ℕd : ∀ i {d} .{{_ : ℕ.NonZero d}} .{{_ : Negative i}} → + ∣ i ∣ ℕ.% d ≡ 0 → i /ℕ d ≡ - (+ (∣ i ∣ ℕ./ d)) + neg[i]∧∣i∣%d≢0⇒i/ℕd : ∀ i d .{{_ : ℕ.NonZero d}} .{{_ : Negative i}} + .{{_ : ℕ.NonZero (∣ i ∣ ℕ.% d)}} → i /ℕ d ≡ -[1+ ∣ i ∣ ℕ./ d ] + *-cancelˡ-/ℕ : ∀ m i n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (m ℕ.* n)}} → + (+ m * i) /ℕ (m ℕ.* n) ≡ i /ℕ n + *-cancelʳ-/ℕ : ∀ i m n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (n ℕ.* m)}} → + (i * + m) /ℕ (n ℕ.* m) ≡ i /ℕ n + *-cancelˡ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (i * k)}} → + .{{_ : NonNegative i}} → (i * j) / (i * k) ≡ j / k + *-cancelʳ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (k * j)}} → + .{{_ : NonNegative j}} → (i * j) / (k * j) ≡ i / k ``` * In `Data.Integer.Properties`: ``` <ᵇ⇒< : T (i <ᵇ j) → i < j <⇒<ᵇ : i < j → T (i <ᵇ j) + nonZero⁻¹ : ∀ i → .{{NonZero i}} → i ≢ 0ℤ + nonNeg∧nonZero⇒Pos : ∀ i → .{{NonNegative i}} → .{{NonZero i}} → Positive i + ∣i-j∣≡0⇒i≡j : ∀ {i} {j} → ∣ i - j ∣ ≡ 0 → i ≡ j + i*j≢0⇒i≢0 : ∀ i {j} .{{_ : NonZero (i * j)}} → NonZero i + i*j≢0⇒j≢0 : ∀ i {j} .{{_ : NonZero (i * j)}} → NonZero j + i≥0∧j≥0⇒i*j≥0 : ∀ i j → .{{NonNegative i}} → .{{NonNegative j}} → + NonNegative (i * j) + i>0∧j<0⇒i*j<0 : ∀ i j → .{{Positive i}} → .{{Negative j}} → + Negative (i * j) ``` * In `Data.List.Fresh`: @@ -319,6 +362,12 @@ Additions to existing modules n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o ``` +* In `Data.Nat.DivMod`: + ```agda + m*n%o≡m*n%[m*o] : ∀ m n o .{{_ : NonZero o}} .{{_ : NonZero (m * o)}} → + m * (n % o) ≡ (m * n) % (m * o) + ``` + * In `Data.Nat.Logarithm` ```agda 2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n @@ -349,6 +398,7 @@ Additions to existing modules m⊔n∸[m∸n]≡n : ∀ m n → m ⊔ n ∸ (m ∸ n) ≡ n m⊔n≡m∸n+n : ∀ m n → m ⊔ n ≡ m ∸ n + n ∣m-n∣≡m⊔n∸m⊓n : ∀ m n → ∣ m - n ∣ ≡ m ⊔ n ∸ m ⊓ n + m*n≡0⇒n≡0 : ∀ m n .{{_ : NonZero m}} → m * n ≡ 0 → n ≡ 0 ``` * In `Data.Product.Properties`: @@ -385,19 +435,43 @@ Additions to existing modules * In `Data.Rational.Unnormalised.Properties`: ```agda - <ᵇ⇒< : T (p <ᵇ q) → p < q - <⇒<ᵇ : p < q → T (p <ᵇ q) - 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ℚᵘ - -q≤p≤q⇒|p|≤q : - q ≤ p → p ≤ q → ∣ p ∣ ≤ q - ⌊q⌋≤q : ⌊ q ⌋ / 1 ≤ q - q<⌊q⌋+1 : q < ⌊ q ⌋ / 1 + 1ℚᵘ - q≤⌈q⌉ : q ≤ ⌈ q ⌉ / 1 - ⌈q⌉-1