-- The commutative ring laws for the usual concrete complex operations.
-- 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.Complex.Ring
import Core

section Coordinates
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)
notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)

theorem complex.add_associative_pair (a b c d e f : Real)
  shows ℂ[ℂ[(a, b) + (c, d)] + (e, f)] = ℂ[(a, b) + ℂ[(c, d) + (e, f)]]
proof
  have horizontal : R[(a+c)+e] = R[a+(c+e)] by ring
  have vertical : R[(b+d)+f] = R[b+(d+f)] by ring
  simp [complexAdd.pair]

theorem complex.add_commutative_pair (a b c d : Real)
  shows ℂ[(a, b) + (c, d)] = ℂ[(c, d) + (a, b)]
proof
  have horizontal : R[a+c] = R[c+a] by ring
  have vertical : R[b+d] = R[d+b] by ring
  simp [complexAdd.pair]

theorem complex.add_zero_pair (a b : Real)
  shows ℂ[(a, b) + 0] = (a, b)
proof
  have horizontal : R[a+0] = R[a] by ring
  have vertical : R[b+0] = R[b] by ring
  simp [complexZero, complexAdd.pair]

theorem complex.add_neg_pair (a b : Real)
  shows ℂ[(a, b) + ℂ[-(a, b)]] = ℂ[0]
proof
  have horizontal : R[a+(-a)] = R[0] by ring
  have vertical : R[b+(-b)] = R[0] by ring
  simp [complexZero, complexNeg.pair, complexAdd.pair]

theorem complex.mul_associative_pair (a b c d e f : Real)
  shows ℂ[ℂ[(a, b) * (c, d)] * (e, f)] = ℂ[(a, b) * ℂ[(c, d) * (e, f)]]
proof
  have horizontal : R[(a*c-b*d)*e-(a*d+b*c)*f] = R[a*(c*e-d*f)-b*(c*f+d*e)] by ring
  have vertical : R[(a*c-b*d)*f+(a*d+b*c)*e] = R[a*(c*f+d*e)+b*(c*e-d*f)] by ring
  simp [complexMul.pair]

theorem complex.mul_commutative_pair (a b c d : Real)
  shows ℂ[(a, b) * (c, d)] = ℂ[(c, d) * (a, b)]
proof
  have horizontal : R[a*c-b*d] = R[c*a-d*b] by ring
  have vertical : R[a*d+b*c] = R[c*b+d*a] by ring
  simp [complexMul.pair]

theorem complex.mul_one_pair (a b : Real)
  shows ℂ[(a, b) * 1] = (a, b)
proof
  have horizontal : R[a*1-b*0] = R[a] by ring
  have vertical : R[a*0+b*1] = R[b] by ring
  simp [complexOne, complexMul.pair]

theorem complex.distributive_pair (a b c d e f : Real)
  shows ℂ[(a, b) * ℂ[(c, d) + (e, f)]] = ℂ[ℂ[(a, b) * (c, d)] + ℂ[(a, b) * (e, f)]]
proof
  have horizontal : R[a*(c+e)-b*(d+f)] = R[(a*c-b*d)+(a*e-b*f)] by ring
  have vertical : R[a*(d+f)+b*(c+e)] = R[(a*d+b*c)+(a*f+b*e)] by ring
  simp [complexAdd.pair, complexMul.pair]

theorem complexAdd.associative
  shows Associative(complexCarrier, complexAdd)
proof
  intros x hx y hy z hz
  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx
  rw xShape
  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy
  rw yShape
  obtain ⟨e, eReal, f, fReal, zShape⟩ := complexCarrier.cases with hz
  rw zShape
  exact complex.add_associative_pair with *

theorem complexAdd.commutative
  shows Commutative(complexCarrier, complexAdd)
proof
  intros x hx y hy
  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx
  rw xShape
  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy
  rw yShape
  exact complex.add_commutative_pair with *

theorem complexMul.associative
  shows Associative(complexCarrier, complexMul)
proof
  intros x hx y hy z hz
  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx
  rw xShape
  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy
  rw yShape
  obtain ⟨e, eReal, f, fReal, zShape⟩ := complexCarrier.cases with hz
  rw zShape
  exact complex.mul_associative_pair with *

theorem complexMul.commutative
  shows Commutative(complexCarrier, complexMul)
proof
  intros x hx y hy
  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx
  rw xShape
  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy
  rw yShape
  exact complex.mul_commutative_pair with *

theorem complexZero.member
  shows complexZero ∈ complexCarrier
proof
  unfold complexZero
  exact complexCarrier.pair with realZero.real, realZero.real

theorem complexOne.member
  shows complexOne ∈ complexCarrier
proof
  unfold complexOne
  exact complexCarrier.pair with realOne.real, realZero.real

theorem complexAdd.identity
  shows Identity(complexCarrier, complexAdd, complexZero)
proof
  unfold Identity
  refine ⟨complexZero.member, ?_⟩
  intros x member
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  have right := complex.add_zero_pair at a, b with *
  rw ← shape at right
  have commutes := complexAdd.commutative
  have swap := commutes with complexZero, complexZero.member, x, member
  constructor
  . cc
  . exact right

theorem complexMul.identity
  shows Identity(complexCarrier, complexMul, complexOne)
proof
  unfold Identity
  refine ⟨complexOne.member, ?_⟩
  intros x member
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  have right := complex.mul_one_pair at a, b with *
  rw ← shape at right
  have commutes := complexMul.commutative
  have swap := commutes with complexOne, complexOne.member, x, member
  constructor
  . cc
  . exact right

theorem complexNeg.inverse
  shows Inverse(complexCarrier, complexAdd, complexZero, complexNeg)
proof
  unfold Inverse
  refine ⟨complexNeg.function, ?_⟩
  intros x member
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  have right := complex.add_neg_pair at a, b with *
  rw ← shape at right
  have negative : complexNeg(x) ∈ complexCarrier
    exact FunctionBetween.apply_closed with complexNeg.function, member
  have commutes := complexAdd.commutative
  have swap := commutes with complexNeg(x), negative, x, member
  constructor
  . cc
  . exact right

theorem complexMul.distributive
  shows Distributive(complexCarrier, complexAdd, complexMul)
proof
  intros x hx y hy z hz
  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx
  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy
  obtain ⟨e, eReal, f, fReal, zShape⟩ := complexCarrier.cases with hz
  have left := complex.distributive_pair at a, b, c, d, e, f with *
  rw [← xShape, ← yShape, ← zShape] at left
  have other := complex.distributive_pair at e, f, a, b, c, d with *
  rw [← xShape, ← yShape, ← zShape] at other
  have sum : complexAdd(x, y) ∈ complexCarrier
    unfold call2
    have pair := product.pair with hx, hy
    exact FunctionBetween.apply_closed with complexAdd.function, pair
  have commutes := complexMul.commutative
  have outer := commutes with z, hz, complexAdd(x, y), sum
  have first := commutes with z, hz, x, hx
  have second := commutes with z, hz, y, hy
  constructor
  . exact left
  . cc

instance complexes.comm_ring
  shows IsCommRing(ℂ)
proof
  constructor
    constructor
      constructor
        constructor
          constructor
            constructor
              exact complexAdd.function
            . exact complexAdd.associative
          . exact complexAdd.identity
        . exact complexNeg.inverse
      . exact complexAdd.commutative
    . constructor
        constructor
          constructor
            exact complexMul.function
          . exact complexMul.associative
        . exact complexMul.identity
      . exact complexMul.distributive
  . exact complexMul.commutative

end Coordinates