Require Import Setoid Field Min List Aux.

Structure eparams: Type := {
 E:> Set;                      (* the vector type *)
 stype:> fparams;              (* the scalar field *)
 E0: E;                        (* 0 *)
 eqE: E -> E -> bool;          (* = as a boolean function *)
 addE : E -> E -> E;          (* + *)
 scalE : (K stype) -> E -> E   (* scalar *)
}.

Delimit Scope vector_scope with v.

Notation "x ?= y" := (eqE _ x y) (at level 70): vector_scope.
Notation "0" := (E0 _): vector_scope.
Notation "x + y" := (addE _ x y): vector_scope.
Notation "x .* y" := (scalE _ x%f y) (at level 31, no associativity): vector_scope.

Arguments scalE _ _%field_scope _%vector_scope.

Section VectorSpace.


(* This is our scalar space *)
Variable p : eparams.

Open Scope vector_scope.

Implicit Type v x y z: p.
Implicit Type k: stype p.

(* Multiple product for characterizing linear combinations *)
Definition  mprod ks vs :=
   fold2 (fun k v r => k .* v + r) ks vs 0.

Notation " x *X* y " := (mprod x y) (at level 40, no associativity): vector_scope.


(* What it means for a sub vector space (i.e a list of vectors)
   to be free *)
Definition free vs := 
  forall ks, length ks = length vs -> ks *X* vs = 0 -> 
    (forall k, In k ks -> k = 0%f).

 
(* What it is to be a linear combination *)
Inductive cbl (l: list (E p)): (E p) -> Prop :=
  cbl0: cbl l 0
| cbl_in: forall v, In v l -> cbl l v
| cbl_add: forall x y, cbl l x -> cbl l y -> cbl l (x + y)
| cbl_scal: forall k x, cbl l x -> cbl l (k .* x).

Lemma cbl_trans l1 l2 x: 
  (forall i, In i l2 -> cbl l1 i) -> cbl l2 x -> cbl l1 x.
Proof.
(* Goal: forall (_ : forall (i : E p) (_ : @In (E p) i l2), cbl l1 i) (_ : cbl l2 x), cbl l1 x *)
intros H1 H2; elim H2; auto.
(* Goal: cbl l1 (E0 p) *)
(* Goal: forall (x y : E p) (_ : cbl l2 x) (_ : cbl l1 x) (_ : cbl l2 y) (_ : cbl l1 y), cbl l1 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l2 x) (_ : cbl l1 x), cbl l1 (scalE p k x) *)
apply cbl0.
(* Goal: forall (x y : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : cbl l1 y) (_ : forall _ : @incl (E p) l1 l2, cbl l2 y) (_ : @incl (E p) l1 l2), cbl l2 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : @incl (E p) l1 l2), cbl l2 (scalE p k x) *)
intros; apply cbl_add; auto.
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : @incl (E p) l1 l2), cbl l2 (scalE p k x) *)
intros; apply cbl_scal; auto.
Qed.
 
Definition is_base vs := free vs /\ forall e, cbl vs e.

Structure vparamsProp: Type := {
 sProp : fparamsProp p;
 eqE_dec: forall x y, if x ?= y then x = y else x <> y;        
          (* Boolean equality *)
 addE_assoc: forall x y z, (x + y) + z = x + (y + z);
          (* Associativity for + *)
 addE_com: forall x y, x + y = y + x;
          (* Commutativity for + *)
 addE0l: forall x, 0 + x = x;
          (* Left neutral  for + *)
 scalE0l: forall x, 0 .* x = 0;
          (* scalar 0 *)
 scalE1: forall x, 1 .* x = x;
          (* scalar 1 *)
 scal_addEl: forall k1 k2 x, (k1 + k2) .* x = (k1.* x) + (k2 .* x);
          (* scalar distributivity left *)
 scal_addEr: forall k x y, k .* (x + y) = k .* x + k .* y;
          (* scalar distributivity right *)
 scal_multE: forall k1 k2 x, (k1 * k2) .* x = k1.* (k2 .* x)
          (* scalar distributivity left *)
}.

Variable Hp: vparamsProp.

Lemma eqE_refl x: (x ?= x) = true.
Proof.
(* Goal: @eq bool (eqE p x x) true *)
generalize (eqE_dec Hp x x); case eqE; auto.
Qed.

Lemma addE0r: forall x, x + 0 = x.
Proof.
(* Goal: forall x : E p, @eq (E p) (addE p x (E0 p)) x *)
intros x; rewrite addE_com; auto; rewrite addE0l; auto.
Qed.

Let sfP := sProp Hp.

Lemma addE_cancell x y z : z + x = z + y -> x = y.
Proof.
(* Goal: forall _ : @eq (E p) (addE p z x) (addE p z y), @eq (E p) x y *)
intros H.
(* Goal: @eq (E p) x y *)
rewrite <-addE0l; auto.
(* Goal: @eq (E p) x (addE p (E0 p) y) *)
rewrite <-(fun xx => scalE0l xx z); auto.
(* Goal: @eq (E p) x (addE p (scalE p (v0 (stype p)) z) y) *)
rewrite <-(oppKl _ sfP 1%f); auto.
(* Goal: @eq (E p) x (addE p (scalE p (addK (stype p) (oppK (stype p) (v1 (stype p))) (v1 (stype p))) z) y) *)
rewrite scal_addEl; auto.
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) (scalE p (v1 (stype p)) z)) y) *)
rewrite scalE1; auto.
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) z) y) *)
rewrite addE_assoc; auto.
(* Goal: @eq (E p) x (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) (addE p z y)) *)
rewrite <-H; rewrite <-addE_assoc; auto.
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) z) x) *)
pattern z at 2; rewrite <-(fun xx => scalE1 xx z); auto.
(* Goal: @eq (E p) (addE p (scalE p (v1 (stype p)) x) (scalE p (oppK (stype p) (v1 (stype p))) x)) (E0 p) *)
rewrite <-scal_addEl; auto.
(* Goal: @eq (E p) x (addE p (scalE p (addK (stype p) (oppK (stype p) (v1 (stype p))) (v1 (stype p))) z) x) *)
rewrite oppKl; auto.
(* Goal: @eq (E p) (scalE p (v0 (stype p)) x) (E0 p) *)
rewrite scalE0l; auto.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
rewrite addE0l; auto.
Qed.

Lemma addE_cancelr x y z : x + z = y + z -> x = y.
Proof.
(* Goal: forall _ : @eq (E p) (addE p x z) (addE p y z), @eq (E p) x y *)
intros H; apply addE_cancell with z.
(* Goal: @eq (E p) (addE p z x) (addE p z y) *)
repeat rewrite (fun xx => addE_com xx z); auto.
Qed.

Lemma scalE0r k : k .* 0 = 0.
Proof.
(* Goal: @eq (E p) (scalE p k (E0 p)) (E0 p) *)
apply addE_cancell with (k .* 0).
(* Goal: @eq (E p) (addE p (scalE p (v1 (stype p)) a) (addE p (scalE p (oppK (stype p) (v1 (stype p))) a) (E0 p))) (E0 p) *)
(* Goal: @uniq (E p) vs *)
rewrite addE0r.
(* Goal: @eq (E p) (addE p (scalE p k (E0 p)) (scalE p k (E0 p))) (scalE p k (E0 p)) *)
rewrite <-scal_addEr; auto.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
rewrite addE0l; auto.
Qed.

(* Opposite for  + *)
Lemma scal_addE0 x : x + (- (1)) .* x = 0.
Proof.
(* Goal: @eq (E p) (addE p x (scalE p (oppK (stype p) (v1 (stype p))) x)) (E0 p) *)
generalize (scal_addEl Hp (1)%f (- (1))%f x).
(* Goal: forall _ : @eq (E p) (scalE p (addK (stype p) (v1 (stype p)) (oppK (stype p) (v1 (stype p)))) x) (addE p (scalE p (v1 (stype p)) x) (scalE p (oppK (stype p) (v1 (stype p))) x)), @eq (E p) (addE p x (scalE p (oppK (stype p) (v1 (stype p))) x)) (E0 p) *)
rewrite oppKr; auto; rewrite scalE1, scalE0l; auto.
Qed.


Lemma addE_eq_opp x y : x + (-(1)) .* y = 0 -> x = y.
Proof.
(* Goal: forall _ : @eq (E p) (addE p x (scalE p (oppK (stype p) (v1 (stype p))) y)) (E0 p), @eq (E p) x y *)
intros H; apply addE_cancell with ((-(1)) .* y).
(* Goal: @eq (E p) (addE p (scalE p (oppK (stype p) (v1 (stype p))) y) x) (addE p (scalE p (oppK (stype p) (v1 (stype p))) y) y) *)
rewrite addE_com, H, addE_com, scal_addE0; auto.
Qed.

(* Recursive equation for multiple product *)
Lemma mprod_S k ks v vs : (k :: ks) *X* (v :: vs) = k .* v + ks *X* vs.
Proof.
assert (Hf: forall ks vs v,
   fold2 (fun k v r => k .* v + r) ks vs v = v + ks *X* vs).
(* Goal: forall (ks : list (K (stype p))) (vs : list (E p)) (v : E p), @eq (E p) (@fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v0 r : E p) => addE p (scalE p k v0) r) ks vs v) (addE p v (mprod ks vs)) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k ks) (@cons (E p) v vs)) (addE p (scalE p k v) (mprod ks vs)) *)
intros ks1; induction ks1 as [| k1 ks1 IH]; simpl.
(* Goal: forall (vs : list (E p)) (v : E p), @eq (E p) v (addE p v (mprod (@nil (K (stype p))) vs)) *)
(* Goal: forall (vs : list (E p)) (v : E p), @eq (E p) match vs with | nil => v | cons b l4 => @fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v0 r : E p) => addE p (scalE p k v0) r) ks1 l4 (addE p (scalE p k1 b) v) end (addE p v (mprod (@cons (K (stype p)) k1 ks1) vs)) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k ks) (@cons (E p) v vs)) (addE p (scalE p k v) (mprod ks vs)) *)
  intros vs1 v1; unfold mprod; simpl; rewrite addE0r; auto.
(* Goal: forall (vs : list (E p)) (v : E p), @eq (E p) match vs with | nil => v | cons b l4 => @fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v0 r : E p) => addE p (scalE p k v0) r) ks1 l4 (addE p (scalE p k1 b) v) end (addE p v (mprod (@cons (K (stype p)) k1 ks1) vs)) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k ks) (@cons (E p) v vs)) (addE p (scalE p k v) (mprod ks vs)) *)
intros [| v' vs1] v1; unfold mprod; simpl.
(* Goal: @eq (E p) v1 (addE p v1 (E0 p)) *)
(* Goal: @eq (E p) (@fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v r : E p) => addE p (scalE p k v) r) ks1 vs1 (addE p (scalE p k1 v') v1)) (addE p v1 (@fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v r : E p) => addE p (scalE p k v) r) ks1 vs1 (addE p (scalE p k1 v') (E0 p)))) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k ks) (@cons (E p) v vs)) (addE p (scalE p k v) (mprod ks vs)) *)
  rewrite addE0r; auto.
rewrite IH; rewrite IH; rewrite addE0r;
  rewrite (fun xx => addE_com xx v1); auto; repeat rewrite addE_assoc; auto;
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  rewrite (fun xx => addE_com xx v1); auto.
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k ks) (@cons (E p) v vs)) (addE p (scalE p k v) (mprod ks vs)) *)
unfold mprod; simpl.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
rewrite Hf; rewrite Hf; rewrite addE0r; rewrite addE0l; auto.
Qed.

Lemma mprod0l vs : nil *X* vs = 0.
Proof. auto. Qed.

Lemma mprod0r ks : ks *X* nil = 0.
Proof. destruct ks as [| k ks]; auto. Qed.

Lemma mprod0 vs1 vs2 : map (fun _ : E p => 0%f) vs1 *X* vs2 = 0.
Proof.
(* Goal: @eq (E p) (mprod (@map (E p) (K (stype p)) (fun _ : E p => v0 (stype p)) vs1) vs2) (E0 p) *)
generalize vs2; clear vs2.
induction vs1 as [| a vs1]; intros [| b vs2]; simpl map; 
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  try rewrite mprod0r; auto.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
rewrite mprod_S; rewrite scalE0l; auto; rewrite addE0l; auto.
Qed.

(* Concation for multiple product *)
Lemma mprod_app ks1 ks2 vs1 vs2 :
   length ks1 = length vs1 -> 
      (ks1 ++ ks2) *X* (vs1 ++ vs2) = ks1 *X* vs1 + ks2 *X* vs2.
Proof.
(* Goal: forall _ : @eq nat (@length (K (stype p)) ks1) (@length (E p) vs1), @eq (E p) (mprod (@app (K (stype p)) ks1 ks2) (@app (E p) vs1 vs2)) (addE p (mprod ks1 vs1) (mprod ks2 vs2)) *)
generalize ks2 vs1 vs2; clear ks2 vs1 vs2.
induction ks1 as [| k ks1 IH]; intros ks2 [| v vs1] vs2 H;
  try discriminate H.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
simpl mprod; unfold mprod; simpl; rewrite addE0l; auto.
simpl app; rewrite mprod_S; rewrite mprod_S; rewrite IH; auto; 
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) z) y) *)
  rewrite addE_assoc; auto.
Qed.

Lemma eqE_spec x y : eq_Spec x y (x ?= y).
Proof.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
generalize (eqE_dec Hp x y); case eqE; constructor; auto.
Qed.

(* Lemmas for free *)

Lemma free_nil : free nil.
Proof.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros [| k ks]; auto.
(* Goal: forall (_ : @eq nat (@length (K (stype p)) (@nil (K (stype p)))) (@length (E p) (@nil (E p)))) (_ : @eq (E p) (mprod (@nil (K (stype p))) (@nil (E p))) (E0 p)) (k : K (stype p)) (_ : @In (K (stype p)) k (@nil (K (stype p)))), @eq (K (stype p)) k (v0 (stype p)) *)
(* Goal: forall (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k ks)) (@length (E p) (@nil (E p)))) (_ : @eq (E p) (mprod (@cons (K (stype p)) k ks) (@nil (E p))) (E0 p)) (k0 : K (stype p)) (_ : @In (K (stype p)) k0 (@cons (K (stype p)) k ks)), @eq (K (stype p)) k0 (v0 (stype p)) *)
intros H1 H2 l Hk; case Hk.
(* Goal: forall (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k ks)) (@length (E p) (@nil (E p)))) (_ : @eq (E p) (mprod (@cons (K (stype p)) k ks) (@nil (E p))) (E0 p)) (k0 : K (stype p)) (_ : @In (K (stype p)) k0 (@cons (K (stype p)) k ks)), @eq (K (stype p)) k0 (v0 (stype p)) *)
intros HH; discriminate HH.
Qed.

Lemma free_cons v vs : free (v::vs) -> free vs.
Proof.
(* Goal: forall _ : free (@cons (E p) v vs), free vs *)
intros Hvs ks Hlks Hpks k Hk.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply (Hvs (0%f::ks)); simpl; auto.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
rewrite mprod_S; rewrite Hpks; rewrite scalE0l; auto; rewrite addE0l; auto.
Qed.

Lemma free_perm vs1 vs2 : perm vs1 vs2 -> free vs2 -> free vs1.
Proof.
(* Goal: forall (_ : @perm (E p) vs1 vs2) (_ : free vs2), free vs1 *)
intros HH Hvs1.
assert (Hf: forall (k1: list _), length k1 = length vs1 ->
  exists (k2:list _), perm k1 k2 /\ k1 *X* vs1 = k2 *X* vs2).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
elim HH; clear vs1 vs2 HH Hvs1; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros l k1 Hk1; exists k1; split; auto.
(* Goal: @perm (K (stype p)) k1 k1 *)
(* Goal: forall (a b : E p) (l : list (E p)) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a (@cons (E p) b l)))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a (@cons (E p) b l))) (mprod k2 (@cons (E p) b (@cons (E p) a l))))) *)
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a l1)) (mprod k2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l2)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l2) (mprod k2 l3)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l3))) *)
(* Goal: free vs1 *)
apply perm_id.
(* Goal: forall (a b : E p) (l : list (E p)) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a (@cons (E p) b l)))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a (@cons (E p) b l))) (mprod k2 (@cons (E p) b (@cons (E p) a l))))) *)
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a l1)) (mprod k2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l2)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l2) (mprod k2 l3)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l3))) *)
(* Goal: free vs1 *)
intros a b vs1 [|k1 [| k2 ks1]] Hl; try discriminate Hl.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists (k2::k1::ks1); split; auto.
(* Goal: @perm (K (stype p)) (@cons (K (stype p)) k1 (@cons (K (stype p)) k2 ks1)) (@cons (K (stype p)) k2 (@cons (K (stype p)) k1 ks1)) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k1 (@cons (K (stype p)) k2 ks1)) (@cons (E p) a (@cons (E p) b vs1))) (mprod (@cons (K (stype p)) k2 (@cons (K (stype p)) k1 ks1)) (@cons (E p) b (@cons (E p) a vs1))) *)
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a l1)) (mprod k2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l2)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l2) (mprod k2 l3)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l3))) *)
(* Goal: free vs1 *)
apply Aux.perm_swap.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
repeat rewrite mprod_S; repeat rewrite <-addE_assoc; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite (addE_com Hp (k1 .* a)); auto.
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a l1)) (mprod k2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l2)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l2) (mprod k2 l3)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l3))) *)
(* Goal: free vs1 *)
intros a vs1 vs2 Hperm IH [| k1 ks1]; intros HH; try discriminate.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
case (IH ks1); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros ks2 (H1ks2, H2ks2); exists (k1::ks2); split; simpl; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply Aux.perm_skip; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
repeat rewrite mprod_S; rewrite H2ks2; auto.
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l2)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l2) (mprod k2 l3)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l3))) *)
(* Goal: free vs1 *)
intros vs1 vs2 vs3 Hp1 IH1 Hp2 IH2 k1 Hk1.
(* Goal: @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 vs1) (mprod k2 vs3))) *)
(* Goal: free vs1 *)
case (IH1 _ Hk1); intros k2 (H1k2, H2k2).
(* Goal: @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 vs1) (mprod k2 vs3))) *)
(* Goal: free vs1 *)
assert (Hk2: length k2 = length vs2).
  rewrite <-(perm_length _ _ _ Hp1);
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  rewrite <-(perm_length _ _ _ H1k2); auto.
(* Goal: @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 vs1) (mprod k2 vs3))) *)
(* Goal: free vs1 *)
case (IH2 _ Hk2); intros k3 (H1k3, H2k3).
(* Goal: @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 vs1) (mprod k2 vs3))) *)
(* Goal: free vs1 *)
exists k3; split.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply Aux.perm_trans with (1 := H1k2); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite H2k2; auto.
(* Goal: free vs1 *)
intros ks Hlks Hpks k Hk.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
case (Hf ks); auto.
(* Goal: forall (x : list (K (stype p))) (_ : and (@perm (K (stype p)) ks x) (@eq (E p) (mprod ks vs1) (mprod x vs2))), @eq (K (stype p)) k (v0 (stype p)) *)
intros ks1 (H1ks1, H2ks1).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply (Hvs1 ks1); auto.
rewrite <-(perm_length _ _ _ HH);
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  rewrite <-(perm_length _ _ _ H1ks1); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite <-H2ks1; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply perm_in with ks; auto.
Qed.

Lemma uniq_free vs : free vs -> uniq vs.
Proof.
(* Goal: forall _ : free vs, @uniq (E p) vs *)
induction vs as [| a vs IH]; intros Hf.
(* Goal: @uniq (E p) (@nil (E p)) *)
(* Goal: @uniq (E p) (@cons (E p) a vs) *)
apply uniq_nil.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply uniq_cons; auto.
(* Goal: not (@In (E p) a vs) *)
(* Goal: @uniq (E p) vs *)
intros HH; case (perm_in_inv _ _ _ HH).
(* Goal: forall (x : list (E p)) (_ : @perm (E p) vs (@cons (E p) a x)), False *)
(* Goal: @uniq (E p) vs *)
intros vs1 Hp1.
(* Goal: False *)
(* Goal: @uniq (E p) vs *)
assert (H1: free (a::a::vs1)).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply free_perm with (a::vs); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply Aux.perm_skip; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply perm_sym; auto.
(* Goal: False *)
(* Goal: @uniq (E p) vs *)
case (one_diff_zero _ sfP).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply (H1 (1%f::(-(1))%f::(map (fun _ => 0%f) vs1))); simpl; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite map_length; auto.
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) (v1 (stype p)) (@cons (K (stype p)) (oppK (stype p) (v1 (stype p))) (@map (E p) (K (stype p)) (fun _ : E p => v0 (stype p)) vs1))) (@cons (E p) a (@cons (E p) a vs1))) (E0 p) *)
(* Goal: @uniq (E p) vs *)
repeat rewrite mprod_S; rewrite mprod0.
(* Goal: @eq (E p) (addE p (scalE p (v1 (stype p)) a) (addE p (scalE p (oppK (stype p) (v1 (stype p))) a) (E0 p))) (E0 p) *)
(* Goal: @uniq (E p) vs *)
rewrite addE0r.
(* Goal: @eq (E p) (addE p (scalE p (v1 (stype p)) x) (scalE p (oppK (stype p) (v1 (stype p))) x)) (E0 p) *)
rewrite <-scal_addEl; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite  oppKr; auto.
(* Goal: @eq (E p) (scalE p (v0 (stype p)) x) (E0 p) *)
rewrite scalE0l; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply IH; apply free_cons with a; auto.
Qed.

Lemma free_incl vs1 vs2 : incl vs1 vs2 -> uniq vs1 -> free vs2 -> free vs1.
Proof.
(* Goal: forall (_ : @incl (E p) vs1 vs2) (_ : @uniq (E p) vs1) (_ : free vs2), free vs1 *)
intros Hi Hu Hf.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
case (perm_incl_inv _ vs1 vs2); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply uniq_free; auto.
(* Goal: forall (x : list (E p)) (_ : @perm (E p) vs2 (@app (E p) vs1 x)), free vs1 *)
intros vs3 H3 ks Hlks Hpks x Hx.
(* Goal: @eq (K (stype p)) x (v0 (stype p)) *)
assert (H1: free (vs1 ++ vs3)).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply free_perm with (1 := perm_sym _ _ _ H3); auto.
(* Goal: @eq (K (stype p)) x (v0 (stype p)) *)
apply (H1 (ks ++ map (fun _ => 0%f) vs3)%list); auto with datatypes.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
repeat rewrite app_length; rewrite map_length; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite mprod_app; auto.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
rewrite Hpks; rewrite addE0l; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite mprod0; auto.
Qed.

(* Lemmas for cbl *)

(* Linear combination  behaves well with inclusion *)
Lemma cbl_incl l1 l2 v : incl l1 l2 -> cbl l1 v -> cbl l2 v.
Proof.
(* Goal: forall (_ : @incl (E p) l1 l2) (_ : cbl l1 v), cbl l2 v *)
intros H1 H2.
(* Goal: cbl l2 v *)
generalize H1; elim H2; clear H1 H2.
(* Goal: cbl l1 (E0 p) *)
(* Goal: forall (x y : E p) (_ : cbl l2 x) (_ : cbl l1 x) (_ : cbl l2 y) (_ : cbl l1 y), cbl l1 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l2 x) (_ : cbl l1 x), cbl l1 (scalE p k x) *)
intros; apply cbl0.
(* Goal: forall (v : E p) (_ : @In (E p) v l1) (_ : @incl (E p) l1 l2), cbl l2 v *)
(* Goal: forall (x y : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : cbl l1 y) (_ : forall _ : @incl (E p) l1 l2, cbl l2 y) (_ : @incl (E p) l1 l2), cbl l2 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : @incl (E p) l1 l2), cbl l2 (scalE p k x) *)
intros; apply cbl_in; auto with datatypes.
(* Goal: forall (x y : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : cbl l1 y) (_ : forall _ : @incl (E p) l1 l2, cbl l2 y) (_ : @incl (E p) l1 l2), cbl l2 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : @incl (E p) l1 l2), cbl l2 (scalE p k x) *)
intros; apply cbl_add; auto.
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l1 x) (_ : forall _ : @incl (E p) l1 l2, cbl l2 x) (_ : @incl (E p) l1 l2), cbl l2 (scalE p k x) *)
intros; apply cbl_scal; auto.
Qed.

Lemma cbl0_inv x : cbl nil x -> x = 0.
Proof. 
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros HH; elim HH; simpl; auto.
(* Goal: forall (v : E p) (_ : @In (E p) v (@nil (E p))), @eq (E p) v (E0 p) *)
(* Goal: forall (x y : E p) (_ : cbl (@nil (E p)) x) (_ : @eq (E p) x (E0 p)) (_ : cbl (@nil (E p)) y) (_ : @eq (E p) y (E0 p)), @eq (E p) (addE p x y) (E0 p) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl (@nil (E p)) x) (_ : @eq (E p) x (E0 p)), @eq (E p) (scalE p k x) (E0 p) *)
intros v [].
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
intros x1 y1 _ H1 _ H2; rewrite H1, H2; rewrite addE0l; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros k x1 _ H1; rewrite H1, scalE0r; auto.
Qed.

(* Multiple products are linear combinations *)
Lemma mprod_cbl l ks : cbl l (ks *X* l).
Proof.
(* Goal: cbl l (mprod ks l) *)
generalize ks; clear ks.
(* Goal: forall ks : list (K (stype p)), cbl l (mprod ks l) *)
induction l as [| x l1 IH].
(* Goal: cbl l1 (E0 p) *)
(* Goal: forall (x y : E p) (_ : cbl l2 x) (_ : cbl l1 x) (_ : cbl l2 y) (_ : cbl l1 y), cbl l1 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l2 x) (_ : cbl l1 x), cbl l1 (scalE p k x) *)
  intros [| k ks]; unfold mprod; simpl; apply cbl0.
(* Goal: forall ks : list (K (stype p)), cbl (@cons (E p) x l1) (mprod ks (@cons (E p) x l1)) *)
intros [| k ks].
(* Goal: cbl l1 (E0 p) *)
(* Goal: forall (x y : E p) (_ : cbl l2 x) (_ : cbl l1 x) (_ : cbl l2 y) (_ : cbl l1 y), cbl l1 (addE p x y) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl l2 x) (_ : cbl l1 x), cbl l1 (scalE p k x) *)
  unfold mprod; simpl; apply cbl0.
(* Goal: cbl (@cons (E p) x l1) (mprod (@cons (K (stype p)) k ks) (@cons (E p) x l1)) *)
rewrite mprod_S; apply cbl_add.
(* Goal: cbl (@cons (E p) x l1) (scalE p k x) *)
(* Goal: cbl (@cons (E p) x l1) (mprod ks l1) *)
apply cbl_scal; apply cbl_in; auto with datatypes.
(* Goal: cbl (@cons (E p) x l1) (mprod ks l1) *)
apply cbl_incl with (2 := IH ks); auto with datatypes.
Qed.

(* Multiple product of a sum *)
Lemma addE_mprod ks1 ks2 vs : length ks1 = length ks2 ->
  map2 (fun k1 k2 => (k1 + k2)%f) ks1 ks2 *X* vs = ks1 *X* vs + ks2 *X* vs.
Proof.
(* Goal: forall _ : @eq nat (@length (K (stype p)) ks1) (@length (K (stype p)) ks2), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) ks1 ks2) vs) (addE p (mprod ks1 vs) (mprod ks2 vs)) *)
generalize ks2 vs; clear ks2 vs.
(* Goal: forall (ks2 : list (K (stype p))) (vs : list (E p)) (_ : @eq nat (@length (K (stype p)) ks1) (@length (K (stype p)) ks2)), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) ks1 ks2) vs) (addE p (mprod ks1 vs) (mprod ks2 vs)) *)
induction ks1 as [| k1 ks1 IH]; intros [| k2 ks2].
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
intros; unfold mprod; simpl; rewrite addE0l; auto.
(* Goal: forall (vs : list (E p)) (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k1 ks1)) (@length (K (stype p)) (@nil (K (stype p))))), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) (@cons (K (stype p)) k1 ks1) (@nil (K (stype p)))) vs) (addE p (mprod (@cons (K (stype p)) k1 ks1) vs) (mprod (@nil (K (stype p))) vs)) *)
(* Goal: forall (vs : list (E p)) (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k1 ks1)) (@length (K (stype p)) (@cons (K (stype p)) k2 ks2))), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) (@cons (K (stype p)) k1 ks1) (@cons (K (stype p)) k2 ks2)) vs) (addE p (mprod (@cons (K (stype p)) k1 ks1) vs) (mprod (@cons (K (stype p)) k2 ks2) vs)) *)
intros vs H; discriminate H.
(* Goal: forall (vs : list (E p)) (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k1 ks1)) (@length (K (stype p)) (@nil (K (stype p))))), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) (@cons (K (stype p)) k1 ks1) (@nil (K (stype p)))) vs) (addE p (mprod (@cons (K (stype p)) k1 ks1) vs) (mprod (@nil (K (stype p))) vs)) *)
(* Goal: forall (vs : list (E p)) (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k1 ks1)) (@length (K (stype p)) (@cons (K (stype p)) k2 ks2))), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) (@cons (K (stype p)) k1 ks1) (@cons (K (stype p)) k2 ks2)) vs) (addE p (mprod (@cons (K (stype p)) k1 ks1) vs) (mprod (@cons (K (stype p)) k2 ks2) vs)) *)
intros vs H; discriminate H.
(* Goal: forall (vs : list (E p)) (_ : @eq nat (@length (K (stype p)) (@cons (K (stype p)) k1 ks1)) (@length (K (stype p)) (@cons (K (stype p)) k2 ks2))), @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) (@cons (K (stype p)) k1 ks1) (@cons (K (stype p)) k2 ks2)) vs) (addE p (mprod (@cons (K (stype p)) k1 ks1) vs) (mprod (@cons (K (stype p)) k2 ks2) vs)) *)
simpl length; intros [| v vs] Hl.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
unfold mprod; simpl; rewrite addE0l; auto.
(* Goal: @eq (E p) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) (@cons (K (stype p)) k1 ks1) (@cons (K (stype p)) k2 ks2)) (@cons (E p) v vs)) (addE p (mprod (@cons (K (stype p)) k1 ks1) (@cons (E p) v vs)) (mprod (@cons (K (stype p)) k2 ks2) (@cons (E p) v vs))) *)
simpl map2; repeat rewrite mprod_S.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite scal_addEl; auto; rewrite IH; auto.
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) z) y) *)
repeat rewrite addE_assoc; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
 apply f_equal2 with (f := addE p); auto.
rewrite addE_com; auto; repeat rewrite addE_assoc; auto; 
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  apply f_equal2 with (f := addE p); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite addE_com; auto.
Qed.

(* Multiple production of a scalar product *)
Lemma scalE_mprod k ks vs : 
 map (fun k1 => (k * k1)%f) ks *X* vs = k .* (ks *X* vs).
Proof.
(* Goal: @eq (E p) (mprod (@map (K (stype p)) (K (stype p)) (fun k1 : K (stype p) => multK (stype p) k k1) ks) vs) (scalE p k (mprod ks vs)) *)
generalize vs; clear vs.
(* Goal: forall vs : list (E p), @eq (E p) (mprod (@map (K (stype p)) (K (stype p)) (fun k1 : K (stype p) => multK (stype p) k k1) ks) vs) (scalE p k (mprod ks vs)) *)
induction ks as [| k1 ks IH].
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros; unfold mprod; simpl; rewrite scalE0r; auto.
(* Goal: forall vs : list (E p), @eq (E p) (mprod (@map (K (stype p)) (K (stype p)) (fun k1 : K (stype p) => multK (stype p) k k1) (@cons (K (stype p)) k1 ks)) vs) (scalE p k (mprod (@cons (K (stype p)) k1 ks) vs)) *)
intros [| v vs].
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
unfold mprod; simpl; rewrite scalE0r; auto.
(* Goal: @eq (E p) (mprod (@map (K (stype p)) (K (stype p)) (fun k1 : K (stype p) => multK (stype p) k k1) (@cons (K (stype p)) k1 ks)) (@cons (E p) v vs)) (scalE p k (mprod (@cons (K (stype p)) k1 ks) (@cons (E p) v vs))) *)
simpl map; repeat rewrite mprod_S.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite scal_multE; auto; rewrite IH; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite scal_addEr; auto.
Qed.

Lemma mprod_perm l1 l2 lk1: perm l1 l2 -> length lk1 = length l1 ->
  exists lk2, perm lk1 lk2 /\ lk1 *X* l1 = lk2 *X* l2.
Proof.
(* Goal: forall (_ : @perm (E p) l1 l2) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2))) *)
intros HH; generalize lk1; elim HH; auto; clear l1 l2 lk1 HH.
(* Goal: @perm (K (stype p)) k1 k1 *)
(* Goal: forall (a b : E p) (l : list (E p)) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a (@cons (E p) b l)))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a (@cons (E p) b l))) (mprod k2 (@cons (E p) b (@cons (E p) a l))))) *)
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 (@cons (E p) a l1)) (mprod k2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l2)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l2) (mprod k2 l3)))) (k1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) k1) (@length (E p) l1)), @ex (list (K (stype p))) (fun k2 : list (K (stype p)) => and (@perm (K (stype p)) k1 k2) (@eq (E p) (mprod k1 l1) (mprod k2 l3))) *)
(* Goal: free vs1 *)
intros l1 lk1 _; exists lk1; split; auto; apply perm_id.
(* Goal: forall (a b : E p) (l : list (E p)) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) (@cons (E p) a (@cons (E p) b l)))), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 (@cons (E p) a (@cons (E p) b l))) (mprod lk2 (@cons (E p) b (@cons (E p) a l))))) *)
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 (@cons (E p) a l1)) (mprod lk2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l2)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l2) (mprod lk2 l3)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l3))) *)
intros a b l1 [| a1 [| b1 lk]] HH; try discriminate HH.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists (b1::a1::lk); split; auto.
(* Goal: @perm (K (stype p)) (@cons (K (stype p)) a1 (@cons (K (stype p)) b1 lk)) (@cons (K (stype p)) b1 (@cons (K (stype p)) a1 lk)) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) a1 (@cons (K (stype p)) b1 lk)) (@cons (E p) a (@cons (E p) b l1))) (mprod (@cons (K (stype p)) b1 (@cons (K (stype p)) a1 lk)) (@cons (E p) b (@cons (E p) a l1))) *)
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 (@cons (E p) a l1)) (mprod lk2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l2)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l2) (mprod lk2 l3)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l3))) *)
apply perm_swap.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite !mprod_S, <-!addE_assoc, (addE_com Hp (a1 .* a)); auto.
(* Goal: forall (a : E p) (l1 l2 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) (@cons (E p) a l1))), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 (@cons (E p) a l1)) (mprod lk2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l2)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l2) (mprod lk2 l3)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l3))) *)
intros a l1 l2 Hp1 IH [|a1 lk1] Hlk1; try discriminate Hlk1.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
case (IH lk1); auto.
(* Goal: forall (x : list (K (stype p))) (_ : and (@perm (K (stype p)) lk1 x) (@eq (E p) (mprod lk1 l1) (mprod x l2))), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) (@cons (K (stype p)) a1 lk1) lk2) (@eq (E p) (mprod (@cons (K (stype p)) a1 lk1) (@cons (E p) a l1)) (mprod lk2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l2)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l2) (mprod lk2 l3)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l3))) *)
intros lk2 (H1lk2, H2lk2).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists (a1 :: lk2); repeat split; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply perm_skip; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite !mprod_S, H2lk2; auto.
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l2)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l2) (mprod lk2 l3)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l3))) *)
intros l1 l2 l3 Hp1 IH1 Hp2 IH2 lk1 Hlk1.
(* Goal: forall (x : list (K (stype p))) (_ : and (@perm (K (stype p)) lk1 x) (@eq (E p) (mprod lk1 l1) (mprod x l2))), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) (@cons (K (stype p)) a1 lk1) lk2) (@eq (E p) (mprod (@cons (K (stype p)) a1 lk1) (@cons (E p) a l1)) (mprod lk2 (@cons (E p) a l2)))) *)
(* Goal: forall (l1 l2 l3 : list (E p)) (_ : @perm (E p) l1 l2) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l2)))) (_ : @perm (E p) l2 l3) (_ : forall (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l2)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l2) (mprod lk2 l3)))) (lk1 : list (K (stype p))) (_ : @eq nat (@length (K (stype p)) lk1) (@length (E p) l1)), @ex (list (K (stype p))) (fun lk2 : list (K (stype p)) => and (@perm (K (stype p)) lk1 lk2) (@eq (E p) (mprod lk1 l1) (mprod lk2 l3))) *)
case (IH1 _ Hlk1); intros lk2 (H1lk2, H2lk2).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
case (IH2 lk2); auto.
rewrite <-(perm_length _ _  _ H1lk2), Hlk1.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply perm_length; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros lk3 (H1lk3, H2lk3); exists lk3; split; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply perm_trans with (1 := H1lk2); auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite H2lk2; auto.
Qed.

(* How to generate the multiple product for a constant *)
Fixpoint lgenk (n: nat) (k: K p) {struct n} : list (K p) :=
  match n  with
    O => nil
  | 1 => k :: nil
  | S n1 => k::lgenk n1 k
  end.

(* The length is ok *)
Lemma lgenk_length n k : length (lgenk n k) = n.
Proof.
(* Goal: @eq nat (@length (K (stype p)) (lgenk n k)) n *)
generalize k; clear k.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
induction n as [| n IH]; simpl; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros k; generalize IH; case n; clear n IH; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros n IH; pattern (S n) at 2; rewrite <- (IH k); auto.
Qed.

(* 0 as a multiple product *)
Lemma genk0_mprod vs :  0 = lgenk (length vs) 0%f *X* vs.
Proof.
induction vs as [| v [| v' vs] IH]; auto;
  simpl lgenk; rewrite mprod_S; rewrite IH; rewrite scalE0l; auto;
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
  rewrite addE0l; auto.
Qed.

(* A linear combination is a multiple product *)
Lemma cbl_mprod vs v : cbl vs v -> 
  exists ks, length ks = length vs /\ v = ks *X* vs.
Proof.
(* Goal: forall _ : cbl vs v, @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) v (mprod ks vs))) *)
intros H; elim H.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists (lgenk (length vs) 0%f); rewrite lgenk_length; split; auto.
(* Goal: @eq (E p) (E0 p) (mprod (lgenk (@length (E p) vs) (v0 (stype p))) vs) *)
(* Goal: forall (v : E p) (_ : @In (E p) v vs), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) v (mprod ks vs))) *)
(* Goal: forall (x y : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))) (_ : cbl vs y) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) y (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
apply genk0_mprod.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros v2; clear H; induction vs as [| v' vs IH]; auto.
(* Goal: forall _ : @In (E p) v2 (@nil (E p)), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) (@nil (E p)))) (@eq (E p) v2 (mprod ks (@nil (E p))))) *)
(* Goal: forall _ : @In (E p) v2 (@cons (E p) v' vs), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) (@cons (E p) v' vs))) (@eq (E p) v2 (mprod ks (@cons (E p) v' vs)))) *)
(* Goal: forall (x y : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))) (_ : cbl vs y) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) y (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
intros HH; absurd (In v2 nil); auto with datatypes.
(* Goal: forall _ : @In (E p) v2 (@cons (E p) v' vs), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) (@cons (E p) v' vs))) (@eq (E p) v2 (mprod ks (@cons (E p) v' vs)))) *)
(* Goal: forall (x y : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))) (_ : cbl vs y) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) y (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
simpl In; intros [H1 | H1].
(* Goal: @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) (@cons (E p) v' vs))) (@eq (E p) v2 (mprod ks (@cons (E p) v' vs)))) *)
(* Goal: @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) (@cons (E p) v' vs))) (@eq (E p) v2 (mprod ks (@cons (E p) v' vs)))) *)
(* Goal: forall (x y : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))) (_ : cbl vs y) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) y (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
  exists (1%f::lgenk (length vs) 0%f); split.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  simpl; rewrite lgenk_length; auto.
  rewrite mprod_S; rewrite scalE1; auto; rewrite <- genk0_mprod; 
(* Goal: @eq (E p) v1 (addE p v1 (E0 p)) *)
(* Goal: @eq (E p) (@fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v r : E p) => addE p (scalE p k v) r) ks1 vs1 (addE p (scalE p k1 v') v1)) (addE p v1 (@fold2 (K (stype p)) (E p) (E p) (fun (k : K (stype p)) (v r : E p) => addE p (scalE p k v) r) ks1 vs1 (addE p (scalE p k1 v') (E0 p)))) *)
(* Goal: @eq (E p) (mprod (@cons (K (stype p)) k ks) (@cons (E p) v vs)) (addE p (scalE p k v) (mprod ks vs)) *)
  rewrite addE0r; auto.
(* Goal: @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) (@cons (E p) v' vs))) (@eq (E p) v2 (mprod ks (@cons (E p) v' vs)))) *)
(* Goal: forall (x y : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))) (_ : cbl vs y) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) y (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
  case IH; auto; intros ks (Hks, Hks1); exists (0%f::ks); split.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  simpl; auto.
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
  rewrite mprod_S; rewrite scalE0l; auto; rewrite addE0l; auto.
(* Goal: forall (x y : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))) (_ : cbl vs y) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) y (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
intros x y Hcx (ks1, (Hlks1, Hks1)) Hcy (ks2, (Hlks2, Hks2)).
(* Goal: @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (addE p x y) (mprod ks vs))) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
exists (map2 (fun k1 k2 => (k1 + k2)%f) ks1 ks2); split.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite map2_length; rewrite min_l; auto.
(* Goal: le (@length (K (stype p)) ks1) (@length (K (stype p)) ks2) *)
(* Goal: @eq (E p) (addE p x y) (mprod (@map2 (K (stype p)) (K (stype p)) (K (stype p)) (fun k1 k2 : K (stype p) => addK (stype p) k1 k2) ks1 ks2) vs) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
rewrite Hlks1; rewrite Hlks2; auto with arith.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite addE_mprod; try rewrite Hks1; try rewrite Hks2; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite Hlks1; auto.
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl vs x) (_ : @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) x (mprod ks vs)))), @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
intros k x Hcx (ks, (Hlks, Hks)).
(* Goal: @ex (list (K (stype p))) (fun ks : list (K (stype p)) => and (@eq nat (@length (K (stype p)) ks) (@length (E p) vs)) (@eq (E p) (scalE p k x) (mprod ks vs))) *)
exists (map (fun k1 => (k * k1)%f) ks); split.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  rewrite map_length; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite scalE_mprod; rewrite Hks; auto.
Qed.

Lemma scalE_add0 x : x + (- (1)) .* x = 0.
Proof.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
pattern x at 1; rewrite <- (fun xx => scalE1 xx x); auto.
(* Goal: @eq (E p) (addE p (scalE p (v1 (stype p)) x) (scalE p (oppK (stype p) (v1 (stype p))) x)) (E0 p) *)
rewrite <-scal_addEl; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite oppKr; auto.
(* Goal: @eq (E p) (scalE p (v0 (stype p)) x) (E0 p) *)
rewrite scalE0l; auto.
Qed.

Lemma scalE_integral k x : k .* x = 0 -> {k = 0%f} + {x = 0}.
Proof.
(* Goal: forall _ : @eq (E p) (scalE p k x) (E0 p), sumbool (@eq (K (stype p)) k (v0 (stype p))) (@eq (E p) x (E0 p)) *)
intros Hk.
(* Goal: sumbool (@eq (K (stype p)) k (v0 (stype p))) (@eq (E p) x (E0 p)) *)
generalize (eqK_dec _ sfP k 0%f); case eqK; auto; intros Hk1.
(* Goal: sumbool (@eq (K (stype p)) k (v0 (stype p))) (@eq (E p) x (E0 p)) *)
right.
(* Goal: @eq (E p) x (E0 p) *)
rewrite <-(scalE1 Hp x).
(* Goal: @eq (E p) (scalE p (v1 (stype p)) x) (E0 p) *)
simpl; rewrite <-(invKr _ sfP _ Hk1).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite scal_multE; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite Hk; rewrite scalE0r; auto.
Defined.

Lemma scalE_opp k1 k2 x : k1 .* ((- (k2)) .* x) = (-k1).* (k2 .* x).
Proof.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite <- scal_multE,  <- opp_multKr, opp_multKl, scal_multE; auto.
Qed.

Lemma scalE_swap k1 k2 x : k1 .* (k2 .* x) = k2 .* (k1 .* x).
Proof.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
repeat rewrite <- scal_multE; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite multK_com; auto.
Qed.

Lemma addE_swap x1 x2 x3 : x1 + (x2 + x3) = x2 + (x1 + x3).
Proof.
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) z) y) *)
rewrite addE_com; auto; repeat rewrite addE_assoc; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply f_equal2 with (f := addE _); auto; rewrite addE_com; auto.
Qed.

Lemma cblnil x : cbl nil x -> x = 0.
Proof. 
(* Goal: forall _ : cbl (@nil (E p)) x, @eq (E p) x (E0 p) *)
intros H; elim H; auto; clear x H.
(* Goal: forall (v : E p) (_ : @In (E p) v (@nil (E p))), @eq (E p) v (E0 p) *)
(* Goal: forall (x y : E p) (_ : cbl (@nil (E p)) x) (_ : @eq (E p) x (E0 p)) (_ : cbl (@nil (E p)) y) (_ : @eq (E p) y (E0 p)), @eq (E p) (addE p x y) (E0 p) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl (@nil (E p)) x) (_ : @eq (E p) x (E0 p)), @eq (E p) (scalE p k x) (E0 p) *)
intros v [].
(* Goal: @eq (E p) (scalE p k (addE p (E0 p) (E0 p))) (scalE p k (E0 p)) *)
intros x y _ Hx _ Hy; rewrite Hx, Hy; rewrite addE0l; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros k x _ Hx; rewrite Hx; rewrite scalE0r; auto.
Qed.

Lemma cbl1 x y : cbl (x::nil) y -> exists k, y = k .* x.
Proof.
(* Goal: forall _ : cbl (@cons (E p) x (@nil (E p))) y, @ex (K (stype p)) (fun k : K (stype p) => @eq (E p) y (scalE p k x)) *)
intros H; elim H; auto; clear y H.
(* Goal: @eq (E p) (scalE p (v0 (stype p)) x) (E0 p) *)
exists 0%f; rewrite scalE0l; auto.
(* Goal: @eq (E p) x (addE p (addE p (scalE p (oppK (stype p) (v1 (stype p))) z) (scalE p (v1 (stype p)) z)) y) *)
simpl; intros v [[]|[]]; exists 1%f; rewrite scalE1; auto.
(* Goal: forall (x0 y : E p) (_ : cbl (@cons (E p) x (@nil (E p))) x0) (_ : @ex (K (stype p)) (fun k : K (stype p) => @eq (E p) x0 (scalE p k x))) (_ : cbl (@cons (E p) x (@nil (E p))) y) (_ : @ex (K (stype p)) (fun k : K (stype p) => @eq (E p) y (scalE p k x))), @ex (K (stype p)) (fun k : K (stype p) => @eq (E p) (addE p x0 y) (scalE p k x)) *)
(* Goal: forall (k : K (stype p)) (x0 : E p) (_ : cbl (@cons (E p) x (@nil (E p))) x0) (_ : @ex (K (stype p)) (fun k0 : K (stype p) => @eq (E p) x0 (scalE p k0 x))), @ex (K (stype p)) (fun k0 : K (stype p) => @eq (E p) (scalE p k x0) (scalE p k0 x)) *)
intros x1 y _ (k1,Hk1) _ (k2,Hk2).
(* Goal: @eq (E p) x (addE p (scalE p (addK (stype p) (oppK (stype p) (v1 (stype p))) (v1 (stype p))) z) y) *)
exists (k1 + k2)%f; subst; rewrite scal_addEl; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros k x1 _ (k1,Hk1); exists (k * k1)%f; rewrite Hk1, scal_multE; auto.
Qed.

End VectorSpace.

Notation " x *X* y " := (mprod _ x y) (at level 40, no associativity): vector_scope.


Section Trans.

Variable p p1 : eparams.
Hypothesis Hp: vparamsProp p.
Hypothesis Hp1: vparamsProp p1.
Variable (f: p -> p1).
Variable (g : stype p -> stype p1).
Variable (g1 : stype p1 -> stype p).
Hypothesis Hf0: f 0%v = 0%v.
Hypothesis Hf1: forall x y : p, (f (x + y) = f x + f y)%v.
Hypothesis Hf2: forall (k: stype p) (x : p), (f (k .* x) = g k .* f x)%v.
Hypothesis Hg: forall k, g (g1 k) = k. 

Lemma cbl_map l v : cbl _ l v -> cbl _ (map f l) (f v).
Proof.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros Hcb; elim Hcb; auto.
(* Goal: cbl p1 (@map (E p) (E p1) f l) (f (E0 p)) *)
(* Goal: forall (v : E p) (_ : @In (E p) v l), cbl p1 (@map (E p) (E p1) f l) (f v) *)
(* Goal: forall (x y : E p) (_ : cbl p l x) (_ : cbl p1 (@map (E p) (E p1) f l) (f x)) (_ : cbl p l y) (_ : cbl p1 (@map (E p) (E p1) f l) (f y)), cbl p1 (@map (E p) (E p1) f l) (f (addE p x y)) *)
(* Goal: forall (k : K (stype p)) (x : E p) (_ : cbl p l x) (_ : cbl p1 (@map (E p) (E p1) f l) (f x)), cbl p1 (@map (E p) (E p1) f l) (f (scalE p k x)) *)
rewrite Hf0; constructor.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros v1 Hv1; constructor; apply in_map; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros; rewrite Hf1; apply cbl_add; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
intros; rewrite Hf2; apply cbl_scal; auto.
Qed.

Lemma cbl_map_inv l v :
 cbl _ (map f l) v -> exists v1, cbl _ l v1 /\ v = f v1.
Proof.
(* Goal: forall _ : cbl p1 (@map (E p) (E p1) f l) v, @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) v (f v1))) *)
assert (exists l1, l1 = map f l).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists (map f l); auto.
(* Goal: forall _ : cbl p1 (@map (E p) (E p1) f l) v, @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) v (f v1))) *)
case H; intros l1 Hl1; rewrite <-Hl1; intros HH.
(* Goal: @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) v (f v1))) *)
generalize Hl1; elim HH; auto; clear HH Hl1.
(* Goal: forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (E0 p1) (f v1))) *)
(* Goal: forall (v : E p1) (_ : @In (E p1) v l1) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) v (f v1))) *)
(* Goal: forall (x y : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : cbl p1 l1 y) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) y (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (addE p1 x y) (f v1))) *)
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
intros H1; exists 0%v; split; auto; constructor.
(* Goal: forall (v : E p1) (_ : @In (E p1) v l1) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) v (f v1))) *)
(* Goal: forall (x y : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : cbl p1 l1 y) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) y (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (addE p1 x y) (f v1))) *)
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
intros v1 Hv1 H1; subst.
(* Goal: @ex (E p) (fun v2 : E p => and (cbl p l v2) (@eq (E p1) v1 (f v2))) *)
(* Goal: forall (x y : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : cbl p1 l1 y) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) y (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (addE p1 x y) (f v1))) *)
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
rewrite in_map_iff in Hv1; case Hv1; intros v2 (H1v2, H2v2); subst.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists v2; split; auto; constructor; auto.
(* Goal: forall (x y : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : cbl p1 l1 y) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) y (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (addE p1 x y) (f v1))) *)
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
intros c y H1 H2 H3 H4 H5.
(* Goal: @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (addE p1 c y) (f v1))) *)
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
case (H2 H5); intros v1 (H1v1, H2v1).
(* Goal: @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (addE p1 c y) (f v1))) *)
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
case (H4 H5); intros v2 (H1v2, H2v2); subst.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists (v1 + v2)%v; split; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply cbl_add; auto.
(* Goal: forall (k : K (stype p1)) (x : E p1) (_ : cbl p1 l1 x) (_ : forall _ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) x (f v1)))) (_ : @eq (list (E p1)) l1 (@map (E p) (E p1) f l)), @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
intros k x H1 H2 H3.
(* Goal: @ex (E p) (fun v1 : E p => and (cbl p l v1) (@eq (E p1) (scalE p1 k x) (f v1))) *)
case (H2 H3); intros v1 (H1v1, H2v1).
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
exists ((g1 k).* v1)%v; split; subst; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
apply cbl_scal; auto.
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
rewrite Hf2, Hg; auto.
Qed.

End Trans.

Structure params: Type := {
 dim:> nat;           (* the dimension of the space *)
 K:> fparams          (* the scalar type *)
}.

Ltac Vrm0 := Krm0;
(* Goal: @eq (E p) (mprod (@nil (K (stype p))) vs) (E0 p) *)
  repeat (rewrite addE0l ||rewrite addE0r || rewrite scalE0l|| rewrite scalE0r); auto.


