{- | Some of the definitions and proofs are taken from
     [] Coquand, Spitters, Constructive Gelfand Duality for C*-algebras, 2009, https://arxiv.org/abs/0808.1518
 -}

\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.QModule
\import Algebra.Ring
\import Analysis.FuncLimit
\import Analysis.Limit
\import Arith.Nat
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.Root \using (sqrt \as sqrtR)
\import Arith.Real.UpperReal
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Biordered
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.BanachSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.CompletionTools
\import Topology.CoverSpace.Product
\import Topology.MetricSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.ExComplete
\import Topology.NormedAbGroup.Real
\import Topology.NormedAbGroup.Real.Functions
\import Topology.NormedRing
\import Topology.TopAbGroup.Complete
\import Topology.TopAbGroup.Product
\import Topology.TopSpace
\import Topology.TopSpace.Product

\class BanachAlgebra \extends BanachSpace, QAlgebra, CompleteExNormedRing {
  \func fromRat (q : Rat) => q *q 
}

\class RealPreBanachAlgebra \extends RealPreBanachSpace, ExPseudoNormedRing

\class RealBanachPseudoAlgebra \extends RealBanachSpace, QPseudoAlgebra, ExPseudoNormedPseudoRing, CompleteExNormedAbGroup {
  \lemma *r-comm-left {r : Real} {a b : E} : r *r (a * b) = r *r a * b
    => dense-lift-unique rat_real rat_real.dense-coverEmbedding. (*r-cover ∘ tuple id (const _)) (*-locally-uniform ∘ tuple (*r-cover ∘ tuple id (const a)) (const b)) (\lam x => *r_*q *> *q-comm-left *> pmap (`* b) (inv *r_*q)) r

  \lemma *r-comm-right {r : Real} {a b : E} : r *r (a * b) = a * (r *r b)
    => dense-lift-unique rat_real rat_real.dense-coverEmbedding. (*r-cover ∘ tuple id (const _)) (*-locally-uniform ∘ tuple (const a) (*r-cover ∘ tuple id (const b))) (\lam x => *r_*q *> *q-comm-right *> pmap (a *) (inv *r_*q)) r

  \lemma *r_>=0-square {r : Real} {a : E} (r>=0 :  <= r) (as : IsSquare a) : IsSquare (r *r a) \elim as
    | inP (b,bb=a) => inP (sqrtR r *r b, inv *r-comm-left *> pmap (_ *r) (inv *r-comm-right) *> inv toRealModule.*c-assoc *> pmap2 (*r) (pow_sqrt r>=0) bb=a)

  \lemma *q_>=0-square {q : Rat} {a : E} (q>=0 :  <= q) (as : IsSquare a) : IsSquare (q *q a)
    => transport IsSquare *r_*q $ *r_>=0-square (rat_real_<=. q>=0) as

  \func toRealAlgebra : PseudoAlgebra RealField \cowith
    | LModule => toRealModule
    | PseudoRing => \this
    | *c-comm-left => *r-comm-left
    | *c-comm-right => *r-comm-right
} \where {
  \open CoverMap
  \open ProductCoverSpace
}

\class RealBanachAlgebra \extends RealBanachPseudoAlgebra, BanachAlgebra, RealPreBanachAlgebra {
  -- | [] Lemma 1
  \sfunc sqrt (x : E) (|1-x|<=1 : norm ( - x) ExUpperReal.<= RatField.ide) : E
    => zfunc-lim (x,|1-x|<=1)
    \where \protected {
      \func UnitBall => ExPseudoMetricTransfer {Set.Total \lam x => norm ( - x) ExUpperReal.<= RatField.ide} __.

      \sfunc yfunc (n : Nat) (x : E) : E \elim n
        |  => 
        | suc n => ratio   *q ( - x + yfunc n x * yfunc n x)

      \lemma yfunc<=rfunc {n : Nat} {s : UnitBall} : norm (yfunc n s.) <= rfunc n \elim n
        |  => rewrite (\peval yfunc  s., \peval rfunc , norm_zro) <=-refl
        | suc n => rewrite (\peval yfunc (suc n) s., \peval rfunc (suc n), norm_*q, inv $ ExUpperReal.*-rat rat_<=-dec $ RatField.<=_+-positive rat_<=-dec $ RatField.<=_*-positive rfunc>=0 rfunc>=0) $
          ExUpperRealSemigroup.<=_* (ExUpperReal.<=-rat. rat_<=-dec) $ transport (_ <=) ExUpperReal.+-rat $ norm_+ <=∘ ExUpperRealAbMonoid.<=_+ s. (transport (_ <=) (ExUpperReal.*-rat rfunc>=0 rfunc>=0) $ norm_*_<= <=∘ ExUpperRealSemigroup.<=_* yfunc<=rfunc yfunc<=rfunc)

      \lemma yfunc-comm {a x : E} (p : a * x = x * a) {n : Nat} : yfunc n x * a = a * yfunc n x \elim n
        |  => pmap (`* a) (\peval yfunc  x) *> zro_*-left *> inv (pmap (a *) (\peval yfunc  x) *> zro_*-right)
        | suc n => pmap (`* _) (\peval yfunc (suc n) x) *> inv *q-comm-left *> pmap (_ *q) (rdistr *> pmap2 (+) (rdistr_- *> pmap2 (-) (ide-left *> inv ide-right) (inv p) *> inv ldistr_-) (*-assoc *> pmap (_ *) (yfunc-comm p) *> inv *-assoc *> pmap (`* _) (yfunc-comm p) *> *-assoc) *> inv ldistr) *> *q-comm-right *> inv (pmap (_ *) (\peval yfunc (suc n) x))

      \lemma yfunc-rec {n : Nat} {x : E} : yfunc (suc (suc n)) x - yfunc (suc n) x = ratio   *q ((yfunc (suc n) x + yfunc n x) * (yfunc (suc n) x - yfunc n x))
        => pmap2 (-) (\peval yfunc (suc (suc n)) x) (\peval yfunc (suc n) x) *> inv toRatModule.*c-ldistr_- *> pmap (_ *q) (simplify $ inv $ *_sum_diff $ yfunc-comm $ yfunc-comm idp)

      \lemma yfunc_rfunc-diff1 {n : Nat} {s : UnitBall} : norm (yfunc (suc n) s. - yfunc n s.) <= rfunc (suc n) - rfunc n \elim n
        |  => rewrite (\peval yfunc  s., \peval rfunc ) (simplify yfunc<=rfunc)
        | suc n => rewrite (yfunc-rec, rfunc-rec, norm_*q, inv $ ExUpperReal.*-rat rat_<=-dec $ RatField.<=_*-positive (RatField.<=_+-positive rfunc>=0 rfunc>=0) (RatField.to>=0 rfunc-inc), inv $ ExUpperReal.*-rat (RatField.<=_+-positive rfunc>=0 rfunc>=0) (RatField.to>=0 rfunc-inc), inv ExUpperReal.+-rat) $ ExUpperRealSemigroup.<=_* <=-refl $ norm_*_<= <=∘ ExUpperRealSemigroup.<=_* (norm_+ <=∘ ExUpperRealAbMonoid.<=_+ yfunc<=rfunc yfunc<=rfunc) yfunc_rfunc-diff1

      \lemma yfunc_rfunc-diff {n k : Nat} {s : UnitBall} : norm (yfunc (n Nat.+ k) s. - yfunc n s.) <= rfunc (n Nat.+ k) - rfunc n \elim k
        |  => simplify $ rewrite norm_zro <=-refl
        | suc k => transport2 (norm __ <= __) {yfunc (suc (n Nat.+ k)) s. - yfunc (n Nat.+ k) s. + (yfunc (n Nat.+ k) s. - yfunc n s.)} {_} {rfunc (suc (n Nat.+ k)) - rfunc (n Nat.+ k) RatField.+ (rfunc (n Nat.+ k) - rfunc n)} simplify simplify $ norm_+ <=∘ transport (_ <=) ExUpperReal.+-rat (ExUpperRealAbMonoid.<=_+ yfunc_rfunc-diff1 yfunc_rfunc-diff)

      \func zfunc (n : Nat) (x : E) =>  - yfunc n x

      \lemma zfunc-comm {a x : E} (p : a * x = x * a) {n : Nat} : zfunc n x * a = a * zfunc n x
        => rdistr_- *> pmap2 (-) (ide-left *> inv ide-right) (yfunc-comm p) *> inv ldistr_-

      \lemma zfunc_rfunc-diff {n k : Nat} (n<=k : n <= k) {s : UnitBall} : norm (zfunc k s. - zfunc n s.) <= rfunc k - rfunc n
        => transport (ExUpperReal.`<= _) norm_negative $ simplify $ rewrite (+-comm, inv $ <=_exists n<=k) yfunc_rfunc-diff

      \lemma zfunc-uni : IsUniFuncConvergent {_} {UnitBall} \lam n s => zfunc n s.
        => metric-uni-funcConvergent. \lam eps>0 => \case convergent-metric-char. (limit-conv rfunc-limit) eps>0 \with {
          | inP (N,g) => inP (N, \lam s p => rewrite norm-dist $ zfunc_rfunc-diff p $ RatField.abs>=id <∘r g p)
        }

      \lemma yfunc-cover (n : Nat) : CoverMap \this \this (yfunc n) \elim n
        |  => transportInv (CoverMap \this \this) (ext \lam x => \peval yfunc  x) (CoverMap.const )
        | suc n => transportInv (CoverMap \this \this) (path \lam i x => (\peval yfunc (suc n) x) i) $ *q-right-uniform ∘ +-uniform ∘ tuple (subtract-uniform ∘ tuple (const ) id) (*-locally-uniform ∘ tuple (yfunc-cover n) (yfunc-cover n))

      \lemma zfunc-cover (n : Nat) : CoverMap UnitBall \this \lam s => zfunc n s.
        => subtract-uniform ∘ tuple (const ) (yfunc-cover n) ∘ CoverTransfer-map __.

      \lemma zfunc-funcConv : IsFuncConvergent {_} {UnitBall} \lam n s => zfunc n s.
        => funcCovergent-uni zfunc-cover zfunc-uni

      \func zfunc-lim => funcLimit {_} {UnitBall} (\lam n s => zfunc n s.) zfunc-funcConv

      \lemma isSquare : sqrt x |1-x|<=1 * sqrt x |1-x|<=1 = x
        => pmap2 (*) (\peval sqrt _ _) (\peval sqrt _ _) *> limit-unique (cont2-limit limit-isLimit limit-isLimit *-cont)
            (limit-metric-char. \lam eps>0 => \case convergent-metric-char.double (limit-conv rfunc-limit) (RatField.half>0 eps>0) \with {
              | inP (N,h) => inP (N, \lam {n} N<=n => rewrite (dist-symm, norm-dist, dist-lem n, norm_*q) $ ExUpperRealSemigroup.<=_* <=-refl (yfunc_rfunc-diff1 {_} {_} {x,|1-x|<=1}) $ rewrite (ExUpperReal.*-rat rat_<=-dec $ RatField.to>=0 rfunc-inc) $ transport (`< _) RatField.*-comm $ RatField.<_rotate-right-conv rat_<-dec $ RatField.abs>=id <∘r h (N<=n <=∘ id<=suc) N<=n)
            })
        \where {
          \lemma dist-lem (n : Nat) : zfunc n x * zfunc n x - x = RatField.natCoef  *q (yfunc (suc n) x - yfunc n x)
            => rewrite (\peval yfunc (suc n) x, toRatModule.*c-ldistr_-, inv *q-assoc, ide_*q, toRatModule.*c-rdistr {RatField.ide} {RatField.ide}, ide_*q) equation.ring
        }

      \lemma comm {y : E} (yx=xy : y * x = x * y) : sqrt x |1-x|<=1 * y = y * sqrt x |1-x|<=1
        => rewrite (\peval sqrt x _) $ limit-apply (*-locally-uniform ∘ tuple id (const y)) *> limit-ext (zfunc __ x * y) (y * zfunc __ x) (\lam i => zfunc-comm yx=xy) *> inv (limit-apply (*-locally-uniform ∘ tuple (const y) id))
    }

  \lemma norm-square {x : E} (p : norm ( - x) <= RatField.ide) : IsSquare x
    => inP (sqrt x p, sqrt.isSquare)

  \lemma norm-square' {x : E} (p : norm x <= RatField.ide) : IsSquare ( - x)
    => norm-square (simplify p)

  \lemma norm_*q-square {q : Rat} (q>0 :  < q) {x : E} (p : norm (q *q  - x) <= q) : IsSquare x
    => \let s => sqrt (RatField.finv q *q x) $ transport2 (ExUpperReal.<=) (inv (norm_*q-ofPos $ <=-less $ RatField.finv>0 q>0) *> pmap norm (toRatModule.*c-ldistr_- *> pmap (`- _) (inv *q-assoc *> pmap (`*q _) (RatField.finv-left $ RatField.>_/= q>0) *> ide_*q))) (ExUpperReal.*-rat (<=-less $ RatField.finv>0 q>0) (<=-less q>0) *> pmap ExUpperReal.fromRat (RatField.finv-left $ RatField.>_/= q>0)) (ExUpperRealSemigroup.<=_* ExUpperRealAbMonoid.<=-refl p)
       \in inP (sqrtR q *r s, inv *r-comm-left *> pmap (_ *r) (inv *r-comm-right) *> inv toRealAlgebra.*c-assoc *> pmap2 (*r) (pow_sqrt $ rat_real_<=. $ <=-less q>0) sqrt.isSquare *> *r_*q *> inv *q-assoc *> pmap (`*q x) (RatField.finv-right $ RatField.>_/= q>0) *> ide_*q)
} \where \protected {
  \open CoverMap
  \open ProductCoverSpace

  \sfunc rfunc (n : Nat) : Rat \elim n
    |  => 
    | suc n => ratio   * ( + rfunc n * rfunc n)

  \lemma rfunc>=0 {n : Nat} :  <= rfunc n \elim n
    |  => rewrite (\peval rfunc ) <=-refl
    | suc n => rewrite (\peval rfunc (suc n)) $ RatField.<=_*-positive rat_<=-dec $ RatField.<=_+-positive rat_<=-dec $ RatField.<=_*-positive rfunc>=0 rfunc>=0

  \lemma rfunc<=1 {n : Nat} : rfunc n <=  \elim n
    |  => rewrite (\peval rfunc ) rat_<=-dec
    | suc n => rewrite (\peval rfunc (suc n)) $ RatField.<=_*_positive-right rat_<=-dec $ RatField.<=_+ <=-refl $ RatField.<=_*_positive-left rfunc<=1 rfunc>=0 <=∘ =_<= ide-left <=∘ rfunc<=1

  \lemma rfunc-inc {n : Nat} : rfunc n <= rfunc (suc n) \elim n
    |  => rewrite (\peval rfunc ) rfunc>=0
    | suc n => rewrite (\peval rfunc (suc (suc n))) $ RatField.from>=0 $ transport ( <=) {ratio   * (( - rfunc (suc n)) * ( - rfunc (suc n)))}
      (later $ rewrite (RatField.ldistr_-, RatField.rdistr_-, RatField.rdistr_-) linarith) -- TODO: equation.ring should work here, but it doesn't support rational coefficients yet
      $ RatField.<=_*-positive rat_<=-dec RatField.square_>=0

  \lemma rfunc-rec {n : Nat} : rfunc (suc (suc n)) - rfunc (suc n) = ratio   * ((rfunc (suc n) + rfunc n) * (rfunc (suc n) - rfunc n))
    => rewrite (\peval rfunc (suc (suc n)), \peval rfunc (suc n)) equation.cRing

  \lemma rfunc-bound {eps : Rat} (eps>0 :  < eps) {n : Nat} (p : rfunc n <=  - eps) :  - rfunc n <= RatField.pow ( - ratio   * eps) n \elim n
    |  => rewrite (\peval rfunc ) <=-refl
    | suc n => transportInv (`<= _) {_} {( - rfunc n) * (ratio   * ( + rfunc n))} (pmap ( -) (\peval rfunc (suc n)) *> equation.cRing idp) (RatField.<=_*_positive-right (linarith $ rfunc<=1 {n}) (linarith $ rfunc-inc <=∘ p)) <=∘ RatField.<=_*_positive-left (rfunc-bound eps>0 $ rfunc-inc <=∘ p) (linarith rfunc>=0)

  \lemma rfunc-limit : TopSpace.IsLimit rfunc 
    => limit-metric-char. \lam {eps} eps>0 =>
      \have B => rat_<1_pow-bound { - ratio   * eps} linarith eps>0
      \in inP (B., \lam {n} B<=n => transportInv (`< _) (RatField.abs-ofPos $ linarith rfunc<=1) \case LinearOrder.dec<_<= ( - rfunc n) eps \with {
        | inl r => r
        | inr r => rfunc-bound eps>0 linarith <∘r RatField.pow_<=-degree (linarith rfunc>=0) linarith B<=n <∘r B.
      })
}

\instance BanachAlgebraCompletion (X : RealPreBanachAlgebra) : RealBanachAlgebra
  | BanachSpace => BanachCompletion X
  | * => *-func
  | *-assoc => unique3 (*-cover ∘ prod *-cover id) (*-cover ∘ tuple (proj1 ∘ proj1) (*-cover ∘ prod proj2 id))
      \lam x y z => pmap (*-func __ _) lift2-char *> lift2-char *> pmap pointCF *-assoc *> inv (pmap (*-func _) lift2-char *> lift2-char)
  | ldistr => unique3 (*-cover ∘ tuple (proj1 ∘ proj1) (+-cover ∘ prod proj2 id)) (+-cover ∘ tuple (*-cover ∘ proj1) (*-cover ∘ tuple (proj1 ∘ proj1) proj2))
      \lam x y z => pmap (*-func _) +-char *> lift2-char *> pmap pointCF X.ldistr *> inv (pmap2 +-func lift2-char lift2-char *> +-char)
  | rdistr => unique3 (*-cover ∘ prod +-cover id) (+-cover ∘ tuple (*-cover ∘ tuple (proj1 ∘ proj1) proj2) (*-cover ∘ tuple (proj2 ∘ proj1) proj2))
      \lam x y z => pmap (*-func __ _) +-char *> lift2-char *> pmap pointCF X.rdistr *> inv (pmap2 +-func lift2-char lift2-char *> +-char)
  | ide => pointCF 
  | ide-left => unique1 (*-cover ∘ tuple (const _) id) id \lam x => lift2-char *> pmap pointCF ide-left
  | ide-right => unique1 (*-cover ∘ tuple id (const _)) id \lam x => lift2-char *> pmap pointCF ide-right
  | norm_*_<= => unique2_<= (norm-metric-map {BanachCompletion X} ∘ *-cover) (ex-upper-*-locally-uniform ∘ prod (bnorm-metric-map {BanachCompletion X}) (bnorm-metric-map {BanachCompletion X}))
      \lam x y => transport2 (<=) (inv $ pmap ExNormedAbGroupCompletion.norm lift2-char *> completion-exNormed-isometry.func-norm-isometry) (inv $ pmap2 (*) completion-exNormed-isometry.func-norm-isometry completion-exNormed-isometry.func-norm-isometry) X.norm_*_<=
  | norm_ide_<= => completion-exNormed-isometry.func-norm <=∘ norm_ide_<=
  \where {
    \open ProductCoverSpace
    \open CoverMap
    \open TopAbGroupCompletion

    \func *-cover : CoverMap (Completion X ⨯ Completion X) (Completion X)
      => lift2 *-locally-uniform

    \func *-func (x y : RegularCauchyFilter X) => *-cover (x,y)
  }