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.
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)).
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
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.
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.
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
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.
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
Multiplication of a constant
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
Lift on constant
Lift on add
Lift on scalar multiplication
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.
(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.
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.
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).
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
An element of the base is a generator
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).
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
Conjugate is involutive
Conjugate of 0 is 0
Conjugate of k is -k
removing negation
removing conj_true
Conjugate of a generator g is -g
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].
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
Conjugate of 0 is 0
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.
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
(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.
Lemma join0 (v1 v2: vect 0) : v1 ∨ v2 = (v1 ∨ v2)%f.
0 \/ x = 0
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.
Hint Rewrite join0r: GRm0.
Lemma joinkl n k (x : vect n) : [k] ∨ x = k .* x.
x ∨ 1 = 1
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.
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).
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
g_i \/ g_i = 0
(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.
Lemma conjf_join n (x y: vect n) : (x ∨ y) ^_'f = x ^_'f ∨ y ^_'f.
We are now ready to prove associativity !
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).
(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).
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.
(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.
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.
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
given a list of vectors produce the list of all products
1 is the only element of empty product
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.
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
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).
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).
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
Every vector is a multiple product of all products of the base
Every vector is a linear combination of all products of the base
All products of the base are free
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).
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.
| 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.
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.
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).
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
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).
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.
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).
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)).
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
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].
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.
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]].
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)
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.
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)
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.
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
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).
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 '@((X∨Y)∧ ( 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.