-- Computable remainder arithmetic on 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.Mod
import Core.Data
import Core
import Foundation

-- Boolean equality is computational evidence; propositional equality remains
-- the kernel relation used by proofs.
def isZero (n : Nat) → Bool
  | zero => Bool.true
  | succ(n) => Bool.false

def equalNat (m n : Nat) → Bool
  | zero, n => isZero(n)
  | succ(m), n => BoolOps.and(BoolOps.not(isZero(n)), equalNat(m, predecessor(n)))

def chooseNat (condition : Bool, yes no : Nat) → Nat
  | Bool.false, yes, no => no
  | Bool.true, yes, no => yes

-- Advance a remainder, wrapping to zero exactly at the divisor.  With divisor
-- zero it never wraps, giving the conventional total equation n % 0 = n.
def nextRemainder (d r : Nat) : Nat :=
  chooseNat(equalNat(succ(r), d), 0, succ(r))

def mod (n d : Nat) → Nat
  | zero, d => zero
  | succ(n), d => nextRemainder(d, mod(n, d))

notation infixl 70 "%" => mod

theorem equalNat.reflexive (n : Nat)
  shows equalNat(n, n) = Bool.true
proof
  induction n
  | zero => settle with equalNat, isZero
  | succ(k) using ih =>
    simp [equalNat, isZero, predecessor, BoolOps.not, BoolOps.and, ih]

theorem equalNat.true_iff (a b : Nat)
  shows equalNat(a, b) = Bool.true ↔ a = b
proof
  induction a generalizing b
  | zero =>
    intros b naturalB
    have shape := natural.zero_or_successor with naturalB
    cases shape with equal | successor
    . rw equal
      simp [equalNat, isZero]
    . rcases successor with ⟨k, naturalK, bShape⟩
      rw bShape
      have distinct := Naturals.disjoint.zero.succ at k
      have computed : equalNat(0, succ(k)) = Bool.false by simp [equalNat, isZero]
      rw computed
      have boolDistinct := Bool.inductive.disjoint.false.true
      tauto
  | succ(k) using ih =>
    intros b naturalB
    have shape := natural.zero_or_successor with naturalB
    cases shape with equal | successor
    . rw equal
      have distinct : succ(k) ≠ 0
        intro h
        have zeroNot := Naturals.disjoint.zero.succ at k
        apply zeroNot
        rw h
        rfl
      have computed : equalNat(succ(k), 0) = Bool.false
        settle with equalNat, isZero, predecessor, BoolOps.not, BoolOps.and
      rw computed
      have boolDistinct := Bool.inductive.disjoint.false.true
      tauto
    . rcases successor with ⟨j, naturalJ, bShape⟩
      rw bShape
      have inner := ih with j, naturalJ
      have reduced : equalNat(succ(k), succ(j)) = equalNat(k, j)
        settle with equalNat, isZero, predecessor, BoolOps.not, BoolOps.and
      rw reduced
      constructor
      . intro same
        have kj := inner.forward with same
        rw kj
        rfl
      . intro same
        have kj := Naturals.injective.succ with same
        exact inner.backward with kj

theorem boolean.cases (b : Bool)
  shows b = Bool.false ∨ b = Bool.true
proof
  induction b
  | Bool.false =>
    left
    rfl
  | Bool.true =>
    right
    rfl

theorem equalNat.boolean (a b : Nat)
  shows Bool(equalNat(a, b))
proof
  induction a generalizing b
  | zero =>
    intros b bNat
    have shape := natural.zero_or_successor with bNat
    cases shape with zero | successor
    . rw zero
      have computed : equalNat(0, 0) = Bool.true by simp [equalNat, isZero]
      rw computed
      exact Bool.inductive.constructor.true
    . rcases successor with ⟨k, hk, equal⟩
      rw equal
      have computed : equalNat(0, succ(k)) = Bool.false by simp [equalNat, isZero]
      rw computed
      exact Bool.inductive.constructor.false
  | succ(k) using ih =>
    intros b bNat
    have shape := natural.zero_or_successor with bNat
    cases shape with zero | successor
    . rw zero
      have computed : equalNat(succ(k), 0) = Bool.false
        settle with equalNat, isZero, BoolOps.not, BoolOps.and
      rw computed
      exact Bool.inductive.constructor.false
    . rcases successor with ⟨j, hj, equal⟩
      rw equal
      have computed : equalNat(succ(k), succ(j)) = equalNat(k, j)
        settle with equalNat, isZero, predecessor, BoolOps.not, BoolOps.and
      rw computed
      exact ih with j, hj

theorem equalNat.false_iff (a b : Nat)
  shows equalNat(a, b) = Bool.false ↔ a ≠ b
proof
  have boolean := equalNat.boolean at a, b with *
  have shape := boolean.cases with boolean
  have truth := Grace.Cumulus.Nat.Mod.equalNat.true_iff at a, b with *
  have distinct := Bool.inductive.disjoint.false.true
  constructor
  . intros falseValue same
    have trueValue := truth.backward with same
    rw falseValue at trueValue
    exact distinct with trueValue
  . intro different
    cases shape with falseValue | trueValue
    . exact falseValue
    . have same := truth.forward with trueValue
      exfalso
      exact different with same

theorem isZero.boolean (n : Nat)
  shows Bool(isZero(n))
proof
  induction n
  | zero =>
    simp [isZero]
    exact Bool.inductive.constructor.true
  | succ(k) using ih =>
    simp [isZero]
    exact Bool.inductive.constructor.false

theorem chooseNat.natural (condition : Bool, yes no : Nat)
  shows Nat(chooseNat(condition, yes, no))
proof
  have shape := boolean.cases with *
  cases shape with falseValue | trueValue
  . rw falseValue
    simp [chooseNat]
  . rw trueValue
    simp [chooseNat]

theorem mod.natural (d n : Nat)
  shows Nat(n % d)
proof
  induction n
  | zero =>
    simp [mod]
    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), 0, succ(k % d) with *
    simpa [mod, nextRemainder] using natural

theorem mod.zero_left (d : Nat)
  shows 0 % d = 0
proof
  simp [mod]

theorem mod.zero_right (n : Nat)
  shows n % 0 = n
proof
  induction n
  | zero => settle with mod
  | succ(k) using ih =>
    settle with mod, nextRemainder, equalNat, isZero,
      predecessor, BoolOps.not, BoolOps.and, chooseNat, ih

theorem mod.one (n : Nat)
  shows n % 1 = 0
proof
  induction n
  | zero => settle with mod
  | succ(k) using ih =>
    settle with mod, nextRemainder, equalNat, isZero, predecessor,
      BoolOps.not, BoolOps.and, chooseNat, ih

theorem mod.sample
  shows 100 % 7 = 2
proof
  compute

eval 100 % 7