-- Division with remainder for natural numbers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Nat.Division
import Mod
import Order

theorem mod.division (d n : Nat)
  requires nonzero : d ≠ 0
  shows (∃ q, Nat(q) ∧ n = d * q + n % d) ∧ n % d < d
proof
  induction n
  | zero =>
    have remainder := mod.zero_left at d with *
    rw remainder
    constructor
    . witness 0
      ring
    . have positive := Less.add_positive at 0, d with *
      simpa [add] using positive
  | succ(k) using ih =>
    rcases ih with ⟨division, bound⟩
    obtain ⟨q, qNat, equation⟩ := division
    have split : succ(k % d) = d ∨ succ(k % d) ≠ d
    . tauto
    cases split with wraps | advances
    . have condition := equalNat.true_iff.backward at succ(k % d), d with *
      have remainder : succ(k) % d = 0
      . simp [mod, nextRemainder, equalNat.reflexive, condition, chooseNat]
      rw remainder
      have increment := add.succ_right at k % d, d * q with *
      rw ← equation at increment
      symm at increment
      constructor
      . witness succ(q)
        rw remainder
        rw wraps at increment
        have product : d * succ(q) + 0 = d * q + d
        . ring
        rwa product
      . have positive := Less.add_positive at 0, d with *
        simpa [add] using positive
    . have condition := equalNat.false_iff.backward at succ(k % d), d with *
      have remainder : succ(k) % d = succ(k % d)
      . simp [mod, nextRemainder, equalNat.reflexive, condition, chooseNat]
      rw remainder
      have increment := add.succ_right at k % d, d * q with *
      rw ← equation at increment
      symm at increment
      constructor
      . witness q
        rw remainder
        exact increment
        have comparison := Less.trichotomy at succ(k % d), d with *
        rcases comparison with less | equal | greater
        . exact less
        . exfalso
          exact advances with equal
        . arith

theorem mod.less (n d : Nat)
  requires nonzero : d ≠ 0
  shows n % d < d
proof
  have division := mod.division at d, n with *
  tauto

theorem mod.equation (n d : Nat)
  requires nonzero : d ≠ 0
  shows ∃ q, Nat(q) ∧ n = d * q + n % d
proof
  have division := mod.division at d, n with *
  tauto

-- Count exactly the same wraps as mod. Division by zero returns zero.
def quotientNat (n d : Nat) → Nat
  | zero, d => zero
  | succ(n), d => chooseNat(equalNat(succ(n % d), d), succ(quotientNat(n, d)), quotientNat(n, d))

theorem quotientNat.natural (d n : Nat)
  shows Nat(quotientNat(n, d))
proof
  induction n
  | zero =>
    simp [quotientNat]
    typecheck
  | succ(k) using ih =>
    have boolean := equalNat.boolean at succ(k % d), d with *
    have natural := chooseNat.natural at equalNat(succ(k % d), d), succ(quotientNat(k, d)), quotientNat(k, d) with *
    simpa [quotientNat] using natural

theorem quotientNat.equation (d n : Nat)
  shows n = d * quotientNat(n, d) + n % d
proof
  induction n
  | zero => simp [quotientNat, mod, mul.right_zero, add]
  | succ(k) using ih =>
    have split : succ(k % d) = d ∨ succ(k % d) ≠ d
    . tauto
    cases split with wraps | advances
    . have condition := equalNat.true_iff.backward at succ(k % d), d with *
      have remainder : succ(k) % d = 0
      . simp [mod, nextRemainder, condition, equalNat.reflexive, chooseNat]
      have quotient : quotientNat(succ(k), d) = succ(quotientNat(k, d))
      . simp [quotientNat, condition, equalNat.reflexive, chooseNat]
      have increment := add.succ_right at k % d, d * quotientNat(k, d) with *
      rw ← ih at increment
      symm at increment
      rw [quotient, remainder]
      rw wraps at increment
      have product : d * succ(quotientNat(k, d)) + 0 = d * quotientNat(k, d) + d
      . ring
      rwa product
    . have condition := equalNat.false_iff.backward at succ(k % d), d with *
      have remainder : succ(k) % d = succ(k % d)
      . simp [mod, nextRemainder, condition, equalNat.reflexive, chooseNat]
      have quotient : quotientNat(succ(k), d) = quotientNat(k, d)
      . simp [quotientNat, condition, equalNat.reflexive, chooseNat]
      have increment := add.succ_right at k % d, d * quotientNat(k, d) with *
      rw ← ih at increment
      symm at increment
      rw quotient
      rwa remainder

theorem quotientNat.zero_right (n : Nat)
  shows quotientNat(n, 0) = 0
proof
  induction n
  | zero => simp [quotientNat]
  | succ(k) using ih =>
    have nonzero : succ(k % 0) ≠ 0
    . intro equal
      have distinct := Naturals.disjoint.zero.succ at k % 0
      symm at equal
      exact distinct with equal
    have condition := equalNat.false_iff.backward at succ(k % 0), 0 with *
    simp [quotientNat, condition, equalNat.reflexive, chooseNat]

theorem quotientNat.division (n d : Nat)
  requires nonzero : d ≠ 0
  shows Nat(quotientNat(n, d)) ∧ n = d * quotientNat(n, d) + n % d ∧ n % d < d
proof
  simp [quotientNat.natural, quotientNat.equation, mod.less]

-- Dividing a bound through by a positive coefficient: these two tightenings
-- keep linear arithmetic over the naturals exact when every coefficient of
-- an atom shares a factor. The coefficient is written succ(k) so that it is
-- visibly nonzero.
theorem LessEqual.quotient_floor (a b k d : Nat)
  requires bound : succ(k) * a ≤ succ(k) * b + d
  shows a ≤ b + quotientNat(d, succ(k))
proof
  have nonzero : succ(k) ≠ 0
    intro zero
    have disjoint := Naturals.disjoint.zero.succ at k
    apply disjoint
    symm at zero
    exact zero
  obtain ⟨qNat, equation, remainder⟩ := quotientNat.division at d, succ(k) with nonzero
  by_contra refuted
  have strict := Less.of_not_LessEqual with refuted
  have scaled := LessEqual.mul_left at succ(b + quotientNat(d, succ(k))), a, succ(k) with strict
  have expand : succ(k) * succ(b + quotientNat(d, succ(k))) = succ(k) * b + succ(k) * quotientNat(d, succ(k)) + succ(k)
    ring
  rw expand at scaled
  rw equation at bound
  have cycle : succ(k) * a < succ(k) * a by arith
  exact Less.irreflexive with *, cycle

theorem LessEqual.quotient_ceiling (a b k e : Nat)
  requires bound : succ(k) * a + (e + 1) ≤ succ(k) * b
  shows a + (quotientNat(e, succ(k)) + 1) ≤ b
proof
  have nonzero : succ(k) ≠ 0
    intro zero
    have disjoint := Naturals.disjoint.zero.succ at k
    apply disjoint
    symm at zero
    exact zero
  obtain ⟨qNat, equation, remainder⟩ := quotientNat.division at e, succ(k) with nonzero
  by_contra refuted
  have strict := Less.of_not_LessEqual with refuted
  have scaled := LessEqual.mul_left at succ(b), a + (quotientNat(e, succ(k)) + 1), succ(k) with strict
  have left : succ(k) * succ(b) = succ(k) * b + succ(k) by ring
  have right : succ(k) * (a + (quotientNat(e, succ(k)) + 1)) = succ(k) * a + succ(k) * quotientNat(e, succ(k)) + succ(k)
    ring
  rw [left, right] at scaled
  rw equation at bound
  have cycle : succ(k) * b < succ(k) * b by arith
  exact Less.irreflexive with *, cycle