-- Distance between 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.Distance
import SubtractionLemmas
import MinMax

def natDist (a b : Nat) : Nat := (a - b) + (b - a)

theorem natDist.value (a b : Nat)
  shows natDist(a, b) = (a - b) + (b - a)
proof
  simp [natDist]

theorem natDist.natural (a b : Nat)
  shows Nat(natDist(a, b))
proof
  have left := sub.closed at a, b
  have right := sub.closed at b, a
  rw natDist.value
  typecheck

theorem natDist.commutative (a b : Nat)
  shows natDist(a, b) = natDist(b, a)
proof
  have left := sub.closed at a, b
  have right := sub.closed at b, a
  rw [natDist.value, natDist.value]
  ring

theorem natDist.self (a : Nat)
  shows natDist(a, a) = 0
proof
  rw [natDist.value, sub.self]
  ring

theorem natDist.of_le (a b : Nat)
  requires below : a ≤ b
  shows natDist(a, b) = b - a
proof
  have zero := sub.eq_zero_of_le with below
  have right := sub.closed at b, a
  rw [natDist.value, zero]
  exact add.left_unit with *

theorem natDist.of_ge (a b : Nat)
  requires above : b ≤ a
  shows natDist(a, b) = a - b
proof
  have zero := sub.eq_zero_of_le with above
  have left := sub.closed at a, b
  rw [natDist.value, zero]
  exact add.right_unit with *

theorem natDist.zero_right (a : Nat)
  shows natDist(a, 0) = a
proof
  have zero : 0 ≤ a by linarith
  have value1 := natDist.of_ge with zero
  rw [value1, sub.zero_right]
  rfl

theorem natDist.zero_left (a : Nat)
  shows natDist(0, a) = a
proof
  rw natDist.commutative
  exact natDist.zero_right with *

theorem natDist.eq_zero_iff (a b : Nat)
  shows natDist(a, b) = 0 ↔ a = b
proof
  constructor
  . intro zero
    have left := sub.closed at a, b
    have right := sub.closed at b, a
    rw natDist.value at zero
    have both := add.eq_zero with zero
    have below := sub.eq_zero_iff.forward with both.left
    have above := sub.eq_zero_iff.forward with both.right
    exact LessEqual.antisymmetric with below, above
  . intro same
    rw same
    exact natDist.self with *

theorem natDist.positive_iff (a b : Nat)
  shows 0 < natDist(a, b) ↔ a ≠ b
proof
  have distNat := natDist.natural at a, b
  constructor
  . intro positive
    intro same
    have zero := natDist.eq_zero_iff.backward with same
    rw zero at positive
    exact Less.irreflexive with positive
  . intro distinct
    have nonzero : natDist(a, b) ≠ 0
      intro zero
      have same := natDist.eq_zero_iff.forward with zero
      exact distinct with same
    exact Less.positive_of_ne_zero with nonzero

theorem natDist.eq_iff (a b d : Nat)
  shows natDist(a, b) = d ↔ b = a + d ∨ a = b + d
proof
  constructor
  . intro same
    have total := LessEqual.total at a, b
    cases total with below | above
    . left
      have value := natDist.of_le with below
      rw value at same
      have cancel := sub.add_cancel_left with below
      rw [← cancel, same]
      rfl
    . right
      have value := natDist.of_ge with above
      rw value at same
      have cancel := sub.add_cancel_left with above
      rw [← cancel, same]
      rfl
  . intro split
    cases split with first | second
    . have below : a ≤ b by linarith
      have value2 := natDist.of_le with below
      rw [value2, first]
      exact sub.add_left with *
    . have above : b ≤ a by linarith
      have value3 := natDist.of_ge with above
      rw [value3, second]
      exact sub.add_left with *

theorem natDist.add_left (a b k : Nat)
  shows natDist(k + a, k + b) = natDist(a, b)
proof
  have swapA := add.commutative at a, k with *
  have swapB := add.commutative at b, k with *
  rw [natDist.value, natDist.value, swapA, swapB, sub.add_add, sub.add_add]
  rfl

theorem natDist.add_right (a b k : Nat)
  shows natDist(a + k, b + k) = natDist(a, b)
proof
  rw [natDist.value, natDist.value, sub.add_add, sub.add_add]
  rfl

theorem natDist.add_one (a b : Nat)
  shows natDist(a + 1, b + 1) = natDist(a, b)
proof
  exact natDist.add_right at a, b, 1

theorem natDist.mul_left (a b k : Nat)
  shows natDist(k * a, k * b) = k * natDist(a, b)
proof
  have left := sub.closed at a, b
  have right := sub.closed at b, a
  have first := sub.mul_left at a, b, k
  have second := sub.mul_left at b, a, k
  rw [natDist.value, natDist.value, ← first, ← second]
  ring

theorem natDist.mul_right (a b k : Nat)
  shows natDist(a * k, b * k) = natDist(a, b) * k
proof
  have distNat := natDist.natural at a, b
  have swapA := mul.commutative at k, a with *
  have swapB := mul.commutative at k, b with *
  have swap := mul.commutative at k, natDist(a, b) with *
  rw [swapA, swapB, swap]
  exact natDist.mul_left with *

theorem natDist.le_add (a b : Nat)
  shows natDist(a, b) ≤ a + b
proof
  have left := sub.le_self at a, b
  have right := sub.le_self at b, a
  have leftNat := sub.closed at a, b
  have rightNat := sub.closed at b, a
  rw natDist.value
  linarith

theorem natDist.triangle (a b c : Nat)
  shows natDist(a, c) ≤ natDist(a, b) + natDist(b, c)
proof
  have ab := sub.closed at a, b
  have ba := sub.closed at b, a
  have bc := sub.closed at b, c
  have cb := sub.closed at c, b
  have ac := sub.closed at a, c
  have ca := sub.closed at c, a
  have reflexiveAB := LessEqual.reflexive at a - b
  have reflexiveBC := LessEqual.reflexive at b - c
  have reflexiveCB := LessEqual.reflexive at c - b
  have reflexiveBA := LessEqual.reflexive at b - a
  have boundA : a ≤ b + (a - b) := sub.le_iff.forward with reflexiveAB
  have boundB : b ≤ c + (b - c) := sub.le_iff.forward with reflexiveBC
  have boundC : c ≤ b + (c - b) := sub.le_iff.forward with reflexiveCB
  have boundB2 : b ≤ a + (b - a) := sub.le_iff.forward with reflexiveBA
  have forward : a - c ≤ (a - b) + (b - c)
    apply sub.le_iff.backward
    linarith
  have backward : c - a ≤ (c - b) + (b - a)
    apply sub.le_iff.backward
    linarith
  rw [natDist.value, natDist.value, natDist.value]
  linarith

theorem natDist.max_sub_min (a b : Nat)
  shows natDist(a, b) = natMax(a, b) - natMin(a, b)
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have minValue := natMin.of_le with below
    have maxValue := natMax.of_le with below
    have value4 := natDist.of_le with below
    rw [value4, minValue, maxValue]
    rfl
  . have minValue := natMin.of_ge with above
    have maxValue := natMax.of_ge with above
    have value5 := natDist.of_ge with above
    rw [value5, minValue, maxValue]
    rfl

theorem natMin.add_natDist (a b : Nat)
  shows natMin(a, b) + natDist(a, b) = natMax(a, b)
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have minValue := natMin.of_le with below
    have maxValue := natMax.of_le with below
    have value6 := natDist.of_le with below
    rw [value6, minValue, maxValue]
    exact sub.add_cancel_left with below
  . have minValue := natMin.of_ge with above
    have maxValue := natMax.of_ge with above
    have value7 := natDist.of_ge with above
    rw [value7, minValue, maxValue]
    exact sub.add_cancel_left with above