-- Cardano's solution of the cubic over the complex numbers: a depressed
-- cubic x³ + px + q has the root s + t whenever s³ + t³ = −q and 3st = −p,
-- such a pair exists for every p and q, and a general monic cubic is
-- depressed by the shift x = y − a/3
-- 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.Cubic
import QuadraticRoots
import FundamentalTheorem
import Field

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

-- Closure of the complex operations, in the shape typecheck can use.
theorem complexAdd.closed (x y : Set)
  requires xIn : x ∈ ℂ
  requires yIn : y ∈ ℂ
  shows ℂ[x + y] ∈ ℂ
proof
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  exact IsRing.add_closed with ordinary, xIn, yIn

theorem complexMul.closed (x y : Set)
  requires xIn : x ∈ ℂ
  requires yIn : y ∈ ℂ
  shows ℂ[x * y] ∈ ℂ
proof
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  exact IsRing.mul_closed with ordinary, xIn, yIn

theorem complexNeg.closed (x : Set)
  requires xIn : x ∈ ℂ
  shows ℂ[-x] ∈ ℂ
proof
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  exact IsRing.neg_closed with ordinary, xIn

theorem complexList.cons_nonempty (c : Set) (cs : List(ℂ))
  requires cIn : c ∈ ℂ
  shows c :: cs ≠ []
proof
  intro same
  have lengths : length{ℂ}(c :: cs) = length{ℂ}([])
    rw same
    rfl
  rw [length.cons, length.nil] at lengths
  have reversed : (0 : Nat) = succ(length{ℂ}(cs)) by cc
  exact Naturals.disjoint.zero.succ at length{ℂ}(cs) with reversed

-- Inverses, zero divisors, and the nonzero constant three.
theorem complex.inverse_exists (x : Set)
  requires xIn : x ∈ ℂ
  requires nonzero : x ≠ ℂ[0]
  shows ∃ y ∈ ℂ, ℂ[x * y] = ℂ[1]
proof
  have field := complexes.is_field
  obtain ⟨y, inverse⟩ := IsField.inverse_exists with field, xIn, nonzero
  have yIn := inverse.right.left
  have law := inverse.right.right.right
  witness y
  exact ⟨yIn, law⟩

theorem complex.zero_of_mul (x y : Set)
  requires xIn : x ∈ ℂ
  requires yIn : y ∈ ℂ
  requires nonzero : x ≠ ℂ[0]
  requires product : ℂ[x * y] = ℂ[0]
  shows y = ℂ[0]
proof
  have field := complexes.is_field
  have noZero := IsField.no_zero_divisors with field
  have forX := noZero with xIn
  have forY := forX with yIn
  have alternatives := forY with product
  cases alternatives with xZero | yZero
  . exfalso
    exact nonzero with xZero
  . exact yZero

theorem complex.mul_nonzero (x y : Set)
  requires xIn : x ∈ ℂ
  requires yIn : y ∈ ℂ
  requires xNonzero : x ≠ ℂ[0]
  requires yNonzero : y ≠ ℂ[0]
  shows ℂ[x * y] ≠ ℂ[0]
proof
  intro product
  have yZero := complex.zero_of_mul with xIn, yIn, xNonzero, product
  exact yNonzero with yZero

theorem complex.zero_of_cube (s : Set)
  requires sIn : s ∈ ℂ
  requires cube : ℂ[s * s * s] = ℂ[0]
  shows s = ℂ[0]
proof
  have alternatives : s = ℂ[0] ∨ s ≠ ℂ[0] by tauto
  cases alternatives with zero | nonzero
  . exact zero
  . have squareIn : ℂ[s * s] ∈ ℂ by typecheck
    have squareNonzero := complex.mul_nonzero with sIn, sIn, nonzero, nonzero
    exact complex.zero_of_mul at ℂ[s * s], s with sIn, squareNonzero, cube

theorem complex.three_nonzero
  shows ℂ[3] ≠ ℂ[0]
proof
  have positive : 0 < 3 by arith
  exact complexNumeral.nonzero with positive

-- Cube roots and roots of monic cubics, from the fundamental theorem.
theorem complex.cube_root (w : Set)
  requires wIn : w ∈ ℂ
  shows ∃ s ∈ ℂ, ℂ[s * s * s] = w
proof
  have negIn : ℂ[-w] ∈ ℂ by typecheck
  have zeroIn := complexZero.member
  have nonempty := complexList.cons_nonempty at ℂ[-w], [ℂ[0], ℂ[0]] with negIn
  obtain ⟨s, sIn, root⟩ := complexPolynomial.has_root with nonempty
  have list : List(ℂ, [ℂ[-w], ℂ[0], ℂ[0]]) by typecheck
  have tail1 : List(ℂ, [ℂ[0], ℂ[0]]) by typecheck
  have tail2 : List(ℂ, [ℂ[0]]) by typecheck
  have empty : List(ℂ, []) by typecheck
  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.cons, hornerAt.nil] at root
  witness s
  constructor
  . exact sIn
  . linear_combination root

theorem cubic.root_exists (a b c : Set)
  requires aIn : a ∈ ℂ
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  shows ∃ x ∈ ℂ, ℂ[x * x * x + a * (x * x) + b * x + c] = ℂ[0]
proof
  have nonempty := complexList.cons_nonempty at c, [b, a] with cIn
  obtain ⟨x, xIn, root⟩ := complexPolynomial.has_root with nonempty
  have list : List(ℂ, [c, b, a]) by typecheck
  have tail1 : List(ℂ, [b, a]) by typecheck
  have tail2 : List(ℂ, [a]) by typecheck
  have empty : List(ℂ, []) by typecheck
  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.cons, hornerAt.nil] at root
  witness x
  constructor
  . exact xIn
  . linear_combination root

-- Cardano: s + t is a root of the depressed cubic when s³ + t³ = −q and
-- 3st = −p.
theorem cubic.cardano_root (p q s t : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  requires sIn : s ∈ ℂ
  requires tIn : t ∈ ℂ
  requires cubes : ℂ[s * s * s + t * t * t] = ℂ[-q]
  requires product : ℂ[3 * (s * t)] = ℂ[-p]
  shows ℂ[(s + t) * (s + t) * (s + t) + p * (s + t) + q] = ℂ[0]
proof
  linear_combination cubes + (s + t) * product

-- Such a pair exists: s is a cube root of a root of the resolvent quadratic
-- and t = −p/(3s), or p = 0 and t is a cube root of −q.
theorem cubic.cardano_pair (p q : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  shows ∃ s ∈ ℂ, ∃ t ∈ ℂ, ℂ[s * s * s + t * t * t] = ℂ[-q] ∧ ℂ[3 * (s * t)] = ℂ[-p]
proof
  have zeroIn := complexZero.member
  have three := complex.three_nonzero
  have threeIn : ℂ[3] ∈ ℂ by typecheck
  have nine := complex.mul_nonzero with threeIn, threeIn, three, three
  have nineIn : ℂ[3 * 3] ∈ ℂ by typecheck
  have twentySeven := complex.mul_nonzero with nineIn, threeIn, nine, three
  have twentySevenIn : ℂ[3 * 3 * 3] ∈ ℂ by typecheck
  have pCubeIn : ℂ[p * p * p] ∈ ℂ by typecheck
  have constantIn : ℂ[-(3 * 3 * 3 * (p * p * p))] ∈ ℂ by typecheck
  have linearIn : ℂ[3 * 3 * 3 * q] ∈ ℂ by typecheck
  obtain ⟨W, WIn, Wroot⟩ := complexPolynomial.quadratic_root at ℂ[-(3 * 3 * 3 * (p * p * p))], ℂ[3 * 3 * 3 * q] with constantIn, linearIn
  have list : List(ℂ, [ℂ[-(3 * 3 * 3 * (p * p * p))], ℂ[3 * 3 * 3 * q]]) by typecheck
  have tail : List(ℂ, [ℂ[3 * 3 * 3 * q]]) by typecheck
  have empty : List(ℂ, []) by typecheck
  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.nil] at Wroot
  have resolvent : ℂ[W * W + 3 * 3 * 3 * q * W + -(3 * 3 * 3 * (p * p * p))] = ℂ[0]
    linear_combination Wroot
  obtain ⟨S, SIn, Scube⟩ := complex.cube_root at W with WIn
  have alternatives : S = ℂ[0] ∨ S ≠ ℂ[0] by tauto
  cases alternatives with SZero | SNonzero
  . have WZero : W = ℂ[0]
      rw SZero at Scube
      have zeroCube : ℂ[0 * 0 * 0] = ℂ[0] by ring
      rw zeroCube at Scube
      symm at Scube
      exact Scube
    have scaled : ℂ[3 * 3 * 3 * (p * p * p)] = ℂ[0]
      rw WZero at resolvent
      linear_combination -resolvent
    have pCubeZero := complex.zero_of_mul at ℂ[3 * 3 * 3], ℂ[p * p * p] with twentySevenIn, pCubeIn, twentySeven, scaled
    have pZero := complex.zero_of_cube at p with pIn, pCubeZero
    have negQIn : ℂ[-q] ∈ ℂ by typecheck
    obtain ⟨T, TIn, Tcube⟩ := complex.cube_root at ℂ[-q] with negQIn
    witness ℂ[0]
    constructor
    . exact zeroIn
    . witness T
      constructor
      . exact TIn
      . constructor
        . linear_combination Tcube
        . rw pZero
          ring
  . obtain ⟨v, vIn, third⟩ := complex.inverse_exists at ℂ[3] with threeIn, three
    obtain ⟨u, uIn, unit⟩ := complex.inverse_exists at S with SIn, SNonzero
    have WNonzero : W ≠ ℂ[0]
      intro WZero
      rw WZero at Scube
      apply SNonzero
      exact complex.zero_of_cube with SIn, Scube
    have scaleNonzero := complex.mul_nonzero with twentySevenIn, WIn, twentySeven, WNonzero
    have scaleIn : ℂ[3 * 3 * 3 * W] ∈ ℂ by typecheck
    have sIn : ℂ[S * v] ∈ ℂ by typecheck
    have tIn : ℂ[-(p * u)] ∈ ℂ by typecheck
    have excessIn : ℂ[(S * v) * (S * v) * (S * v) + (-(p * u)) * (-(p * u)) * (-(p * u)) + q] ∈ ℂ by typecheck
    have key : ℂ[(3 * 3 * 3 * W) * ((S * v) * (S * v) * (S * v) + (-(p * u)) * (-(p * u)) * (-(p * u)) + q)] = ℂ[0]
      linear_combination resolvent + (ℂ[3 * 3 * 3 * W * (v * v * v) + 3 * 3 * 3 * (p * p * p) * (u * u * u)]) * Scube + (ℂ[W * W * ((3 * v) * (3 * v) + 3 * v + 1)]) * third + (ℂ[-(3 * 3 * 3 * (p * p * p)) * ((S * u) * (S * u) + S * u + 1)]) * unit
    have excessZero := complex.zero_of_mul at ℂ[3 * 3 * 3 * W], ℂ[(S * v) * (S * v) * (S * v) + (-(p * u)) * (-(p * u)) * (-(p * u)) + q] with scaleIn, excessIn, scaleNonzero, key
    witness ℂ[S * v]
    constructor
    . exact sIn
    . witness ℂ[-(p * u)]
      constructor
      . exact tIn
      . constructor
        . linear_combination excessZero
        . linear_combination (-(p * (S * u))) * third + (-p) * unit

-- Every depressed cubic has a root of Cardano's form.
theorem cubic.depressed_solution (p q : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  shows ∃ x ∈ ℂ, ℂ[x * x * x + p * x + q] = ℂ[0] ∧ ∃ s ∈ ℂ, ∃ t ∈ ℂ, x = ℂ[s + t] ∧ ℂ[s * s * s + t * t * t] = ℂ[-q] ∧ ℂ[3 * (s * t)] = ℂ[-p]
proof
  obtain ⟨s, sIn, t, tIn, cubes, product⟩ := cubic.cardano_pair with pIn, qIn
  have root := cubic.cardano_root with pIn, qIn, sIn, tIn, cubes, product
  have sumIn : ℂ[s + t] ∈ ℂ by typecheck
  witness ℂ[s + t]
  constructor
  . exact sumIn
  . constructor
    . exact root
    . witness s
      constructor
      . exact sIn
      . witness t
        constructor
        . exact tIn
        . exact ⟨rfl, ⟨cubes, product⟩⟩

-- The shift x = y − a·v with 3v = 1 depresses a monic cubic.
theorem cubic.depress (a b c v y : Set)
  requires aIn : a ∈ ℂ
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  requires vIn : v ∈ ℂ
  requires yIn : y ∈ ℂ
  requires third : ℂ[3 * v] = ℂ[1]
  shows ℂ[(y + -(a * v)) * (y + -(a * v)) * (y + -(a * v)) + a * ((y + -(a * v)) * (y + -(a * v))) + b * (y + -(a * v)) + c] = ℂ[y * y * y + (b + -(a * a * v)) * y + (c + -(a * b * v) + 2 * (a * a * a * (v * v * v)))]
proof
  linear_combination (-(a * y * y) + a * a * v * y + -(a * a * a * v * v)) * third

-- Cardano's solution of the general monic cubic.
theorem cubic.solution (a b c : Set)
  requires aIn : a ∈ ℂ
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  shows ∃ x ∈ ℂ, ℂ[x * x * x + a * (x * x) + b * x + c] = ℂ[0] ∧ ∃ v ∈ ℂ, ∃ y ∈ ℂ, ℂ[3 * v] = ℂ[1] ∧ x = ℂ[y + -(a * v)] ∧ ∃ s ∈ ℂ, ∃ t ∈ ℂ, y = ℂ[s + t] ∧ ℂ[s * s * s + t * t * t] = ℂ[-(c + -(a * b * v) + 2 * (a * a * a * (v * v * v)))] ∧ ℂ[3 * (s * t)] = ℂ[-(b + -(a * a * v))]
proof
  have three := complex.three_nonzero
  obtain ⟨v, vIn, third⟩ := complex.inverse_exists with three
  have linearIn : ℂ[b + -(a * a * v)] ∈ ℂ by typecheck
  have constantIn : ℂ[c + -(a * b * v) + 2 * (a * a * a * (v * v * v))] ∈ ℂ by typecheck
  obtain ⟨y, yIn, root, s, sIn, t, tIn, shape, cubes, product⟩ := cubic.depressed_solution with
    linearIn, constantIn
  have identity := cubic.depress with aIn, bIn, cIn, vIn, yIn, third
  have xIn : ℂ[y + -(a * v)] ∈ ℂ by typecheck
  witness ℂ[y + -(a * v)]
  constructor
  . exact xIn
  . constructor
    . rw identity
      exact root
    . witness v
      constructor
      . exact vIn
      . witness y
        constructor
        . exact yIn
        . constructor
          . exact third
          . constructor
            . rfl
            . witness s
              constructor
              . exact sIn
              . witness t
                constructor
                . exact tIn
                . exact ⟨shape, ⟨cubes, product⟩⟩

end Complexes