Library Grassmann

Require Import ArithRing Div2 Bool Even Setoid Min List Aux Field VectorSpace Kn.

Section Vect.

Variable p : params.
Hypothesis Hp : fparamsProp p.

Delimit Scope g_scope with g.
Open Scope g_scope.
Open Scope vector_scope.

We recover the usual mathematical notation 
Definition K1 := K.
Notation "'K'" := (K1 p) : g_scope.
Notation "'kn'" := (kn p).
Notation projk := (proj p).

Ltac Kfold n :=
     change (Kn.add p n) with (addE (Kn.vn_eparams p n));
     change (Kn.scal p n) with (scalE (Kn.vn_eparams p n));
     change (Kn.genk p n 0%f) with (E0 (Kn.vn_eparams p n)).

A vector is a full-binary tree of hight n 

Equality over two trees: Equality on leaves 

Adding two trees: adding its leaves 

Generate the constant k for the dimension n 
Notation " [ k ] " := (genk _ k%f) (at level 9): g_scope.

Multiplication by a scalar 

Canonical Structure vn_eparams (n: nat) :=
  Build_eparams (vect n) K [0] (eq n) (add n) (scal n).

Definition fn n : vparamsProp (vn_eparams n).
Qed.

Hint Resolve fn.

Notation "1" := ([1]): g_scope.

Ltac Vfold n :=
     change (add n) with (addE (vn_eparams n));
     change (scal n) with (scalE (vn_eparams n));
     change (genk n 0) with (E0 (vn_eparams n)).

Hint Rewrite multK0l multK0r oppK0 addK0l addK0r
             addE0r addE0l scalE0r scalE0l: GRm0.

Ltac Grm0 := autorewrite with GRm0; auto.

Subtraction  

Notation "x - y" := (sub _ x y): g_scope.

Lemma sub_add n (v1 v2: vect n) : v1 - v2 = v1 + (-(1)).* v2.

Lemma sub0l n (v: vect n) : 0 - v = (-(1)) .* v.

Hint Rewrite sub0l: GRm0.

Lemma sub0r n (v: vect n) : v - 0 = v.

Hint Rewrite sub0r: GRm0.

Some properties of constants 
Lemma injk n k1 k2 : [k1] = [k2] :> vect n -> k1 = k2.

Lemma oppk n k : [-k] = (-(1)).* [k] :> vect n.

Lemma genkE n k : [k] = k .* 1 :> vect n.

Lemma deck0 n (x: vect n): x = 0 \/ x <> 0.

Generate the p element of the base in dimension n 

Notation "''e_' p" := (gen _ p) (at level 8, format "''e_' p"): g_scope.

Lemma inj_e n p1 p2 : p1 < n -> p2 < n ->
  'e_p1 = 'e_p2 :> vect n -> p1 = p2.

Get the constant part of a vector 
Fixpoint const (n: nat): (vect n) -> K :=
  match n return vect n -> K with
  | O => fun a => a
  | S n1 => fun l => let (l1,l2) := l in const n1 l2
  end.

Notation "'C[ x ]" := (const _ x).

Lemma const0 n : 'C[ 0: vect n ] = 0%f.

Hint Rewrite const0: GRm0.

Lemma constk n k : 'C[[k]: vect n] = k.

Lemma const_scal n k (x: vect n): 'C[k .* x] = (k * 'C[x])%f.

Lemma const_add n (x1 x2: vect n): 'C[x1 + x2] = ('C[x1] + 'C[x2])%f.

Equality to zero: Equality to zero on leaves 

Notation "x ?= 0" := (eq0 _ x) (at level 70): g_scope.

Equality to zero 
Lemma eq0_dec n (x: vect n) : if x ?= 0 then x = 0 else x <> 0.

Lemma eq0_spec n (x: vect n) : eq_Spec x 0 (x ?= 0).

Lemma eq0I n : ((0: vect n) ?= 0) = true.

Lemma en_def n : 'e_n = 1 :> vect n.

Lemma addk n k1 k2 : [k1] + [k2] = [k1 + k2] :> vect n.

scal is integral 
Lemma scal_integral n k (x: vect n) : k .* x = 0 -> k = 0%f \/ x = 0.

Multiplication of a constant 
Lemma scalk n k1 k2 : k1 .* [k2] = [k1 * k2] :> vect n.

Homogeneity 

Lemma homk0 n k : hom n k 0.

Hint Resolve homk0.

Lemma hom0K n k : hom n 0 [k].

Hint Resolve hom0K.

Lemma const_hom n k x : hom n k x -> 0 < k -> 'C[x] = 0%f.

Lemma hom0E n (x: vect n) : hom n 0 x -> x = ['C[x]].

Lemma hom1e n i : i < n -> hom n 1 'e_i.

Lemma homE n k1 k2 (x: vect n) :
  hom n k1 x -> hom n k2 x -> k1 = k2 \/ x = 0.

Lemma hom_lt n k v : n < k -> hom n k v -> v = 0.

Lemma add_hom n k (x y: vect n) :
  hom n k x -> hom n k y -> hom n k (x + y).

Hint Resolve add_hom.

Lemma scal_hom n k1 k2 (x: vect n) :
  hom n k1 x -> hom n k1 (k2 .* x).

Hint Resolve scal_hom.

Get homogeneity part 

Lemma get_hom0 n m : get_hom n m [0] = [0].

Lemma get_homk0 n k: get_hom n 0 [k] = [k].

Lemma get_homkS n m k: get_hom n m.+1 [k] = [0].

Lemma get_hom_ei n m i : i < n ->
  get_hom n m 'e_i = match m with 1 => 'e_i | _ => [0] end.

Lemma get_hom_scal n m k x :
  get_hom n m (k .* x) = k .* get_hom n m x.

Lemma get_hom_add n m x y :
  get_hom n m (x + y) = get_hom n m x + get_hom n m y.

Lemma get_hom_up n m x : n < m -> get_hom n m x = [0].


Lemma sumEl n f m :
  sum n f m.+1 = f 0%nat + sum n (fun m => f m.+1) m.

Lemma sumEr n f m : sum n f m.+1 = f m.+1 + sum n f m.

Lemma sum_ext (n : nat) (f1 f2: (nat -> vect n)) (m : nat) :
  sum n.+1 (fun m => (f1 m, f2 m)) m = (sum n f1 m, sum n f2 m).

Lemma get_hom_sum n (x : vect n) :
   x = sum n (fun m => get_hom n m x) n.

Lemma hom_get_hom n (x : vect n) m : hom n m (get_hom n m x).

First degre that is used to guess if a vector is homegene 

Lemma first_deg0 n : first_deg n 0 = 0%nat.

Lemma first_deg0i n v : first_deg n v = 0%nat -> hom n 0 v.

Lemma hom_first_deg n k x : x <> 0 -> hom n k x -> first_deg n x = k.

Definition lift (n: nat) (v: vect n) : (vect n.+1) := ((0: vect n), v).

Notation " x ^'l " := (lift _ x) (at level 9, format "x ^'l"): g_scope.

Lift of generator of the base 
Lemma gen_lift n i : 'e_i.+1 = 'e_i^'l :> vect n.+1.

Lift on constant 
Lemma lift_k n k : [k] = [k]^'l :> vect n.+1.

Lift on add 
Lemma lift_add n x y : (x + y)^'l = x^'l + y^'l :> vect n.+1.

Lift on scalar multiplication 
Lemma lift_scal n (k: K) x : (k .* x)^'l = k .* x^'l :> vect n.+1.

Lift on the multiple product 
Lemma lift_mprod (n: nat) (ks: list K) vs : ks *X* map (lift n) vs =
  (ks *X* vs)^'l.

Lemma lift_cbl n l (x: vect n) :
  cbl _ l x -> cbl _ (map (lift n) l) x^'l.

Lemma lift_inj n (x1 x2: vect n) : x1^'l = x2^'l -> x1 = x2.

Dual lift
Definition dlift (n: nat) (v: vect n) : (vect n.+1) := (v,(0: vect n)).

Notation "x ^'dl" := (dlift _ x) (at level 9, format "x ^'dl" ): g_scope.

Lemma dlift_add n x y : (x + y)^'dl = x^'dl + y^'dl :> vect n.+1.

Lemma dlift_scal n (k: K) x : (k .* x)^'dl = k .* x^'dl :> vect n.+1.

Lemma dlift_mprod (n: nat) (ks: list K) vs :
   ks *X* map (dlift n) vs = (ks *X* vs)^'dl.

Coordinates for k vector 
Fixpoint proj (n: nat) k: (vect n) -> (list K) :=
  match n return vect n -> list K with
  | O => fun a =>
          match k with | O => a::nil | _ => nil end
  | S n1 => fun l => let (l1,l2) := l in
          match k with | O => proj n1 k l2 | S k1 =>
           (proj n1 k1 l1 ++ proj n1 k l2)%list
          end
  end.

Lemma proj0 n x : proj n 0 x = 'C[x]:: nil.

Lemma proj_hom0_eq n x y :
  hom n 0 x -> hom n 0 y ->
  nth 0 (proj n 0 x) 0%f = nth 0 (proj n 0 y) 0%f -> x = y.

Lemma proj_lt n m x : n < m -> proj n m x = nil.

Lemma proj_homn_eq n x y :
  hom n n x -> hom n n y ->
  nth 0 (proj n n x) 0%f = nth 0 (proj n n y) 0%f -> x = y.

Fixpoint all (n: nat): vect n :=
  match n return vect n with
  | 0 => 1
  | S n1 => (all n1, 0: vect n1)
  end.

Notation "'E'" := (all _).

Lemma all_hom n : hom n n E.

Hint Resolve all_hom.

Base of k vector 
Fixpoint base (n: nat) k:list (vect n) :=
  match n return list (vect n) with
  | O => match k with | O => 1%f::nil | _ => nil end
  | S n1 =>
          match k with | O =>
                     map (lift n1) (base n1 k) | S k1 =>
           (map (dlift n1) (base n1 k1) ++
            map (lift n1) (base n1 k))%list
          end
  end.

Lemma proj_base_length n (x: vect n) k :
  length (proj n k x) = length (base n k).

Lemma base0 n : base n 0 = 'e_n::nil.

Lemma base_lt_nil m n : m < n -> base m n = nil.

Lemma base_n n : base n n = all n::nil.

Lemma base_length n k : length (base n k) = bin n k.

Lemma base_lift n k : incl (map (lift n) (base n k)) (base n.+1 k).

Lemma base_hom n k v : k <= n -> In v (base n k) -> hom n k v.

Lemma proj_homk n (x: vect n) k :
  hom n k x -> proj n k x *X* base n k = x.

Lemma base_free n k : free _ (base n k).

Each generator is in the base 
Lemma e_in_base1 n i : i < n -> In 'e_i (base n 1).

An element of the base is a generator 
Lemma e_in_base1_ex n v :
  In v (base n 1) -> exists p1, p1 < n /\ v = 'e_p1.

The length of the base is n 
Lemma base1_length n : length (base n 1) = n.

Lemma base1_S n:
  base n.+1 1 = ('e_0: vect n.+1) :: map (lift n) (base n 1).

Lemma base_nil n k : n < k -> base n k = nil.

Lemma cbl1_hom1_equiv n (x: vect n) : cbl _ (base n 1) x <-> hom n 1 x.

Lemma cblk_homk_equiv n k (x: vect n): cbl _ (base n k) x <-> hom n k x.

Lemma cbl_base1_split n x :
 cbl _ (base n.+1 1) x -> exists k, exists y, cbl _ (base n 1) y /\ x = ([k], y).

Lemma cbl_base1_list_split n l:
 (forall x, In x l -> cbl _ (base n.+1 1) x) ->
   exists lk, exists ly,
    (forall i, In i lk -> (fst i) <> 0%f) /\
    (forall i, In i lk -> cbl _ (base n 1) (snd i)) /\
    (forall i, In i ly -> cbl _ (base n 1) i) /\
    perm l ((map (fun x => ([fst x],(snd x))) lk) ++ map (lift n) ly).

Lemma hom_induct n k (P: vect n -> Prop) :
  P 0 -> (forall v, In v (base n k) -> P v) ->
     (forall v1 v2, P v1 -> P v2 -> P (v1 + v2)) ->
     (forall k v, P v -> P (k .* v)) ->
     (forall v, hom n k v -> P v).


Notation "x ^_ b" := (conj _ b x) (at level 30).
Notation "x ^_'t" := (conj _ true x) (at level 30).
Notation "x ^_'f" := (conj _ false x) (at level 30).

Conjugate behave well with the sum 
Lemma conj_add n b (x y: vect n) : (x + y) ^_ b = x ^_ b + y ^_ b.

Conjugate is involutive 
Lemma conj_invo n b (x: vect n) : x ^_ b ^_ b = x.

Conjugate of 0 is 0 
Lemma conj0 n b : 0 ^_ b = (0 : vect n).

Hint Rewrite conj0: GRm0.

Conjugate of k is -k 
Lemma conjk n b k : [k] ^_ b= if b then [-k] else ([k]: vect n).

removing negation 
Lemma conj_neg n b (v: vect n) : v ^_ (negb b) = (-(1)) .* (v ^_ b).

removing conj_true 
Lemma conjt n (v: vect n) : v ^_'t = (-(1)) .* (v ^_'f).

Conjugate of a generator g is -g 
Lemma conj_e n b i : i < n ->
  'e_i ^_ b = if b then ('e_i: vect n) else (- (1)).* 'e_i.

Conjugate behaves well with scalar multiplication 
Lemma conj_scal n b k (x: vect n) : (k .* x) ^_ b = k .* x ^_ b.

Lemma conj_hom n b k (x: vect n) : hom n k x -> hom n k (x ^_ b).

Hint Resolve conj_hom.

Lemma conjf_hom n k (M: vect n) : hom n k M -> M ^_'f = (- (1))^k .* M.

Lemma conjt_hom n k (M: vect n) : hom n k M -> M ^_'t = (- (1))^k.+1 .* M.

Lemma conj_const n b (x: vect n) : 'C[x ^_ b] = if b then (-'C[x])%f else 'C[x].

We can swap add-hoc conjugate 
Lemma conj_swap n b1 b2 (x: vect n) : x ^_ b2 ^_ b1 = x ^_ b1 ^_ b2.

Conjugate of 0 is 0 
Lemma conj_all n b: (E ^_ b) =
   (if b then (-((-(1))^ n))%f else ((-(1))^ n)%f) .* E :> vect n.

We are now ready to define our multiplication 
Fixpoint join (n : nat) : vect n -> vect n -> vect n :=
  match n return (vect n -> vect n -> vect n) with
  | 0%nat => fun x y => (x * y)%f
  | S n1 =>
      fun x y =>
      let (x1, x2) := x in
      let (y1, y2) := y in (join n1 x1 y2 + join n1 (x2 ^_'f) y1,
                             join n1 x2 y2)
  end.

Unicode u2228 
Notation "x '∨' y" := (join _ x y) (at level 40, left associativity): type_scope.

(k.x) \/  y = k. (x \/ y) 
Lemma join_scall n k (x y : vect n) : k .* x y = k .* (x y).

Lemma join0 (v1 v2: vect 0) : v1 v2 = (v1 v2)%f.

0 \/ x = 0 
Lemma join0l n (x : vect n) : 0 x = 0.

Hint Rewrite join0l: GRm0.

x \/ 0  = 0 
Lemma join0r n (x : vect n) : x 0 = 0.

Hint Rewrite join0r: GRm0.

Lemma joinkl n k (x : vect n) : [k] x = k .* x.

x ∨ 1 = 1 
Lemma joinkr n k (x : vect n) : x [k] = k .* x.

1 \/ x  = x 
Lemma join1l n (x : vect n) : 1 x = x.

x \/ 1 = 1 
Lemma join1r n (x : vect n) : x 1 = x.

Lemma join_alll n (x: vect n) : all n x = 'C[x] .* all n.

Lemma join_allr n (x: vect n) : x all n = 'C[x] .* all n.

Lemma join_allhr k n x : hom n k x -> 0 < k -> x E = 0.

Lemma join_allhl k n x : hom n k x -> 0 < k -> E x = 0.

x \/ (k.y) = k. (x \/ y) 
Lemma join_scalr n k (x y : vect n) : x (k .* y) = k .* (x y).

Lemma joink n k1 k2 : [k1] [k2] = [k1 * k2] :> vect n.

Lemma join_e0 n (M : vect n.+1) : 'e_0 M = (snd M, [0]).

Lemma join_ei n i (M : vect n.+1) : i < n ->
  'e_i.+1 M = ((-(1))%f .* ('e_i fst M), 'e_i snd M).

g_i \/ g_j + g_j \/ g_i = 0 
Lemma join_es n i j :
   i < n -> j < n -> 'e_ i 'e_ j + 'e_ j 'e_ i = (0: vect n).

g_i \/ g_i = 0 
Lemma join_e n i : i < n -> 'e_ i 'e_ i = (0 : vect n).

(x + y) \/ z = (x \/ z) + (y \/ z) 
Lemma join_addl n (x y z : vect n) : (x + y) z = x z + y z.

z \/ (x + y) = (z \/ x) + (z \/ y) 
Lemma join_addr n (x y z : vect n) : z (x + y) = z x + z y.

Lemma conjf_join n (x y: vect n) : (x y) ^_'f = x ^_'f y ^_'f.

We are now ready to prove associativity ! 
Lemma join_assoc n (x y z : vect n) : x y z = x (y z).

Anti-commutativity is stable by linear combination 
Lemma cbl_join_com n (vs: list (vect n)) :
  (forall x y, In x vs -> In y vs -> y x = (- (1)).* (x y)) ->
  forall x y, cbl _ vs x -> cbl _ vs y -> y x = (- (1)).* (x y).

Anti-commutativity is true for the base 
Lemma cbl_base_join_com n x y :
 cbl _ (base n 1) x -> cbl _ (base n 1) y -> y x = (- (1)).* (x y).

x*x = 0 is stable by linear combination 
Lemma cbl_join_id n vs :
  (forall x y, In x vs -> In y vs -> join n y x = (- (1)).* (x y)) ->
  (forall x, In x vs -> x x = 0) -> forall x, cbl _ vs x -> x x = 0.

x*x = 0 is true for the base 
Lemma cbl_base_join_id n x : cbl _ (base n 1) x -> x x = 0.

Lemma join_hom1_id n x : hom n 1 x -> x x = 0.

Lift for the production 
Lemma lift_join n x y : lift n (x y) = lift n x lift n y.

Lemma join_hom n k1 k2 (x y: vect n) :
  hom n k1 x -> hom n k2 y -> hom n (k1 + k2) (x y).

Hint Resolve join_hom.

Lemma join_big n k1 k2 (x y : vect n) :
  hom n k1 x -> hom n k2 y -> n < k1 + k2 -> x y = 0.

Lemma const_join n (x y: vect n): 'C[x y] = ('C[x] * 'C[y])%f.

Lemma lift_decomp n (x y: vect n) : (x, y) = 'e_0 x^'l + y^'l.

Base as product 
Lemma base_in n k x: In x (base n k.+1) ->
    exists i, exists y, x = 'e_i y /\ In y (base n k).

given a list of vectors produce the list of all products 

1 is the only element of empty product 
Lemma all_prods_nil n : all_prods n nil = 1 :: nil.

Recursive definition of all products 
Lemma all_prods_cons n v vs :
  all_prods n (v :: vs) = (map (join n v) (all_prods n vs) ++ (all_prods n vs))%list.

1 is always in the list of all products 
Lemma all_prods1 n vs : In (1) (all_prods n vs).

The initial vectors are in the list of all products 
Lemma all_prods_id n vs : incl vs (all_prods n vs).

Lemma all_prods_length n vs :
  length (all_prods n vs) = exp 2 (length vs).

Lift of all products 
Lemma all_prods_lift n vs :
  all_prods n.+1 (map (lift n) vs) = map (lift n) (all_prods n vs).

Lemma all_prods_hom n vs :
  (forall i, In i vs -> exists k, hom n k i) ->
  (forall i, In i (all_prods n vs) -> exists k, hom n k i).

Turn a vector in a list of scalar to be used for multiple product 

The length is 2^n 
Lemma v2l_length n v : length (v2l n v) = exp 2 n.

Every vector is a multiple product of all products of the base 
Lemma mprod_2l n (v: vect n) : v2l n v *X* all_prods n (base n 1) = v.

Every vector is a linear combination of all products of the base 
Lemma cbl_all_prods n v : cbl _ (all_prods _ (base n 1)) v.

All products of the base are free 
Lemma all_prods_free n: free _ (all_prods _ (base n 1)).

Ad-hoc inductive principes for vectors 
Lemma vect_induct n (P: vect n -> Prop) :
  P (1: vect n) -> (forall v, In v (base n 1) -> P v) ->
     (forall v1 v2, P v1 -> P v2 -> P (v1 v2)) ->
     (forall v1 v2, P v1 -> P v2 -> P (v1 + v2)) ->
     (forall k v, P v -> P (k .* v)) ->
     (forall v, P v).

Lemma vect_hom_induct n (P: vect n -> Prop) :
  (forall k v, hom n k v -> P v) ->
  (forall v1 v2, P v1 -> P v2 -> P (v1 + v2)) ->
     (forall v, P v).

Iterated product of a list of vectors 
Fixpoint joinl n (l: list (vect n)) := match l with
| nil => 0
| a::nil => a
| a::l => a joinl n l
end.

Lemma joinl0 n : joinl n nil = 0.

Hint Rewrite joinl0 : GRm0.

Lemma joinl1 n x : joinl n (x::nil) = x.

Lemma joinlS n x l : l <> nil -> joinl n (x::l) = x joinl n l.

Lemma joinl_scal n k (a: vect n) l :
   joinl _ (k .* a::l) = k .* joinl _ (a::l).

Lemma joinl_app n l1 l2 :
  l1 <> nil -> l2 <> nil -> joinl n (l1 ++ l2)%list = joinl n l1 joinl n l2.

Lemma joinl_base1_perm n l1 l2 :
 perm l1 l2 ->
 (forall x, In x l1 -> cbl _ (base n 1) x) ->
  (joinl n l1 = joinl n l2) \/ (joinl n l1 = (-(1)).* joinl n l2) .

Lemma joinl0_base1_perm n l1 l2 : perm l1 l2 ->
 (forall x, In x l1 -> cbl _ (base n 1) x) -> joinl n l1 = 0 -> joinl n l2 = 0.

Lemma lift_joinl n l : lift n (joinl n l) = joinl n.+1 (map (lift n) l).

Lemma joinl_hom1 n l :
 (forall x, In x l -> hom n 1 x) -> hom n (length l) (joinl n l).

Hint Resolve joinl_hom1.

Lemma joinl_swap n (a b: vect n) l:
 cbl _ (base n 1) a -> cbl _ (base n 1) b ->
   joinl _ (a::b::l) = (-(1)).* joinl _ (b::a::l).

Lemma joinl_top n (a: vect n) l1 l2 :
 (forall i, In i (a :: l1) -> cbl _ (base n 1) i) ->
   joinl _ (l1 ++ (a::l2)) = (-(1))^length l1 .* joinl _ (a:: (l1 ++ l2)%list).

Lemma joinl_all n : 0 < n -> joinl n (base n 1) = E.

Definition is_vector n v := cbl _ (base n 1) v.

Definition is_vector_space n l := forall x, In x l -> is_vector n x.

Lemma joinl0_mprod n M : M <> nil -> is_vector_space n M ->
   joinl n M = 0 ->
   exists lk, exists i, length lk = length M /\ In i lk /\ i <> 0%f /\ lk *X* M = 0.

Lemma cbl_joinl0_mprod n M x : is_vector_space n M ->
  cbl _ M x -> joinl n (x::M) = 0.

M is decomposable and l is its decomposition 
Definition decomposable n l M := is_vector_space n l /\ M = joinl n l.

Lemma decomp_cbl n M l x : is_vector n x ->
  decomposable n l M -> M <> 0 -> (x M = 0 <-> cbl _ l x).

Lemma hom1_decomposable n x : hom n 1 x -> decomposable n (x::nil) x.

Lemma decomp_hom n (l: list (vect n)) M : decomposable n l M -> hom n (length l) M.

The linear form is defined by its finger print on the base 


Notation "#< l , x ># " := (contra _ l x) (format "#< l , x >#").

Lemma contraE n l (M : vect n.+1) :
  #<l, M ># =
      ((- (1))%f.* #< snd l, fst M>#, (fst l : K) .* fst M + #<snd l, snd M>#).

Lemma contra0r n lf : #<lf, 0># = (0: vect n).

Hint Rewrite contra0r: GRm0.

Lemma contra0l n (x:vect n) : #<0, x># = 0.

Lemma contrak n i lf : #<lf, [i]># = 0 :> vect n.

Lemma contra_e n i lf : i < n -> #<lf, 'e_i># = [projk _ i lf] :> vect n.

Lemma contra_scalr n k lf (x: vect n) : #< lf, k .* x ># = k .* #< lf , x >#.

Lemma contra_addr n lf (x y: vect n) : #< lf, x + y ># = #< lf, x ># + #< lf, y >#.

Lemma contra_scall n (k : K) (x : kn n) (M : vect n) :
 #< (scalE (Kn.vn_eparams p n) k x), M># = k .* #<x, M>#.

Lemma contra_addl n (x y : kn n) (M : vect n) :
 #< x + y, M ># = #< x, M ># + #<y, M >#.

Lemma contra_conj n lf b (x: vect n) : #< lf, x ^_ b ># = #< lf, x ># ^_ (negb b).

Lemma contra_hom n lf k M : hom n k.+1 M -> hom n k #<lf , M>#.

Hint Resolve contra_hom.

Lemma contra_hom0 n lf M : hom n 0 M -> #<lf , M># = 0.

Lemma contra_id n lf (M: vect n) : #<lf, #< lf, M># ># = 0.

Lemma contra_swap n lf1 lf2 (M: vect n) :
  #<lf1, #< lf2, M># ># = (-(1)).* #<lf2, #< lf1, M># >#.

Fixpoint v2k (n : nat) : vect n -> kn n :=
  match n return vect n -> kn n with
  | O => fun v : vect 0 => tt
  | S n1 => fun v => let (v1,v2) := v in
             ('C[v1], v2k n1 v2)
  end.

Lemma contra_const n lf M : hom n 1 M ->
  #<lf, M># = [(lf [.] v2k n M)%Kn].

Lemma contra_join n lf k1 k2 M1 M2 : hom n k1 M1 -> hom n k2 M2 ->
  #<lf, M1 M2># = #<lf, M1># M2 + ((- (1))^k1).* M1 #<lf, M2>#.

Anti-commutativity for homegeonous vectors, generalization of  cbl_base_prod_com  
Lemma join_hom_com n k1 k2 x y :
 hom n k1 x -> hom n k2 y -> y x = ((- (1)) ^(k1 * k2)).* (x y).

Lemma join_hom_odd n k x : (1+1 <> (0: K))%f -> hom n k x -> odd k -> x x = 0.

Lemma join_hom_id n k x : hom n k x -> odd k -> x x = 0.

Lemma is_vector_space_swap n x l :
  is_vector_space n l -> In x l ->
  exists l1, is_vector_space n (x::l1) /\ joinl n l = joinl n (x::l1).

Fixpoint factor n: (vect n) -> (vect n) -> vect n :=
  match n return vect n -> vect n -> vect n with
  | O => fun x1 x2 => (x2 * x1^-1)%f
  | S n1 =>
        fun x1 x2 =>
        let (x11, x12) := x1 in
        let (x21, x22) := x2 in
        if x12 ?= 0 then
        
        ((0: vect n1), ('C[x11]^-1).* x21: vect n1) else
        let x32 := factor n1 x12 x22 in
          
             
             
             (factor n1 x12 (add n1 (('C[x11]) .* x32: vect n1) (scal n1 (-(1))%f x21: vect n1))
               , x32)
   end.

Lemma factor0 n x : factor n x 0 = 0.

Lemma factor_scal n k x M : factor n x (k .* M) = k .* factor n x M.

Lemma factor_id n x : x <> 0 -> hom n 1 x -> factor n x x = 1.

Lemma factor_hom0E n x1 x2 : x1 <> 0 -> hom n 1 x1 -> hom n 0 x2 ->
  factor n x1 (x1 x2) = x2.

Lemma factor_factor n x1 x2 : hom n 1 x1 -> x1 <> 0 ->
  x1 x2 = 0 -> x2 = x1 factor n x1 x2.

Lemma factork n x k : x <> 0 -> hom n 1 x -> factor n x [k] = 0.

Lemma factor0_hom0 n x1 x2 : x1 <> 0 -> hom n 1 x1 -> hom n 0 x2 ->
  factor n x1 x2 = 0.

Lemma factor_hom n k x1 x2 : x1 <> 0 -> x1 x2 = 0 ->
  hom n 1 x1 -> hom n k.+1 x2 -> hom n k (factor n x1 x2).

Lemma factor_add n k x1 x2 x3 : x1 <> 0 ->
  hom n 1 x1 -> hom n k.+1 x2 -> hom n k.+1 x3 ->
  x1 x2 = 0 -> x1 x3 = 0 ->
  factor n x1 (x2 + x3) = factor n x1 x2 + factor n x1 x3.

Orthogonalité for factorisation, i.e. condition for factorisation to be idempotent 
Fixpoint fortho n : (vect n) -> (vect n) -> bool :=
  match n return vect n -> vect n -> bool with
  | O => fun x1 x2 => false
  | S n1 =>
        fun x1 x2 =>
        let (x11, x12) := x1 in
        let (x21, x22) := x2 in
        if x12 ?= 0 then x21 ?= 0 else fortho n1 x12 x21 && fortho n1 x12 x22
   end.

Lemma fortho0 n : 0 < n -> fortho n 0 0.

Lemma fortho_refl n x : fortho n x x -> x = 0.

Lemma forthok n k1 k2 (v: vect n) : v <> 0 -> hom n k1.+1 v -> fortho n v [k2].

Lemma fortho_scal n k v1 v2 : fortho n v1 v2 -> fortho n v1 (k .* v2).

Lemma fortho_add n v1 v2 v3 :
  fortho n v1 v2 -> fortho n v1 v3 -> fortho n v1 (v2 + v3).

Lemma fortho_conj n b v1 v2 : fortho n v1 v2 -> fortho n v1 (v2 ^_ b).

Lemma fortho_join n v1 v2 v3 :
  fortho n v1 v2 -> fortho n v1 v3 -> fortho n v1 (v2 v3).

Lemma fortho_joinl n k v l : v <> 0 -> hom n k.+1 v ->
  (forall v1, In v1 l -> fortho n v v1) -> fortho n v (joinl n l).

Here we are 
Lemma factor_ortho n x1 x2 : x1 <> 0 -> hom n 1 x1 ->
    fortho n x1 x2 -> factor n x1 (x1 x2) = x2.

Getting the canceling factor for fortho 
Fixpoint fget n : (vect n) -> (vect n) -> K :=
  match n return vect n -> vect n -> K with
  | O => fun x1 x2 => 0%f
  | S n1 =>
        fun x1 x2 =>
        let (x11, x12) := x1 in
        let (x21, x22) := x2 in
        if x12 ?= 0 then (('C[x11])^-1 * 'C[x21])%f else fget n1 x12 x22
   end.

Lemma fget_scal n k x1 x2 : fget n x1 (k .* x2) = (k * fget n x1 x2)%f.

Lemma fortho_fget n x1 x2 : x1 <> 0 -> hom n 1 x1 -> hom n 1 x2 ->
    fortho n x1 (x2 + (-(1) * fget n x1 x2)%f .* x1).

Lemma joinl_addmult n (f: vect n -> vect n -> K) x l :
hom n 1 x -> (forall i, In i l -> hom n 1 i) ->
x joinl n l = x joinl n (map (fun y => (y + (f x y) .* x)) l).

Lemma mprod_hom n k l1 l2 :
  (forall i, In i l2 -> hom n k i) -> hom n k (l1 *X* l2).

Hint Resolve mprod_hom.

Definition is_decomposable n M := exists l, decomposable n l M.

Lemma joinl_factor n x M : x <> 0 -> hom n 1 x ->
  is_decomposable n M -> x M = 0 ->
    exists k, exists l, (forall v, In v l -> hom n 1 v) /\ M = k .* joinl n (x::l).

Lemma decomposable_factor n k x M : x <> 0 -> hom n 1 x -> hom n k.+2 M ->
  is_decomposable n M -> x M = 0 -> is_decomposable n (factor n x M).

A factor of a special degre 
Fixpoint one_factor (n: nat) k : vect n -> vect n :=
  match n return vect n -> vect n with
  | O => fun a => a
  | S n1 => fun l =>
          match k with
          | O => l
          | S k1 =>
            let (l1,l2) := l in
            let r := one_factor n1 k1 l1 in
            (0:vect n1, if r ?= 0 then one_factor n1 k l2 else r)
          end
  end.

Lemma one_factor0 n k : one_factor n k 0 = 0.

Lemma one_factor_hom n k1 k2 (x: vect n) :
 k2 < k1 -> hom n k1 x -> hom n (k1 - k2) (one_factor n k2 x).

Hint Resolve one_factor_hom.

Lemma one_factor_zero n k1 k2 (x: vect n) :
 k2 < k1 -> hom n k1 x -> one_factor n k2 x = 0 -> x = 0.

Iterated contraction 

Definition mcontra n (ll: list (kn n)) (x: vect n) :=
  fold_left (fun x l => #<l,x>#) ll x.

Notation "#<< l , x >>#" := (mcontra _ l x).

Lemma mcontra_nil n (x: vect n) : #<<nil, x>># = x.

Lemma mcontra_cons n (x: vect n) a l : #<<a::l, x>># = #<<l, #<a,x>#>>#.

Lemma mcontra_app n l1 l2 (M: vect n) :
  #<< l1 ++ l2, M>># = #<<l2, #<<l1, M>>#>>#.

Lemma mcontra0 n lfs : #<< lfs, 0 >># = (0: vect n).

Hint Rewrite mcontra0: GRm0.

Lemma mcontra_id n a l (M: vect n) : #<< a::a::l, M>># = 0.

Lemma mcontrak n lfs i : lfs <> nil -> #<< lfs, [i] >># = (0: vect n).

Lemma mcontra_scal n k lfs (x: vect n) : #<< lfs, k .* x >># = k .* #<< lfs , x >>#.

Lemma mcontra_swap n a b l (M: vect n) :
  #<< a::b::l, M>># = (-(1)).* #<<b::a::l, M>>#.

Lemma mcontra_add n lfs (x y: vect n) :
  #<< lfs, x + y >># = #<< lfs, x >># + #<< lfs, y >>#.

Lemma mcontra_conj n lfs b (x: vect n) :
  #<<lfs, x ^_ b >># = #<< lfs, x >># ^_ (iter negb (length lfs) b).

Lemma mcontra_hom n k (x: vect n) l :
  hom n k x -> hom n (k - length l) #<<l, x>>#.

Hint Resolve mcontra_hom.

Lemma mcontra_hom0 n lfs M : lfs <> nil -> hom n 0 M -> #<<lfs , M>># = 0.

Notation liftk := (Kn.lift p).

Lemma lift_contra n lf1 x : #< liftk n lf1, lift n x ># = lift n #<lf1, x>#.

Lemma lift_mcontra n lfs1 x :
  #<< map (liftk n) lfs1, lift n x >># = lift n #<<lfs1, x>>#.

Lemma mcontra_one_factor n k1 k2 (x: vect n) :
  k2 < k1 -> hom n k1 x ->
 exists lfs, length lfs = k2 /\ #<<lfs , x>># = one_factor n k2 x.

Inductive cbl n (l: list (vect n)): nat -> (vect n) -> Prop :=
| cbl_in: forall v, In v l -> cbl n l 0%nat v
| cbl_add: forall k x y, cbl n l k x -> cbl n l k y -> cbl n l k (x + y)
| cbl_scal: forall k k1 x, cbl n l k x -> cbl n l k (k1 .* x)
| cbl_join: forall k v x, In v l -> cbl n l k x -> cbl n l k.+1 (v x).

Lemma cbl_cons n (a: vect n) l k x : cbl n l k x -> cbl n (a::l) k x.

Lemma joinl_join n l (v: vect n) :
  (forall x, In x l -> hom n 1 x) -> In v l -> v joinl n l = 0.

Lemma cbl_joinl n (l: list (vect n)) :
  l <> nil -> (forall x, In x l -> hom n 1 x) -> cbl n l (pred (length l)) (joinl n l).

Lemma cbl_joinl0 n (l: list (vect n)) k x :
  (forall x, In x l -> hom n 1 x) -> cbl n l k x -> x joinl n l = 0.

Lemma cbl_hom n (l: list (vect n)) k x :
  (forall x, In x l -> hom n 1 x) -> cbl n l k x -> hom n k.+1 x.

Lemma cbl_contra n (l: list (vect n)) lf k x :
  (forall x, In x l -> hom n 1 x) -> cbl n l k.+1 x -> cbl n l k #<lf, x>#.

Lemma cbl_mcontra n (l: list (vect n)) lfs k x :
  length lfs <= k ->
  (forall x, In x l -> hom n 1 x) -> cbl n l k x -> cbl n l (k - length lfs) #<<lfs, x>>#.

Lemma decomp_one_factor_hom n (l: list (vect n)) M : l <> nil ->
 decomposable n l M -> hom n 1 (one_factor n (pred (length l)) M).

Lemma decomp_one_factor0 n (l: list (vect n)) M :
 decomposable n l M -> one_factor n (pred (length l)) M = 0 -> M = 0.

Lemma decomp_one_factor_join n (l: list (vect n)) M :
 decomposable n l M -> one_factor n (pred (length l)) M M = 0.

Fixpoint decomposek (n: nat) k (v: vect n) {struct k} : list (vect n) :=
  match k with
  | O => nil
  | S O => v::nil
  | S k1 => let v1 := one_factor n k1 v in
            v1::decomposek n k1 (factor n v1 v)
  end.

Lemma decomposekSS (n: nat) k (v: vect n) :
  decomposek n k.+2 v =
    one_factor n k.+1 v::
       decomposek n k.+1 (factor n (one_factor n k.+1 v) v).

Lemma decomposek_cor n k v :
v <> 0 -> is_decomposable n v -> hom n k v -> decomposable n (decomposek n k v) v.

Definition all_hom1 n l := fold_left (fun c x => c && hom n 1 x) l true.

Lemma all_hom1_cor n l :
 if all_hom1 n l then forall i, In i l -> hom n 1 i else
     exists i, In i l /\ ~ hom n 1 i.

Definition decompose n (v: vect n) : option (list (vect n)) :=
  let d := first_deg n v in
  let l := decomposek n d v in
  if all_hom1 n l then
      if v ?= joinl n l then Some l else None
  else None.

Lemma decompose_cor n v :
   match decompose n v with
   | None => ~ is_decomposable n v
   | Some l => decomposable n l v
   end.

Grade definition 
Definition grade n k x := hom n k x &&
  if decompose n x then true else false.

Lemma gradeE n k x :
  grade n k x <-> hom n k x /\
                   exists l, x = joinl n l /\
                             (forall y, In y l -> hom n 1 y).

Lemma grade0 n k : grade n k 0.

Lemma grade0E n x : grade n 0 x -> x = 0.

Lemma grade_hom n k x : grade n k x -> hom n k x.

Lemma grade1_hom n x : grade n 1 x = hom n 1 x.

Lemma grade_scal n k1 k2 x : grade n k1 x -> grade n k1 (k2 .* x).

Lemma grade_join n k1 k2 x y :
   grade n k1 x -> grade n k2 y -> grade n (k1 + k2) (x y).

Hodge Duality 
Fixpoint dual n : vect n -> vect n :=
  match n return vect n -> vect n with
  | 0 => fun a => a
  | S n1 => fun v => let (x,y) := v in (dual n1 (y ^_'f), dual n1 x)
  end.
Notation "'@ x " := (dual _ x) (at level 9).

Lemma dual0 n : '@0 = 0 :> vect n.

Hint Rewrite dual0: GRm0.

Lemma dual0E n (x: vect n) : '@x = 0 -> x = 0.

Lemma dual_hom n k v : hom n k v -> hom n (n - k) '@v.

Hint Resolve dual_hom.

Lemma dual_scal n k (v: vect n) : '@(k .* v) = k .* '@v.

Lemma dual_add n (v1 v2: vect n) : '@(v1 + v2) = '@v1 + '@v2.

Lemma dual_invo n k (v: vect n): hom n k v -> '@('@v) = (-(1)) ^(k * n.+1) .* v.

Lemma dual_invoE n k (v: vect n) : hom n k v -> v = ((-(1)) ^(k * n.+1)) .* '@('@v).

Lemma dual_all n : '@E = 1 :> vect n.

Lemma dual1 n : '@1 = E :> vect n.

Lemma homn_ex n v : hom n n v -> exists k, v = '@[k].

Lemma dual_base n k v :
  In v (base n k) -> In '@v (base n (n - k)) \/ In ((-(1)) .* '@v) (base n (n - k)).

Ad-hoc conjugate function in order to define the join 

Notation "x ^d_ b" := (dconj _ b x) (at level 29, left associativity).
Notation "x ^d_'t" := (dconj _ true x) (at level 29, left associativity).
Notation "x ^d_'f" := (dconj _ false x) (at level 29, left associativity).

Lemma dconj0 n b : 0 ^d_ b = 0 :> vect n.

Hint Rewrite dconj0: GRm0.

Lemma dconj_all n b :
       E ^d_ b = (if b then (-(1)) .* E else E) :> vect n.

Lemma dconj_scal n b k (x: vect n) : (k .* x)^d_ b = k .* x ^d_ b.

Dual conjugate behave well with the sum 
Lemma dconj_add n b (x y: vect n) : (x + y) ^d_ b = x ^d_ b + y ^d_ b.

Dual conjugate is involutive 
Lemma dconj_invo n b (v: vect n) : v ^d_ b ^d_ b = v.

Lemma dconj_neg n b (v: vect n) : v ^d_ (negb b) = (-(1)) .* (v ^d_ b).

Lemma dconjt n (v: vect n) : v ^d_'t = (-(1)) .* (v ^d_'f).

Lemma dconjf_hom n k (M: vect n) :
  hom n k M -> M ^d_'f = (- (1))^(n + k) .* M.

Lemma dconjt_hom n k (M: vect n) :
 hom n k M -> M ^d_'t = (- (1))^(n + k).+1 .* M.

Lemma dconj_swap n b1 b2 (x: vect n) : x ^d_ b2 ^d_ b1 = x ^d_ b1 ^d_ b2.

Lemma dconj_conj_swap n b1 b2 (x: vect n) : (x ^_ b2) ^d_ b1 = x ^d_ b1 ^_ b2.

Lemma dconj_conj n b (x: vect n) : (x ^_ b) ^d_ b = (-(1))^n .* x.

Lemma dconj_hom n b k (x: vect n) : hom n k x -> hom n k (x ^d_ b).

Hint Resolve dconj_hom.

Lemma dconjf_joinl n (x y: vect n) : (x y) ^d_'f = x ^d_'f y ^_'f.

Lemma dconjf_joinr n (x y: vect n) : (x y) ^d_'f = x ^_'f y ^d_'f.

Lemma conj_dual n b (x: vect n): '@(x ^_ b) = '@x ^d_ b.

Lemma dconj_dual n b (x: vect n) : '@(x ^d_ b) = '@x ^_ b.

Lemma dualk n k : '@([k]) = k .* E :> vect n.

Definition dconst n (x: vect n) := 'C['@x].
Notation "'dC[ x ]" := (dconst _ x).

Lemma dconjk n b k :
  [k] ^d_ b = (if b then [(-(1))^n.+1 * k] else [(-(1))^n * k]:vect n).

Lemma dconj_const n b (x: vect n) :
  'C[x ^d_ b] = (if b then ((-(1))^n.+1 * 'C[x])%f else ((-(1))^n * 'C[x])%f).

Lemma conj_dconst n b (x: vect n) :
  'dC[x ^_ b] = (if b then ((-(1))^n.+1 * 'dC[x])%f else ((-(1))^n * 'dC[x])%f).

Lemma dconj_dconst n b (x: vect n) :
  'dC[x ^d_ b] = (if b then (- 'dC[x])%f else 'dC[x]).

Lemma projn n (x : vect n) : proj n n x = 'dC[x] :: nil.

Lemma dconst_all n : 'dC[(E: vect n)] = 1%f .

Lemma dconst0 n : 'dC[0:vect n] = 0%f.

Hint Rewrite dconst0: GRm0.

Lemma dconst_scal n k (x: vect n) : 'dC[k .* x] = (k * 'dC[x])%f.

Lemma dconst_add n (x1 x2 : vect n) : 'dC[x1 + x2] = ('dC[x1] + 'dC[x2])%f.

Lemma dconst_hom n k x : hom n k x -> n <> k -> 'dC[x] = 0%f.

Lemma homn_all n x : hom n n x -> x = 'dC[x] .* E.

Lemma const_dual n (x: vect n) : 'C['@x] = 'dC[x].

Lemma dconst_dual n (x: vect n) : 'dC['@x] = 'C[x].

Defining the meet 
Fixpoint meet (n : nat) : vect n -> vect n -> vect n :=
  match n return (vect n -> vect n -> vect n) with
  | 0%nat => fun a b => (a * b)%f
  | S n1 =>
      fun v1 v2 =>
      let (x1, y1) := v1 in
      let (x2, y2) := v2 in (meet n1 x1 x2,
                                meet n1 x1 y2 +
                                meet n1 y1 (x2 ^d_'f))
  end.

unicode 2227 
Notation "x '∧' y" := (meet _ x y) (at level 45, left associativity).

Lemma meet0l n (x: vect n) : 0 x = 0.

Hint Rewrite meet0l: GRm0.

Lemma meet0r n (x: vect n) : x 0 = 0.

Hint Rewrite meet0r: GRm0.

Lemma meet1l n (x: vect n) : 1 x = ['C['@x]].

Lemma meet1r n (x: vect n) : x 1 = ['C['@x]].

(k.x) ∧ y = k. (x ∧ y) 
Lemma meet_scall n k (x y : vect n) : k .* x y = k .* (x y).

x ∧ (k . y) = k. (x ∧ y) 
Lemma meet_scalr n k (x y : vect n) : x k .* y = k .* (x y).

Lemma meet0 (v1 v2 : vect 0) : v1 v2 = (v1 * v2)%f.

Lemma meetS n (x1 x2 y1 y2 : vect n) :
 ((x1,y1): vect n.+1) (x2,y2) =
  (x1 x2, x1 y2 + y1 (x2 ^d_'f)).

Lemma dual_meet n (v1 v2 : vect n) : '@(v1 v2) = '@v1 '@v2.

Lemma conjf_meetl n (x y : vect n) : (x y) ^_'f = x ^_'f y ^d_'f.

Lemma conjf_meetr n (x y : vect n) : (x y) ^_'f = x ^d_'f y ^_'f.

Lemma dconjf_meet n (x y : vect n) : (x y) ^d_'f = x ^d_'f y ^d_'f.

Lemma dconjf_meetd n (x y : vect n) : (x y) ^d_'f = x ^_'f y ^_'f.

Lemma dconst_meet n (x y: vect n) : 'dC[x y] = ('dC[x] * 'dC[y])%f.

Lemma dual_join n (v1 v2: vect n) : '@(v1 v2) = '@v1 '@v2.

(x + y) ∧ z = (x ∧ z) + (y ∧ z) 
Lemma meet_addl n (x y z : vect n) : (x + y) z = x z + y z.

z ∧ (x + y) = (z ∧ x) + (z ∧ y) 
Lemma meet_addr n (x y z : vect n) : z (x + y) = z x + z y.

Lemma meet_assoc n (x y z : vect n) : x y z = x (y z).

Lemma meet_alll n (x: vect n) : all n x = x.

Lemma meet_allr n (x: vect n) : x all n = x.

By duality 
Lemma meet_small n k1 k2 (x y : vect n) :
  hom n k1 x -> hom n k2 y -> k1 + k2 < n -> x y = 0.

By duality 
Lemma meet_hom n k1 k2 (x y : vect n) :
  hom n k1 x -> hom n k2 y -> hom n (k1 + k2 - n) (x y).

Hint Resolve meet_hom.

Lemma meetkl0 n k1 k2 x : hom n k1 x -> n <> k1 -> [k2] x = 0.

Lemma meetkl n k x : hom n n x -> [k] x = [k * 'dC[x]].

Lemma meetkr0 n k1 k2 x : hom n k1 x -> n <> k1 -> x [k2] = 0.

Lemma meetkr n k x : hom n n x -> x [k] = ['dC[x] * k].

Lemma meet_hom_com n k1 k2 (x y : vect n) :
  hom n k1 x ->
  hom n k2 y -> y x = ((- (1))^((n + k1) * (n + k2))).* (x y).

Lemma meet_hom_id n k x : hom n k x -> odd (n - k) -> x x = 0.

Lemma dual_join_compl n k v :
  In v (base n k) -> (v '@v = all n) \/ v '@v = (-(1)) .* all n.

Lemma join01E n x y : hom n 1 x -> hom n 1 y ->
   x y = 0 -> exists k, x = k .* y \/ y = k .* x.

Lemma homn_1 n k1 k2 x y :
  hom n k1 x -> hom n k2 y -> n = (k1 + k2)%nat -> x y = 'dC[x y] .* 1.

Lemma join2_meetE n k1 k2 (x y : vect n) :
  hom n k1 x -> hom n k2 y -> n <= k1 + k2 -> x y = (x y) E.

Lemma join_meet_swap n k1 k2 k3 (x y z : vect n) :
   hom n k1 x -> hom n k2 y -> hom n k3 z -> (k1 + k2 + k3 = n)%nat ->
    x (y z) = (x y) z.

Lemma join3_meetE n k1 k2 (x y z : vect n) :
  hom n n x -> hom n k1 y -> hom n k2 z -> n <= k1 + k2 ->
  x (y z) = (x y z) E.

Lemma splitlr n k1 k2 x y z : hom n k1 x -> hom n 1 y -> hom n k2 z ->
  (x y) z = (-(1))^(n + (k1 + k2).+1) .* (x (y z)) +
                         (x z) y.

Lemma splitll n k1 k2 x y z : hom n k1 x -> hom n 1 y -> hom n k2 z ->
  (y x) z = (-(1))^(n + k2.+1) .* ((x (y z)) - y (x z)).

Lemma splitrr n k1 k2 x y z : hom n k1 x -> hom n 1 y -> hom n k2 z ->
  z (x y) = (-(1))^(n + k2.+1) .* ((z y) x - (z x) y).

Lemma splitrl n k1 k2 x y z : hom n k1 x -> hom n 1 y -> hom n k2 z ->
  z (y x) = (-(1))^(n + (k1 + k2).+1) .* (z y) x + y (z x).

Lemma inter n k1 k2 x y z : hom n 1 x -> hom n k1 y -> hom n k2 z ->
  x y = 0 -> x z = 0 -> x (y z) = 0.

Lemma join_meet_distrl n k1 k2 x y z :
   hom n k1 x -> hom n 1 y -> hom n k2 z ->
    y (x z) = (-(1))^(n + k2) .* ((y x) z) + x (y z).

Lemma meet_join_distrl n k1 k2 x y z :
  hom n k1 x -> hom n 1 y -> hom n k2 z ->
  '@y (x z) = (-(1))^k2 .* (('@y x) z) + x ('@y z).

Lemma grade_dual n k x : k < n -> grade n k x -> grade n (n - k) '@x.

Lemma grade_meet n k1 k2 x y : n < k1 + k2 ->
  grade n k1 x -> grade n k2 y -> grade n (k1 + k2 - n) (x y).

Defining the natural injection of Kn in Gn 

Definition Kn := kn p.


Notation "'v_ x" := (k2g _ x) (at level 9).
Notation "'kn n" := (vn_eparams p (pred n)) (at level 10).

Lemma k2g0 n : 'v_0 = 0 :> vect n.

Lemma k2g_add n x y : 'v_(x + y) = 'v_x + 'v_y :> vect n.

Lemma k2g_scal n k x : 'v_(k .* x) = (k: K) .* 'v_x :> vect n.

Lemma k2g_unit n i : i < n -> 'v_('e_i)%Kn = 'e_i :> vect n.

Lemma k2g_hom n x : hom n 1 ('v_x).

Lemma hom1E n x : hom n 1 x -> exists y, x = 'v_y.

Lemma k2glift n x : 'v_(Kn.lift p n x) = ('v_x)^'l.

Lemma pscal_join n x y : 'v_x '@('v_y) = ((x [.] y)%Kn:K) .* E :> vect n.

Lemma pscal_meet n x y : 'v_x '@('v_y) = ((x [.] y)%Kn:K) .* 1 :> vect n.

Definition V0 := genk (dim p) 0.
Definition V1 := genk (dim p) 1.
Definition Vect := vect p.
Definition Veq: Vect -> Vect -> bool := eq p.
Definition Vadd: Vect -> Vect -> Vect := add p.
Definition Vscal: K -> Vect -> Vect := scal (dim p).
Definition Vgen := gen p.
Definition Vgenk := genk p.
Definition Vconj: bool -> Vect -> Vect := conj (dim p).
Definition Vjoin: Vect -> Vect -> Vect := join (dim p).
Definition Vmeet: Vect -> Vect -> Vect := meet (dim p).
Definition Vcontra: Kn -> Vect -> Vect := contra (dim p).
Definition Vdual: Vect -> Vect := dual (dim p).
Definition Vdecompose: Vect -> option (list Vect) := decompose (dim p).
Definition K2G: Kn -> Vect := k2g p.

Definition v_eparams :=
  Build_eparams Vect K V0 Veq Vadd Vscal.

Definition f: vparamsProp (Kn.v_eparams p) := (Kn.fn p Hp p).

End Vect.

Delimit Scope Gn_scope with Gn.
Notation " 'e_ p" := (gen _ _ p) : Gn_scope.
Notation " [ k ] " := (genk _ _ k) (at level 9) : Gn_scope.

Require Import QArith.

Open Scope Q_scope.

Definition Qparams (n:nat) := Build_params
   n
  (Build_fparams
  Q
  0%Q
  1%Q
 Qeq_bool
 Qopp
 Qplus
 Qmult
 Qinv)
.

Module Ex2D.

Q in 2 D 

Let p := Qparams 2.

Notation "[[ X: x , Y: y , X**Y: xy ]]" := ((xy,x),(y,0)).

Definition X := (Vgen p 0).
Eval compute in X.
Definition Y := (Vgen p 1).
Eval compute in Y.

Notation "x '∨' y" := (Vjoin p x y) (at level 40, left associativity).
Notation "x + y" := (Vadd p x y).
Notation "k .* x" := (Vscal p k x).
Notation "x '∧' y" := (Vmeet p x y) (at level 40, left associativity).
Notation "'@ x" := (Vdual p x) (at level 100).

Eval vm_compute in (X Y) (X Y).

Eval vm_compute in '@(X + Y).

Eval vm_compute in (X + Y) '@(X + Y).

End Ex2D.

Module Ex3D.

Q in 3 D 

Let p := Qparams 3.

Notation "[[ X: x , Y: y , Z: z , X**Y: xy , Y**Z: yz , X**Z: xz , X**Y**Z: xyz ]]" :=
  ((((xyz,xy),(xz,x)), ((yz,y),(z,0)))).

Definition X := (Vgen p 0).
Eval compute in X.
Definition Y := (Vgen p 1).
Eval compute in Y.
Definition Z := (Vgen p 2).
Eval compute in Z.

Notation "x '∨' y" := (Vjoin p x y) (at level 40, left associativity).
Notation "x + y" := (Vadd p x y).
Notation "k .* x" := (Vscal p k x).
Notation "x '∧' y" := (Vmeet p x y) (at level 40, left associativity).
Notation "'@ x" := (Vdual p x) (at level 100).

Eval vm_compute in '@(Vgen p 3).

Eval vm_compute in (X Z) (Y Z).

Eval vm_compute in '@((XY)∧ ( Z)).

Eval vm_compute in (X + Y) '@(X + Y).

Eval vm_compute in Vdecompose p ((X Y) (Y Z)).

Eval vm_compute in Vdecompose p ((X + Y) (X + Z)).

Eval vm_compute in Vdecompose p ((X + Y + Z) (X + Z) (X + Y)).

Eval vm_compute in Vdecompose p ((X + Y) (Y + Z)).

Eval vm_compute in (X + Y) (X + Z) +
  (-1#1)%Q .* (((-1#1)%Q .* Y + Z) ((-1#1)%Q .* (X + Y))).

Eval vm_compute in ((-1#1)%Q .* Y + Z) (X + Y) (X + Z).

Eval vm_compute in (X Y Z) (X Y Z).
Eval vm_compute in (X + Y + Z) (X + Y + Z).
Eval vm_compute in Z Y X.
Eval vm_compute in X Z.
Eval vm_compute in Z X.
Eval vm_compute in X Y Z.
Eval vm_compute in Z X Y.
Eval vm_compute in Y X Z.
Eval vm_compute in Y X.

End Ex3D.

Module Ex4D.

Q in 4 D 

Let p := Qparams 4.

Notation " '[[' 'X:' x ',' 'Y:' y ',' 'Z:' z , 'T:' t ',' 'X**Y:' xy ',' 'X**Z:' xz ',' 'X**T:' xt ',' 'Y**Z:' yz ',' 'Y**T:' yt ',' 'Z**T:' zt ',' 'X**Y**Z:' xyz ',' 'X**Y**T:' xyt ',' 'X**Z**T:' xzt ',' 'Y**Z**T:' yzt ',' 'X**Y**Z**T:' xyzt ',' 'K:' vv ']]'" :=
 ((((xyzt, xyz), (xyt, xy)), ((xzt, xz), (xt, x))) ,
  (((yzt, yz), (yt, y)), ((zt,z), (t, vv)))).

Definition X := (Vgen p 0).
Eval compute in X.
Definition Y := (Vgen p 1).
Eval compute in Y.
Definition Z := (Vgen p 2).
Eval compute in Z.
Definition T := (Vgen p 3).
Eval compute in T.

Notation "x '∨' y" := (Vjoin p x y) (at level 40, left associativity).
Notation "x + y" := (Vadd p x y).
Notation "k .* x" := (Vscal p k x).
Notation "x '∧' y" := (Vmeet p x y) (at level 40, left associativity).
Notation "'@ x" := (Vdual p x) (at level 100).
Notation "#< l , x ># " := (Vcontra p l x).

Eval vm_compute in '@X.

Eval vm_compute in (X + Y) '@(X + Y).

Definition X' := (1, (0, (0, (0, tt)))).
Definition Y' := (0, (1, (0, (0, tt)))).
Definition Z' := (0, (0, (1, (0, tt)))).
Definition T' := (0, (0, (0, (1, tt)))).

Definition U := (X + Y) Z.

Eval vm_compute in U.

Definition fxy := #<Y', #< X', U ># >#.
Definition fxz := #<Z', #< X', U ># >#.
Definition fxt := #<T', #< X', U ># >#.
Definition fyz := #<Z', #< Y', U ># >#.
Definition fyt := #<T', #< Y', U ># >#.
Definition fzt := #<T', #< Z', U ># >#.

Eval vm_compute in fxy.

Eval vm_compute in #< Y', X>#.

Eval vm_compute in (X Y Z) (X Y Z).

Eval vm_compute in (X + Y + Z) (X + Y + Z).
Eval vm_compute in Z Y X.
Eval vm_compute in X Z.
Eval vm_compute in Z X.
Eval vm_compute in X Y Z.
Eval vm_compute in Z X Y.
Eval vm_compute in Y X Z.
Eval vm_compute in Y X.
Eval vm_compute in X T.
Eval vm_compute in T X.

Eval vm_compute in Vconj p false (Z T) (X Y).

Eval vm_compute in (X Y Z T) (X Y Z T).

End Ex4D.

Module Ex5D.

Q in 5 D 

Let p := Qparams 5.

Notation " [[ X: x , Y: y , Z: z , T: t , U: u , X**Y: xy , X**Z: xz , X**T: xt , X**U: xu , Y**Z: yz , Y**T: yt , Y**U: yu , Z**T: zt , Z**U: zu , T**U: tu , X**Y**Z: xyz , X**Y**T: xyt , X**Y**U: xyu , X**Z**T: xzt , X**Z**U: xzu , X**T**U: xtu , Y**Z**T: yzt , Y**Z**U: yzu , Y**T**U: ytu , Z**T**U: ztu , X**Y**Z**T: xyzt , X**Y**Z**U: xyzu , X**Y**T**U: xytu , X**Z**T**U: xztu , Y**Z**T**U: yztu , X**Y**Z**T**U: xyztu , 'K:' vv ]]" :=
(
 ((((xyztu, xyzt), (xyzu, xyz)), ((xytu, xyt), (xyu, xy))) ,
  (((xztu, xzt), (xzu, xz)), ((xtu,xt), (xu, x)))),
 ((((yztu, yzt), (yzu, yz)), ((ytu, yt), (yu, y))) ,
  (((ztu, zt), (zu, z)), ((tu,t), (u, vv))))).

Definition X := (Vgen p 0).
Eval compute in X.
Definition Y := (Vgen p 1).
Eval compute in Y.
Definition Z := (Vgen p 2).
Eval compute in Z.
Definition T := (Vgen p 3).
Eval compute in T.
Definition U := (Vgen p 4).
Eval compute in U.

Notation "x '∨' y" := (Vjoin p x y) (at level 40, left associativity).
Notation "x + y" := (Vadd p x y).
Notation "k .* x" := (Vscal p k x).
Notation "x '∧' y" := (Vmeet p x y) (at level 40, left associativity).
Notation "'@ x" := (Vdual p x) (at level 100).

Eval vm_compute in Vconj p false (T U) (X Y Z).
Eval vm_compute in Vconj p false (X Y Z T U).

End Ex5D.

Module Ex6D.

Q in 6 D 

Let p := Qparams 6.

Definition X := (Vgen p 0).
Eval compute in X.
Definition Y := (Vgen p 1).
Eval compute in Y.
Definition Z := (Vgen p 2).
Eval compute in Z.
Definition T := (Vgen p 3).
Eval compute in T.
Definition U := (Vgen p 4).
Eval compute in U.
Definition K := (Vgen p 5).
Eval compute in K.

Notation "x '∨' y" := (Vjoin p x y) (at level 40, left associativity).
Notation "x + y" := (Vadd p x y).
Notation "k .* x" := (Vscal p k x).
Notation "x '∧' y" := (Vmeet p x y) (at level 40, left associativity).
Notation "'@ x" := (Vdual p x) (at level 100).

Eval vm_compute in
  ((X (Y Z T)) + (U K))
  ((X (Y Z T)) + (U K)).

Eval vm_compute in Vconj p false (T U) (X Y Z).
Eval vm_compute in Vconj p false (X Y Z T U).

Eval vm_compute in
  ((X T) + (Y Z)) ((X T) + (Y Z)).

End Ex6D.