-- Commutative-ring interface for 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.Ring
import Arithmetic
import Algebra.Ring.Core

defunique integerAddPairValue (p : Set) (z ∈ ℤ) :=
  ∃ x ∈ ℤ, ∃ y ∈ ℤ, p = (x, y) ∧ z = integerAddValue(x, y)
requires pair : p ∈ ℤ × ℤ
proof
  have shape := product.membership.forward at ℤ, ℤ, p with pair
  rcases shape with ⟨bound, x, xMember, y, yMember, equation⟩
  have xInteger : Integer(x)
  . typecheck
  have yInteger : Integer(y)
  . typecheck
  have result := integerAddValue.integer at x, y with *
  unfold Integer at result
  witness integerAddValue(x, y)
  refine ⟨result, x, xMember, y, yMember, equation, rfl⟩

uniqueness
  intros z zMember zProperty w wMember wProperty
  obtain ⟨a, aMember, b, bMember, shape, value⟩ := zProperty
  obtain ⟨c, cMember, d, dMember, otherShape, otherValue⟩ := wProperty
  have same : (a, b) = (c, d)
    cc
  have coordinates := orderedPair.injective at a, b, c, d with same
  rcases coordinates with ⟨left, right⟩
  cc

defgraph integerAdd (p ∈ ℤ × ℤ) : ℤ := integerAddPairValue(p)
proof
  have selected := integerAddPairValue.selected at p with member
  tauto

theorem integerAddValue.notation (x y : Integer)
  shows call2(integerAdd, x, y) = integerAddValue(x, y)
proof
  have xMember : x ∈ ℤ
  . settle with Integer
  have yMember : y ∈ ℤ
  . settle with Integer
  have pair := product.pair at x, y, ℤ, ℤ with *
  have evaluated := integerAdd.value at (x, y) with *
  have selected := integerAddPairValue.selected at (x, y) with *
  rcases selected with ⟨member, a, aMember, b, bMember, shape, value⟩
  obtain ⟨left, right⟩ := orderedPair.injective with shape
  unfold call2
  cc

defunique integerMulPairValue (p : Set) (z ∈ ℤ) :=
  ∃ x ∈ ℤ, ∃ y ∈ ℤ, p = (x, y) ∧ z = integerMulValue(x, y)
requires pair : p ∈ ℤ × ℤ
proof
  obtain ⟨bound, x, xMember, y, yMember, equation⟩ := product.membership.forward with pair
  have xInteger : Integer(x)
  . typecheck
  have yInteger : Integer(y)
  . typecheck
  have result := integerMulValue.integer at x, y with *
  witness integerMulValue(x, y)
  refine ⟨result, x, xMember, y, yMember, equation, rfl⟩

uniqueness
  intros z zMember zProperty w wMember wProperty
  obtain ⟨a, aMember, b, bMember, shape, value⟩ := zProperty
  obtain ⟨c, cMember, d, dMember, otherShape, otherValue⟩ := wProperty
  have same : (a, b) = (c, d) by cc
  obtain ⟨left, right⟩ := orderedPair.injective with same
  cc

defgraph integerMul (p ∈ ℤ × ℤ) : ℤ := integerMulPairValue(p)
proof
  have selected := integerMulPairValue.selected with member
  tauto

theorem integerMulValue.notation (x y : Integer)
  shows call2(integerMul, x, y) = integerMulValue(x, y)
proof
  have xMember : x ∈ ℤ
  . settle with Integer
  have yMember : y ∈ ℤ
  . settle with Integer
  have pair := product.pair at x, y, ℤ, ℤ with *
  have evaluated := integerMul.value at (x, y) with *
  have selected := integerMulPairValue.selected at (x, y) with *
  rcases selected with ⟨member, a, aMember, b, bMember, shape, value⟩
  obtain ⟨left, right⟩ := orderedPair.injective with shape
  unfold call2
  cc

defgraph integerNeg (x ∈ ℤ) : ℤ := integerNegValue(x)
proof
  . typecheck

theorem integerNegValue.notation (x : Integer)
  shows integerNeg(x) = integerNegValue(x)
proof
  have member : x ∈ ℤ
  . settle with Integer
  exact integerNeg.value at x with *

def integerOne : Integer := integerOfNat(1)

theorem integerOne.integer
  shows Integer(integerOne)
proof
  unfold integerOne
  exact integerOfNat.integer with *

theorem integerAddValue.zero_left (x : Integer)
  shows integerZero + x = x
proof
  rw integerAddValue.commutative
  exact integerAddValue.zero_right with *

theorem integerAddValue.neg_left (x : Integer)
  shows (-x) + x = integerZero
proof
  rw integerAddValue.commutative
  exact integerAddValue.neg_right with *

theorem integerMulValue.one_right (x : Integer)
  shows x * integerOne = x
proof
  obtain ⟨a, aNat, b, bNat, shape⟩ := Integer.representatives at x with *
  simp [integerOne, integerOfNat, integerMulValue.classes, integerClassMul, mul.right_unit, mul.right_zero, add.right_unit, add]

theorem integerMulValue.one_left (x : Integer)
  shows integerOne * x = x
proof
  rw integerMulValue.commutative
  exact integerMulValue.one_right with *

theorem integerMulValue.distribute_left (x y z : Integer)
  shows (x + y) * z = x * z + y * z
proof
  have left := integerMulValue.commutative at x, z with *
  have right := integerMulValue.commutative at y, z with *
  have outer := integerMulValue.commutative at x + y, z with *
  have distribution := integerMulValue.distribute_right at z, x, y with *
  rw [outer, distribution, ← left, ← right]
  rfl

instance integerAdd.comm_monoid
  shows IsCommMonoid(ℤ, integerAdd, integerZero)
proof
  constructor
    constructor
      constructor
        exact integerAdd.function
        intros A integerA B integerB C integerC
        have typedA : Integer(A) by typecheck
        have typedB : Integer(B) by typecheck
        have typedC : Integer(C) by typecheck
        simpa [integerAddValue.notation] using integerAddValue.associative at A, B, C with typedA, typedB, typedC
      constructor
      . exact integerZero.integer
      . intros A integerA
        have typedA : Integer(A) by typecheck
        constructor
        . simpa [integerAddValue.notation] using integerAddValue.zero_left at A with typedA
        . simpa [integerAddValue.notation] using integerAddValue.zero_right at A with typedA
    intros A integerA B integerB
    have typedA : Integer(A) by typecheck
    have typedB : Integer(B) by typecheck
    simpa [integerAddValue.notation] using integerAddValue.commutative at A, B with typedA, typedB

instance integerAdd.abelian_group
  shows IsAbelianGroup(ℤ, integerAdd, integerZero, integerNeg)
proof
  constructor
    constructor
    . have additive := integerAdd.comm_monoid
      simp [IsCommMonoid]
      constructor
      . exact integerNeg.function
      . intros A integerA
        have typedA : Integer(A) by typecheck
        constructor
        . simpa [integerAddValue.notation, integerNegValue.notation] using integerAddValue.neg_left at A with typedA
        . simpa [integerAddValue.notation, integerNegValue.notation] using integerAddValue.neg_right at A with typedA
  . have additive := integerAdd.comm_monoid
    simp [IsCommMonoid]

instance integerMul.monoid
  shows IsMonoid(ℤ, integerMul, integerOne)
proof
  constructor
    constructor
      exact integerMul.function
      intros A integerA B integerB C integerC
      have typedA : Integer(A) by typecheck
      have typedB : Integer(B) by typecheck
      have typedC : Integer(C) by typecheck
      simpa [integerMulValue.notation] using integerMulValue.associative at A, B, C with typedA, typedB, typedC
    constructor
    . exact integerOne.integer
    . intros A integerA
      have typedA : Integer(A) by typecheck
      constructor
      . simpa [integerMulValue.notation] using integerMulValue.one_left at A with typedA
      . simpa [integerMulValue.notation] using integerMulValue.one_right at A with typedA

instance integerMul.distributive
  shows Distributive(ℤ, integerAdd, integerMul)
proof
  intros A integerA B integerB C integerC
  have typedA : Integer(A) by typecheck
  have typedB : Integer(B) by typecheck
  have typedC : Integer(C) by typecheck
  constructor
  . simpa [integerAddValue.notation, integerMulValue.notation] using integerMulValue.distribute_right at A, B, C with typedA, typedB, typedC
  . simpa [integerAddValue.notation, integerMulValue.notation] using integerMulValue.distribute_left at A, B, C with typedA, typedB, typedC

instance integerMul.commutative
  shows Commutative(ℤ, integerMul)
proof
  intros A integerA B integerB
  have typedA : Integer(A) by typecheck
  have typedB : Integer(B) by typecheck
  simpa [integerMulValue.notation] using integerMulValue.commutative at A, B with typedA, typedB

instance integers.comm_ring
  shows IsCommRing(ℤ, integerAdd, integerZero, integerNeg, integerMul,
    integerOne)
proof
  constructor
    constructor
    . exact integerAdd.abelian_group
    . constructor
      . exact integerMul.monoid
      . exact integerMul.distributive
  . exact integerMul.commutative


instance integerZero.of_nat
  shows OfNat(ℤ, 0, integerZero)
proof
  constructor
  . typecheck
  . exact integerZero.integer

instance integerOne.of_nat
  shows OfNat(ℤ, 1, integerOne)
proof
  constructor
  . typecheck
  . exact integerOne.integer

notation numeral "0" via OfNat(ℤ, 0, _) for Integer
notation numeral "1" via OfNat(ℤ, 1, _) for Integer

def integerSubValue (x y : Integer) : Integer := call2(integerAdd, x, integerNeg(y))
notation infixl 60 "-" => integerSubValue for Integer

theorem integerSubValue.integer (x y : Integer)
  shows Integer(x - y)
proof
  have sum := integerAddValue.integer at x, integerNegValue(y) with *
  simpa [integerSubValue, integerAddValue.notation, integerNegValue.notation] using sum