\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Solver
\import Algebra.Solver.Monoid
\import Algebra.Solver.Semiring
\import Arith.Fin.Order
\import Arith.Int
\import Data.Array(Big, map \as arrayMap)
\import Data.List
\import Function.Meta
\import Meta
\import Order.Lexicographical
\import Paths
\import Paths.Meta
\import Set
\open SemiringSolverModel

\func RingSolverModel (R : Ring) : SolverModel R \cowith
  | Term => Term Int
  | NF => NF Int
  | normalize => normalize
  | interpret env => interpret env
  | interpretNF env => ringInterpretNF env
  | interpretNF-consistent {_} {env} {_} => ringInterpretNF-correct *> (RingData env).interpretNF-correct *> normalize-consistent
  \where {
    \data Term (C : \Set) (n : Nat)
      | var (Fin n)
      | coef C
      | :zro
      | :ide
      | :negative (Term C n)
      | \infixl  :+ (t s : Term C n)
      | \infixl  :* (t s : Term C n)

    \func normalize {n : Nat} {C : Ring.Dec} (t : Term C n) : NF C n \elim t
      | var v => (v :: nil, ) :: nil
      | coef c => (nil, c) :: nil
      | :zro => nil
      | :ide => (nil, ) :: nil
      | :negative t => map (\lam s => (s., C.negative s.)) (normalize t)
      | t :+ s => normalize t ++ normalize s
      | t :* s => remove0 (collapse (multiply (normalize t) (normalize s)))

    \func interpret (env : Array R) (t : Term Int env.len) : R \elim t
      | coef c => R.intCoef c
      | var c => env c
      | :zro => 
      | :ide => 
      | :negative t => negative (interpret env t)
      | :+ t s => interpret env t + interpret env s
      | :* t s => interpret env t * interpret env s

    \func intCoef (x : Int) : R
      | pos n => natCoef n
      | neg  => negative ide
      | neg (suc _ \as n) => negative (R.natCoef n)

    \lemma intCoef-correct {x : Int} : R.intCoef x = intCoef x \elim x
      | pos n => natCoef-correct
      | neg  => pmap negative $ R.natCoefSuc  *> pmap (`+ ide) R.natCoefZero *> zro-left
      | neg (suc (suc n)) => idp

    \lemma intMap' : RingHom IntRing R intCoef
      => transport (RingHom IntRing R) (path \lam i x => intCoef-correct {_} {x} i) intMap

    \func RingData (env : Array R) : Data R IntRing IntRing intMap' env \cowith
      | alg-comm x a => inv (pmap (`* a) intCoef-correct) *> intComm x a *> pmap (a *) intCoef-correct

    \func signMulCoef (c : Int) (r : R) : R \elim c
      | pos _ => r
      | neg (suc _) => negative r

    \func ringMulCoef {env : Array R} (c : Int) (l : List (Fin env.len)) : R
      => signMulCoef c $ (RingData env).mulCoef (iabs c) l

    \func ringInterpretNF' {env : Array R} (l : SemiringSolverModel.NF Int env.len) : R \elim l
      | nil => 
      | x :: nil => ringMulCoef x. x.
      | x :: l => ringMulCoef x. x. + ringInterpretNF' l

    \func ringInterpretNF (env : Array R) (l : SemiringSolverModel.NF Int env.len) => ringInterpretNF' (remove0 (collapse (Sort.RedBlack.sort l)))

    \lemma ringMulCoef-correct {env : Array R} {c : Int} {l : List (Fin env.len)} : ringMulCoef c l = (RingData env).mulCoef c l \elim c
      | pos n => idp
      | neg (suc n) => pmap negative (RingData env).mulCoef-consistent *> inv R.negative_*-left *> pmap (`* _) (inv $ intMap'.func-negative {suc n}) *> inv (RingData env).mulCoef-consistent

    \lemma ringInterpretNF-correct {env : Array R} {l : SemiringSolverModel.NF Int env.len} : ringInterpretNF' l = (RingData env).interpretNF' l \elim l
      | nil => idp
      | x :: nil => ringMulCoef-correct
      | x :: y :: l => pmap2 (+) ringMulCoef-correct ringInterpretNF-correct

    \lemma interpretNF_negative {env : Array R} {l : NF Int env.len}
      : (RingData env).interpretNF' (map (\lam s => (s., negative s.)) l) = negative ((RingData env).interpretNF' l) \elim l
      | nil => inv R.negative_zro
      | a :: l => (RingData env).interpretNF_:: *> +-comm *> pmap2 (+) interpretNF_negative (pmap (`* _) intMap'.func-negative *> R.negative_*-left) *> inv (pmap negative (RingData env).interpretNF_:: *> R.negative_+)

    \lemma normalize-consistent {env : Array R} {t : Term Int env.len} : (RingData env).interpretNF' (normalize t) = interpret env t \elim t
      | coef c => inv intCoef-correct
      | var v => idp
      | :zro => idp
      | :ide => idp
      | :negative t => interpretNF_negative *> pmap negative normalize-consistent
      | :+ t s => (RingData env).interpretNF_++ *> pmap2 (+) normalize-consistent normalize-consistent
      | :* t s => (RingData env).remove0-consistent *> (RingData env).collapse-consistent *> (RingData env).interpretNF_multiply *> pmap2 (*) normalize-consistent normalize-consistent

    \lemma terms-equality (env : Array R) (t s : Term Int env.len) (p : ringInterpretNF env (normalize (t :+ :negative s)) = ) : interpret env t = interpret env s
      => R.fromZero $ inv ((RingData env).interpretNF-correct *> (RingData env).interpretNF_++ *> pmap2 (+) normalize-consistent (interpretNF_negative *> pmap negative normalize-consistent)) *> inv ringInterpretNF-correct *> p

    \lemma terms-equality-conv (env : Array R) (t s : Term Int env.len) (p : interpret env t = interpret env s) : ringInterpretNF env (normalize (t :+ :negative s)) = 
      => ringInterpretNF-correct *> (RingData env).interpretNF-correct *> (RingData env).interpretNF_++ *> pmap (_ +) interpretNF_negative *> R.toZero (normalize-consistent *> p *> inv normalize-consistent)

    \lemma apply-axioms (env : Array R) (l : Array (\Sigma (NF Int env.len) (t s : Term Int env.len) (p : interpret env t = interpret env s))) (add : NF Int env.len)
      : ringInterpretNF env (Big (++) add (arrayMap (\lam s => multiply s. (normalize (s. :+ :negative s.))) l)) = ringInterpretNF' add
      => \have d => RingData env
         \in ringInterpretNF-correct *> d.interpretNF-correct *> d.interpretNF_Big_++ *> pmap (`+ _) (R.BigSum_zro \lam j => d.interpretNF_multiply *> pmap (_ *) (d.interpretNF_++ *> pmap (_ +) interpretNF_negative *> R.toZero (normalize-consistent *> later (l j). *> inv normalize-consistent)) *> R.zro_*-right) *> zro-left *> inv ringInterpretNF-correct
  }