[Add] Division properties for Nat, Integer, and Rational

[aortega0703]

Hi, I saw there weren't many properties for division outside of Naturals so I went ahead and proved some for (Unnormalised) Rationals and Integers (and Naturals too):

Data.Rational.Unnormalised:

• /-distribʳ-+: fractions with sums on the numerator can be "split" into sums of fractions
• n/d≡[n/1]*[1/d]: this was more of a convenience to prove /-distribʳ-+ but I thought it could be useful enough to add it separately (maybe not?).
• /-monoˡ-<, /-monoʳ-<-pos, /-monoʳ-<-neg, /-monoˡ-≤, /-monoʳ-≤-nonNeg, and /-monoʳ-≤-nonPos: In Rational denominators are ℕs, so there isn't a sign hell as with Integer.

Data.Integer.DivMod:

• n<0⇒n/ℕd<0: there was already 0≤n⇒0≤n/ℕd so I added "the other case".
• 0/d≡0 and n/1≡n (also for /ℕ).
• n/ℕd≡0⇒∣n∣<d and n/d≡0⇒∣n∣<∣d∣: the integer version of m/n≡0⇒m<n.
• 0≤n<d⇒n/d≡0 (also /ℕ): the "converse" (not really), an int version of m<n⇒m/n≡0.
• /ℕ-monoˡ-≤ (and helpers), /ℕ-monoʳ-≤-nonNeg and /ℕ-monoʳ-≤-nonPos.
• /-monoˡ-≤-pos and /-monoˡ-≤-neg: I put a reduntant NonZero to make _/_ happy where only Positive/Negative should really suffice. I admit I tried deriving the NonZero but I don't know how to do it without making the type too verbose/ugly.
• /-monoʳ-≤-nonNeg-eq-signs and /-monoʳ-≤-nonPos-eq-signs: The proofs for these are basically the same, extremely so (just swapping the denominators names), but I can't figure a way to prove one with the other. (- n) / d and - (n / d) are not always equal so I can't just convert the numerator from nonPos to nonNeg, but maybe there's another way?
• /-monoʳ-≤-nonNeg-op-signs and /-monoʳ-≤-nonPos-op-signs: I also noticed how /-monoʳ-≤-nonNeg-eq-signs and /-monoʳ-≤-nonPos-op-signs have basically the same type (their counterparts too) but I don't know If it's better to keep them separate or combine them and ask for something like sign (n * d₁ * d₂) ≡ Sign.+ in the type.

Data.Nat.DivMod:

• sn%d≡0⇒sn/d≡s[n/d] and sn%d>0⇒sn/d≡n/d: These really really (really) helped to reason about Integer division. Also, they are nice in that they describe whether the quotient increases with the dividend or it stays the same.
• %-pred-≡suc: This is "the other case" of %-pred-≡0, it says that the remainder increases on par with the dividend (exept for the jump at remainder 0). I don't like the name on this one but I retained the name style of %-pred-≡0.

I have yet to translate the Unnormalised proofs to normalised Rationals and I'm not sure about the whole deal with the signs on the types for /-mono on Integers so it's a draft for now.

[JacquesCarette]

Nice. Some of the proofs seem to go rather "low level" though.

[JacquesCarette]

This small bit of reasoning feels like a lemma that should be pulled out.

[aortega0703]

I actually had a question about this bit. The definition for /ℕ has

(-[1+ n ] /ℕ d) with ℕ.suc n ℕ.% d
... | ℕ.zero  = - (+ (ℕ.suc n ℕ./ d))
... | ℕ.suc r = -[1+ (ℕ.suc n ℕ./ d) ]

That bit of reasoning (that I used a lot) transforms that - (+ (ℕ.suc n ℕ./ d)) into -[1+ n ℕ./ d ] which I found easier to work with (so that agda doesn't entertain the possibility of it being + 0). I tried pulled it out as its own thing

sn%d≡0⇒-[1+n]/d≡-[1+[n/d]] : ∀ n d .{{_ : ℕ.NonZero d}} →
                            ℕ.suc n ℕ.% d ≡ 0 → -[1+ n ] /ℕ d ≡ -[1+ n ℕ./ d ]
sn%d≡0⇒-[1+n]/d≡-[1+[n/d]] n d _ with ℕ.zero ← ℕ.suc n ℕ.% d in sn%d≡0 =
  cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d sn%d≡0)

but when I try to use it after a with abstraction, say

n<0⇒n/ℕd<0 : ∀ n d .{{_ : ℕ.NonZero d}} → n < 0ℤ → (n /ℕ d) < 0ℤ
n<0⇒n/ℕd<0 -[1+ n ] d -<+
  with ℕ.suc n ℕ.% d in sn%d
... | ℕ.zero  = begin-strict
  {! -[1+ n ] /ℕ d !} ≡⟨ {!!} ⟩ {!!}
... | ℕ.suc _ = -<+

Agda seems to "forget" that the starting term should be equal to -[1+ n ] /ℕ d (I get [UnequalTerms] (-[1+ n ] /ℕ d | ℕ.suc n ℕ.% d) != - (+ (ℕ.suc n ℕ./ d))) so I can't apply my lemma. Is there a way to get around this I'm not aware of, or how should I go about extracting this lemma?

[JacquesCarette]

I think you're running into the fragility of with here. Personally, the first thing I would do is to create a /ℕ-helper function that does the current with "by hand". And export it, so lemmas about it can be proved.

Then you'll find that downstream uses of with in proofs won't forget quite as much.

[JacquesCarette]

Shouldn't there be a proof that does not need to split on n? The assumptions imply that n is 0, and since d is NonZero, the conclusion ought to follow from properties of abs.

[aortega0703]

But n is not necessarily 0 here (e.g. + 1 / -[1+ 1 ] ≡ + 0). That said, integer division evaluates to 0 whenever 0 ≤ n < d (negative numerator never divides to 0) so maybe I should split this into two proofs for n / d ≡ 0ℤ → n ℕ.< ∣ d ∣ and n / d ≡ 0ℤ → NonNegative n?

[JacquesCarette]

My mistake, I mis-interpreted / here. Your comment, on the other hand, is a good idea.