-- Truncated subtraction on the natural numbers: sub(m, n) is m − n when
-- n ≤ m and zero otherwise
-- 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.Subtraction
import OrderLemmas

-- Truncated subtraction: m - n is 0 whenever n exceeds m.
def sub (m n : Nat) → Nat
  | m, zero => m
  | m, succ(n) => predecessor(sub(m, n))
  descends n

notation infixl 60 "-" => sub for Nat

theorem sub.one (n : Nat)
  shows n - 1 = predecessor(n)
proof
  simp [sub]

theorem sub.zero_right (m : Nat)
  shows m - 0 = m
proof
  simp [sub]

theorem sub.succ_right (m n : Nat)
  shows m - succ(n) = predecessor(m - n)
proof
  simp [sub]

theorem predecessor.zero
  shows predecessor(0) = 0
proof
  compute

theorem predecessor.succ (n : Nat)
  shows predecessor(succ(n)) = n
proof
  simp [predecessor]

theorem predecessor.closed (n : Nat)
  shows Nat(predecessor(n))
proof
  induction n
  | zero =>
    rw predecessor.zero
    typecheck
  | succ(k) using ih =>
    rw predecessor.succ
    typecheck

theorem sub.closed (m n : Nat)
  shows Nat(m - n)
proof
  induction n
  | zero =>
    rw sub.zero_right
    typecheck
  | succ(k) using ih =>
    rw sub.succ_right
    exact predecessor.closed at sub(m, k) with ih

theorem sub.zero_left (n : Nat)
  shows 0 - n = 0
proof
  induction n
  | zero => compute
  | succ(k) using ih =>
    rw [sub.succ_right, ih]
    exact predecessor.zero

theorem sub.succ_succ (m n : Nat)
  shows succ(m) - succ(n) = m - n
proof
  induction n
  | zero =>
    rw [sub.succ_right, sub.zero_right, sub.zero_right]
    exact predecessor.succ at m
  | succ(k) using ih =>
    rw [sub.succ_right, ih]
    rw sub.succ_right
    rfl

theorem sub.add_right (m n : Nat)
  shows (m + n) - n = m
proof
  induction n
  | zero =>
    have shape : m + 0 = m by ring
    rw shape
    exact sub.zero_right at m
  | succ(k) using ih =>
    have shape : m + succ(k) = succ(m + k) by ring
    rw [shape, sub.succ_succ]
    exact ih

-- Peeling one unit off the subtrahend below the minuend.
theorem sub.succ_of_Less (k : Nat)
  shows ∀ n, Nat(n) → k < n → n - k = succ(n - succ(k))
proof
  induction k
  | zero =>
    intros n nNat below
    obtain ⟨d, dNat, shape⟩ := below
    have form : succ(0) + d = succ(d) by ring
    rw form at shape
    rw ← shape
    rw [sub.zero_right, sub.succ_succ, sub.zero_right]
    rfl
  | succ(j) using ih =>
    intros n nNat below
    obtain ⟨d, dNat, shape⟩ := below
    have form : succ(succ(j)) + d = succ(j + succ(d)) by ring
    rw form at shape
    have innerNat : Nat(j + succ(d)) by typecheck
    have innerBelow : j < j + succ(d)
      witness d
      ring
    have inner := ih with j + succ(d), innerNat, innerBelow
    rw ← shape
    rw [sub.succ_succ, sub.succ_succ]
    exact inner