\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} (__ = __ ++  :: nil)
  \where {
    \data \infix  ~ {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 { | , 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  ++_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  p => eq-left  (++_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  (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  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} {}) in p))
      | eq-right  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} {}) 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  p => \case pmap (DArray.len {__}) p
        | eq-left (suc n) p => (unhead p, from~to= $ ~-isEquiv.lists-lem2 {_} {_} {nil}  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 = ) \elim p
      | in~ l => \case from=to~ s \with {
        | eq-left n ()
        | eq-right n p => (inv $ from~to= $ ~-isEquiv.lists-lem2 {_} {_} {nil}  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)
      }
  }