-- Absolute values of the existing quotient integers
-- 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.AbsoluteValue
import Arithmetic

theorem integerClass.positive_difference (a b d : Nat)
  requires difference : b + d = a
  shows integerClass(a, b) = integerOfNat(d)
proof
  unfold integerOfNat
  apply integerClass.eq with *{4}
  ring

theorem integerClass.negative_difference (a b d : Nat)
  requires difference : a + d = b
  shows integerClass(a, b) = integerNegativeOfNat(d)
proof
  unfold integerNegativeOfNat
  apply integerClass.eq with *{4}
  ring

theorem Integer.signed_natural (z : Integer)
  shows ∃ n, Nat(n) ∧ (z = integerOfNat(n) ∨ z = integerNegativeOfNat(n))
proof
  obtain ⟨a, aNat, b, bNat, shape⟩ := Integer.representatives at z with *
  rw under shape
  have total := LessEqual.total at a, b with *
  cases total with negative | positive
  . obtain ⟨d, dNat, difference⟩ := negative
    have value := integerClass.negative_difference with *
    witness d
    right
    exact value
  . obtain ⟨e, eNat, equation⟩ := positive
    have value := integerClass.positive_difference with *
    witness e
    left
    exact value

theorem integerOfNat.neg (n : Nat)
  shows -(integerOfNat(n)) = integerNegativeOfNat(n)
proof
  simp [integerOfNat, integerNegativeOfNat, integerNegValue.classes, integerClassNeg]

theorem integerNegativeOfNat.neg (n : Nat)
  shows -(integerNegativeOfNat(n)) = integerOfNat(n)
proof
  simp [integerOfNat, integerNegativeOfNat, integerNegValue.classes, integerClassNeg]

theorem integerNegativeOfNat.injective (m n : Nat)
  requires same : integerNegativeOfNat(m) = integerNegativeOfNat(n)
  shows m = n
proof
  simp [integerNegativeOfNat] at same
  have sums := integerClass.equivalent_of_eq with *
  simp [add] at sums
  symm
  exact sums

theorem integerOfNat.eq_negative (m n : Nat)
  requires same : integerOfNat(m) = integerNegativeOfNat(n)
  shows m = 0 ∧ n = 0
proof
  simp [integerOfNat, integerNegativeOfNat] at same
  have sums := integerClass.equivalent_of_eq with *
  simp [add] at sums
  exact add.eq_zero with *, sums

theorem integerMagnitude.unique_of_sign (z : Integer, m n : Nat)
  requires first : z = integerOfNat(m) ∨ z = integerNegativeOfNat(m)
  requires second : z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)
  shows m = n
proof
  cases first with positiveM | negativeM
  . cases second with positiveN | negativeN
    . have same : integerOfNat(m) = integerOfNat(n)
      . cc
      exact integerOfNat.injective with *
    . have same : integerOfNat(m) = integerNegativeOfNat(n)
      . cc
      have zeros := integerOfNat.eq_negative with *
      cc
  . cases second with positiveN | negativeN
    . have same : integerOfNat(n) = integerNegativeOfNat(m)
      . cc
      have zeros := integerOfNat.eq_negative with *
      cc
    . have same : integerNegativeOfNat(m) = integerNegativeOfNat(n)
      . cc
      exact integerNegativeOfNat.injective with *

-- Extract the unique natural magnitude in ZF, without Choice.
defunique integerMagnitude (z : Set) (n ∈ ℕ) :=
  z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)
requires integer : Integer(z)
proof
  obtain ⟨n, nNat, sign⟩ := Integer.signed_natural at z with *
  have member := nat.omega.forward with nNat
  refine ⟨n, member, sign⟩

uniqueness
  intros m mMember first n nMember second
  have mNat := nat.omega.backward with mMember
  have nNat := nat.omega.backward with nMember
  exact integerMagnitude.unique_of_sign with *

def integerNatAbs (z : Integer) : Nat := integerMagnitude(z)
def integerAbs (z : Integer) : Integer := integerOfNat(integerNatAbs(z))

theorem integerNatAbs.natural (z : Integer)
  shows Nat(integerNatAbs(z))
proof
  have selected := integerMagnitude.selected at z with *
  rcases selected with ⟨member, sign⟩
  unfold integerNatAbs
  exact nat.omega.backward with member

theorem integerNatAbs.cases (z : Integer)
  shows z = integerOfNat(integerNatAbs(z)) ∨ z = integerNegativeOfNat(integerNatAbs(z))
proof
  have selected := integerMagnitude.selected at z with *
  rcases selected with ⟨member, sign⟩
  simpa [integerNatAbs] using sign

theorem integerNatAbs.eq_of_sign (z : Integer, n : Nat)
  requires sign : z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)
  shows integerNatAbs(z) = n
proof
  have selected := integerNatAbs.cases with *
  exact integerMagnitude.unique_of_sign with *

theorem integerNatAbs.ofNat (n : Nat)
  shows integerNatAbs(integerOfNat(n)) = n
proof
  apply integerNatAbs.eq_of_sign with *{2}
  left
  rfl

theorem integerNatAbs.ofNegativeNat (n : Nat)
  shows integerNatAbs(integerNegativeOfNat(n)) = n
proof
  apply integerNatAbs.eq_of_sign with *{2}
  right
  rfl

theorem integerNatAbs.neg (z : Integer)
  shows integerNatAbs(-z) = integerNatAbs(z)
proof
  have sign := integerNatAbs.cases with *
  apply integerNatAbs.eq_of_sign with *{2}
  cases sign with positive | negative
  . right
    have negated := integerOfNat.neg at integerNatAbs(z) with *
    rwa ← positive at negated
  . left
    have negated := integerNegativeOfNat.neg at integerNatAbs(z) with *
    rwa ← negative at negated

theorem integerAbs.integer (z : Integer)
  shows Integer(integerAbs(z))
proof
  unfold integerAbs
  exact integerOfNat.integer with *

theorem integerAbs.neg (z : Integer)
  shows integerAbs(-z) = integerAbs(z)
proof
  have equal := integerNatAbs.neg with *
  simp [integerAbs]

theorem integerAbs.idempotent (z : Integer)
  shows integerAbs(integerAbs(z)) = integerAbs(z)
proof
  simp [integerAbs, integerNatAbs.ofNat]

theorem integerNatAbs.mul (x y : Integer)
  shows integerNatAbs(x * y) = integerNatAbs(x) * integerNatAbs(y)
proof
  obtain ⟨m, mNat, xSign⟩ := Integer.signed_natural at x with *
  obtain ⟨n, nNat, ySign⟩ := Integer.signed_natural at y with *
  cases xSign with xPositive | xNegative
  . cases ySign with yPositive | yNegative
    . simp [integerMulValue.ofNat, integerNatAbs.ofNat]
    . simp [integerMulValue.ofNat_negative, integerNatAbs.ofNat, integerNatAbs.ofNegativeNat]
  . cases ySign with yPositive | yNegative
    . simp [integerMulValue.negative_ofNat, integerNatAbs.ofNat, integerNatAbs.ofNegativeNat]
    . simp [integerMulValue.negative_negative, integerNatAbs.ofNat, integerNatAbs.ofNegativeNat]

-- Adjust a coefficient when its input is represented with the opposite sign.
theorem integerMulValue.sign_adjust (u z : Integer, n : Nat)
  requires sign : z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)
  shows ∃ v, Integer(v) ∧ v * z = u * integerOfNat(n)
proof
  cases sign with positive | negative
  . witness u
    rw positive
    rfl
  . have negativeInteger := integerNegValue.integer at u with *
    have product := integerMulValue.neg_both at u, integerOfNat(n) with *
    have flipped := integerOfNat.neg with *
    rw [flipped, ← negative] at product
    refine ⟨-u, negativeInteger, product⟩

theorem integerNatAbs.zero
  shows integerNatAbs(integerZero) = 0
proof
  have value := integerNatAbs.ofNat at 0 with *
  simpa [integerZero, integerOfNat] using value

theorem integerNatAbs.zero_iff (z : Integer)
  shows integerNatAbs(z) = 0 ↔ z = integerZero
proof
  constructor
  . intro zero
    have sign := integerNatAbs.cases with *
    rw zero at sign
    unfold integerZero
    cases sign with positive | negative
    . simpa [integerOfNat] using positive
    . simpa [integerNegativeOfNat] using negative
  . intro zero
    rw zero
    exact integerNatAbs.zero