\import Algebra.Field
\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Data.List
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\open AddGroup(toZero, negative_zro)
\open Ring(negative_*-right)
\class VectorSpace (F : Field) \extends AbGroup
  | \infixl 7 * : F -> E -> E
  | *-compat (a b : F) (v : E) : a * (b * v) = a F.* b * v
  | *-ide (v : E) : F.ide * v = v
  | *-distrib-vector (a : F) (v u : E) : a * (v + u) = a * v + a * u
  | *-distrib-scalar (a b : F) (v : E) : (a F.+ b) * v = a * v + b * v

\lemma *-distrib-scalar' {V : VectorSpace} (a b : V.F) (v : V) : (a - b) * v = a * v + negative b * v =>
  unfold (-) $ *-distrib-scalar a (negative b) v

\lemma zro-* {V : VectorSpace} (v : V) : zro * v = zro =>
  inv $ consumeIsZro (ide * v, rewriteF zro-right $ *-distrib-scalar ide zro v)
  \where {
    \lemma consumeIsZro {G : AddGroup} {z : G} (p : \Sigma (x : G) (x = x + z)) : zro = z \elim p
      | (x,p) => rewriteF (negative-left, zro-left) $ rewriteI +-assoc $ pmap (negative x +) p
  }

\lemma negative-compat' {V : VectorSpace} (v : V) : negative ide * v = negative v =>
  \let
    | p => *-distrib-scalar' ide ide v
    | p' => rewrite (V.F.toZero {ide} {ide} idp, *-ide) p
    | p'' => rewrite (inv +-assoc, negative-left, zro-left, zro-right) $ pmap (negative v +) $ inv p' *> zro-* v
  \in p''

\lemma negative-compat {V : VectorSpace} {a : V.F} {v : V} : negative a * v = a * negative v =>
  \let
    | q => rewrite (negative_*-right, ide-right) $ *-compat a (negative ide) v
  \in inv $ pmap (a *) (inv $ negative-compat' v) *> q

\lemma negative_* {V : VectorSpace} {a : V.F} {v : V} : negative (a * v) = a * negative v =>
  \let
    | p => unfold (-) $ V.toZero {a V.* v} {a * v} idp
    | q : zro = (a * v) + a * negative v => rewriteI (*-distrib-vector, inv negative-right) $ inv $ *-zro a
  \in AddGroup.cancel-left (a * v) $ p *> q

\lemma negative_*' {V : VectorSpace} {a : V.F} {v : V} : negative (a * v) = negative a * v =>
  negative_* *> inv negative-compat

\lemma *-zro {V : VectorSpace} (a : V.F) : a * zro = zro =>
  \let
    | p => rewriteF (inv negative-compat) $ pmap (a * ) (inv negative-right) *> *-distrib-vector a zro (negative zro)
  \in rewriteF (negative-right, zro-*) $ p *> (inv $ *-distrib-scalar a (negative a) zro)

\data LinComb {V : VectorSpace} (xs : List V) (v : V) \elim xs
  | nil => lc-nil (v = zro)
  | :: x xs => lc-cons (a : V.F) (LinComb xs (v - a * x))
  \where {

    \lemma transport-nil {V : VectorSpace} {v u : V} {e : v = zro} (p : v = u) : transport (LinComb nil) p (lc-nil e) = lc-nil (transport (\lam x => x = V.zro) p e) \elim p
      | idp => idp

    \lemma transport-cons {V : VectorSpace} {vs : List V} {x v u : V} {a : V.F} {t : LinComb vs (v - a * x)} (p : v = u) : transport (LinComb (x :: vs)) p (lc-cons a t) = lc-cons a (transport (\lam e => LinComb vs (e - a * x)) p t) \elim p
      | idp => idp

    \lemma lc-cons-ext {V : VectorSpace} {vs : List V} {x v : V} {a a' : V.F}
                       {t : LinComb vs (v - a * x)} {t' : LinComb vs (v - a' * x)}
                       (p : a' = a) (q : t = transport (\lam s => LinComb vs (v - s * x)) p t')
      : lc-cons a t = lc-cons a' t' \elim p
      | idp => pmap (lc-cons a) q

    \func extend {V : VectorSpace} (vs : List V) (v u : V) (p : LinComb vs u) : LinComb (v :: vs) u =>
      lc-cons zro (unfold (-) $ rewrite (zro-*, negative_zro, zro-right) p)

    \func lin-+ {V : VectorSpace} {vs : List V} {u w : V} (p : LinComb vs u) (q : LinComb vs w) : LinComb vs (u + w) \elim vs, p, q
      | nil, lc-nil p, lc-nil q => lc-nil $ pmap2 (+) p q *> zro-right
      | :: v vs, lc-cons a p, lc-cons b q => lc-cons (a + b) (rewriteI arith-helper $ lin-+ p q)
      \where {
        \lemma arith-helper {V : VectorSpace} {a b : V.F} {v u w : V}
          : u - a * v + (w - b * v) = u + w - (a + b) * v =>
          \let a' => V.F.negative a | b' => V.F.negative b \in
            (u - a * v) + (w - b * v) ==< unfold (-) (repeat (rewrite (negative_*, inv negative-compat)) idp) >==
            (u + a' * v) + (w + b' * v) ==< inv +-assoc >==
            ((u + a' * v) + w) + b' * v ==< pmap (`+ _) +-assoc >==
            (u + (a' * v + w)) + b' * v ==< pmap (`+ _) (pmap (_ +) +-comm) >==
            (u + (w + a' * v)) + b' * v ==< inv (pmap (`+ _) +-assoc) >==
            ((u + w) + a' * v) + b' * v ==< +-assoc >==
            (u + w) + (a' * v + b' * v) ==< inv (pmap (_ +) (*-distrib-scalar a' b' v)) >==
            u + w + (a' + b') * v ==< pmap (_ +) (pmap (`* _) negative_+' *> inv negative_*') >==
            u + w - (a + b) * v `qed
      }

    \lemma lin-+-assoc {V : VectorSpace} {vs : List V} {u w l : V} (p : LinComb vs u) (q : LinComb vs w) (k : LinComb vs l) : p `lin-+` (q `lin-+` k) = transport (LinComb vs) +-assoc ((p `lin-+` q) `lin-+` k) \elim vs, p, q, k
      | nil, lc-nil p, lc-nil q, lc-nil k => rewrite transport-nil $ pmap lc-nil $ Path.inProp _ _
      | :: v vs, lc-cons a p, lc-cons b q, lc-cons c k => rewrite transport-cons $ lc-cons-ext +-assoc {?}

    \func negative_+' {G : AbGroup} {a b : G} : G.negative a G.+ G.negative b = G.negative (a G.+ b) =>
      (unfold (-) $ G.+-comm) *> inv G.negative_+

    \func lin-* {V : VectorSpace} {vs : List V} {u : V} (a : V.F) (p : LinComb vs u) : LinComb vs (a * u) \elim vs, p
      | nil, lc-nil idp => lc-nil $ *-zro a
      | :: v vs, lc-cons b p => lc-cons (a V.F.* b) (rewriteF (*-distrib-vector, negative_*, *-compat, inv negative_*) $ lin-* a p)

    \func negative {V : VectorSpace} {vs : List V} {u : V} (p : LinComb vs u) : LinComb vs (V.negative u) \elim vs, p
      | nil, lc-nil p => lc-nil $ pmap V.negative p *> negative_zro
      | :: v vs, lc-cons a p => lc-cons (V.F.negative a) (rewriteF (inv negative_+', negative_*') $ negative p)

    \func trans {V : VectorSpace} {vs ws : List V} (p : \Pi (k : Fin (length ws)) -> LinComb vs (ws !! k)) {u : V} (q : LinComb ws u) : LinComb vs u \elim vs, ws, q
      | nil, nil, lc-nil idp => lc-nil idp
      | nil, :: w ws, lc-cons a q =>
        \let
          | (lc-nil p') => p 0
        \in rewriteF (p', *-zro, negative_zro, zro-right) $ unfold (-) $ trans (\lam k => p (suc k)) q
      | :: v vs, nil, q => extend vs v u $ trans (\lam k => \case k) q
      | :: v vs, :: w ws, lc-cons a q => rewriteF (inv +-assoc, +-comm, inv +-assoc, negative-left, zro-left)
        $ lin-+ (lin-* a $ p 0) $ trans (\lam k => p (suc k)) q
  }

\data TrivialComp {V : VectorSpace} {xs : List V} {v : V} (p : LinComb xs v) \elim xs, p
  | nil, lc-nil _ => nil-trivial
  | :: x xs, lc-cons a p => cons-trivial (zro = a) (TrivialComp p)
  \where {
    \func pmap3 {A B C D : \Type} (f : A -> B -> C -> D) {a a' : A} (p : a = a') {b b' : B} (q : b = b') {c c' : C} (r : c = c') : f a b c = f a' b' c' =>
      path (\lam i => f (p @ i) (q @ i) (r @ i))

    \lemma singleTrivial {V : VectorSpace} {xs : List V} {v : V} {a b : LinComb xs v} (p : TrivialComp a) (q : TrivialComp b) : a = b
    \elim xs, a, b, p, q
      | nil, lc-nil p, lc-nil q, nil-trivial, nil-trivial => pmap lc-nil $ Path.inProp p q
      | :: x xs, lc-cons n a, lc-cons m b, cons-trivial idp p, cons-trivial idp q =>
        pmap (lc-cons zro) (singleTrivial p q)
  }

\func makeTrivialComp {V : VectorSpace} (xs : List V) : \Sigma (p : LinComb xs zro) (TrivialComp p) =>
  makeTrivialComp' xs idp
  \where {
    \func makeTrivialComp' {V : VectorSpace} (xs : List V) {v : V} (e : v = zro) : \Sigma (p : LinComb xs v) (TrivialComp p) \elim xs
      | nil => (lc-nil e, nil-trivial)
      | :: x xs =>
        \let
          | k : v - zro * x = zro => rewrite e $ zro-left *> pmap negative (zro-* x) *> negative_zro
          | (p, q) => makeTrivialComp' xs k
        \in (lc-cons zro p, cons-trivial idp q)
  }

\func LinIndep {V : VectorSpace} (vs : List V) => \Pi (p : LinComb vs zro) -> TrivialComp p
  \where {
    \func uniqueness {V : VectorSpace} (vs : List V) : LinIndep vs <-> (\Pi {x : V} (p q : LinComb vs x) -> p = q) =>
      (
        \lam l {x} p q =>
            \let
              | (p', k) => reduceComp p q
              | (q', k') => reduceComp q q
              | pq : p' = q' => TrivialComp.singleTrivial (l p') (l q')
            \in k *> rewrite pq idp *> inv k',
        \lam f p => \let (z, q) => makeTrivialComp vs \in rewrite (f p z) q
      )

    \func reduceComp {V : VectorSpace} {vs : List V} {v : V} (p : LinComb vs v) (q : LinComb vs v)
      : \Sigma (x : LinComb vs zro) (p = transport (LinComb vs) zro-left (LinComb.lin-+ x q))
      => {?} -- (transport (LinComb vs) negative-right (LinComb.lin-+ p (LinComb.negative q)), reduceComp' p q)
      \where {
        \func reduceComp' {V : VectorSpace} {vs : List V} {v u : V} (p : LinComb vs v) (q : LinComb vs u)
          : p = transport (LinComb vs) arith-helper
                    (LinComb.lin-+ (LinComb.lin-+ p (LinComb.negative q)) q) \elim vs, p, q
          | nil, lc-nil p, lc-nil q =>  {?} -- rewrite helper $ pmap lc-nil (Path.inProp _ _)
          | :: x vs, lc-cons a p, lc-cons b q => {?} -- rewrite helper' $ lc-cons-ext arith-helper {?}

        \lemma arith-helper {F : AbGroup} {a b : F} : a F.+ negative b F.+ b = a
          => F.+-assoc *> pmap (a F.+) F.negative-left *> F.zro-right
      }
  }

\func LinDep {V : VectorSpace} (vs : List V) => \Sigma (p : LinComb vs zro) (Not $ TrivialComp p)

\func DepIndep {V : VectorSpace} (vs : List V) (p : LinIndep vs) (q : LinDep vs) : Empty =>
  \let (l, q') => q | p' => p l \in q' p'

--\func zrp-dep {V : VectorSpace} : LinDep (zro :: nil) =>
--  (lc-cons ide zro (rewrite *-zro $ inv zro-left) (lc-nil idp), \lam t => \case t \with {
--    | cons-trivial p _ => zro/=ide p
--  })

\func Spans {V : VectorSpace} (vs : List V) => \Pi (x : V) -> LinComb vs x

\func Basis {V : VectorSpace} (vs : List V) =>
  \Pi (x : V) -> \Sigma (p : LinComb vs x) (\Pi (q : LinComb vs x) -> p = q)
  \where {
    \func spans {V : VectorSpace} (vs : List V) (b : Basis vs) : Spans vs => \lam x => (b x).1

    \func indep {V : VectorSpace} (vs : List V) (b : Basis vs) : LinIndep vs => \lam p => {?}

    \func Basis-maximal-indep {V : VectorSpace} (vs : List V) => \Sigma (LinIndep vs) (\Pi (v : V) -> LinDep (v :: vs))
      \where {
        \func fromBasis {V : VectorSpace} (vs : List V) : Basis vs -> Basis-maximal-indep vs => \lam b => (
          \lam p => {?},
          \lam v => {?}
        )
      }
  }

\data BasisComb {V : VectorSpace} {xs : List V} (b : Basis xs) (v : V)
  | basis (LinComb xs v)
  \where {
    \use \level isProp {V : VectorSpace} {xs : List V} {b : Basis xs} {v : V} (p q : BasisComb b v) : p = q \elim p, q
      | basis p, basis q => pmap basis $ (inv $ (b v).2 p) *> (b v).2 q
  }