-- Arithmetic on quotient integers, independent of representatives
-- 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.Arithmetic
import Operations

-- The output class is unique by representative independence.
-- Extract it in ZF; no representative selector or Choice axiom is used.
defunique selectedIntegerSum (x y : Set) (z ∈ ℤ) :=
  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧
    x = integerClass(a, b) ∧ y = integerClass(c, d) ∧ z = integerClassSum(a, b, c, d)
requires xInteger : Integer(x)
requires yInteger : Integer(y)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with xInteger
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with yInteger
  have result := integerClassSum.integer at a, b, c, d with *
  unfold Integer at result
  witness integerClassSum(a, b, c, d)
  refine ⟨result, a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, rfl⟩

uniqueness
  intros z zMember zProperty w wMember wProperty
  obtain ⟨a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, zShape⟩ := zProperty
  obtain ⟨e, eNat, f, fNat, g, gNat, h, hNat, xOther, yOther, wShape⟩ := wProperty
  have xSame : integerClass(a, b) = integerClass(e, f)
    cc
  have ySame : integerClass(c, d) = integerClass(g, h)
    cc
  have left := integerClass.equivalent_of_eq at a, b, e, f with *
  have right := integerClass.equivalent_of_eq at c, d, g, h with *
  have independent := integerClassSum.well_defined at a, b, e, f, c, d, g, h with *
  cc

def integerAddValue (x y : Integer) : Integer := selectedIntegerSum(x, y)

theorem integerAddValue.integer (x y : Integer)
  shows Integer(integerAddValue(x, y))
proof
  have selected := selectedIntegerSum.selected at x, y with *
  unfold integerAddValue
  unfold Integer
  tauto

theorem integerAddValue.classes (a b c d : Nat)
  shows integerAddValue(integerClass(a, b), integerClass(c, d)) = integerClassSum(a, b, c, d)
proof
  have selected := selectedIntegerSum.selected at integerClass(a, b), integerClass(c, d) with *
  rcases selected with ⟨integer, a2, a2Nat, b2, b2Nat, c2, c2Nat, d2, d2Nat, xShape, yShape, value⟩
  have left := integerClass.equivalent_of_eq at a, b, a2, b2 with *
  have right := integerClass.equivalent_of_eq at c, d, c2, d2 with *
  have independent := integerClassSum.well_defined at a, b, a2, b2, c, d, c2, d2 with *
  unfold integerAddValue
  rw independent
  exact value

defunique selectedIntegerProduct (x y : Set) (z ∈ ℤ) :=
  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧
    x = integerClass(a, b) ∧ y = integerClass(c, d) ∧ z = integerClassMul(a, b, c, d)
requires xInteger : Integer(x)
requires yInteger : Integer(y)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives with xInteger
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives with yInteger
  have result := integerClassMul.integer at a, b, c, d with *
  witness integerClassMul(a, b, c, d)
  refine ⟨result, a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, rfl⟩

uniqueness
  intros z zMember zProperty w wMember wProperty
  obtain ⟨a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, zShape⟩ := zProperty
  obtain ⟨e, eNat, f, fNat, g, gNat, h, hNat, xOther, yOther, wShape⟩ := wProperty
  have xSame : integerClass(a, b) = integerClass(e, f) by cc
  have ySame : integerClass(c, d) = integerClass(g, h) by cc
  have left := integerClass.equivalent_of_eq at a, b, e, f with *
  have right := integerClass.equivalent_of_eq at c, d, g, h with *
  have independent := integerClassMul.well_defined at a, b, e, f, c, d, g, h with *
  cc

def integerMulValue (x y : Integer) : Integer := selectedIntegerProduct(x, y)

theorem integerMulValue.integer (x y : Integer)
  shows Integer(integerMulValue(x, y))
proof
  have selected := selectedIntegerProduct.selected at x, y with *
  unfold integerMulValue
  unfold Integer
  tauto

theorem integerMulValue.classes (a b c d : Nat)
  shows integerMulValue(integerClass(a, b), integerClass(c, d)) = integerClassMul(a, b, c, d)
proof
  have selected := selectedIntegerProduct.selected at integerClass(a, b), integerClass(c, d) with *
  rcases selected with ⟨integer, a2, a2Nat, b2, b2Nat, c2, c2Nat, d2, d2Nat, xShape, yShape, value⟩
  have left := integerClass.equivalent_of_eq at a, b, a2, b2 with *
  have right := integerClass.equivalent_of_eq at c, d, c2, d2 with *
  have independent := integerClassMul.well_defined at a, b, a2, b2, c, d, c2, d2 with *
  unfold integerMulValue
  rw independent
  exact value

defunique selectedIntegerNegative (x : Set) (z ∈ ℤ) :=
  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ x = integerClass(a, b) ∧ z = integerClassNeg(a, b)
requires xInteger : Integer(x)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives with xInteger
  have result := integerClassNeg.integer at a, b with *
  witness integerClassNeg(a, b)
  refine ⟨result, a, aNat, b, bNat, xShape, rfl⟩

uniqueness
  intros z zMember zProperty w wMember wProperty
  obtain ⟨a, aNat, b, bNat, xShape, zShape⟩ := zProperty
  obtain ⟨c, cNat, d, dNat, xOther, wShape⟩ := wProperty
  have same : integerClass(a, b) = integerClass(c, d) by cc
  have equivalent := integerClass.equivalent_of_eq with *
  have independent := integerClassNeg.well_defined with *
  cc

def integerNegValue (x : Integer) : Integer := selectedIntegerNegative(x)

theorem integerNegValue.integer (x : Integer)
  shows Integer(integerNegValue(x))
proof
  have selected := selectedIntegerNegative.selected at x with *
  unfold integerNegValue
  unfold Integer
  tauto

theorem integerNegValue.classes (a b : Nat)
  shows integerNegValue(integerClass(a, b)) = integerClassNeg(a, b)
proof
  have selected := selectedIntegerNegative.selected at integerClass(a, b) with *
  rcases selected with ⟨integer, a2, a2Nat, b2, b2Nat, xShape, value⟩
  have equivalent := integerClass.equivalent_of_eq with *
  have independent := integerClassNeg.well_defined with *
  unfold integerNegValue
  rw independent
  exact value

-- Operations retain the existing quotient integer carrier.
notation infixl 60 "+" => integerAddValue for Integer
notation infixl 70 "*" => integerMulValue for Integer
notation prefix 75 "-" => integerNegValue for Integer

theorem integerAddValue.commutative (x y : Integer)
  shows x + y = y + x
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  simp [integerAddValue.classes]
  exact integerClassSum.commutative with *

theorem integerMulValue.commutative (x y : Integer)
  shows x * y = y * x
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  simp [integerMulValue.classes]
  exact integerClassMul.commutative with *

theorem integerAddValue.zero_right (x : Integer)
  shows x + integerZero = x
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  simp [integerZero, integerAddValue.classes, integerClassSum.zero_right]

theorem integerAddValue.neg_right (x : Integer)
  shows x + (-x) = integerZero
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  simp [integerNegValue.classes, integerClassNeg, integerAddValue.classes, integerClassSum.neg_right]

theorem integerNegValue.involutive (x : Integer)
  shows -(-x) = x
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  simp [integerNegValue.classes, integerClassNeg]

theorem integerAddValue.associative (x y z : Integer)
  shows (x + y) + z = x + (y + z)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  obtain ⟨e, eNat, f, fNat, zShape⟩ := Integer.representatives at z with *
  simp [integerAddValue.classes, integerClassSum]
  apply integerClass.eq with *{4}
  ring

theorem integerMulValue.associative (x y z : Integer)
  shows (x * y) * z = x * (y * z)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  obtain ⟨e, eNat, f, fNat, zShape⟩ := Integer.representatives at z with *
  simp [integerMulValue.classes, integerClassMul]
  apply integerClass.eq with *{4}
  ring

theorem integerMulValue.distribute_right (x y z : Integer)
  shows x * (y + z) = x * y + x * z
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  obtain ⟨e, eNat, f, fNat, zShape⟩ := Integer.representatives at z with *
  simp [integerAddValue.classes, integerClassSum, integerMulValue.classes, integerClassMul]
  apply integerClass.eq with *{4}
  ring

theorem integerOfNat.add (a b : Nat)
  shows integerOfNat(a + b) = integerAddValue(integerOfNat(a), integerOfNat(b))
proof
  simp [integerOfNat, integerAddValue.classes, integerClassSum, add]

theorem integerOfNat.mul (a b : Nat)
  shows integerOfNat(a * b) = integerMulValue(integerOfNat(a), integerOfNat(b))
proof
  simp [integerOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]

theorem integerMulValue.neg_left (x y : Integer)
  shows (-x) * y = -(x * y)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  simp [integerNegValue.classes, integerClassNeg, integerMulValue.classes, integerClassMul]
  apply integerClass.eq with *{4}
  ring

theorem integerMulValue.neg_right (x y : Integer)
  shows x * (-y) = -(x * y)
proof
  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *
  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *
  simp [integerNegValue.classes, integerClassNeg, integerMulValue.classes, integerClassMul]

theorem integerMulValue.neg_both (x y : Integer)
  shows (-x) * (-y) = x * y
proof
  simp [integerMulValue.neg_left, integerMulValue.neg_right, integerNegValue.involutive]

theorem integerMulValue.ofNat (m n : Nat)
  shows integerOfNat(m) * integerOfNat(n) = integerOfNat(m * n)
proof
  symm
  exact integerOfNat.mul with *

theorem integerMulValue.ofNat_negative (m n : Nat)
  shows integerOfNat(m) * integerNegativeOfNat(n) = integerNegativeOfNat(m * n)
proof
  simp [integerOfNat, integerNegativeOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]

theorem integerMulValue.negative_ofNat (m n : Nat)
  shows integerNegativeOfNat(m) * integerOfNat(n) = integerNegativeOfNat(m * n)
proof
  simp [integerOfNat, integerNegativeOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]

theorem integerMulValue.negative_negative (m n : Nat)
  shows integerNegativeOfNat(m) * integerNegativeOfNat(n) = integerOfNat(m * n)
proof
  simp [integerOfNat, integerNegativeOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]