[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]

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?