Library G3

Require Import Div2 Bool Even Setoid Min List Aux Field VectorSpace Grassmann.
Require Import Field_tac.

Section Vect.

Our Field 

Variable F: fparams.

Hypothesis FT:
  @field_theory (Field.K F) (v0 F) (v1 F) (addK F) (multK F)
        (fun x y => (addK F) x (oppK F y)) (oppK F)
        (fun x y => (multK F) x (invK F y)) (invK F) (@Logic.eq F).
Add Field Kfth : FT.

  Instanciation of Grassman for n = 3                                      

Definition Pp: params := {| dim := 3; K := F |}.
Variable HP : fparamsProp Pp.

SubClass point := Kn Pp.
SubClass vect := Vect Pp.

Definition Vjoin (x y : vect): vect := Vjoin Pp x y.
Notation "x '∨' y" := (Vjoin x y) (at level 40, left associativity).
Definition Vadd (x y : vect): vect := Vadd Pp x y.
Notation "x + y" := (Vadd x y).
Definition Vsub (x y : vect): vect := sub Pp Pp x y.
Notation "x - y" := (Vsub x y).
Definition Vscal (k : F) (x : vect): vect := Vscal Pp k x.
Notation "k .* x" := (Vscal k x).
Definition Vmeet (x y : vect): vect := Vmeet Pp x y.
Notation "x '∧' y" := (Vmeet x y) (at level 45, left associativity).
Definition Vdual (x : vect): vect := Vdual Pp x.
Notation "'@ x" := (Vdual x) (at level 9).
Definition Veq (x y : vect): bool := Veq Pp x y.
Notation "x ?= y" := (Veq x y).
Definition Vgenk (k : F): vect := (Vgenk Pp k).
Notation "0" := (Vgenk 0%f).
Notation "1" := (Vgenk 1%f).
Definition hom (n: nat) (x : vect) := (hom Pp Pp n x).
Notation "'dC[ x ]" := (dconst Pp 3 x).
Notation "'C[ x ]" := (const Pp 3 x).
Notation "'E'" := (all Pp 3: vect).

Coercion p2v (x : point) := (K2G Pp x): vect.

Let scal0l x : 0%f .* x = 0.

Let scal1l x : 1%f .* x = x.

Let scal_integral k x : k .* x = 0 -> {k = 0%f} + {x = 0}.

Lemma sub_add x y : x - y = x + (-(1))%f .* y.

Lemma join1l x : 1 ∨ x = x.

Lemma join1r x : x ∨ 1 = x.

Lemma join_addl x y z : (x + y) ∨ z = x ∨ z + y ∨ z.

Lemma join_addr x y z : z ∨ (x + y) = z ∨ x + z ∨ y.

Lemma join_scall k x y : k .* x ∨ y = k .* (x ∨ y).

Lemma join_scalr k x y : x ∨ (k .* y) = k .* (x ∨ y).

Theorem join_swap (x y : point) : x ∨ y = (-(1))%f .* (y ∨ x).

Let join_id: forall (x : point), x ∨ x = 0.

Let add_com x y : x + y = y + x.

Let add_assoc x y z : x + y + z = x + (y + z).

Let add0l x : 0 + x = x.

Let add0r x : x + 0 = x.

Let scal_mul k1 k2 x : (k1 * k2)%f .* x = k1.* (k2 .* x).

Let scal0r k : k .* 0 = 0.

Let join0r x : x ∨ 0 = 0.

Let join0l x : 0 ∨ x = 0.

Let join_assoc x y z : (x ∨ y) ∨ z = x ∨ (y ∨ z).

Let scal_addl k1 k2 x : (k1 + k2)%f .* x = k1.* x + (k2 .* x).

Let scal_addr k x y : k .* (x + y) = k.* x + (k .* y).

Let scal_mult k1 k2 x : (k1 * k2)%f .* x = k1 .* (k2 .* x).

Let meet_assoc x y z : (x ∧ y) ∧ z = x ∧ (y ∧ z).

Let meet_alll x : (E ∧ x) = x.

Let meet_allr x : (x ∧ E) = x.

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

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

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

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

Lemma hom3_1 k1 k2 x y : hom k1 x -> hom k2 y -> 3 = (k1 + k2)%nat ->
   x ∧ y = 'dC[ x ∨ y] .* 1.

Lemma splitrr k1 k2 x y z : hom k1 x -> hom 1 y -> hom k2 z ->
  z ∧ (x ∨ y) = ((-(1))^(3 + k2.+1))%f .* ((z ∨ y) ∧ x - (z ∧ x) ∨ y).

Lemma dual_invoE k v: hom k v -> v = ((-(1)) ^(k * 3.+1))%f .* '@('@v).

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

Lemma const1 x : 'C[x .* 1] = x.

  Definition of the bracket operator                                       

Definition bracket x y z : F := 'dC[x ∨ y ∨ z].

Notation "'E'" := (all Pp 3: vect).
Notation "'[ x , y , z ]" := (bracket x y z).

A tactic to prove homogeneity                                              

Lemma hom3E: hom 3 E.

Lemma hom3l x y : hom 1 x -> hom 2 y -> hom 3 (x ∨ y).

Lemma hom3r x y : hom 2 x -> hom 1 y -> hom 3 (x ∨ y).

Lemma hom2 x y : hom 1 x -> hom 1 y -> hom 2 (x ∨ y).

Lemma hom1p (x : point) : hom 1 x.

Lemma hom1d x y : hom 2 x -> hom 2 y -> hom 1 (x ∧ y).

Lemma hom0l x y : hom 1 x -> hom 2 y -> hom 0 (x ∧ y).

Lemma hom0r x y : hom 2 x -> hom 1 y -> hom 0 (x ∧ y).

Lemma hom0p x y : hom 0 x -> hom 0 y -> hom 0 (x ∨ y).

Lemma hom01 : hom 0 1.

Lemma hom0_E x : hom 0 x -> x ∨ E = 0 -> x = 0.

Lemma homd k x : hom k x -> hom (3 - k) '@x.

Ltac homt :=
  first [ apply scal_hom; auto; homt |
          apply add_hom; auto; homt |
          apply hom3E |
          apply hom3l; homt |
          apply hom3r; homt |
          apply hom2; homt |
          apply hom1p |
          apply hom1d; homt |
          apply hom0l; homt |
          apply hom0r; homt |
          apply hom0p; homt |
          apply hom01 |
          apply homd
   ].

Ltac hom3t :=
  apply proj_homn_eq; auto; try homt.

Ltac hom0t :=
  apply proj_hom0_eq; auto; try homt.

  Some properties of the bracket operator                                  

Lemma bracket_defE (x y z : point) :
  x ∨ y ∨ z = '[x,y,z] .* E.

Lemma bracket_defl (x y z : point) :
  x ∧ (y ∨ z) = '[x, y, z] .* 1.

Lemma bracket_defr (x y z : point) :
  (x ∨ y) ∧ z = '[x, y, z] .* 1.

Lemma bracket0l (a b: point) : '[a,a,b] = 0%f.

Lemma bracket0m (a b: point) : '[a,b,a] = 0%f.

Lemma bracket0r (a b: point) : '[a,b,b] = 0%f.

Lemma bracket_swapl (x y z : point) : '[y,x,z] = (- ('[x,y,z]))%f.

Lemma bracket_swapr (x y z : point) : '[x,z,y] = (- ('[x,y,z]))%f.

Lemma bracket_norm (a b c: point) :
  ('[a,c,b] = (-(1)) * '[a,b,c] /\
  '[b,a,c] = (-(1))%f * '[a,b,c] /\
  '[b,c,a] = '[a,b,c] /\
  '[c,a,b] = '[a,b,c] /\
  '[c,b,a] = (-(1))%f * '[a,b,c])%f.

A tactic to normalize one specific bracket 

Ltac normb a b c :=
 generalize (bracket_norm a b c);
 intros (Hn1, (Hn2, (Hn3, (Hn4, Hn5))));
 rewrite ?Hn1, ?Hn2, ?Hn3, ?Hn4, ?Hn5;
 clear Hn1 Hn2 Hn3 Hn4 Hn5.

Definition fbracket a b c:= '[a, b, c].

Lemma fbracket_norm (a b c: point) :
  ('[a,b,c] = fbracket a b c /\
  '[a,c,b] = (-(1)) * (fbracket a b c) /\
  '[b,a,c] = (-(1))%f * (fbracket a b c) /\
  '[b,c,a] = (fbracket a b c) /\
  '[c,a,b] = (fbracket a b c) /\
  '[c,b,a] = (-(1))%f * (fbracket a b c))%f.

A tactic to globally normalize brackets 

Ltac normbs :=
repeat match goal with |- context['[p2v ?a,p2v ?b,p2v ?c]] =>
 generalize (fbracket_norm a b c);
 intros (Hn1, (Hn2, (Hn3, (Hn4, (Hn5, Hn6)))));
 rewrite ?Hn1, ?Hn2, ?Hn3, ?Hn4, ?Hn5, ?Hn6;
 clear Hn1 Hn2 Hn3 Hn4 Hn5 Hn6
end; unfold fbracket.

  Some distributivity rules                                                

Lemma expand_meetr (x y x1 y1: point) :
(x ∨ y1) ∧ (x1 ∨ y) = '[x,y1,y] .* x1 - '[x,y1,x1] .* y.

Lemma meet_swap (x y x1 y1: point) :
  (x ∨ y1) ∧ (x1 ∨ y) = (-(1))%f .* (x1 ∨ y) ∧ (x ∨ y1).

Lemma expand_meetl (x y x1 y1: point) :
  (x1 ∨ y) ∧ (x ∨ y1) = '[x,y1,x1] .* y - '[x,y1,y] .* x1.

Lemma split_meetl (x1 x2 x3 x4 x5 x6: point) :
  (x1 ∨ x2) ∧ (x3 ∨ x4) ∧ (x5 ∨ x6) =
     (x1 ∧ (x3 ∨ x4)) ∨ (x2 ∧ (x5 ∨ x6)) +
     (-(1))%f .* ((x2 ∧ (x3 ∨ x4)) ∨ (x1 ∧ (x5 ∨ x6))).

Lemma split_meetr (x1 x2 x3 x4 x5 x6: point) :
  ((x1 ∨ x2) ∧ (x3 ∨ x4)) ∧ (x5 ∨ x6) =
     ((x1 ∨ x2) ∧ x5) ∨ ((x3 ∨ x4) ∧ x6) +
     (-(1))%f .* ((x3 ∨ x4) ∧ x5) ∨ ((x1 ∨ x2) ∧ x6).

Lemma meet_swapr (x y x1 y1: point) :
  (x ∨ x1) ∧ (y ∨ y1) = (x1 ∨ x) ∧ (y1 ∨ y).

Lemma join_meet3l (a b c d e f: point) :
  (a ∨ b) ∨ ((c ∨ d) ∧ (e ∨ f)) = ((a ∨ b) ∧ (c ∨ d) ∧ (e ∨ f)) ∨ E.

Lemma join_meet3r (a b c d e f: point) :
  ((a ∨ b) ∧ (c ∨ d)) ∨ (e ∨ f) = ((a ∨ b) ∧ (c ∨ d) ∧ (e ∨ f)) ∨ E.

Lemma split3l (a b c d : point) :
  (a ∨ b ∨ c) ∧ d = '[b,c,d] .* a - '[a,c,d] .* b + '[a,b,d] .* c.

 

                         Some plucker relations                            
                                                                           

Lemma split3b (a b c d e f : point) :
  ('[a,b,c] * '[d,e,f] =
   '[b,c,d] * '[a,e,f] + (-(1)) * '[a,c,d] * '[b,e,f] + '[a,b,d] * '[c,e,f])%f.

Lemma split3b_v1 (a b c d e f : point) :
  ('[a,b,c] * '[d,e,f] =
   '[a,d,e] * '[b,c,f] + (-(1)) * '[a,d,f] * '[b,c,e] + '[a,e,f] * '[b,c,d])%f.

Lemma split3b_v2 (a b c d e f : point) :
  ('[a,b,c] * '[d,e,f] =
   '[a,b,d] * '[c,e,f] + (-(1)) * '[a,b,e] * '[c,d,f] + '[a,b,f] * '[c,d,e])%f.

 

                         Expansions                                        
                                                                           

Lemma bracket_expand (x a b c d a1 b1: point) :
 x = (a ∨ b) ∧ (c ∨ d) :> vect ->
 ('[x, a1, b1] =
   (-(1)) * '[a, a1, b1] * '[b, c, d] + '[b, a1, b1] * '[a, c, d])%f.

Lemma bracket_free (x : point) k1 (a: point) k2 (b a1 b1: point) :
 x = k1 .* a + k2 .* b :> vect ->
 '[x, a1, b1] =
   (k1 * '[a, a1, b1] + k2 * '[b, a1, b1] )%f.

   Contraction                                                             

Lemma contraction_v0 (a b c d e: point) :
  ('[a, b, c] * '[a, d, e] + -(1) * '[a, b, e] * '[a, d, c] =
   '[a, b, d] * '[a, c, e])%f.

Lemma contraction_v1 (a b c d e: point) :
  ('[a, b, c] * '[b, d, e] + -(1) * '[a, b, e] * '[b, d, c] =
   '[a, b, d] * '[b, c, e])%f.

Lemma contraction_v2 (a b c d e: point) :
  ('[a, b, c] * '[d, b, e] + - (1) * '[a, b, e] * '[d, b, c] =
   '[b, a, d] * '[b, c, e])%f.

Lemma contraction_v3 (a b c d e: point) :
  ('[a, b, c] * '[d, a, e] + - (1) * '[a, b, e] * '[d, a, c] =
   '[a, b, d] * '[c, a, e])%f.

  Some standard geometry definitions                                       

Definition collinear x y z := x ∨ y ∨ z = 0.
Definition line (x y : point) := x ∨ y.
Definition intersection (x y : vect) := x ∧ y.
Definition concur (l1 l2 l3 : vect) := l1 ∧ l2 ∧ l3 = 0.
Definition online (x y z : point) := y ∨ z <> 0 /\ x ∨ y ∨ z = 0.
Definition online1 (x : point) k1 (y : point) k2 (z : point) :=
  x = k1 .* y + k2 .* z :> vect.
Definition inter_lines (x a b c d : point) : Prop :=
  x = (a ∨ b) ∧ (c ∨ d) :> vect.

Lemma online_def x y z :
  online x y z -> exists pk, online1 x (fst pk) y (snd pk) z.

Lemma collinear_bracket (x y z : point) :
  collinear x y z <-> '[x,y,z] = 0%f.

Lemma collinear_bracket0 (x y z : point) :
  collinear x y z -> '[x,y,z] = 0%f.

Lemma bracket0_collinear (x y z : point) :
  '[x,y,z] = 0%f -> collinear x y z.

  Pappus theorem                                                           

Theorem Pappus (a b c a' b' c': point) :
  let AB' := line a b' in
  let A'B := line a' b in
  let p := intersection AB' A'B in
  let BC' := line b c' in
  let B'C := line b' c in
  let q := intersection BC' B'C in
  let CA' := line c a' in
  let C'A := line c' a in
  let r := intersection CA' C'A in
  collinear a b c -> collinear a' b' c' -> collinear p q r.

Theorem Desargues (a b c a' b' c': point) :
  let AB := line a b in
  let A'B' := line a' b' in
  let p := intersection AB A'B' in
  let AC := line a c in
  let A'C' := line a' c' in
  let q := intersection AC A'C' in
  let BC := line b c in
  let B'C' := line b' c' in
  let r := intersection BC B'C' in
  let AA' := line a a' in
  let BB' := line b b' in
  let CC' := line c c' in
  collinear p q r <-> collinear a b c \/ collinear a' b' c' \/ concur AA' BB' CC'.

End Vect.

Notation "x '∨' y" := (Vjoin _ x y) (at level 40, left associativity).
Notation "x + y" := (Vadd _ x y).
Notation "x - y" := (Vsub _ x y).
Notation "k .* x" := (Vscal _ k x).
Notation "x '∧' y" := (Vmeet _ x y) (at level 45, left associativity).
Notation "'@ x" := (Vdual _ x) (at level 9).
Notation "x ?= y" := (Veq _ x y).
Notation "0" := (Vgenk _ 0%f).
Notation "1" := (Vgenk _ 1%f).
Notation "'dC[ x ]" := (dconst _ _ 3 x).
Notation "'C[ x ]" := (const _ _ 3 x).
Notation "'E'" := (all _ _ 3: vect).
Notation "'[ x , y , z ]" := (bracket _ x y z).
Notation " x 'is_the_intersection_of' [ a , b ] 'and' [ c , d ] " :=
  (inter_lines _ x a b c d) (at level 10, format
                " x 'is_the_intersection_of' [ a , b ] 'and' [ c , d ]").
Notation " x 'is_free_on' [ a , b ]" :=
  (online _ x a b) (at level 10, format
             " x 'is_free_on' [ a , b ]").
Notation " x ':=:' 'xfree' 'on' [ a , b ] ( c , d ) " :=
  (online1 _ x c a d b) (at level 10, format
             " x ':=:' 'xfree' 'on' [ a , b ] ( c , d )").

Notation "'[' a , b , c ']' 'are_collinear' " := (collinear _ a b c) (at level 10).