-- Concrete complex numbers as ordered pairs of Dedekind reals.
-- 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.Core
import Real.Squares

def complexCarrier : Set := ℝ × ℝ
def complexZero : Set := (realZero, realZero)
def complexOne : Set := (realOne, realZero)
def complexAdd : Set := {p ∈ (complexCarrier × complexCarrier) × complexCarrier | ∃ a ∈ ℝ, ∃ b ∈ ℝ, ∃ c ∈ ℝ, ∃ d ∈ ℝ, p = (((a, b), (c, d)), (realAdd(a, c), realAdd(b, d)))}
def complexNeg : Set := {p ∈ complexCarrier × complexCarrier | ∃ a ∈ ℝ, ∃ b ∈ ℝ, p = ((a, b), (realNeg(a), realNeg(b)))}
def complexMul : Set := {p ∈ (complexCarrier × complexCarrier) × complexCarrier | ∃ a ∈ ℝ, ∃ b ∈ ℝ, ∃ c ∈ ℝ, ∃ d ∈ ℝ, p = (((a, b), (c, d)), (realAdd(realMul(a, c), realNeg(realMul(b, d))), realAdd(realMul(a, d), realMul(b, c))))}

theorem complexCarrier.pair (a b : Real)
  shows (a, b) ∈ complexCarrier
proof
  unfold complexCarrier
  apply product.pair
  . typecheck
  . typecheck

theorem complexCarrier.cases (x : Set)
  requires member : x ∈ complexCarrier
  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ x = (a, b)
proof
  rw complexCarrier at member
  obtain ⟨bounded, a, ha, b, hb, shape⟩ := product.membership.forward with member
  have aReal : Real(a) by typecheck
  have bReal : Real(b) by typecheck
  refine ⟨a, aReal, b, bReal, shape⟩

theorem complexAdd.relates (a b c d : Real)
  shows relates(complexAdd, ((a, b), (c, d)), (a + c, b + d))
proof
  have aIn : a ∈ ℝ by typecheck
  have bIn : b ∈ ℝ by typecheck
  have cIn : c ∈ ℝ by typecheck
  have dIn : d ∈ ℝ by typecheck
  have first := complexCarrier.pair at a, b with *
  have second := complexCarrier.pair at c, d with *
  have input := product.pair with first, second
  have output : (a + c, b + d) ∈ complexCarrier by apply complexCarrier.pair at a + c, b + d
  have bounded := product.pair with input, output
  unfold relates
  exact complexAdd.membership.backward with ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, rfl⟩

theorem complexAdd.factors (x y : Set)
  requires related : relates(complexAdd, x, y)
  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ ∃ c, Real(c) ∧ ∃ d, Real(d) ∧ x = ((a, b), (c, d)) ∧ y = (a + c, b + d)
proof
  obtain ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, shape⟩ := complexAdd.membership.forward at (x, y) with related
  have pair := orderedPair.injective with shape
  have aReal : Real(a) by typecheck
  have bReal : Real(b) by typecheck
  have cReal : Real(c) by typecheck
  have dReal : Real(d) by typecheck
  refine ⟨a, aReal, b, bReal, c, cReal, d, dReal, pair⟩

theorem complexAdd.function
  shows complexAdd : complexCarrier × complexCarrier → complexCarrier
proof
  constructor
    intros p member
    have data := complexAdd.membership.forward with member
    exact data.left
  . constructor
      intros x y first z second
      obtain ⟨a, aReal, b, bReal, c, cReal, d, dReal, input, output⟩ := complexAdd.factors with first
      obtain ⟨e, eReal, f, fReal, g, gReal, h, hReal, input2, output2⟩ := complexAdd.factors with second
      have same : ((a, b), (c, d)) = ((e, f), (g, h)) by cc
      have outer := orderedPair.injective with same
      have left := orderedPair.injective with outer.left
      have right := orderedPair.injective with outer.right
      cc
    . intros x member
      obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with member
      obtain ⟨a, aReal, b, bReal, first⟩ := complexCarrier.cases with hu
      obtain ⟨c, cReal, d, dReal, second⟩ := complexCarrier.cases with hv
      rw [first, second] at shape
      witness (a + c, b + d)
      constructor
      . apply complexCarrier.pair at a + c, b + d
      . rw shape
        exact complexAdd.relates with *

theorem complexAdd.pair (a b c d : Real)
  shows complexAdd((a, b), (c, d)) = (a + c, b + d)
proof
  have first := complexCarrier.pair at a, b with *
  have second := complexCarrier.pair at c, d with *
  have input := product.pair with first, second
  have related := complexAdd.relates at a, b, c, d with *
  have value := FunctionBetween.apply_value with complexAdd.function, input, related
  simp [call2]

theorem complexNeg.relates (a b : Real)
  shows relates(complexNeg, (a, b), (-a, -b))
proof
  have aIn : a ∈ ℝ by typecheck
  have bIn : b ∈ ℝ by typecheck
  have first := complexCarrier.pair at a, b with *
  have input := first
  have output : (-a, -b) ∈ complexCarrier by apply complexCarrier.pair at -a, -b
  have bounded := product.pair with input, output
  unfold relates
  exact complexNeg.membership.backward with ⟨bounded, a, aIn, b, bIn, rfl⟩

theorem complexNeg.factors (x y : Set)
  requires related : relates(complexNeg, x, y)
  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ x = (a, b) ∧ y = (-a, -b)
proof
  unfold relates at related
  obtain ⟨bounded, a, aIn, b, bIn, shape⟩ := complexNeg.membership.forward with related
  have pair := orderedPair.injective with shape
  have aReal : Real(a) by typecheck
  have bReal : Real(b) by typecheck
  refine ⟨a, aReal, b, bReal, pair⟩

theorem complexNeg.function
  shows complexNeg : complexCarrier → complexCarrier
proof
  constructor
    intros p member
    have data := complexNeg.membership.forward with member
    exact data.left
  . constructor
      intros x y first z second
      obtain ⟨a, aReal, b, bReal, input, output⟩ := complexNeg.factors with first
      obtain ⟨e, eReal, f, fReal, input2, output2⟩ := complexNeg.factors with second
      have same : (a, b) = (e, f) by cc
      have coordinates := orderedPair.injective with same
      cc
    . intros x member
      obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
      witness (-a, -b)
      constructor
      . apply complexCarrier.pair at -a, -b
      . rw shape
        exact complexNeg.relates with *

theorem complexNeg.pair (a b : Real)
  shows complexNeg((a, b)) = (-a, -b)
proof
  have first := complexCarrier.pair at a, b with *
  have input := first
  have related := complexNeg.relates at a, b with *
  have value := FunctionBetween.apply_value with complexNeg.function, input, related
  assumption

theorem complexMul.relates (a b c d : Real)
  shows relates(complexMul, ((a, b), (c, d)), (a * c + -(b * d), a * d + b * c))
proof
  have aIn : a ∈ ℝ by typecheck
  have bIn : b ∈ ℝ by typecheck
  have cIn : c ∈ ℝ by typecheck
  have dIn : d ∈ ℝ by typecheck
  have first := complexCarrier.pair at a, b with *
  have second := complexCarrier.pair at c, d with *
  have input := product.pair with first, second
  have output : (a * c + -(b * d), a * d + b * c) ∈ complexCarrier by apply complexCarrier.pair
  have bounded := product.pair with input, output
  unfold relates
  exact complexMul.membership.backward with ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, rfl⟩

theorem complexMul.factors (x y : Set)
  requires related : relates(complexMul, x, y)
  shows ∃ a, Real(a) ∧ ∃ b, Real(b) ∧ ∃ c, Real(c) ∧ ∃ d, Real(d) ∧ x = ((a, b), (c, d)) ∧ y = (a * c + -(b * d), a * d + b * c)
proof
  unfold relates at related
  obtain ⟨bounded, a, aIn, b, bIn, c, cIn, d, dIn, shape⟩ := complexMul.membership.forward with related
  have pair := orderedPair.injective with shape
  have aReal : Real(a) by typecheck
  have bReal : Real(b) by typecheck
  have cReal : Real(c) by typecheck
  have dReal : Real(d) by typecheck
  refine ⟨a, aReal, b, bReal, c, cReal, d, dReal, pair⟩

theorem complexMul.function
  shows complexMul : complexCarrier × complexCarrier → complexCarrier
proof
  constructor
    intros p member
    have data := complexMul.membership.forward with member
    exact data.left
  . constructor
      intros x y first z second
      obtain ⟨a, aReal, b, bReal, c, cReal, d, dReal, input, output⟩ := complexMul.factors with first
      obtain ⟨e, eReal, f, fReal, g, gReal, h, hReal, input2, output2⟩ := complexMul.factors with second
      have same : ((a, b), (c, d)) = ((e, f), (g, h)) by cc
      have outer := orderedPair.injective with same
      have left := orderedPair.injective with outer.left
      have right := orderedPair.injective with outer.right
      cc
    . intros x member
      obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with member
      obtain ⟨a, aReal, b, bReal, first⟩ := complexCarrier.cases with hu
      obtain ⟨c, cReal, d, dReal, second⟩ := complexCarrier.cases with hv
      rw [first, second] at shape
      witness (a * c + -(b * d), a * d + b * c)
      constructor
      . apply complexCarrier.pair at a * c + -(b * d), a * d + b * c
      . rw shape
        exact complexMul.relates with *

theorem complexMul.pair (a b c d : Real)
  shows complexMul((a, b), (c, d)) = (a * c + -(b * d), a * d + b * c)
proof
  have first := complexCarrier.pair at a, b with *
  have second := complexCarrier.pair at c, d with *
  have input := product.pair with first, second
  have related := complexMul.relates at a, b, c, d with *
  have value := FunctionBetween.apply_value with complexMul.function, input, related
  simp [call2]