Skip to content

[Add] Properties of rounding in Rational #2953

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
aortega0703 wants to merge 20 commits into
base: master
Choose a base branch
from
Draft

[Add] Properties of rounding in Rational #2953

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
6fe6a4a
floor upper bound, ceil lower bound
aortega0703 Feb 19, 2026
c900d0b
Add bounds for floor and ceil
aortega0703 Feb 21, 2026
9c6018a
add introduction of absolute value via inequalities
aortega0703 Feb 24, 2026
1a25ede
Add rounding error for floor, ceil, and round
aortega0703 Feb 25, 2026
90d1ab8
Merge branch 'master' into rounding-properties
aortega0703 Feb 25, 2026
b164b41
Apply suggestions from code review
aortega0703 Feb 25, 2026
585f6f7
Remove unnecessary lambda notation
aortega0703 Feb 25, 2026
3a2ee47
Switch syntax of sym on equalities
aortega0703 Feb 26, 2026
9d2818c
Apply suggestions from code review
aortega0703 Feb 26, 2026
8476db7
Simplify proofs using group properties
aortega0703 Feb 27, 2026
baf6c2c
change use of subst in favour of equational reasoning
aortega0703 Feb 27, 2026
64b0b08
remove subst and rewrite from proof
aortega0703 Feb 28, 2026
5fa0001
prove ceil <= floor + 1
aortega0703 Feb 28, 2026
2b072f9
Replace lambda notation and sym use
aortega0703 Feb 28, 2026
dc9708f
clean ceil <= floor + 1 proof
aortega0703 Mar 2, 2026
60cae8c
floor and ceil of integers
aortega0703 Mar 2, 2026
c62939a
Merge branch 'master' of github.com:agda/agda-stdlib into rounding-pr…
aortega0703 Mar 2, 2026
c78eaba
Merge branch 'master' of github.com:agda/agda-stdlib into rounding-pr…
aortega0703 Mar 12, 2026
bfacc6e
Remove unnecessary lemma
aortega0703 Mar 18, 2026
50a0707
Merge branch 'master' of github.com:agda/agda-stdlib into rounding-pr…
aortega0703 Mar 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 11 additions & 3 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -347,9 +347,17 @@ Additions to existing modules
```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ℚᵘ
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<q : ⌈ q ⌉ / 1 - 1ℚᵘ < q
∣q-⌊q⌋∣≤1 : ∣ q - ⌊ q ⌋ / 1 ∣ ≤ 1ℚᵘ
∣q-⌈q⌉∣≤1 : ∣ q - ⌈ q ⌉ / 1 ∣ ≤ 1ℚᵘ
∣q-round[q]∣≤½ : ∣ q - (round q) / 1 ∣ ≤ ½
```

* In `Data.Rational.Unnormalised.Show`:
Expand Down
125 changes: 125 additions & 0 deletions src/Data/Rational/Unnormalised/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 as ℤ using ()
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver)
import Data.Integer.Properties as ℤ
open import Data.Rational.Unnormalised.Base
Expand Down Expand Up @@ -1933,6 +1934,130 @@ 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
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
-q≤p≤q⇒∣p∣≤q p q -q≤p p≤q =
Copy link
Copy Markdown
Collaborator

@JacquesCarette JacquesCarette Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm pretty sure this proof would be much nicer if it used with on ∣p∣≡p∨∣p∣≡-p p followed by pattern-matching all the way down to refl, which would remove the need for subst.

Alternatively, create two lemmas, one for each of the cases, and then use them here.

Perhaps even simpler would be to case on whether p is non-negative or not?

Copy link
Copy Markdown
Contributor Author

@aortega0703 aortega0703 Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried following the first approach:

-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₁ x = {!!}
... | inj₂ y = {!!}

but when I try splitting either x or y to pattern-match against refl I'm hit with

I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  ∣ p₁ ∣ ≟ p₁

so I don't know how to proceed there. In the meantime I changed my proof to

-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)

which is a bit nicer? On the third approach, I tried with on p <ᵇ 0ℚ (which I think is what you meant?) to work on the true/false arms but I can't figure how to tell Agda to reduce the ∣ p ∣ in the goal to either - p or p in each case. I'm still finding my way around Agda and the standard lib so thanks for the patience and comments!

[ (λ ∣p∣≡p → subst (λ h → h ≤ q) (sym ∣p∣≡p) p≤q)
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
, (λ ∣p∣≡-p → subst (λ h → h ≤ q) (sym ∣p∣≡-p)
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
(subst (λ h → _ ≤ h) (neg-involutive-≡ q) (neg-mono-≤ -q≤p))) ]′
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
(∣p∣≡p∨∣p∣≡-p p)

------------------------------------------------------------------------
-- Properties of Rounding functions
------------------------------------------------------------------------
-- Bounds of ⌊_⌋ and ⌈_⌉

⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q
Copy link
Copy Markdown
Collaborator

@JacquesCarette JacquesCarette Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That floor changes type and so we have to change back to do ≤ makes sense. But this / 1 idiom seems too low-level. Do we not have some nicer way of saying this?

Copy link
Copy Markdown
Contributor Author

@aortega0703 aortega0703 Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a 1/_ for reciprocals but I don't see anything like a _/1 to simply "cast" the type. I saw that fracPart used / 1 and ran with it as the nicer constructor compared to mkℚᵘ.

Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 27, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I'd be happy with introducing an explicit coercion from ℤ to ℚᵘ as mkℚᵘ_ 0... choosing a good name for such a thing being the hard part! Possible solution:

ℤtoℚᵘ : ℤ → ℚᵘ
ℤtoℚᵘ i = mkℚᵘ i 0

syntax ℤtoℚᵘ i = [ i ]ℤ

There's a separate question as to whether new syntax declarations is a good idea at all, and/or whether, as in this case, because the associated function is in fact a pattern (specialising mkℚᵘ), whether it itself should be introduced as

pattern ℤtoℚᵘ i = mkℚᵘ i 0

syntax ℤtoℚᵘ i = [ i ]ℤ

... but it's not clear whether we could ever use this in a pattern match!?

Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Mar 2, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alternatively, we can use my favourite identifier $$\iota$$ for an inclusion/monomorphism, and write:

ι : ℤ → ℚᵘ -- ℤ⇒ℚᵘ
ι i = mkℚᵘ i 0

ιℕ : ℕ → ℚᵘ -- ℕ⇒ℚᵘ
ιℕ n = ι (+ n)

⌊q⌋≤q q@record{} = *≤* (begin
⌊ q ⌋ ℤ.* (↧ q) ≤⟨ ℤ.[n/d]*d≤n (↥ q) (↧ q) ⟩
(↥ q) ≡⟨ sym (ℤ.*-identityʳ (↥ q)) ⟩
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
(↥ q) ℤ.* (↧ (⌊ q ⌋ / 1)) ∎) where open ℤ.≤-Reasoning

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 ⟩
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
n ≡⟨ ℤ.a≡a%n+[a/n]*n n d ⟩
ℤ.+ (n ℤ.% d) ℤ.+ ⌊ q ⌋ ℤ.* d
<⟨ ℤ.+-monoˡ-< (⌊ q ⌋ ℤ.* d) (ℤ.+<+ (ℤ.n%d<d n d)) ⟩
d ℤ.+ ⌊ q ⌋ ℤ.* d
Copy link
Copy Markdown
Collaborator

@JacquesCarette JacquesCarette Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

feels like the steps from here to the end should be pulled out as a lemma.

Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna Feb 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See my comments above: this is really the proof that floor and ceil are tight bounds, and is properly a lemma about integers?

≡⟨ cong (λ h → h ℤ.+ ⌊ q ⌋ ℤ.* d) (sym (ℤ.*-identityˡ d)) ⟩
(1ℤ ℤ.* d) ℤ.+ ⌊ q ⌋ ℤ.* d
≡⟨ sym (ℤ.*-distribʳ-+ d 1ℤ (n ℤ./ d)) ⟩
(1ℤ ℤ.+ ⌊ q ⌋) ℤ.* d
≡⟨ cong (λ h → h ℤ.* d) (ℤ.+-comm 1ℤ ⌊ q ⌋) ⟩
(⌊ q ⌋ ℤ.+ 1ℤ) ℤ.* d
≡⟨ cong (λ h → (h ℤ.+ 1ℤ) ℤ.* d) (sym (ℤ.*-identityʳ ⌊ q ⌋)) ⟩
(↥ (⌊ q ⌋ / 1 + 1ℚᵘ)) ℤ.* d ∎) where open ℤ.≤-Reasoning

q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1
q≤⌈q⌉ q@record{} = subst
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
(λ h → h ≤ - (⌊ - q ⌋ / 1))
(neg-involutive-≡ q)
(neg-mono-≤ (⌊q⌋≤q (- q)))

⌈q⌉-1<q : ∀ q → ⌈ q ⌉ / 1 - 1ℚᵘ < q
⌈q⌉-1<q q@record{} = subst₂ _<_
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
(neg-distrib-+ (⌊ - q ⌋ / 1) 1ℚᵘ)
(neg-involutive-≡ q)
(neg-mono-< (q<⌊q⌋+1 (- q)))

------------------------------------------------------------------------
-- Approximation errors of ⌊_⌋ ⌈_⌉ and round(_)

∣q-⌊q⌋∣≤1 : ∀ q → ∣ q - ⌊ q ⌋ / 1 ∣ ≤ 1ℚᵘ
∣q-⌊q⌋∣≤1 q = let ⌊q⌋ = ⌊ q ⌋ / 1 in -q≤p≤q⇒∣p∣≤q (q - ⌊ q ⌋ / 1) 1ℚᵘ
(begin
Comment thread
aortega0703 marked this conversation as resolved.
Outdated
- 1ℚᵘ ≤⟨ *≤* ℤ.-≤+ ⟩
0ℚᵘ ≃⟨ ≃-sym (+-inverseʳ ⌊q⌋) ⟩
⌊q⌋ - ⌊q⌋ ≤⟨ +-monoˡ-≤ _ (⌊q⌋≤q q) ⟩
q - ⌊q⌋ ∎)
(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⌉∣≤1 : ∀ q → ∣ q - ⌈ q ⌉ / 1 ∣ ≤ 1ℚᵘ
∣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⌋) ∣ ≡⟨ cong (λ h → ∣ h ∣) (neg-distrib-+ q ⌊-q⌋) ⟩
∣ - q - ⌊-q⌋ ∣ ≤⟨ ∣q-⌊q⌋∣≤1 (- q) ⟩
1ℚᵘ ∎ where open ≤-Reasoning

private
-½≤q-⌊q+½⌋ : ∀ q → - ½ ≤ q - ⌊ q + ½ ⌋ / 1
-½≤q-⌊q+½⌋ q = begin
- ½ ≃⟨ ≃-sym (+-identityˡ _) ⟩
0ℚᵘ - ½ ≃⟨ +-congˡ (- ½) (≃-sym (+-inverseʳ q)) ⟩
q - q - ½ ≃⟨ +-assoc q _ _ ⟩
q + (- q - ½) ≡⟨ cong (λ h → q + h) (sym (neg-distrib-+ q ½)) ⟩
q - (q + ½) ≤⟨ +-monoʳ-≤ q (neg-mono-≤ (⌊q⌋≤q (q + ½))) ⟩
q - ⌊ q + ½ ⌋ / 1 ∎ where open ≤-Reasoning

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+½⌋ + 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

ceil-to-floor : ∀ q → ⌈ q - ½ ⌉ ≡ ℤ.- ⌊ - q + ½ ⌋
ceil-to-floor q@record{} = begin
ℤ.- ⌊ - (q - ½) ⌋ ≡⟨ cong (λ h → ℤ.- ⌊ h ⌋) (neg-distrib-+ q (- ½)) ⟩
ℤ.- ⌊ - q - (- ½) ⌋ ≡⟨ cong (λ h → ℤ.- ⌊ - q + h ⌋) (neg-involutive-≡ ½) ⟩
ℤ.- ⌊ - q + ½ ⌋ ∎ where open ≡-Reasoning

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+½⌋) ≡⟨ sym (neg-distrib-+ (- q) _) ⟩
- (- q - ⌊-q+½⌋) ≤⟨ neg-mono-≤ (-½≤q-⌊q+½⌋ (- q)) ⟩
- (- ½) ≡⟨ neg-involutive-≡ ½ ⟩
½ ∎ where open ≤-Reasoning

-½≤q-⌈q-½⌉ : ∀ q → - ½ ≤ q - ⌈ q - ½ ⌉ / 1
-½≤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 (λ h → q - h / 1) (sym (ceil-to-floor q)) ⟩
q - ⌈ q - ½ ⌉ / 1 ∎ where open ≤-Reasoning

∣q-round[q]∣≤½ : ∀ q → ∣ q - (round q) / 1 ∣ ≤ ½
∣q-round[q]∣≤½ q with q ≤ᵇ 0ℚᵘ
... | false = -q≤p≤q⇒∣p∣≤q (q - ⌊ q + ½ ⌋ / 1) ½ (-½≤q-⌊q+½⌋ q) (q-⌊q+½⌋≤½ q)
... | true = -q≤p≤q⇒∣p∣≤q (q - ⌈ q - ½ ⌉ / 1) ½ (-½≤q-⌈q-½⌉ q) (q-⌈q-½⌉≤½ q)

------------------------------------------------------------------------
-- DEPRECATED NAMES
Expand Down