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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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)