-- The embedding of the natural numbers in the integers: order, subtraction,
-- distance, minimum, and maximum
-- 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.Int.Embedding
import MinMax
import Nat.Distance

theorem integerOfNat.one
  shows integerOfNat(1) = integerOne
proof
  unfold integerOne
  rfl

theorem integerOfNat.add_one (n : Nat)
  shows integerOfNat(n + 1) = integerOfNat(n) + 1
proof
  have sum := integerOfNat.add at n, 1
  rw [sum, integerOfNat.one]
  rfl

theorem integerOfNat.injective_iff (a b : Nat)
  shows integerOfNat(a) = integerOfNat(b) ↔ a = b
proof
  constructor
  . intro same
    exact integerOfNat.injective with same
  . intro same
    rw same
    rfl

theorem integerOfNat.eq_zero_iff (n : Nat)
  shows integerOfNat(n) = integerZero ↔ n = 0
proof
  rw ← integerOfNat.zero
  exact integerOfNat.injective_iff at n, 0

theorem integerOfNat.positive_iff (n : Nat)
  shows integerZero < integerOfNat(n) ↔ 0 < n
proof
  rw ← integerOfNat.zero
  exact integerLess.ofNat_iff at 0, n

theorem integerClass.difference (a b : Nat)
  shows integerClass(a, b) = integerOfNat(a) - integerOfNat(b)
proof
  have negated := integerOfNat.neg at b
  have shape : integerOfNat(a) - integerOfNat(b) =
      integerOfNat(a) + (-integerOfNat(b))
    ring
  rw [shape, negated]
  unfold integerOfNat
  unfold integerNegativeOfNat
  rw integerAddValue.classes
  unfold integerClassSum
  have left := add.right_unit at a
  have right := add.left_unit at b
  rw [left, right]
  rfl

theorem integerNegativeOfNat.eq_neg (n : Nat)
  shows integerNegativeOfNat(n) = -integerOfNat(n)
proof
  symm
  exact integerOfNat.neg with *

theorem integerNegativeOfNat.add (a b : Nat)
  shows
    integerNegativeOfNat(a + b) =
      integerNegativeOfNat(a) + integerNegativeOfNat(b)
proof
  have sum := integerOfNat.add at a, b
  rw [integerNegativeOfNat.eq_neg, integerNegativeOfNat.eq_neg]
  rw [integerNegativeOfNat.eq_neg, sum]
  ring

theorem integerNegativeOfNat.le_iff (a b : Nat)
  shows integerNegativeOfNat(a) ≤ integerNegativeOfNat(b) ↔ b ≤ a
proof
  have flipped := integerLe.neg at integerOfNat(b), integerOfNat(a)
  have bridge := integerLe.ofNat_iff at b, a
  rw [integerNegativeOfNat.eq_neg, integerNegativeOfNat.eq_neg]
  constructor
  . intro below
    have lifted := flipped.backward with below
    exact bridge.forward with lifted
  . intro below
    have lifted := bridge.backward with below
    exact flipped.forward with lifted

theorem integerOfNat.sub (a b : Nat)
  requires below : b ≤ a
  shows integerOfNat(a - b) = integerOfNat(a) - integerOfNat(b)
proof
  have subNat := sub.closed at a, b
  have cancel := sub.add_cancel with below
  have sum := integerOfNat.add at a - b, b
  rw [← cancel, sum]
  have restore : (a - b) + b - b = a - b by arith
  rw restore
  ring

theorem integerOfNat.sub_of_le (a b : Nat)
  requires below : a ≤ b
  shows integerOfNat(a) - integerOfNat(b) = integerNegativeOfNat(b - a)
proof
  have lifted := integerOfNat.sub at b, a with below
  rw [integerNegativeOfNat.eq_neg, lifted]
  ring

theorem integerNatAbs.ofNat_sub (a b : Nat)
  shows integerNatAbs(integerOfNat(a) - integerOfNat(b)) = natDist(a, b)
proof
  have total := LessEqual.total at b, a
  cases total with below | above
  . have lifted := integerOfNat.sub with below
    have subNat := sub.closed at a, b
    have value := natDist.of_ge with below
    rw [← lifted, integerNatAbs.ofNat, value]
    rfl
  . have lifted := integerOfNat.sub_of_le with above
    have subNat := sub.closed at b, a
    have value := natDist.of_le with above
    rw [lifted, integerNatAbs.ofNegativeNat, value]
    rfl

theorem integerAbs.ofNat_sub (a b : Nat)
  shows
    integerAbs(integerOfNat(a) - integerOfNat(b)) = integerOfNat(natDist(a, b))
proof
  have difference := integerSubValue.integer at integerOfNat(a), integerOfNat(b)
  rw [integerAbs.value, integerNatAbs.ofNat_sub]
  rfl

theorem integerOfNat.natMin (a b : Nat)
  shows
    integerOfNat(natMin(a, b)) = integerMin(integerOfNat(a), integerOfNat(b))
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have lifted := integerLe.ofNat_iff.backward with below
    have left := natMin.of_le with below
    have right := integerMin.of_le with lifted
    rw [left, right]
    rfl
  . have lifted := integerLe.ofNat_iff.backward with above
    have left := natMin.of_ge with above
    have right := integerMin.of_ge with lifted
    rw [left, right]
    rfl

theorem integerOfNat.natMax (a b : Nat)
  shows
    integerOfNat(natMax(a, b)) = integerMax(integerOfNat(a), integerOfNat(b))
proof
  have total := LessEqual.total at a, b
  cases total with below | above
  . have lifted := integerLe.ofNat_iff.backward with below
    have left := natMax.of_le with below
    have right := integerMax.of_le with lifted
    rw [left, right]
    rfl
  . have lifted := integerLe.ofNat_iff.backward with above
    have left := natMax.of_ge with above
    have right := integerMax.of_ge with lifted
    rw [left, right]
    rfl

theorem integerOfNat.monotone (a b : Nat)
  requires below : a ≤ b
  shows integerOfNat(a) ≤ integerOfNat(b)
proof
  exact integerLe.ofNat_iff.backward with below

theorem integerOfNat.strict_monotone (a b : Nat)
  requires below : a < b
  shows integerOfNat(a) < integerOfNat(b)
proof
  exact integerLess.ofNat_iff.backward with below

theorem integerNatAbs.le_of_le (x y : Integer)
  requires nonnegative : 0 ≤ x
  requires below : x ≤ y
  shows integerNatAbs(x) ≤ integerNatAbs(y)
proof
  have xNat := integerNatAbs.natural at x
  have yNat := integerNatAbs.natural at y
  have bound := integerAbs.monotone_nonneg with nonnegative, below
  rw [integerAbs.value, integerAbs.value] at bound
  exact integerLe.ofNat_iff.forward with bound