\import Algebra.Domain.Euclidean
\import Algebra.Domain.GCD
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Monoid.GCD
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Ring.Local
\import Data.Or
\import Equiv
\import Function.Meta ($)
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set
\open Monoid(Inv)

-- | A field is a commutative local ring such that non-invertible elements equal to {zro}.
\class Field \extends LocalCRing, GCDDomain
  | #0 x => Inv x
  | #0-+ => LocalRing.sumInv=>eitherInv
  | #0-zro (j : Inv zro) => zro/=ide (inv zro_*-right *> j.inv-left)
  | #0-*-left => Inv.cfactor-left
  | zro#ide => Inv.lmake ide ide-left
  | #0-* xj yj => Inv.product xj yj

  | isGCDDomain x y x#0 y#0 => inP \new GCD {
    | gcd => 1
    | gcd|val1 => \new Monoid.LDiv {
      | inv => x
      | inv-right => ide-left
    }
    | gcd|val2 => \new Monoid.LDiv {
      | inv => y
      | inv-right => ide-left
    }
    | gcd-univ g g|x g|y => \new Monoid.LDiv {
      | inv => Monoid.LDiv.inv {g|x} * Inv.inv {x#0}
      | inv-right => inv *-assoc *> pmap (`* _) Monoid.LDiv.inv-right *> Inv.inv-right
    }
  }

-- | A discrete field is a commutative ring such that every element is either {zro} or invertible.
\class DiscreteField \extends Field, EuclideanDomain {
  | finv : E -> E
  | finv_zro : finv 0 = 0
  | finv-right {x : E} (x/=0 : x /= 0) : x * finv x = 1
  \field eitherZeroOrInv (x : E) : (x = 0) || Inv x

  | isEuclidean => inP \new EuclideanRingData {
    | euclideanMap x => 0
    | divMod x y => \case decideEq y 0 \with {
      | yes _ => (0, x)
      | no _ => (finv y * x, 0)
    }
    | isDivMod x y => mcases \with {
      | yes _ => equation
      | no q => zro-right *> inv *-assoc *> rewrite (finv-right q) ide-left
    }
    | isEuclideanMap x y y/=0 => mcases {1} \with {
      | yes y=0 => absurd (y/=0 y=0)
      | no _ => \lam p => absurd (p idp)
    }
  }

  \default finv \as finv-impl x => \case aux zro/=ide x (eitherZeroOrInv x) \with {
    | inl _ => 0
    | inr (j : Inv) => j.inv
  }
  \default finv_zro \as finv_zroImpl : finv-impl 0 = 0 => unfold finv-impl (mcases \with {
    | inl _ => idp
    | inr (j : Inv) => absurd (zro/=ide (inv zro_*-left *> j.inv-right))
  })
  \default finv-right \as id_finvImpl {x} x/=0 : x * finv-impl x = 1 => unfold finv-impl (mcases \with {
    | inl x=0 => absurd (x/=0 x=0)
    | inr (j : Inv) => j.inv-right
  })
  \default eitherZeroOrInv x => \case decideEq x 0 \with {
    | yes x=0 => byLeft x=0
    | no x/=0 => byRight (Inv.rmake (finv x) (finv-right x/=0))
  }

  | locality x => \case eitherZeroOrInv x \with {
    | byLeft x=0 => byRight (Inv.lmake ide equation)
    | byRight xInv => byLeft xInv
  }
  \default decideEq x y => \case eitherZeroOrInv (x - y) \with {
    | byLeft x-y=0 => yes (fromZero x-y=0)
    | byRight x-y-isInv => no \lam x=y => #-irreflexive (rewrite x=y in x-y-isInv)
  }
  | nonZeroApart {x} x/=0 => \case eitherZeroOrInv x \with {
    | byLeft x=0 => absurd (x/=0 x=0)
    | byRight x#0 => x#0
  }

  \lemma finv-left {x : E} (x/=0 : x /= 0) : finv x * x = 1
    => *-comm *> finv-right x/=0

  \lemma finv-Inv {x : E} (x/=0 : x /= 0) : Inv (finv x) x
    => Inv.lmake x (finv-right x/=0)

  \lemma nonZero-Inv {x : E} (x/=0 : x /= 0) : Inv x (finv x)
    => Inv.rmake (finv x) (finv-right x/=0)

  \lemma finv/=0 {x : E} (x/=0 : x /= 0) : finv x /= 0
    => inv-nonZero (finv-Inv x/=0)

  \lemma finv_* {x y : E} : finv (x * y) = finv y * finv x
    => \case decideEq x 0, decideEq y 0 \with {
      | yes x=0, _ => rewrite (x=0,zro_*-left,finv_zro) (inv zro_*-right)
      | _, yes y=0 => rewrite (y=0,zro_*-right,finv_zro) (inv zro_*-left)
      | no x/=0, no y/=0 => Inv.inv-isUnique (nonZero-Inv (nonZero_* x/=0 y/=0))
          (Inv.lmake (finv y * finv x) (equation {usingOnly (finv-left x/=0, finv-left y/=0)})) idp
    }

  \lemma finv_finv {x : E} : finv (finv x) = x
    => \case decideEq x 0 \with {
      | yes x=0 => rewrite (x=0,finv_zro) finv_zro
      | no x/=0 => Inv.inv-isUnique (nonZero-Inv (finv/=0 x/=0)) (Inv.lmake x (finv-right x/=0)) idp
    }

  \lemma zeroDimensional : IsZeroDimensional
    => \lam a => \case eitherZeroOrInv a \with {
      | byLeft a=0 => inP (0, 1, rewrite a=0 simplify)
      | byRight (r : Inv) => inP (r.inv, 0, simplify $ inv r.inv-right)
    }

  \lemma decideZeroOrInv (x : E) : (x = 0) `Or` Inv x
    => aux zro/=ide x (eitherZeroOrInv x)

  \lemma finv-diff {x : E} (xi : x /= 0) (x+1i : x + 1 /= 0) : finv x - finv (x + 1) = finv (x * (x + 1))
    => equation {usingOnly (finv-right xi, finv-right x+1i, finv-right $ nonZero_* xi x+1i)}
} \where {
  \private \lemma aux {R : CRing} (p : zro /= {R} ide) (x : R) (q : (x = 0) || Inv x) : (x = 0) `Or` Inv x
    \level Or.levelProp (\lam x=0 (j : Inv x) => p $ inv zro_*-left *> pmap (`* _) (inv x=0) *> j.inv-right)
    => \case q \with {
         | byLeft r => inl r
         | byRight r => inr r
       }

  \func backwards (f : RingHom) (e : Equiv f) (D : DiscreteField { | Ring => f.Cod }) : DiscreteField { | Ring => f.Dom } \cowith
    | *-comm => e.isInj $ f.func-* *> *-comm *> inv f.func-*
    | zro/=ide q => D.zro/=ide $ inv f.func-zro *> pmap f q *> f.func-ide
    | eitherZeroOrInv a => ||.map (\lam q => e.isInj $ q *> inv f.func-zro) (\lam (fai : Inv (f a)) => \new Inv a {
      | inv => e.ret fai.inv
      | inv-left => e.isInj $ f.func-* *> pmap (`* _) (e.f_ret _) *> fai.inv-left *> inv f.func-ide
      | inv-right => e.isInj $ f.func-* *> pmap (_ *) (e.f_ret _) *> fai.inv-right *> inv f.func-ide
    }) (D.eitherZeroOrInv (f a))

  \func forward {f : RingHom} (e : Equiv f) (D : DiscreteField { | Ring => f.Dom }) : DiscreteField { | Ring => f.Cod }
    => backwards (\new RingHom f.Cod f.Dom e.ret {
      | func-+ => e.isInj $ e.f_ret _ *> inv (f.func-+ *> pmap2 (+) (e.f_ret _) (e.f_ret _))
      | func-ide => e.isInj $ e.f_ret _ *> inv f.func-ide
      | func-* => e.isInj $ e.f_ret _ *> inv (f.func-* *> pmap2 (*) (e.f_ret _) (e.f_ret _))
    }) (symQEquiv e) D
}