symgeoalg

commit 6b735780b681ed96b9212b6966b376db6cbf3178
parent 6cd1e492c505b19678418a0938f1bf5c89a42ee8
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Tue, 23 Jul 2024 20:57:45 -0700

Model vector spaces

Diffstat:
M
Main.lean
 | 
84
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
M
lake-manifest.json
 | 
11
++++++++++-
M
lakefile.lean
 | 
2
++

3 files changed, 95 insertions(+), 2 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -1,2 +1,84 @@
+import Batteries.Data.Rat
+
+class SMul (α β : Type) where
+  smul : α -> β -> β
+infixr:75 " ⋅ " => SMul.smul
+
+class AddSemigroup (A : Type) where
+  add : A -> A -> A
+class AddMonoid (A : Type) extends AddSemigroup A where
+  zero : A
+class AddGroup (A : Type) extends AddMonoid A where
+  sub : A -> A -> A
+  neg : A -> A := fun x => sub zero x
+
+-- Notation for AddXxx
+instance [AddMonoid A] : OfNat A 0 where
+  ofNat := AddMonoid.zero
+instance [AddSemigroup A] : Add A where
+  add := AddSemigroup.add
+instance [AddGroup A] : Sub A where
+  sub := AddGroup.sub
+instance [AddGroup A] : Neg A where
+  neg := AddGroup.neg
+
+class MulSemigroup (M : Type) where
+  mul : M -> M -> M
+class MulMonoid (M : Type) extends MulSemigroup M where
+  one : M
+class MulGroup (M : Type) extends MulMonoid M where
+  div : M -> M -> M
+  inv : M -> M := fun x => div one x
+
+-- Notation for MulXxx
+instance [MulMonoid M] : OfNat M 1 where
+  ofNat := MulMonoid.one
+instance [MulSemigroup M] : Mul M where
+  mul := MulSemigroup.mul
+instance [MulGroup M] : Div M where
+  div := MulGroup.div
+
+-- Convention: (∀a. div a 0 = 0) and (inv 0 = 0).
+class Field (F : Type) extends AddGroup F, MulGroup F
+
+instance : Field Rat where
+  zero := 0
+  add := Rat.add
+  sub := Rat.sub
+  one := 1
+  mul := Rat.mul
+  div := Rat.div
+
+class VectorSpace (F : Type) [Field F] (V : Type) [AddGroup V] where
+  smul : F -> V -> V
+
+-- Notation for VectorSpace
+instance [Field F] [AddGroup V] [VectorSpace F V] : SMul F V where
+  smul := VectorSpace.smul
+
+-- Fields F are vector spaces over F.
+instance [Field F] : VectorSpace F F where
+  smul := MulSemigroup.mul
+
+-- Given a type X and a vector space V over F, the type of functions X -> V is a vector space over F.
+def FunctionSpace (X V : Type) := X -> V
+instance [AddGroup V] : AddGroup (FunctionSpace X V) where
+  zero := fun _ => 0
+  add f g := fun x => f x + g x
+  sub f g := fun x => f x - g x
+instance [Field F] [AddGroup V] [VectorSpace F V] : VectorSpace F (FunctionSpace X V) where
+  smul a f := fun x => a ⋅ f x
+
+abbrev NSpace (n : Nat) (V : Type) := FunctionSpace (Fin n) V
+instance [ToString V] : ToString (NSpace n V) where
+  toString f :=
+    let coordStr i acc := toString (f i) :: acc
+    s!"({String.intercalate ", " $ Fin.foldr n coordStr []})"
+
+def vec3 (x y z : Rat) : NSpace 3 Rat := fun
+| 0 => x
+| 1 => y
+| 2 => z
+
 def main : IO Unit :=
-  IO.println "whoa"
+  IO.println $ vec3 1 0 0 + vec3 0 1 0
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,5 +1,14 @@
 {"version": "1.0.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "vslean",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -1,6 +1,8 @@
 import Lake
 open Lake DSL
 
+require batteries from git "https://github.com/leanprover-community/batteries" @ "main"
+
 package «vslean» where
 
 @[default_target]