9 files changed, 196 insertions(+), 0 deletions(-)

A .gitignore
A Demo.lean
A Demo/Imperative.lean
A Demo/Match.lean
A Demo/Math.lean
A Demo/Syntax.lean
A Demo/Unification.lean
A Demo/Vec.lean
A leanpkg.toml

@@ 1,1 @@
+build/*

@@ 1,5 @@
+import Init.System.IO
+
+def main : IO UInt32 := do
+  IO.println "Hello world!"
+  return 0

@@ 1,9 @@
+def List.countNumElements {a} (l : List a) : Nat := do
+  let mut num := 20
+  for element in l do
+    num := num + 1
+  num := num - 20
+  return num
+
+#eval [1,2,3,4,5].countNumElements
+#print List.countNumElements

@@ 1,23 @@
+--Something that I had to write in Agda:
+--
+-- wtf : ∀ {ℓ} {X : Set ℓ} {Y : X → Set ℓ} →
+--   (f : (x : X) → Y x) → (x₀ : X)
+--   ------------------------------
+--   → Σ[ y ∈ (Y x₀) ] (f x₀ ≡ y)
+-- wtf f x = f x , refl
+--
+-- Why?
+-- case wtf p₁ x of λ (x, pf) -> .....
+-- How would we write this in lean?
+
+theorem listStructure {a n} (l : List a) (lenPos : l.length = Nat.succ n) : (∃  (x : a) (xs : List a), l = x::xs) :=
+  match proof:l with
+    | [] => have l = [] from proof
+            have lenZero : l.length = 0 from congrArg List.length this
+            have ¬ (Nat.succ n) = 0 from Nat.succNeZero n
+            have ¬ l.length = 0 from fun eq => this $ Eq.subst (motive := fun x => x = 0) lenPos eq
+            absurd lenZero this
+    | x::xs => Exists.intro x $ Exists.intro xs rfl
+
+#check listStructure
+#print listStructure

@@ 1,21 @@
+theorem pow2' {a : Nat} : a^2=a*a :=
+  have a*a*1=a*a from Nat.mulOne (a*a)
+  have 1*a*a=a*a from (Nat.mulAssoc 1 a a).trans $ (Nat.mulComm (a*a) 1).symm.trans this
+  have a^0*a*a=a*a from Eq.subst (motive := fun x => x*a*a=a*a) (Nat.powZero a) this
+  have a^2=a*a from (Nat.powSucc a 1).trans this
+  this
+
+theorem pow2 {a : Nat} : a^2=a*a := by
+  rw [Nat.powSucc,Nat.powSucc, Nat.powZero]
+  have 1*a = a by rw [Nat.mulComm, Nat.mulOne]
+  rw this
+
+theorem add_mul_self_eq (a b : Nat) : (a+b)*(a+b)=a*a+2*a*b+b*b := by
+  rw [Nat.leftDistrib, Nat.rightDistrib, Nat.rightDistrib]
+  have 2*a*b=a*b+a*b by
+    rw [Nat.mulAssoc, Nat.mulComm, Nat.mulSucc, Nat.mulOne]
+  rw [this, Nat.mulComm]
+  rw [Nat.mulComm a b, Nat.addAssoc, Nat.addAssoc, Nat.addAssoc]
+
+theorem pow2Expansion {a b : Nat} : (a+b)^2=a^2 + 2*a*b + b^2:= by
+  rw [pow2, pow2, pow2, add_mul_self_eq]

@@ 1,27 @@
+import Lean
+import Demo.Vec
+
+-- Agda like dependent pairs with hygenic macros!
+syntax "Σ[" ident "∈" term "]" term : term
+
+macro_rules
+  | `(Σ[ $x ∈ $A ] $B) => `(PSigma (fun ($x : $A) => $B))
+
+def mulId : Σ[ x ∈ Nat ] ∀(y : Nat), y*x=y := PSigma.mk 1 Nat.mulOne
+def addId : Σ[x∈Nat]     ∀(y : Nat), y+x=y := PSigma.mk 0 Nat.addZero
+
+#check mulId
+#check addId
+
+def f (x y : Nat) := x + 2*y
+
+#check f 1 2
+
+-- prefix-call style
+syntax term noWs "(" term,* ")" : term
+
+macro_rules
+  | `($f($args,*)) => `($f $args*)
+
+#check f(1,2)
+#check_failure f (1,2)

@@ 1,42 @@
+structure Magma.{u} where
+  α   : Type u
+  mul : α → α → α
+
+def Nat.Magma : Magma where
+  α       := Nat
+  mul a b := a * b
+
+def Prod.Magma (m : Magma.{u}) (n : Magma.{v}) : Magma where
+  α  := m.α × n.α
+  mul | (a₁, b₁), (a₂, b₂) => (m.mul a₁ a₂, n.mul b₁ b₂)
+
+instance : CoeSort Magma.{u} (Type u) where
+  coe m := m.α
+
+def mul {s : Magma} (a b : s) : s :=
+  s.mul a b
+
+unif_hint (s : Magma) where
+  s =?= Nat.Magma |- s.α =?= Nat
+
+unif_hint (s : Magma) (m : Magma) (n : Magma) (β : Type u) (δ : Type v) where
+  m.α =?= β
+  n.α =?= δ
+  s =?= Prod.Magma m n
+  |-
+  s.α =?= β × δ
+
+def f1 (x : Nat) : Nat :=
+  mul x x
+
+#eval f1 10
+
+def f2 (x y : Nat) : Nat × Nat :=
+  mul (x, y) (x, y)
+
+#eval f2 10 20
+
+def f3 (x y : Nat) : Nat × Nat × Nat :=
+  mul (x, y, y) (x, y, y)
+
+#eval f3 7 24

@@ 1,63 @@
+structure Vec (n : Nat) (a : Type u) where
+  as : Array a
+  pf : as.size = n
+
+namespace Vec
+  def mt {α} :  Vec 0 α := ⟨#[], rfl⟩
+
+  def cons {n} (v : Vec n α) (a : α) : Vec (Nat.succ n) α :=
+      ⟨Array.mk $ a::v.as.data, by
+        have (Array.mk $ a::v.as.data).size = (a::v.as.data).length by rfl
+        rw [this, List.lengthConsEq]
+        have v.as.data.length = n from v.pf
+        rw this⟩
+
+  def get {n} (v : Vec n α) (m : Fin n) : α :=
+      v.as.get ⟨m.val, by rw v.pf; exact m.isLt⟩
+
+  instance {n : Nat} {a} [ToString a] : ToString (@Vec n a) where
+    toString (v : Vec n a) : String := toString v.as
+
+  def fromFunc {n} (f : Fin n -> α) : Vec n α := fromFunc' (f ∘ Fin.inv)
+    where Nat.toFin {n} (m : Nat) : Fin (Nat.succ n) :=
+            ⟨m % Nat.succ n, Nat.modLt _ (Nat.zeroLtSucc _)⟩
+          Fin.inv {n} : Fin n  -> Fin n := match ns:n with
+            | 0 => Fin.elim0
+            | Nat.succ n' =>
+              fun (num : Fin (Nat.succ n')) => ((Nat.toFin Nat.zero) - (Nat.toFin num)) - (Nat.toFin 1)
+          Fin.retr {n m α} (lt : n < m) (f : Fin m -> α) : (Fin n -> α)
+            | ⟨num, h⟩ => f ⟨num, Nat.ltTrans h lt⟩
+          fromFunc' {n} (f : Fin n -> α) : Vec n α := match ns:n with
+            | 0 => ⟨#[], rfl⟩
+            | (Nat.succ n') => by
+              have (n : Nat) -> n < (Nat.succ n) by
+                intro m
+                induction m with
+                  | zero => rfl
+                  | Nat.succ n' => assumption
+              have h1 : n' < n from Eq.subst ns.symm (this n')
+              have Fin n' -> α from Fin.retr h1 f
+              exact (@fromFunc' n' this).cons $ f ⟨n', h1⟩
+
+  -- the proof that (v.as.map f).size = n is just "made up"
+  -- lcProof : (a : Prop) : a. Unsafe and unsound! but contained in the unsafe namespace.
+  unsafe def false : False := lcProof
+
+  unsafe def map' {α β n} (f : α -> β) (v : Vec n α) : Vec n β :=
+    ⟨v.as.map f, lcProof⟩
+
+  @[implementedBy map']
+  constant map {α β n} (f : α -> β) (v : Vec n α) : Vec n β :=
+    fromFunc $ f ∘ v.get
+
+  syntax "⟦" term,* "⟧" : term
+  
+  macro_rules
+    | `(⟦ $elems,* ⟧ ) => `(Vec.mk #[$elems,*] rfl)
+
+  instance {n : Nat} : Functor (Vec n) where
+    map := map
+
+#eval ⟦1,2,3,4,5⟧.map (. + 1)
+
+end Vec

@@ 1,5 @@
+[package]
+name = "Sudoku"
+version = "0.1"
+lean_version = "leanprover/lean4:nightly"
+path = "."