Library Clifford

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

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 projk := (Kn.proj p _).

Notation gvp := (Grassmann.vn_eparams p).

Notation "x '∧' y" := (join p _ x y) (at level 40, left associativity).
Notation "x + y" := (addE _ x y).
Notation "k .* x" := (scalE (gvp _) k x).
Notation "k .* x" := (scalE _ k x) : Kn_scope.
Notation vect := (vect p).
Notation "x ^_'f" := (conj p _ false x) (at level 30).
Notation "'C[ x ]" := (const p _ x).
Notation " [ k ] " := (genk p _ k%f) (at level 9).
Notation kn := (kn p).
Notation "#< l , x ># " := (contra p _ l x).
Notation "'v_ x" := (k2g p _ x) (at level 9).
Notation "''e_' i" := (gen p _ i).
Notation "'@ x " := (dual p _ x) (at level 9).
Notation E := (all p _).

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

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

Hint Resolve (fn _ Hp).

The geometric product (Clifford product)    
 the quadratic form is encoded as the list l 

Fixpoint gprod (n : nat) : kn n -> vect n -> vect n -> vect n :=
  match n return (kn n -> vect n -> vect n -> vect n) with
  | 0%nat => fun k x y => (x * y)%f
  | S n1 =>
    fun l x y =>
      let (k1, l1) := l in
      let (x1, x2) := x in
      let (y1, y2) := y in
     ( gprod n1 l1 x1 y2 + gprod n1 l1 (x2 ^_'f) y1,
           gprod n1 l1 x2 y2 + k1 .* gprod n1 l1 (x1 ^_'f) y1)
  end.

Notation "a [* l ] b " := (gprod _ l a b) (at level 9).

Lemma grpod_l0_join n x y : x [* 0] y = x ∧ y :> vect n.

Lemma gprodE n l (M1 M2 : vect n.+1) :
  M1 [* l] M2 =
     ( (fst M1) [* snd l] (snd M2) + ((snd M1) ^_'f) [* snd l] (fst M2),
           (snd M1) [* snd l] (snd M2) +
              fst l .* (((fst M1) ^_'f) [* snd l] (fst M2))).

Lemma gprod0r n l x : x [* l] 0 = 0 :> vect n.

Lemma gprod0l n l y : 0 [* l] y = 0 :> vect n.

Lemma gprodkl n l k y : [k] [* l] y = k .* y :> vect n.

Lemma gprodkr n l k x : (x [* l] [k]) = k .* x :> vect n.

Lemma gprod_spec1 n l i :
   i < n -> 'e_i [* l] 'e_i = [projk i l] :> vect n.

Lemma gprod_spec2 n l i j : i < n -> j < n -> i <> j ->
  'e_i [* l] 'e_j = (-(1))%f .* 'e_j [* l] 'e_i :> vect n.

Lemma gprod_scall n l k x y : (k .* x) [* l] y = k .* (x [* l] y) :> vect n.

Lemma gprod_scalr n l k x y : x [* l] (k .* y) = k .* (x [* l] y) :> vect n.

Lemma gprod_addl n l x y z :
  (x + y) [* l] z = x [* l] z + y [* l] z :> vect n.

Lemma gprod_addr n l x y z :
   x [* l] (y + z) = x [* l] y + x [* l] z :> vect n.

Lemma conjf_gprod n l (x y: vect n) :
   (x [* l] y) ^_'f = (x ^_'f) [* l] (y ^_'f) :> vect n.

Lemma gprod_assoc n l x y z :
  (x [* l] y) [* l] z = x [* l] (y [* l] z) :> vect n.

Lemma gprod_e0 n l (M : vect n.+1 ) :
    'e_0 [* l] M = (snd M, fst l .* fst M).

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

Lemma gprodE_ei n l i M :
  i < n ->
  'e_i [* l] M = 'e_i ∧ M + #<('e_i [*] l)%Kn, M># :> vect n.

Lemma gprodE_v n l x M :
  'v_x [* l] M = 'v_x ∧ M + #< (x [*] l)%Kn, M ># :> vect n.

reverse of a multivector each basis element is reversed 

Fixpoint rev 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 (rev n1 x ^_'f, rev n1 y)
  end.

Notation "''R[' x ]" := (rev _ x).

Lemma rev0 n : 'R[0] = 0 :> vect n.

Lemma revk n k : 'R[[k]] = [k] :> vect n.

Lemma rev_scal n k x : 'R[(k .* x)] = k .* 'R[x] :> vect n.

Lemma rev_add n x y : 'R[x + y] = 'R[x] + 'R[y] :> vect n.

Lemma rev_conj n x : 'R[x ^_'f] = 'R[x]^_'f :> vect n.

Lemma rev_invo n x : 'R['R[x]] = x :> vect n.

Lemma rev_hom n m x : (m <= n)%nat -> hom p n m x ->
   'R[x] = ((-(1)) ^ (div2 (m * (m - 1))))%f .* x.

Lemma rev_join n x y : 'R[x ∧ y] = 'R[y] ∧ 'R[x] :> vect n.

Definition of the inverse of the pseudoscalar element 
 with the geometric product  

Definition pseudo_inv n l :=
  let a := (E : vect n) in let b := 'R[a] in (a [* l] b) [* l] b.

Notation "''Pi[' l ]" := (pseudo_inv _ l).

product of all elements in a vector 

Fixpoint prodk n : (kn n -> K) :=
  match n return kn n -> K with
         0 => fun _ => 1%f
  | (S n1) => fun x => let (a, x1) := x in (a * prodk n1 x1)%f
  end.

Notation "''P[' x ]" := (prodk _ x).

Lemma gprod_all_rev n l : E [* l] 'R[E] = ['P[l]] :> vect n.

Lemma pseudo_invE n l : 'Pi[l] = 'P[l] .* 'R[E] :> vect n.

Definition of the Clifford dual with the geometric product 

Definition cdual n l x : vect n := 'P[l] .* (x [* l] 'R[E]).

Direct (in terms of binary trees) definition of the Clifford dual 

Fixpoint cliff_starb n b : kn n -> vect n -> vect n :=
  match n return kn n -> vect n -> vect n with
  | 0 => fun _ a => a
  | S n1 => fun l v =>
                     let b1 := negb b in
                     let (c, l1) := l in
                     let (x, y) := v in
       ((if b then c else (-c)%f) .* cliff_starb n1 b1 l1 y,
        (c * c)%f .* cliff_starb n1 b1 l1 x)
  end.

Require Import Wf_nat.

Actual definition of Clifford dual 

Definition cliff_star n l := cliff_starb n true l.

OK usual definition and direct definition match 

Lemma cdual_cliff n l x : cdual n l x = cliff_star n l x.

The left contraction (Dorst inner product) 

Fixpoint l_contra (n : nat) : kn n -> vect n -> vect n -> vect n :=
  match n return (kn n -> vect n -> vect n -> vect n) with
  | 0%nat => fun _ x y => (x * y)%f
  | S n1 =>
    fun l x y =>
      let (k, l1) := l in
      let (x1, x2) := x in
      let (y1, y2) := y in
     (l_contra n1 l1 (x2^_'f) y1,
      k .* l_contra n1 l1 (x1^_'f) y1 + l_contra n1 l1 x2 y2)
  end.

Notation "x ''L[' l ] y " := (l_contra _ l x y) (at level 40).
Notation hom := (hom p _).

Lemma l_contra_addl n l x y z :
   (x + y) 'L[l] z = x 'L[l] z + y 'L[l] z :> vect n.

Lemma l_contra_addr n l x y z :
   x 'L[l] (y + z) = x 'L[l] y + x 'L[l] z :> vect n.

Lemma l_contra_scall n l k x y :
   (k .* x) 'L[l] y = k .* (x 'L[l] y) :> vect n.

Lemma l_contra_scalr n l k x y :
   x 'L[l] (k .* y) = k .* (x 'L[l] y) :> vect n.

Lemma l_contra_0l n l y : 0 'L[l] y = 0 :> vect n.

Lemma l_contra_0r n l x : x 'L[l] 0 = 0 :> vect n.

Lemma l_contra_kl n l k y : [k] 'L[l] y = k .* y :> vect n.

Lemma l_contra_kr n l k x : x 'L[l] [k] = ['C[x] * k] :> vect n.

Lemma l_contra_joinl n l x y z :
  (x ∧ y) 'L[l] z = x 'L[l] (y 'L[l] z) :> vect n.

Lemma l_contra_ei n l i :
   i < n -> 'e_i 'L[l] 'e_i = [projk i l] :> vect n.

Lemma l_contra_eij n l i j :
   i < n -> j < n -> i <> j -> 'e_i 'L[l] 'e_j = 0 :> vect n.

Lemma l_contra_conj n l x y :
   (x 'L[l] y)^_'f = (x^_'f) 'L[l] (y^_'f) :> vect n.

Retrieve the Hodge dual from geometric product 
 when the quadratic form is nul 
 Thanks to Lounesto: Clifford Algebra and Spinors 

Lemma dualE n x : '@x = 'R[x] [* [1%f]%Kn] E :> vect n.

Fixpoint prod_scal (n : nat) : kn n -> vect n -> vect n -> K :=
  match n return (kn n -> vect n -> vect n -> K) with
  | 0%nat => fun _ x y => (x * y)%f
  | S n1 =>
    fun l x y =>
      let (k, l1) := l in
      let (x1, x2) := x in
      let (y1, y2) := y in
        (prod_scal n1 l1 x2 y2 + k * prod_scal n1 l1 x1 (y1 ^_'f))%f
  end.

Notation "a '[.' l ] b " := (prod_scal _ l a b)
  (at level 40).

Lemma prod_scal0r n l (x : vect n) : x [.l] 0 = 0%f.

Lemma prod_scal0l n l (x : vect n) : 0 [.l] x = 0%f.

Lemma prod_scal_scall n l k (x y : vect n) :
  (k .* x) [.l] y = (k * (x [.l] y))%f.

Lemma prod_scal_scalr n l k (x y : vect n) :
  x [.l] (k .* y) = (k * (x [.l] y))%f.

Lemma prod_scal_addl n l (x y z : vect n) :
  (x + y) [.l] z = (x [.l] z + y [.l] z)%f.

Lemma prod_scal_addr n l (x y z : vect n) :
  x [.l] (y + z) = (x [.l] y + x [.l] z)%f.

Lemma conjf_prod_scal n l (x y: vect n) :
   (x^_'f) [.l] y = x [.l] (y^_'f).

Lemma prod_scal_sym n l (x y: vect n) :
   x [.l] y = y [.l] x.

End Vect.