\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Solver
\import Algebra.Solver.CSemiring
\import Algebra.Solver.Ring
\import Algebra.Solver.Semiring
\import Arith.Int
\import Data.Array(Big, map)
\import Data.List(++)
\import Function.Meta
\import Paths
\open RingSolverModel
\open SemiringSolverModel(NF,multiply)
\open CSemiringSolverModel

\func CRingSolverModel (R : CRing) : SolverModel R \cowith
  | Term => Term Int
  | NF => NF Int
  | normalize => normalize
  | interpret env => interpret env
  | interpretNF env nf => ringInterpretNF env (sortMonomials nf)
  | interpretNF-consistent {_} {env} {_} => ringInterpretNF-correct *> (RingData env).interpretNF-correct *> interpretNF_sort {R} {RingData env} *> normalize-consistent
  \where {
    \lemma terms-equality (env : Array R) (t s : Term Int env.len) (p : ringInterpretNF env (sortMonomials (normalize (t :+ :negative s))) = ) : interpret env t = interpret env s
      => RingSolverModel.terms-equality env t s $ ringInterpretNF-correct *> (RingData env).interpretNF-correct *> inv ((RingData env).interpretNF-correct *> interpretNF_sort {R} {RingData env}) *> 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 (sortMonomials (normalize (t :+ :negative s))) = 
      => ringInterpretNF-correct *> (RingData env).interpretNF-correct *> interpretNF_sort {R} {RingData env} *> inv (RingData env).interpretNF-correct *> inv ringInterpretNF-correct *> RingSolverModel.terms-equality-conv env t s p

    \lemma diffNF (env : Array R) (left right : NF Int env.len) (p : (RingData env).interpretNF' (left ++ Data.List.map (\lam s => (s., negative s.)) right) = )
      : (RingData env).interpretNF' left = (RingData env).interpretNF' right
      => AddGroup.fromZero $ inv (inv p *> (RingData env).interpretNF_++ {left} {Data.List.map (\lam s => (s., negative s.)) right} *> pmap ((+) ((RingData env).interpretNF' left)) (interpretNF_negative {_} {_} {right}))

    \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 (sortMonomials (Big (++) add (map (\lam s => multiply s. (normalize (s. :+ :negative s.))) l))) = ringInterpretNF' add
      => ringInterpretNF-correct *> (RingData env).interpretNF-correct *> interpretNF_sort {R} {RingData env} *> inv (RingData env).interpretNF-correct *> inv ringInterpretNF-correct *> RingSolverModel.apply-axioms env l add
  }