Library VectorSpace

Require Import Setoid Field Min List Aux.

Structure eparams: Type := {
 E:> Set;
 stype:> fparams;
 E0: E;
 eqE: E -> E -> bool;
 addE : E -> E -> E;
 scalE : (K stype) -> E -> E
}.

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.


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.

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.

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;
          
 addE_assoc: forall x y z, (x + y) + z = x + (y + z);
          
 addE_com: forall x y, x + y = y + x;
          
 addE0l: forall x, 0 + x = x;
          
 scalE0l: forall x, 0 .* x = 0;
          
 scalE1: forall x, 1 .* x = x;
          
 scal_addEl: forall k1 k2 x, (k1 + k2) .* x = (k1.* x) + (k2 .* x);
          
 scal_addEr: forall k x y, k .* (x + y) = k .* x + k .* y;
          
 scal_multE: forall k1 k2 x, (k1 * k2) .* x = k1.* (k2 .* x)
          
}.

Variable Hp: vparamsProp.

Lemma eqE_refl x: (x ?= x) = true.

Lemma addE0r: forall x, x + 0 = x.

Let sfP := sProp Hp.

Lemma addE_cancell x y z : z + x = z + y -> x = y.

Lemma addE_cancelr x y z : x + z = y + z -> x = y.

Lemma scalE0r k : k .* 0 = 0.

Opposite for  +
Lemma scal_addE0 x : x + (- (1)) .* x = 0.

Lemma addE_eq_opp x y : x + (-(1)) .* y = 0 -> x = y.

Recursive equation for multiple product
Lemma mprod_S k ks v vs : (k :: ks) *X* (v :: vs) = k .* v + ks *X* vs.

Lemma mprod0l vs : nil *X* vs = 0.

Lemma mprod0r ks : ks *X* nil = 0.

Lemma mprod0 vs1 vs2 : map (fun _ : E p => 0%f) vs1 *X* vs2 = 0.

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.

Lemma eqE_spec x y : eq_Spec x y (x ?= y).

Lemmas for free

Lemma free_nil : free nil.

Lemma free_cons v vs : free (v::vs) -> free vs.

Lemma free_perm vs1 vs2 : perm vs1 vs2 -> free vs2 -> free vs1.

Lemma uniq_free vs : free vs -> uniq vs.

Lemma free_incl vs1 vs2 : incl vs1 vs2 -> uniq vs1 -> free vs2 -> free vs1.

Lemmas for cbl 


Linear combination  behaves well with inclusion
Lemma cbl_incl l1 l2 v : incl l1 l2 -> cbl l1 v -> cbl l2 v.

Lemma cbl0_inv x : cbl nil x -> x = 0.

Multiple products are linear combinations
Lemma mprod_cbl l ks : cbl l (ks *X* l).

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.

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).

Lemma mprod_perm l1 l2 lk1: perm l1 l2 -> length lk1 = length l1 ->
  exists lk2, perm lk1 lk2 /\ lk1 *X* l1 = lk2 *X* l2.

How to generate the multiple product for a constant 


The length is ok
Lemma lgenk_length n k : length (lgenk n k) = n.

0 as a multiple product
Lemma genk0_mprod vs : 0 = lgenk (length vs) 0%f *X* vs.

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.

Lemma scalE_add0 x : x + (- (1)) .* x = 0.

Lemma scalE_integral k x : k .* x = 0 -> {k = 0%f} + {x = 0}.

Lemma scalE_opp k1 k2 x : k1 .* ((- (k2)) .* x) = (-k1).* (k2 .* x).

Lemma scalE_swap k1 k2 x : k1 .* (k2 .* x) = k2 .* (k1 .* x).

Lemma addE_swap x1 x2 x3 : x1 + (x2 + x3) = x2 + (x1 + x3).

Lemma cblnil x : cbl nil x -> x = 0.

Lemma cbl1 x y : cbl (x::nil) y -> exists k, y = k .* x.

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).

Lemma cbl_map_inv l v :
 cbl _ (map f l) v -> exists v1, cbl _ l v1 /\ v = f v1.

End Trans.

Structure params: Type := {
 dim:> nat;
 K:> fparams
}.

Ltac Vrm0 := Krm0;
  repeat (rewrite addE0l ||rewrite addE0r || rewrite scalE0l|| rewrite scalE0r); auto.