symgeoalg

commit 92379316f0d3fb3929a117863c6282a5a53fd827
parent a6c66052d01a7925848f6de02bd5b9e74a772179
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Sat, 27 Jul 2024 14:06:42 -0700

Fix GeometricAlgebra mul and toString

Diffstat:
M
Main.lean
 | 
69
++++++++++++++++++++++++++++++++++++++++++++++++++++-----------------

1 file changed, 52 insertions(+), 17 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -42,6 +42,18 @@ def bitVecEnuml (n : Nat) (f : α -> BitVec n -> α) (init : α) : α :=
   let loop acc i := f acc (BitVec.ofFin i)
   Fin.foldl (2^n) loop init
 
+def bitVecChoose (n k : Nat) (f : α -> BitVec n -> α) (acc : α) : α :=
+  match n, k with
+  | 0, 0 => f acc BitVec.nil
+  | 0, _ + 1 => acc
+  | _ + 1, 0 => f acc 0
+  | n' + 1, k' + 1 =>
+    let f' (msb : Bool) (acc : α) (bv' : BitVec n') : α :=
+      let bv := BitVec.cons msb bv'
+      f acc bv
+    let acc := bitVecChoose n' k (f' false) acc
+    bitVecChoose n' k' (f' true) acc
+
 def bitVecPopCount (bv : BitVec n) : Nat :=
   bitVecFoldl (fun acc bit => acc + bit.toNat) bv 0
 
@@ -282,10 +294,11 @@ instance [Field F] [DecidableEq F] [ToString F] [AddGroup V] [VectorSpace F V]
         termString :: acc
       else
         acc
-    let termStrings := bitVecEnuml n termToString []
+    let termStrings := Fin.foldl (n + 1)
+      (fun acc k => bitVecChoose n k.val termToString acc) []
 
     if termStrings.length > 0 then
-      String.intercalate " + " termStrings
+      String.intercalate " + " (List.reverse termStrings)
     else
       "0"
 
@@ -300,10 +313,10 @@ instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
   smul a v := ⟨a ⋅ v.coords⟩
 
 -- Multiplication algorithm:
--- Given v w : GeometricAlgebra q and bld : BasisBlade n, the bld-th component
+-- Given v w : GeometricAlgebra q and bld : BitVec n, the bld-th component
 -- of the product v * w is a sum of 2^n terms, where each term is the product of
 -- the vbld-th component of v and the wbld-th component of w, for all
--- vbld wbld : BasisBlade n that multiply (XOR) to bld (modulo a scalar). For
+-- vbld wbld : BitVec n that multiply (XOR) to bld (modulo a scalar). For
 -- example, if we take n = 3 and denote blades as bit vectors, then we can write
 -- generic vectors v and w as follows:
 --    v0 * 000 + v1 * 001 + v2 * 010 + v3 * 011 + v4 * 100 + v5 * 101 + v6 * 110 + v7 * 111
@@ -333,7 +346,7 @@ instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
   mul v w :=
     let sign (x y : BitVec n) : F :=
       let addSwaps (acc : Nat) (i : Fin n) : Nat :=
-        acc + bitVecPopCount (x &&& (y >>> (i.val + 1)))
+        acc + bitVecPopCount (x &&& (y <<< (i.val + 1)))
       let nSwaps := Fin.foldl n addSwaps 0
       if nSwaps % 2 = 0 then 1 else -1
 
@@ -356,20 +369,42 @@ instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
 --------------------------------------------------------------------------------
 -- Main
 
+abbrev F : Type := Rat
+abbrev n : Nat := 3
+abbrev V : Type := F ^ n
+abbrev b : FiniteBasis V n := FiniteBasis.pow (FiniteBasis.field F) n
+abbrev q : OrthoQuadraticForm b := ⟨
+    fun
+    | 0 => 1
+    | 1 => 1
+    | 2 => 1
+  ⟩
+abbrev G : Type := GeometricAlgebra q
+
 def main : IO Unit := do
-  let F : Type := Rat
-  let V : Type := F ^ 3
-  let b : FiniteBasis V 3 := FiniteBasis.pow (FiniteBasis.field F) 3
-  let q : OrthoQuadraticForm b := ⟨
+  let v : G := ⟨
       fun
-      | 0 => 1
-      | 1 => 1
-      | 2 => 1
+      | 0 => 0
+      | 1 => 2
+      | 2 => 0
+      | 3 => 0
+      | 4 => 0
+      | 5 => 0
+      | 6 => 0
+      | 7 => 0
     ⟩
-  let G : Type := GeometricAlgebra q
-
-  let v : G := ⟨fun _ => 1⟩
-  let w : G := v * v
-
+  let w : G := ⟨
+      fun
+      | 0 => 0
+      | 1 => 0
+      | 2 => 3
+      | 3 => 0
+      | 4 => 0
+      | 5 => 0
+      | 6 => 0
+      | 7 => 0
+    ⟩
+  let x : G := v * w
   IO.println v
   IO.println w
+  IO.println x