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 all 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 @@ -387,9 +387,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
12 changes: 10 additions & 2 deletions src/Data/Integer/DivMod.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<s; s<s)
import Data.Nat.Properties as ℕ using (m∸n≤m)
import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n)
import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n; n/1≡n; n%1≡0)
open import Function.Base using (_∘′_)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; cong; sym; subst)
using (_≡_; cong; sym; subst; trans)
open ≤-Reasoning

------------------------------------------------------------------------
Expand Down Expand Up @@ -129,6 +129,14 @@ 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)
... | ℕ.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)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
Expand Down
197 changes: 197 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 @@ -34,6 +34,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ℤ)
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
Expand Down Expand Up @@ -1938,6 +1939,202 @@ 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 with ∣p∣≡p∨∣p∣≡-p 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
------------------------------------------------------------------------
-- Bounds of ⌊_⌋ and ⌈_⌉

⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q
Copy link
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
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
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
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) ≡⟨ ℤ.*-identityʳ (↥ q) ⟨
(↥ 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 ⟩
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
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
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 (ℤ._+ ⌊ q ⌋ ℤ.* d) (ℤ.*-identityˡ d) ⟨
(1ℤ ℤ.* d) ℤ.+ ⌊ q ⌋ ℤ.* d
≡⟨ ℤ.*-distribʳ-+ d 1ℤ ⌊ q ⌋ ⟨
(1ℤ ℤ.+ ⌊ q ⌋) ℤ.* d
≡⟨ cong (ℤ._* d) (ℤ.+-comm 1ℤ ⌊ q ⌋) ⟩
(⌊ q ⌋ ℤ.+ 1ℤ) ℤ.* d
≡⟨ cong (λ h → (h ℤ.+ 1ℤ) ℤ.* d) (ℤ.*-identityʳ ⌊ q ⌋) ⟨
(↥ (⌊ q ⌋ / 1 + 1ℚᵘ)) ℤ.* d ∎) where open ℤ.≤-Reasoning

q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1
q≤⌈q⌉ q@record{} = begin
q ≡⟨ neg-involutive-≡ q ⟨
- (- q) ≤⟨ neg-mono-≤ (⌊q⌋≤q (- q)) ⟩
⌈ q ⌉ / 1 ∎ where open ≤-Reasoning

⌈q⌉-1<q : ∀ q → ⌈ q ⌉ / 1 - 1ℚᵘ < q
⌈q⌉-1<q q@record{} = neg-cancel-< (begin-strict
- q <⟨ q<⌊q⌋+1 (- q) ⟩
⌊ - q ⌋ / 1 + 1ℚᵘ ≡⟨ neg-involutive-≡ (⌊ - q ⌋ / 1 + 1ℚᵘ) ⟨
- (- (⌊ - q ⌋ / 1 + 1ℚᵘ)) ≡⟨ cong -_ (neg-distrib-+ (⌊ - q ⌋ / 1) 1ℚᵘ) ⟩
- (⌈ q ⌉ / 1 - 1ℚᵘ) ∎) where open ≤-Reasoning

private
-[-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<j⇒i≤pred[j] (⌈q⌉-⌊q⌋<2 q)
where
⌈q⌉-⌊q⌋<2 : ∀ q → ⌈ q ⌉ ℤ.- ⌊ q ⌋ ℤ.< (ℤ.+ 2)
⌈q⌉-⌊q⌋<2 q@record{} =
let n = ↥ q; d = ↧ q; -n = ℤ.- n
n%d = ℤ.+ (n ℤ.% d); -n%d = ℤ.+ (-n ℤ.% d)
[n/d]*d = (n ℤ./ d) ℤ.* d; [-n/d]*d = (-n ℤ./ d) ℤ.* d
in ℤ.*-cancelʳ-<-nonNeg d (begin-strict
(⌈ q ⌉ ℤ.- ⌊ q ⌋) ℤ.* d
≡⟨ ℤ.*-distribʳ-+ d ⌈ q ⌉ (ℤ.- ⌊ q ⌋) ⟩
(ℤ.- ⌊ - q ⌋) ℤ.* d ℤ.+ (ℤ.- ⌊ q ⌋) ℤ.* d
≡⟨ cong₂ (ℤ._+_) (ℤ.neg-distribˡ-* ⌊ - q ⌋ d)
(ℤ.neg-distribˡ-* ⌊ q ⌋ d) ⟨
ℤ.- [-n/d]*d ℤ.- [n/d]*d
≡⟨ ℤ.neg-distrib-+ [-n/d]*d [n/d]*d ⟨
ℤ.- ([-n/d]*d ℤ.+ [n/d]*d)
≡⟨ cong₂ (λ x y → ℤ.- (x ℤ.+ y))
(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)
≡⟨ -[-n-m]≡n+m -n%d n%d ⟩
-n%d ℤ.+ n%d
<⟨ ℤ.+-mono-< (ℤ.+<+ (ℤ.n%d<d -n d)) (ℤ.+<+ (ℤ.n%d<d n d)) ⟩
d ℤ.+ d
≡⟨ n+n≡2n d ⟩
(ℤ.+ 2) ℤ.* d ∎)
where
open ℤ.≤-Reasoning
open import Algebra.Properties.AbelianGroup ℤ.+-0-abelianGroup

⌈q⌉≤⌊q⌋+1 : ∀ q → ⌈ q ⌉ ℤ.≤ ⌊ q ⌋ ℤ.+ 1ℤ
⌈q⌉≤⌊q⌋+1 q = begin
⌈ q ⌉ ≡⟨ //-rightDividesˡ ⌊ q ⌋ ⌈ q ⌉ ⟨
(⌈ q ⌉ ℤ.- ⌊ q ⌋) ℤ.+ ⌊ q ⌋ ≤⟨ ℤ.+-monoˡ-≤ ⌊ q ⌋ (⌈q⌉-⌊q⌋≤1 q) ⟩
1ℤ ℤ.+ ⌊ q ⌋ ≡⟨ ℤ.+-comm 1ℤ ⌊ q ⌋ ⟩
floor q ℤ.+ 1ℤ ∎
where
open ℤ.≤-Reasoning
open import Algebra.Properties.AbelianGroup ℤ.+-0-abelianGroup

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

private
-1≤q-⌊q⌋ : ∀ q → - 1ℚᵘ ≤ q - ⌊ q ⌋ / 1
-1≤q-⌊q⌋ q = let ⌊q⌋ = ⌊ q ⌋ / 1 in begin
- 1ℚᵘ ≤⟨ *≤* ℤ.-≤+ ⟩
0ℚᵘ ≃⟨ +-inverseʳ ⌊q⌋ ⟨
⌊q⌋ - ⌊q⌋ ≤⟨ +-monoˡ-≤ _ (⌊q⌋≤q q) ⟩
q - ⌊q⌋ ∎ where open ≤-Reasoning

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⌋ ≃⟨ 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)

∣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⌋ ∣ ≡⟨ ∣-p∣≡∣p∣ (q + ⌊-q⌋) ⟨
∣ - (q + ⌊-q⌋) ∣ ≡⟨ cong ∣_∣ (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
- ½ ≃⟨ \\-leftDividesˡ q (- ½) ⟨
q + (- q - ½) ≡⟨ cong (q +_) (neg-distrib-+ q ½) ⟨
q - (q + ½) ≤⟨ +-monoʳ-≤ q (neg-mono-≤ (⌊q⌋≤q (q + ½))) ⟩
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ˡ _ (//-rightDividesʳ ½ q) ⟨
q + ½ - ½ - ⌊q+½⌋ <⟨ +-monoˡ-< _ (+-monoˡ-< _ (q<⌊q⌋+1 (q + ½))) ⟩
⌊q+½⌋ + 1ℚᵘ - ½ - ⌊q+½⌋ ≃⟨ +-congˡ (- ⌊q+½⌋) (+-assoc ⌊q+½⌋ 1ℚᵘ (- ½)) ⟩
⌊q+½⌋ + ½ - ⌊q+½⌋ ≃⟨ xyx⁻¹≈y ⌊q+½⌋ ½ ⟩
½ ∎
where
open ≤-Reasoning
open import Algebra.Properties.AbelianGroup +-0-abelianGroup

ceil-minus : ∀ p q → ⌈ p - q ⌉ ≡ ℤ.- ⌊ - p + q ⌋
ceil-minus p@record{} q@record{} = begin
ℤ.- ⌊ - (p - q) ⌋ ≡⟨ cong (λ h → ℤ.- ⌊ h ⌋) (neg-distrib-+ p (- q)) ⟩
ℤ.- ⌊ - p - (- q) ⌋ ≡⟨ cong (λ h → ℤ.- ⌊ - p + h ⌋) (neg-involutive-≡ q) ⟩
ℤ.- ⌊ - p + 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-minus q ½) ⟩
q - (- ⌊-q+½⌋) ≡⟨ cong (_- (- ⌊-q+½⌋)) (neg-involutive-≡ q) ⟨
- (- q) - (- ⌊-q+½⌋) ≡⟨ 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 (_- (- ⌊-q+½⌋)) (neg-involutive-≡ q) ⟩
q - (- ⌊-q+½⌋) ≡⟨ cong (λ h → q - h / 1) (ceil-minus 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+½⌋ q) (q-⌊q+½⌋≤½ q)
... | true = -q≤p≤q⇒∣p∣≤q (-½≤q-⌈q-½⌉ q) (q-⌈q-½⌉≤½ q)

⌊n/1⌋≡n : ∀ n → ⌊ n / 1 ⌋ ≡ n
⌊n/1⌋≡n n = ℤ.n/1≡n n

⌈n/1⌉≡n : ∀ n → ⌈ n / 1 ⌉ ≡ n
⌈n/1⌉≡n n = trans (cong ℤ.-_ (⌊n/1⌋≡n (ℤ.- n))) (ℤ.neg-involutive n)

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