-- Integer operations lifted from natural-pair 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.Operations
import Core

def integerPairSum (a b c d : Set) : Set := (add(a, c), add(b, d))
def integerClassSum (a b c d : Set) : Set := integerClass(add(a, c), add(b, d))
def integerClassNeg (a b : Set) : Set := integerClass(b, a)

theorem integerPairSum.pair (a b c d : Nat)
  shows integerPairSum(a, b, c, d) ∈ integerPairs
proof
  unfold integerPairSum
  have leftNat := add.closed at c, a with *
  have rightNat := add.closed at d, b with *
  exact integerPairs.pair with leftNat, rightNat

theorem integerPairSum.cross_sums (a b a2 b2 c d c2 d2 : Nat)
  requires leftEquivalent : add(a, b2) = add(a2, b)
  requires rightEquivalent : add(c, d2) = add(c2, d)
  shows add(add(a, c), add(b2, d2)) = add(add(a2, c2), add(b, d))
proof
  ring

theorem integerClassSum.well_defined (a b a2 b2 c d c2 d2 : Nat)
  requires leftEquivalent : add(a, b2) = add(a2, b)
  requires rightEquivalent : add(c, d2) = add(c2, d)
  shows integerClassSum(a, b, c, d) = integerClassSum(a2, b2, c2, d2)
proof
  unfold integerClassSum
  have sums := integerPairSum.cross_sums at a, b, a2, b2, c, d, c2, d2 with *
  exact integerClass.eq with sums

theorem integerClassSum.integer (a b c d : Nat)
  shows Integer(integerClassSum(a, b, c, d))
proof
  unfold integerClassSum
  have leftNat := add.closed at c, a with *
  have rightNat := add.closed at d, b with *
  exact integerClass.integer with leftNat, rightNat

theorem integerClassNeg.well_defined (a b c d : Nat)
  requires equivalent : add(a, d) = add(c, b)
  shows integerClassNeg(a, b) = integerClassNeg(c, d)
proof
  unfold integerClassNeg
  have reverse := integerEquivalent.cross_symmetric with *
  have leftCommute := add.commutative at c, b with *
  have rightCommute := add.commutative at d, a with *
  have negatedSums := reverse
  rewrite ← leftCommute at negatedSums
  rewrite rightCommute at negatedSums
  exact integerClass.eq with *

theorem integerClassSum.zero_right (a b : Nat)
  shows integerClassSum(a, b, 0, 0) = integerClass(a, b)
proof
  simp [integerClassSum, add.right_unit]

theorem integerClassSum.commutative (a b c d : Nat)
  shows integerClassSum(a, b, c, d) = integerClassSum(c, d, a, b)
proof
  unfold integerClassSum
  have positive := add.commutative at c, a with *
  have negative := add.commutative at d, b with *
  rewrite positive
  rewrite negative
  rfl

theorem integerClassSum.neg_right (a b : Nat)
  shows integerClassSum(a, b, b, a) = integerZero
proof
  unfold integerClassSum
  unfold integerZero
  have sumNat := add.closed at b, a with *
  have reverseNat := add.closed at a, b with *
  have commute := add.commutative at b, a with *
  have classes := integerClass.eq with sumNat, reverseNat, Naturals.constructor.zero, Naturals.constructor.zero
  apply classes
  simp [add, add.right_unit, commute]

-- Multiplication of differences: (a-b)(c-d) = (ac+bd)-(ad+bc).
def integerClassMul (a b c d : Nat) : Integer :=
  integerClass(a * c + b * d, a * d + b * c)

theorem integerClassMul.integer (a b c d : Nat)
  shows Integer(integerClassMul(a, b, c, d))
proof
  unfold integerClassMul
  exact integerClass.integer with *

theorem integerClassMul.commutative (a b c d : Nat)
  shows integerClassMul(a, b, c, d) = integerClassMul(c, d, a, b)
proof
  unfold integerClassMul
  apply integerClass.eq with *{4}
  ring

theorem integerClassMul.transport_left (a b a2 b2 c d : Nat)
  requires equivalent : a + b2 = a2 + b
  shows integerClassMul(a, b, c, d) = integerClassMul(a2, b2, c, d)
proof
  have combined : (a + b2) * c + (a2 + b) * d = (a2 + b) * c + (a + b2) * d
  . rw equivalent
    rfl
  unfold integerClassMul
  apply integerClass.eq with *{4}
  ring

theorem integerClassMul.well_defined (a b a2 b2 c d c2 d2 : Nat)
  requires leftEquivalent : a + b2 = a2 + b
  requires rightEquivalent : c + d2 = c2 + d
  shows integerClassMul(a, b, c, d) = integerClassMul(a2, b2, c2, d2)
proof
  have first := integerClassMul.transport_left at a, b, a2, b2, c, d with *
  have swap := integerClassMul.commutative at a2, b2, c, d with *
  have second := integerClassMul.transport_left at c, d, c2, d2, a2, b2 with *
  have back := integerClassMul.commutative at c2, d2, a2, b2 with *
  simp

theorem integerClassNeg.integer (a b : Nat)
  shows Integer(integerClassNeg(a, b))
proof
  unfold integerClassNeg
  exact integerClass.integer with *