From 88ba8bc96e92359817f4f4d1cd4fa5a00b9a984a Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Fri, 29 Jan 2021 12:01:43 -0700 Subject: [PATCH] Initial commit --- .gitignore | 1 + Demo.lean | 5 ++++ Demo/Imperative.lean | 9 +++++++ Demo/Match.lean | 23 ++++++++++++++++ Demo/Math.lean | 21 +++++++++++++++ Demo/Syntax.lean | 27 +++++++++++++++++++ Demo/Unification.lean | 42 +++++++++++++++++++++++++++++ Demo/Vec.lean | 63 +++++++++++++++++++++++++++++++++++++++++++ leanpkg.toml | 5 ++++ 9 files changed, 196 insertions(+) create mode 100644 .gitignore create mode 100644 Demo.lean create mode 100644 Demo/Imperative.lean create mode 100644 Demo/Match.lean create mode 100644 Demo/Math.lean create mode 100644 Demo/Syntax.lean create mode 100644 Demo/Unification.lean create mode 100644 Demo/Vec.lean create mode 100644 leanpkg.toml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..a007fea --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +build/* diff --git a/Demo.lean b/Demo.lean new file mode 100644 index 0000000..ad256dc --- /dev/null +++ b/Demo.lean @@ -0,0 +1,5 @@ +import Init.System.IO + +def main : IO UInt32 := do + IO.println "Hello world!" + return 0 diff --git a/Demo/Imperative.lean b/Demo/Imperative.lean new file mode 100644 index 0000000..5ca56fa --- /dev/null +++ b/Demo/Imperative.lean @@ -0,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 diff --git a/Demo/Match.lean b/Demo/Match.lean new file mode 100644 index 0000000..89e2646 --- /dev/null +++ b/Demo/Match.lean @@ -0,0 +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 diff --git a/Demo/Math.lean b/Demo/Math.lean new file mode 100644 index 0000000..fcbb2c6 --- /dev/null +++ b/Demo/Math.lean @@ -0,0 +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] diff --git a/Demo/Syntax.lean b/Demo/Syntax.lean new file mode 100644 index 0000000..57597be --- /dev/null +++ b/Demo/Syntax.lean @@ -0,0 +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) diff --git a/Demo/Unification.lean b/Demo/Unification.lean new file mode 100644 index 0000000..5cad7fc --- /dev/null +++ b/Demo/Unification.lean @@ -0,0 +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 diff --git a/Demo/Vec.lean b/Demo/Vec.lean new file mode 100644 index 0000000..efacdda --- /dev/null +++ b/Demo/Vec.lean @@ -0,0 +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 diff --git a/leanpkg.toml b/leanpkg.toml new file mode 100644 index 0000000..afafdb0 --- /dev/null +++ b/leanpkg.toml @@ -0,0 +1,5 @@ +[package] +name = "Sudoku" +version = "0.1" +lean_version = "leanprover/lean4:nightly" +path = "." -- 2.45.2