\import Algebra.Field
\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Local
\import Algebra.Semiring
\import Arith.Real
\import Function.Meta
\import Logic
\import Meta
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Arith.Real.Field
\open Complex \using (iunit \as i)

\record Complex (re im : Real)
  \where {
    \use \coerce fromReal (x : Real) : Complex => \new Complex x 0

    {- | The imaginary unit $iunit = 0 + i \in \mathbb{C}$. -}
    \func iunit => \new Complex 0 1

    -- | $i^2 = -1$ in $\mathbb{C}$.
    \lemma iunit-square : i ComplexField.* i = ComplexField.negative ComplexField.ide
      => ext (pmap2 (-) zro_*-left ide-left *> zro-left,
              pmap2 (+) zro_*-left zro_*-right *> zro-left *> inv RealAbGroup.negative_zro)

    -- | $i^2 = -1$.
    \lemma pow-iunit-2 : Monoid.pow {ComplexField} i 2 = ComplexField.negative ComplexField.ide
      => pmap (ComplexField.* i) ComplexField.ide-left *> iunit-square

    -- | $i^{2k} = (-1)^k$.
    \lemma pow-iunit-even (k : Nat) : Monoid.pow i (2 Nat.* k) = Monoid.pow (ComplexField.negative ComplexField.ide) k
      => ComplexField.pow_* *> pmap (Monoid.pow __ k) pow-iunit-2

    -- | $i^{2k+1} = (-1)^k\,i$.
    \lemma pow-iunit-odd (k : Nat)
      : ComplexField.pow i (2 Nat.* k Nat.+ 1) = Monoid.pow (ComplexField.negative ComplexField.ide) k ComplexField.* i
      => pmap (ComplexField.* i) (pow-iunit-even k)

    {- | $\mathrm{fromReal}$ preserves addition:
         $\mathrm{fromReal}\,(x + y) = \mathrm{fromReal}\ x + \mathrm{fromReal}\ y$. -}
    \lemma fromReal_+ {x y : Real} : fromReal (x + y) = fromReal x ComplexField.+ fromReal y
      => ext (idp, inv zro-left)

    {- | $\mathrm{fromReal}$ preserves multiplication:
         $\mathrm{fromReal}\,(xy) = \mathrm{fromReal}\ x \cdot \mathrm{fromReal}\ y$. -}
    \lemma fromReal_* {x y : Real} : fromReal (x * y) = fromReal x ComplexField.* fromReal y
      => ext (simplify, simplify)

    {- | $\mathrm{fromReal}$ preserves negation:
         $\mathrm{fromReal}\,(-x) = -\mathrm{fromReal}\ x$. -}
    \lemma fromReal_negative {x : Real} : fromReal (negative x) = ComplexField.negative (fromReal x)
      => ext (idp, inv RealAbGroup.negative_zro)

    -- | The embedding $\mathbb{R} \to \mathbb{C}$ commutes with $n$-th powers.
    \lemma fromReal_pow {x : Real} {n : Nat}
      : Complex.fromReal (RealField.pow x n) = ComplexField.pow (Complex.fromReal x) n \elim n
      | 0 => idp
      | suc n => fromReal_* *> pmap (ComplexField.* _) fromReal_pow
  }

\instance ComplexField : Field Complex
  | zro => \new Complex 0 0
  | + (x y : Complex) => \new Complex (x.re + y.re) (x.im + y.im)
  | zro-left => ext (zro-left, zro-left)
  | +-assoc => ext (+-assoc, +-assoc)
  | +-comm => ext (+-comm, +-comm)
  | CMonoid => ComplexMonoid
  | ldistr => ext (equation.ring, equation.ring)
  | negative x => \new Complex (negative x.re) (negative x.im)
  | negative-left => ext (negative-left, negative-left)
  | zro/=ide p => zro/=ide $ pmap (\lam (x : Complex) => x.re) p
  | locality x => \case locality x.re \with {
    | byLeft r => byLeft $ inv-char.2 $ byLeft r
    | byRight r => byRight $ inv-char.2 $ byLeft r
  }
  | #0-tight c => ext (AddGroup.#0-tight \lam p => c $ inv-char.2 $ byLeft p, AddGroup.#0-tight \lam p => c $ inv-char.2 $ byRight p)
  \where {
    \open Monoid(Inv)

    \private \instance ComplexMonoid : CMonoid Complex
      | ide => \new Complex 1 0
      | * (x y : Complex) => \new Complex (x.re * y.re - x.im * y.im) (x.re * y.im + x.im * y.re)
      | ide-left => ext (simplify, simplify)
      | *-assoc => ext (equation.ring, equation.ring)
      | *-comm => ext (pmap2 (__ - __) *-comm *-comm, +-comm *> pmap2 (+) *-comm *-comm)

    \lemma inv-char {x : Complex} : Inv x <-> Inv x.re || Inv x.im
      => (\lam p => \case RealField.sum1=>eitherInv {_} {negative _} $ pmap (\lam (x : Complex) => x.re) (Inv.inv-left {p}) \with {
                      | byLeft r => byLeft (Inv.cfactor-right r)
                      | byRight r => byRight $ Inv.cfactor-right $ transportInv Inv Ring.negative_*-left r
                    },
          \lam p => \have d : Inv (x.re * x.re + x.im * x.im) => RealField.positive=>#0 $ RealField.>0_pos {x.re * x.re + x.im * x.im} (transport (0 <) linarith $ RealField.sum_squares_>0 {x.re,x.im} \case \elim p \with {
                      | byLeft r => inP (0, ||.map real_<_L.2 (\lam c => real_<_U.2 $ RealAbGroup.negative_L.1 c) $ RealField.#0=>eitherPosOrNeg r)
                      | byRight r => inP (1, ||.map real_<_L.2 (\lam c => real_<_U.2 $ RealAbGroup.negative_L.1 c) $ RealField.#0=>eitherPosOrNeg r)
                    })
                    \in Inv.lmake (\new Complex (x.re * d.inv) (negative (x.im * d.inv))) $ ext (equation.cRing {d.inv-left}, equation.cRing))
  }

-- | Complex conjugation $\overline{a + bi} := a - bi$.
\func conj (z : Complex) : Complex => \new Complex z.re (negative z.im)

-- | $\overline{\overline{z}} = z$ — {conj} is its own inverse.
\lemma conj_conj {z : Complex} : conj (conj z) = z
  => ext (idp, AddGroup.negative-isInv)

-- | $\overline{0} = 0$.
\lemma conj_zro : conj 0 = (0 : Complex)
  => ext (idp, RealAbGroup.negative_zro)

-- | $\overline{1} = 1$.
\lemma conj_ide : conj 1 = (1 : Complex)
  => ext (idp, RealAbGroup.negative_zro)

-- | $\overline{x + y} = \overline{x} + \overline{y}$ — {conj} preserves addition.
\lemma conj_+ {x y : Complex} : conj (x + y) = conj x + conj y
  => ext (idp, RealAbGroup.negative_+ *> +-comm)

-- | $\overline{xy} = \overline{x} \cdot \overline{y}$ — {conj} preserves multiplication.
\lemma conj_* {x y : Complex} : conj (x * y) = conj x * conj y
  => ext (simplify, equation.ring)

-- | $\overline{i} = -i$.
\lemma conj_i : conj i = negative i
  => ext (inv RealAbGroup.negative_zro, idp)

-- | $\overline{i x} = - i x$.
\lemma conj_i_* {x : Real} : conj (i * x) = negative (i * x)
  => conj_* *> pmap2 (*) conj_i conj_fromReal *> Ring.negative_*-left

-- | $\overline{\mathrm{fromReal}\ x} = \mathrm{fromReal}\ x$ — {conj} fixes the real-line embedding.
\lemma conj_fromReal {x : Real} : conj x = Complex.fromReal x
  => ext RealAbGroup.negative_zro

-- | $\overline{z^n} = (\overline{z})^n$ — {conj} commutes with monoid powers.
\lemma conj_pow {z : Complex} (n : Nat) : conj (Monoid.pow z n) = Monoid.pow (conj z) n \elim n
  | 0 => conj_ide
  | suc n => conj_* *> pmap (* conj z) (conj_pow n)

-- | {conj} as an additive-group endomorphism of $\mathbb{C}$.
\func conjAddHom : AddGroupHom ComplexField ComplexField \cowith
  | func => conj
  | func-+ => conj_+