[Add] Properties of rounding in Rational

[aortega0703]

Hi, I added some properties of the rounding functions for Rational.Unnormalised. Namely, bounds for floor and ceil:

• $\lfloor q \rfloor \leq q < \lfloor q \rfloor + 1$
• $\lceil q \rceil - 1 < q \leq \lceil q \rceil$

And approximation errors (absolute difference) for floor, ceil, and round:

• $|q - \lfloor q \rfloor| \leq 1$
• $|q - \lceil q \rceil| \leq 1$
• $|q - \mathrm{round}(q)| \leq \frac{1}{2}$

I also added a property of ∣_∣ to help me prove the errors:

• $- q \leq p \leq q \implies | p | \leq q$

I still haven't translated these proofs to normalised Rationals, and the proof for ∣q-round[q]∣≤½ is quite long, so any advice is welcome.

[jamesmckinna]

As to 'advice', it might be worth mentioning #1434 ...

... and speculating whether it is more 'efficient' to prove instead: (these may be false, or else insufficiently sharp; I haven't checked ;-)) as somehow 'what we want from the specification of floor and ceiling'

• ⌊ q ⌋ ≤ q ≤ ⌈ q ⌉ (floor and ceil really are lower- and upper- bounds)
• ⌈ q ⌉ < ⌊ q ⌋ + 1 (and they're not too far apart) UPDATED: using ℤ.n<s[n/ℕd]*d from Data.Integer.DivMod.

from which some of your properties would follow...but I confess its a while since I could remember any approximation theory ;-) so maybe take these with a pinch of salt. Not sure how to deal with the bounds on rounding, either ;-)

[JacquesCarette]

Review pass 1. There will likely be a pass 2.

[JacquesCarette]

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?

[aortega0703]

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!

[JacquesCarette]

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?

[aortega0703]

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ℚᵘ.

[jamesmckinna]

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!?

[jamesmckinna]

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

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

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

[JacquesCarette]

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

[jamesmckinna]

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

[aortega0703]

@jamesmckinna Sorry for not replying to your first comment earlier, proving ⌈ q ⌉ ≤ ⌊ q ⌋ + 1 was harder than I thought haha. The idea for my original bounds was

• ⌊ q ⌋ ≤ q < ⌊ q ⌋ + 1 (floor is a lower bound and is close to q)
• ⌈ q ⌉ - 1 < q ≤ ⌈ q ⌉ (ceil is an upper bound and is close to q)

⌈ q ⌉ ≤ ⌊ q ⌋ + 1 is very nice (and true!) as it means they are also close to each other, and it's a tighter bound that does imply my original ⌈ q ⌉ - 1 < q and q < ⌊ q ⌋ + 1 that I use later on ∣q-round[q]∣≤½. I typed it as ℤ.≤ as I think it does make more sense not coercing them to ℚᵘ here

⌈q⌉≤⌊q⌋+1 : ∀ q →  ⌈ q ⌉ ℤ.≤ ⌊ q ⌋ ℤ.+ 1ℤ

but when I tried actually proving the implications I hit

q≤⌊q⌋+1  : ∀ q → q ≤ ⌊ q ⌋ / 1 + 1ℚᵘ
q≤⌊q⌋+1 q = begin
  q ≤⟨ q≤⌈q⌉ q ⟩
  ⌈ q ⌉ / 1 ≤⟨ {!!} ⟩ {!!} -- ≤ (⌊ q ⌋ + 1) / 1
  where open ≤-Reasoning

and I don't think there's anything like n₁ < n₂ → n₁ / d < n₂ / d for me to use there, or even (n₁ + n₂) / d ≃ n₁ / d + n₂ / d to use afer that. Should I add those and proceed to prove ⌈ q ⌉ - 1 < q and q < ⌊ q ⌋ + 1 using ⌈ q ⌉ ≤ ⌊ q ⌋ + 1, or leave them as independent?

[jamesmckinna]

Thanks @aortega0703 for querying my original half-baked thoughts.

I wrote something manifestly incorrect in the night when only half-awake (and when I should have been asleep ;-)), and my version of the story seems a bit less clear than yours. Once I've worked out the details, I'll try and repost.

But there is something about all these functions being piecewise-linear, indeed piecewise constant, with discontinuities at the ℤ points on ℚᵘ which suggest to me a different angle of attack: namely to split not on +/-, but on integer/non-integer, and analyse the various functions accordingly.

But that analysis, and the fiddliness involved in constructing the corresponding view machinery to instrument that case analysis, seems ... differently complicated to your approach.

[aortega0703]

I tried cleaning my proof a bit, mostly by adding some integer lemmas (me shufling things around). Although, after thinking about it some more and fiddling with some proofs I no longer think ⌈ q ⌉ - 1 < q and q < ⌊ q ⌋ + 1 should be proven via ⌈ q ⌉ ≤ ⌊ q ⌋ + 1. Doing q ≤ ⌈ q ⌉ ≤ ⌊ q ⌋ + 1 means we no longer get the strict inequality q < ⌊ q ⌋ + 1 but the weaker version q ≤ ⌊ q ⌋ + 1 (similarly with ⌈ q ⌉ - 1 ≤ q).
That said, it's interesting as the distance between floor and ceil, and ⌈ q ⌉ = ⌊ q ⌋ + 1 for everything but the integers!
Thinking about the piece-constant behaviour you mentioned I just added ⌈ q ⌉ = ⌊ q ⌋ = q for q integer (actually as n / 1 hehe), but I think after lifting some properties from Data.Nat.DivMod to Data.Integer.DivMod I could do something more general with (↥ q) % (↧ q). Maybe say that ⌊ n / 1 + q ⌋ = n for 0 ≤ q < 1?

[jamesmckinna]

Thanks @aortega0703 . Indeed, where I had got to was:

• for q = [ i ]ℤ, we have ⌊ q ⌋ ≡ i ≡ ⌈ q ⌉ (and hence surely ⌈ q ⌉ < ⌊ q ⌋ + 1 and [ ⌊ q ⌋ ]ℤ ≤ q ≤ [ ⌈ q ⌉ ]ℤ)
• otherwise (and the case analysis is Decidable! because divisibility on integers is...), we have [ ⌊ q ⌋ ]ℤ < q < [ ⌈ q ⌉ ]ℤ ≡ [ ⌊ q ⌋ ]ℤ + 1

Is everything else provable from this case analysis?

[aortega0703]

@jamesmckinna The non-integer case is not clear to me. I think an outline for floor would be
n = [n/d]*d + n%d by a≡a%n+[a/n]*n
q = n / d = ([n/d]*d + n%d) / d
= ([n/d]*d / d) + (n%d / d) with /-distrib-+ (need to prove)
= [n/d] + (n%d / d) by *-cancelʳ-/
= ⌊ q ⌋ + (n%d / d)
Which until here I think it can be it's own result. Then n % d = 0 implies q = ⌊ q ⌋, otherwise 0 < (n%d / d) < 1 and ⌊ q ⌋ < q < ⌊ q ⌋ + 1.

Ceil is defined as - ⌊ - q ⌋ so in the end
q = - [-n/d] - (-n%d / d)
= ⌈ q ⌉ - (-n%d / d)
If n % d = 0 (which need to prove, implies -n % d = 0) then q = ⌈ q ⌉, otherwise 0 < (-n%d / d) < 1 and ⌈ q ⌉ - 1 < q < ⌈ q ⌉.

But I don't know how to get ⌈ q ⌉ = ⌊ q ⌋ + 1 from that (maybe equating both and proving n%d + -n%d = d (or 0)?). I feel like maybe I'm complicating things more than necessary? what do you think?

[jamesmckinna]

Well it's entirely possible that I'm complicating things more than necessary!