\import Algebra.Pointed
\import Arith.Nat
\import Data.Array
\import Function.Meta
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence

\func QPoly (R : AddPointed) => Quotient {Array R} (__ = __ ++ 0 :: nil)
\where {
\data \infix 5 ~ {R : AddPointed} (l l' : Array R)
| eq-left (n : Nat) (l ++ replicate n zro = l')
| eq-right (n : Nat) (l' ++ replicate (suc n) zro = l)
\where {
\lemma lists-lem1 {R : AddPointed} {l l' : Array R} (n m : Nat) (p : l ++ replicate n zro = l') (q : l ++ replicate m zro = l') : n = m
=> NatSemiring.cancel-left _ (inv len_++ *> pmap (DArray.len {__}) (p *> inv q) *> len_++)

\lemma lists-lem2 {R : AddPointed} {l l' : Array R} {n m : Nat} (p : l ++ replicate n zro = l') (q : l' ++ replicate (suc m) zro = l) : Empty
=> \have t => ++-cancel-left $inv ++-assoc *> pmap (++ _) p *> q *> inv ++_nil \in \case \elim n, \elim t \with { | 0, t => \case pmap (DArray.len {__}) t } \use \level levelProp {R : AddPointed} {l l' : Array R} (x y : l ~ l') : x = y \elim x, y | eq-left n p, eq-left m q => path (\lam i => eq-left (lists-lem1 n m p q i) (prop-dpi _ _ _ i)) | eq-left n p, eq-right m q => absurd (lists-lem2 p q) | eq-right n p, eq-left m q => absurd (lists-lem2 q p) | eq-right n p, eq-right m q => path (\lam i => eq-right (pmap pred (lists-lem1 (suc n) (suc m) p q) @ i) (prop-dpi _ _ _ i)) } \func ~-isEquiv {R : AddPointed} : Equivalence (Array R) \cowith | ~ => ~ | ~-reflexive => eq-left 0 ++_nil | ~-symmetric => symm | ~-transitive => \case __, __ \with { | eq-left n p, eq-left m q => eq-left (n Nat.+ m) (pmap (_ ++) replicate_+ *> inv ++-assoc *> pmap (++ _) p *> q) | eq-left n p, eq-right m q => \case totality (suc m) n \with { | byLeft s => lists-lem1 n (suc m) (p *> inv q) s | byRight s => symm (lists-lem1 (suc m) n (q *> inv p) s) } | eq-right n p, eq-left m q => \case totality (suc n) m \with { | byLeft s => lists-lem2 (suc n) m p q s | byRight s => symm (lists-lem2 m (suc n) q p s) } | eq-right n p, eq-right m q => eq-right (suc m Nat.+ n) (pmap (_ ++) (replicate_+ {_} {suc m} {suc n}) *> inv ++-assoc *> pmap (++ zro :: _) q *> p) } \where { \lemma symm {R : AddPointed} {x y : Array R} (p : x ~ y) : y ~ x \elim p | eq-left 0 p => eq-left 0 (++_nil *> inv p *> ++_nil) | eq-left (suc n) p => eq-right n p | eq-right n p => eq-left (suc n) p \lemma lists-lem1 {R : AddPointed} {x z : Array R} (n m : Nat) (p : x ++ replicate n zro = z ++ replicate m zro) (q : m <= n) : x ~ z => eq-left (n -' m)$ ++-cancel-right $rewrite (inv (<=_exists q), NatSemiring.+-comm, replicate_+, inv ++-assoc) in p \lemma lists-lem2 {R : AddPointed} {x y z : Array R} (n m : Nat) (p : y ++ replicate n zro = x) (q : y ++ replicate m zro = z) (s : n <= m) : x ~ z => eq-left (m -' n)$ rewrite (inv (<=_exists s), replicate_+, inv ++-assoc, p) in q
}

\lemma from=to~ {R : AddPointed} {l l' : Array R} (p : in~ l = {QPoly R} in~ l') : l ~ l'
=> Quotient.equalityClosure ~-isEquiv (\lam q => eq-right 0 (inv q)) p

\lemma from~to= {R : AddPointed} {l l' : Array R} (p : l ~ l') : in~ l = {QPoly R} in~ l' \elim p
| eq-left 0 p => pmap in~ (inv ++_nil *> p)
| eq-left (suc n) p => from~to= (eq-left n idp) *> inv (path $~-equiv _ _$ inv $++-assoc *> (rewrite (replicate_+ {_} {n} {1}) in p)) | eq-right 0 p => path (~-equiv l l' (inv p)) | eq-right (suc n) p => path (~-equiv _ _$ inv $++-assoc {_} {l'} {replicate (suc n) zro} *> (rewrite (replicate_+ {_} {suc n} {1}) in p)) *> from~to= (eq-right n idp) -- | qadd p e is equivalent to p * X + e \func qadd {R : AddPointed} (p : QPoly R) (e : R) : QPoly R \elim p | in~ l => in~ (e :: l) | ~-equiv x y r => path (~-equiv _ _ (pmap (e ::) r)) \lemma nil_cons {R : AddPointed} {e : R} {l : Array R} (s : in~ nil = {QPoly R} in~ (e :: l)) : \Sigma (zro = e) (in~ nil = {QPoly R} in~ l) => \case from=to~ s \with { | eq-left 0 p => \case pmap (DArray.len {__}) p | eq-left (suc n) p => (unhead p, from~to=$ ~-isEquiv.lists-lem2 {_} {_} {nil} 0 n idp (untail p) zero<=_)
| eq-right n ()
}

\lemma qadd_nil {R : AddPointed} {p : QPoly R} {e : R} (s : qadd p e = in~ nil) : \Sigma (p = in~ nil) (e = 0) \elim p
| in~ l => \case from=to~ s \with {
| eq-left n ()
| eq-right n p => (inv $from~to=$ ~-isEquiv.lists-lem2 {_} {_} {nil} 0 n idp (untail p) zero<=_, inv $unhead p) } \lemma qadd_cons {R : AddPointed} {e a : R} {p : QPoly R} {l' : Array R} (s : qadd p e = in~ (a :: l')) : \Sigma (e = a) (p = in~ l') \elim p | in~ l => \case from=to~ s \with { | eq-left n p => (unhead p, from~to=$ eq-left n $untail p) | eq-right n p => (inv$ unhead p, from~to= $eq-right n$ untail p)
}
}`