-- Laws of truncated subtraction on the 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.SubtractionLemmas
import Subtraction
import OrderLemmas

theorem predecessor.le (n : Nat)
  shows predecessor(n) ≤ n
proof
  have shape := natural.zero_or_successor at n
  cases shape with zero | successor
  . rw [zero, predecessor.zero]
    exact LessEqual.reflexive with *
  . obtain ⟨k, kNat, equation⟩ := successor
    rw [equation, predecessor.succ]
    exact LessEqual.successor with *

theorem predecessor.add_one (n : Nat)
  shows predecessor(n + 1) = n
proof
  have shape := add.right_one at n
  rw shape
  exact predecessor.succ with *

theorem predecessor.add_one_of_positive (n : Nat)
  requires positive : 0 < n
  shows predecessor(n) + 1 = n
proof
  have shape := natural.zero_or_successor at n
  cases shape with zero | successor
  . rw zero at positive
    exfalso
    exact Less.irreflexive with positive
  . obtain ⟨k, kNat, equation⟩ := successor
    rw [equation, predecessor.succ]
    exact add.right_one with *

theorem predecessor.Less_of_positive (n : Nat)
  requires positive : 0 < n
  shows predecessor(n) < n
proof
  have predNat := predecessor.closed at n
  have shape := predecessor.add_one_of_positive with positive
  have bound : predecessor(n) < predecessor(n) + 1 by linarith
  rw shape at bound
  exact bound

theorem predecessor.monotone (m n : Nat)
  requires below : m ≤ n
  shows predecessor(m) ≤ predecessor(n)
proof
  have shape := natural.zero_or_successor at m
  cases shape with zero | successor
  . rw [zero, predecessor.zero]
    have predNat := predecessor.closed at n
    linarith
  . obtain ⟨k, kNat, equation⟩ := successor
    rw equation at below
    have nShape := natural.zero_or_successor at n
    cases nShape with nZero | nSuccessor
    . rw nZero at below
      exfalso
      have impossible : succ(k) ≤ 0 := below
      have positive : 0 < succ(k) by linarith
      exact Less.not_LessEqual with positive, impossible
    . obtain ⟨j, jNat, nEquation⟩ := nSuccessor
      rw nEquation at below
      rw [equation, nEquation, predecessor.succ, predecessor.succ]
      have stepK : succ(k) = k + 1 by ring
      have stepJ : succ(j) = j + 1 by ring
      rw [stepK, stepJ] at below
      linarith

theorem sub.add_left (m n : Nat)
  shows (n + m) - n = m
proof
  have swap := add.commutative at m, n with *
  rw swap
  exact sub.add_right with *

theorem sub.self (n : Nat)
  shows n - n = 0
proof
  have shape := sub.add_right at 0, n
  have unit := add.left_unit at n
  rw unit at shape
  exact shape

theorem sub.of_add_eq (a b c : Nat)
  requires sum : a + b = c
  shows c - b = a
proof
  rw ← sum
  exact sub.add_right with *

theorem sub.of_add_eq_left (a b c : Nat)
  requires sum : a + b = c
  shows c - a = b
proof
  rw ← sum
  exact sub.add_left with *

theorem sub.add_cancel (a b : Nat)
  requires below : b ≤ a
  shows a - b + b = a
proof
  obtain ⟨k, kNat, equation⟩ := below
  have value := sub.of_add_eq_left with equation
  rw value
  have swap := add.commutative at b, k with *
  rw swap
  exact equation

theorem sub.add_cancel_left (a b : Nat)
  requires below : b ≤ a
  shows b + (a - b) = a
proof
  have subNat := sub.closed at a, b
  have cancel := sub.add_cancel with below
  have swap := add.commutative at a - b, b with *
  rw swap
  exact cancel

theorem sub.sub (a b c : Nat)
  shows a - (b + c) = (a - b) - c
proof
  induction c
  | zero =>
    have unit := add.right_unit at b
    rw unit
    have subNat := sub.closed at a, b
    rw sub.zero_right
    rfl
  | succ(k) using ih =>
    have shape := add.succ_right at k, b
    rw shape
    have subNat := sub.closed at a, b
    have innerNat := sub.closed at a, b + k
    rw [sub.succ_right, ih, sub.succ_right]
    rfl

theorem sub.swap (a b c : Nat)
  shows (a - b) - c = (a - c) - b
proof
  have first := sub.sub at a, b, c
  have second := sub.sub at a, c, b
  have swap := add.commutative at c, b with *
  rw [← first, ← second, swap]
  rfl

theorem sub.eq_zero_of_le (a b : Nat)
  requires below : a ≤ b
  shows a - b = 0
proof
  obtain ⟨k, kNat, equation⟩ := below
  rw [← equation, sub.sub, sub.self]
  exact sub.zero_left with *

theorem sub.positive_of_Less (a b : Nat)
  requires below : a < b
  shows 0 < b - a
proof
  have peeled := sub.succ_of_Less at a with b, below
  have innerNat := sub.closed at b, succ(a)
  rw peeled
  have step : succ(b - succ(a)) = (b - succ(a)) + 1 by ring
  rw step
  linarith

theorem sub.eq_zero_iff (a b : Nat)
  shows a - b = 0 ↔ a ≤ b
proof
  constructor
  . intro zero
    have split := Less.or_LessEqual at b, a
    cases split with above | below
    . have positive := sub.positive_of_Less with above
      rw zero at positive
      exfalso
      exact Less.irreflexive with positive
    . exact below
  . intro below
    exact sub.eq_zero_of_le with below

theorem sub.positive_iff (a b : Nat)
  shows 0 < b - a ↔ a < b
proof
  have subNat := sub.closed at b, a
  constructor
  . intro positive
    have split := Less.or_LessEqual at a, b
    cases split with below | above
    . exact below
    . have zero := sub.eq_zero_of_le with above
      rw zero at positive
      exfalso
      exact Less.irreflexive with positive
  . intro below
    exact sub.positive_of_Less with below

theorem sub.le_self (a b : Nat)
  shows a - b ≤ a
proof
  induction b
  | zero =>
    rw sub.zero_right
    exact LessEqual.reflexive with *
  | succ(k) using ih =>
    have subNat := sub.closed at a, k
    have pred := predecessor.le at a - k
    rw sub.succ_right
    exact LessEqual.transitive with pred, ih

theorem sub.monotone_left (a b c : Nat)
  requires below : a ≤ b
  shows a - c ≤ b - c
proof
  induction c
  | zero =>
    rw [sub.zero_right, sub.zero_right]
    exact below
  | succ(k) using ih =>
    have leftNat := sub.closed at a, k
    have rightNat := sub.closed at b, k
    rw [sub.succ_right, sub.succ_right]
    exact predecessor.monotone with ih

theorem sub.antitone_right (a b c : Nat)
  requires below : b ≤ c
  shows a - c ≤ a - b
proof
  obtain ⟨k, kNat, equation⟩ := below
  have subNat := sub.closed at a, b
  rw [← equation, sub.sub]
  exact sub.le_self with *

theorem sub.Less_self (a b : Nat)
  requires aPositive : 0 < a
  requires bPositive : 0 < b
  shows a - b < a
proof
  have one : 1 ≤ b by linarith
  have bound := sub.antitone_right at a, 1, b with one
  have oneShape := sub.one at a
  rw oneShape at bound
  have pred := predecessor.Less_of_positive with aPositive
  exact LessEqual.transitive_Less with bound, pred

theorem sub.add_one_of_le (a b : Nat)
  requires below : b ≤ a
  shows (a + 1) - b = (a - b) + 1
proof
  obtain ⟨k, kNat, equation⟩ := below
  have value := sub.of_add_eq_left with equation
  rw [value, ← equation]
  have shape : b + k + 1 = (k + 1) + b by ring
  rw shape
  exact sub.add_right with *

theorem sub.add_sub_assoc (a b c : Nat)
  requires below : c ≤ b
  shows a + (b - c) = (a + b) - c
proof
  obtain ⟨k, kNat, equation⟩ := below
  have value := sub.of_add_eq_left with equation
  rw [value, ← equation]
  have shape : a + (c + k) = (a + k) + c by ring
  rw shape
  symm
  exact sub.add_right with *

theorem sub.sub_cancel (a b : Nat)
  requires below : b ≤ a
  shows a - (a - b) = b
proof
  obtain ⟨k, kNat, equation⟩ := below
  have value := sub.of_add_eq_left with equation
  rw [value, ← equation]
  exact sub.add_right with *

theorem sub.add_add (a b c : Nat)
  shows (a + c) - (b + c) = a - b
proof
  have swap := add.commutative at c, b with *
  rw [swap, sub.sub]
  have cancel := sub.add_right at a, c
  rw cancel
  rfl

theorem sub.add_one_both (a b : Nat)
  shows (a + 1) - (b + 1) = a - b
proof
  exact sub.add_add at a, b, 1

theorem sub.add_one_right (n : Nat)
  shows (n + 1) - 1 = n
proof
  exact sub.add_right at n, 1

theorem sub.le_iff (a b c : Nat)
  shows a - b ≤ c ↔ a ≤ b + c
proof
  have subNat := sub.closed at a, b
  constructor
  . intro below
    have split := LessEqual.total at b, a
    cases split with first | second
    . have cancel := sub.add_cancel_left with first
      rw ← cancel
      linarith
    . linarith
  . intro below
    have shifted := sub.monotone_left at a, b + c, b with below
    have cancel := sub.add_left at c, b
    rw cancel at shifted
    exact shifted

theorem sub.Less_iff (a b c : Nat)
  requires below : b ≤ a
  shows a - b < c ↔ a < b + c
proof
  have subNat := sub.closed at a, b
  have cancel := sub.add_cancel_left with below
  constructor
  . intro strict
    rw ← cancel
    linarith
  . intro strict
    rw ← cancel at strict
    linarith

theorem sub.eq_iff_of_le (a b c : Nat)
  requires below : b ≤ a
  shows a - b = c ↔ a = b + c
proof
  have subNat := sub.closed at a, b
  have cancel := sub.add_cancel_left with below
  constructor
  . intro same
    rw ← same
    symm
    exact cancel
  . intro same
    rw same
    exact sub.add_left with *

theorem sub.Less_monotone_left (a b c : Nat)
  requires below : c ≤ a
  requires strict : a < b
  shows a - c < b - c
proof
  have leftNat := sub.closed at a, c
  have rightNat := sub.closed at b, c
  have weak : c ≤ b by linarith
  have leftCancel := sub.add_cancel_left with below
  have rightCancel := sub.add_cancel_left at b, c with weak
  rw [← leftCancel, ← rightCancel] at strict
  linarith

theorem sub.mul_right (a b c : Nat)
  shows (a - b) * c = a * c - b * c
proof
  have split := LessEqual.total at b, a
  cases split with below | above
  . obtain ⟨k, kNat, equation⟩ := below
    have value := sub.of_add_eq_left with equation
    rw [value, ← equation]
    have shape : (b + k) * c = b * c + k * c by ring
    rw shape
    symm
    exact sub.add_left with *
  . have zero := sub.eq_zero_of_le with above
    have scaled := LessEqual.mul_right at a, b, c with above
    have productZero := sub.eq_zero_of_le with scaled
    rw [zero, productZero]
    exact mul.left_zero with *

theorem sub.mul_left (a b c : Nat)
  shows c * (a - b) = c * a - c * b
proof
  have subNat := sub.closed at a, b
  have swap := mul.commutative at a - b, c with *
  have swapA := mul.commutative at a, c with *
  have swapB := mul.commutative at b, c with *
  rw [swap, swapA, swapB]
  exact sub.mul_right with *

theorem sub.le_of_le_add (a b c : Nat)
  requires below : a ≤ b + c
  shows a - c ≤ b
proof
  have shifted := sub.monotone_left at a, b + c, c with below
  have cancel := sub.add_right at b, c
  rw cancel at shifted
  exact shifted

theorem sub.injective_of_le (a b c : Nat)
  requires first : c ≤ a
  requires second : c ≤ b
  requires same : a - c = b - c
  shows a = b
proof
  have leftCancel := sub.add_cancel_left with first
  have rightCancel := sub.add_cancel_left at b, c with second
  rw [← leftCancel, ← rightCancel, same]
  rfl

-- A product splits along a subtraction of the first factor.
theorem mul.split_sub (p q C : Nat)
  requires le : q ≤ p
  shows p * C = (p - q) * C + q * C
proof
  have pieces := sub.add_cancel with le
  have difference := sub.closed at p, q
  have expanded : (p - q + q) * C = (p - q) * C + q * C by ring
  rw pieces at expanded
  exact expanded