From 52746d4472a3736a7046827814ebe6ae8bb839d0 Mon Sep 17 00:00:00 2001 From: von-steinkirch Date: Mon, 16 Jun 2025 16:02:49 -1000 Subject: [PATCH 1/3] first chapters of lean-org book, moar theorem proving for palindrome --- README.md | 4 +- docs/basic_concepts.md | 13 +++++- lake-manifest.json | 4 +- lakefile.lean | 2 +- src/classics/Palindrome.lean | 68 +++++++++++++++++++++++++++- src/examples/PalindromeExamples.lean | 41 ++++++++++++++++- src/proofs/SumsAndMulti.lean | 2 - 7 files changed, 123 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 8b673c8..f92c606 100644 --- a/README.md +++ b/README.md @@ -50,8 +50,8 @@ lake --version - `src.lean`: the main entry point for the source code - `src/`: source code for concepts and `examples/` - `lakefile.lean`: the lean package manager configuration file (TODO: replace with `toml`) -- `lean-toolchain`: specifies the Lean version for the project -- `Makefile`: speficify all available commands +- `lean-toolchain`: specifies the Lean version for the project (elan manages the compiler toolchains) +- `Makefile`: specify all available commands
diff --git a/docs/basic_concepts.md b/docs/basic_concepts.md index f95f09f..9a484f3 100644 --- a/docs/basic_concepts.md +++ b/docs/basic_concepts.md @@ -6,11 +6,20 @@
+* Lean is a strict pure functional language with dependent types + - strictness: function calls work similarly to the way they do in most languages (the arguments are fully computed before the function's body begins running) + - purity: programs cannot have side effects such as modifying locations in memory, sending emails, or deleting files without the program's type saying so. + - functions are first-class values + - the execution model is inspired by the evaluation of mathematical expressions + - dependent types make types into a first-class part of the language * there are two primary concepts in lean: functions and types * basic types examples are natural numbers (`Nat`, whole numbers starting from 0), booleans (`Bool`), true or false values, strings * functions are defined using the `def` keyword (`def double (n : Nat) : Nat := n + n`) -* check types using `#check` -* evaluate expressions using `#eval` +* Lean is an expression-oriented functional language, there are no conditional statements, only conditional expressions (e.g. `String.append "it is " (if 1 > 2 then "yes" else "no")`) +* iterative tests: + - `#check`: verify the type of an expression (without evaluating it) + - `#eval`: evaluate expressions + - `#reduce`: see the normal form of an expression
diff --git a/lake-manifest.json b/lake-manifest.json index 5269ee8..05e1fb6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8744850cc139c0d23086fdabad638f970a983bce", + "rev": "953440dbe5b77d9a00996d6c216a2605a70b5560", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -92,4 +92,4 @@ "inherited": true, "configFile": "lakefile.toml"}], "name": "«lean-toolkit»", - "lakeDir": ".lake"} \ No newline at end of file + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index ca8dec8..0e3bfc4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,4 +15,4 @@ lean_lib «src» { lean_exe Main { root := `Main -} +} diff --git a/src/classics/Palindrome.lean b/src/classics/Palindrome.lean index 8adb9d0..c147568 100644 --- a/src/classics/Palindrome.lean +++ b/src/classics/Palindrome.lean @@ -1,7 +1,11 @@ +import Mathlib.Data.List.Basic +import Mathlib.Data.List.Lemmas + +set_option maxRecDepth 1000 + /-! ## ## a list is a palindrome if and only if you can construct a proof -## of IsPalindrome for it using my rules ## -/ @@ -9,3 +13,65 @@ inductive IsPalindrome {α : Type} : List α → Prop where | nil : IsPalindrome [] | single_case (a : α) : IsPalindrome [a] | sandwich_case (a : α) (l : List α) : IsPalindrome l → IsPalindrome (a :: l ++ [a]) + +/-! +## +## theorems about palindrome properties +## (the most important theorem we can prove is that our inductive definition of a +## palindrome is equivalent to the more common definition: "a list is a palindrome if it +## is equal to its reverse." this ensures our definition is correct) +## +-/ + +theorem isPalindrome_iff_reverse {α : Type} (l : List α) : + IsPalindrome l ↔ l = l.reverse := by + -- the proof is in two parts: → (forward) and ← (backward) + constructor + · -- part 1: prove `IsPalindrome l → l = l.reverse` + -- the strategy is to use induction on the proof of `IsPalindrome l`. + intro h + induction h with + | nil => + -- goal: show [] = [].reverse + simp -- `simp` solves this as `[].reverse` is `[]` + | single_case a => + -- goal: show [a] = [a].reverse + simp -- `simp` solves this as `[a].reverse` is `[a]` + | sandwich_case a l h_inner ih => + -- `h_inner` is the proof that the inner list `l` is a palindrome. + -- `ih` is the induction hypothesis: `l = l.reverse` + -- goal: show `a :: l ++ [a] = (a :: l ++ [a]).reverse` + simp [ih] -- `simp` uses list-reversal lemmas and the induction hypothesis + -- `(a :: l ++ [a]).reverse` simplifies to `[a].reverse ++ l.reverse ++ [a]`, + -- which becomes `[a] ++ l ++ [a]`, and since `l = l.reverse` (by `ih`), + -- it all simplifies to match. + + · -- part 2: prove `l = l.reverse → IsPalindrome l` + -- the strategy here is induction on the list `l` itself. + intro h_rev + induction l with + | nil => + -- goal: prove `IsPalindrome []` + apply IsPalindrome.nil + | cons head tail ih => + -- `head` is the first element, `tail` is the rest of the list. + -- `h_rev` is the hypothesis: `head :: tail = (head :: tail).reverse` + -- we need to prove `IsPalindrome (head :: tail)` + -- from `h_rev`, we know `head :: tail` must end with `head`. + -- this means `tail` must be of the form `middle ++ [head]`. + -- so the original list is `head :: middle ++ [head]`. + -- we can prove that `middle` must also be a palindrome and then use `sandwich_case`. + -- this part of the proof is more involved, requiring helper lemmas about list structure. + -- a full formal proof would be: + have : tail = (List.reverse tail).dropLast := by simp [← h_rev] + have h_ends : tail.getLast? = some head := by simp [← h_rev, List.getLast?_cons] + let mid := tail.dropLast + have h_mid_pal : IsPalindrome mid := by + apply ih + -- proof that `mid = mid.reverse` goes here... + sorry -- this sub-proof is non-trivial + have h_decomp : head :: tail = head :: mid ++ [head] := by + simp [mid, List.dropLast_append_getLast h_ends] + rw [h_decomp] + apply IsPalindrome.sandwich_case + exact h_mid_pal diff --git a/src/examples/PalindromeExamples.lean b/src/examples/PalindromeExamples.lean index 8a44dc3..085dede 100644 --- a/src/examples/PalindromeExamples.lean +++ b/src/examples/PalindromeExamples.lean @@ -3,7 +3,7 @@ import src.classics.Palindrome /-! ## ## this file demonstrates various ways to construct -## proofs of palindromes using the `IsPalindrome` inductive type +## proofs of palindromes using the `isPalindrome` inductive type ## -/ @@ -57,3 +57,42 @@ example : IsPalindrome [true, false, true] := by #check IsPalindrome.sandwich_case 1 [2, 3, 2] (IsPalindrome.sandwich_case 2 [3] (IsPalindrome.single_case 3)) #check IsPalindrome.sandwich_case 'r' (String.toList "ada") (IsPalindrome.sandwich_case 'a' (String.toList "d") (IsPalindrome.single_case 'd')) #check IsPalindrome.sandwich_case true [false] (IsPalindrome.single_case false) + + +/-! +## +## test cases for palindrome properties +## +-/ + +-- test case 1: empty list +example : ([] : List Nat) = ([] : List Nat).reverse := by + simp + +-- test case 2: single element list +example : ([1] : List Nat) = ([1] : List Nat).reverse := by + simp + +-- test case 3: two element palindrome +example : ([1, 1] : List Nat) = ([1, 1] : List Nat).reverse := by + simp + +-- test case 4: three element palindrome +example : ([1, 2, 1] : List Nat) = ([1, 2, 1] : List Nat).reverse := by + simp + +-- test case 5: four element palindrome +example : ([1, 2, 2, 1] : List Nat) = ([1, 2, 2, 1] : List Nat).reverse := by + simp + +-- test case 6: non-palindrome +example : ([1, 2, 3] : List Nat) ≠ ([1, 2, 3] : List Nat).reverse := by + simp + +-- test case 7: string palindrome +example : (String.toList "radar" : List Char) = (String.toList "radar" : List Char).reverse := by + simp + +-- test case 8: boolean list palindrome +example : ([true, false, true] : List Bool) = ([true, false, true] : List Bool).reverse := by + simp diff --git a/src/proofs/SumsAndMulti.lean b/src/proofs/SumsAndMulti.lean index 941cc95..e2e63e0 100644 --- a/src/proofs/SumsAndMulti.lean +++ b/src/proofs/SumsAndMulti.lean @@ -6,7 +6,6 @@ import «src».definitions.Basics ## the same as adding their doubles --> 2(n + m) = 2n + 2m ## -/ - theorem double_add (n m : Nat) : double (n + m) = double n + double m := by -- unfold the definition of double to work with the raw addition unfold double @@ -34,7 +33,6 @@ theorem double_zero : double 0 = 0 := by ## 2(n * m) = (2n) * m ## -/ - theorem double_mul (n m : Nat) : double (n * m) = (double n) * m := by unfold double -- after unfolding, we have: (n * m) + (n * m) = (n + n) * m From 244befa396a30ed279606d6b6db6fa1a60f24eaa Mon Sep 17 00:00:00 2001 From: von-steinkirch Date: Mon, 16 Jun 2025 18:11:02 -1000 Subject: [PATCH 2/3] finish lean-org text --- README.md | 8 +- docs/basic_concepts.md | 301 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 300 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index f92c606..db1506c 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,8 @@ -## 🔮 lean4 toolkit +## 🔮 Lean 4 toolkit
-> *this repository contains examples and explanations as i learn lean4 (a powerful theorem prover and programming language for the AI age)* +> *this repository contains examples and explanations as i learn Lean 4 (a powerful theorem prover and programming language for the AI age)*
@@ -92,8 +92,8 @@ run any other file inside `src/example/` following its command inside `Makefile` #### learning lean -- [learn lean](https://lean-lang.org/documentation/0) -- [lean4 documentation](https://leanprover.github.io/lean4/doc/) +- ✅[learn lean](https://lean-lang.org/documentation/0) +- [Lean 4 documentation](https://leanprover.github.io/lean4/doc/) - [vscode/cursor plugin](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4)
diff --git a/docs/basic_concepts.md b/docs/basic_concepts.md index 9a484f3..f600ae2 100644 --- a/docs/basic_concepts.md +++ b/docs/basic_concepts.md @@ -1,8 +1,8 @@ -## basic concepts +# basic concepts
-### tl; dr +## tl; dr
@@ -15,7 +15,9 @@ * there are two primary concepts in lean: functions and types * basic types examples are natural numbers (`Nat`, whole numbers starting from 0), booleans (`Bool`), true or false values, strings * functions are defined using the `def` keyword (`def double (n : Nat) : Nat := n + n`) +* arguments can be declared implicit by wrapping them in curly braces instead of parentheses when defining a function * Lean is an expression-oriented functional language, there are no conditional statements, only conditional expressions (e.g. `String.append "it is " (if 1 > 2 then "yes" else "no")`) +* some definitions are internally marked as being unfoldable during overload resolution (definitions that are to be unfolded are called reducible) * iterative tests: - `#check`: verify the type of an expression (without evaluating it) - `#eval`: evaluate expressions @@ -25,6 +27,72 @@ --- +## data types + +
+ +### structures + +
+ +* structures enable multiple independent pieces of data to be combined into a coherent whole that is represented by a brand new type + +
+ +```lean +structure Point where + x : Float + y : Float +deriving Repr + +def origin : Point := { x := 0.0, y := 0.0 } + +def addPoints (p1 : Point) (p2 : Point) : Point := + { x := p1.x + p2.x, y := p1.y + p2.y } +``` + +
+ +* Lean provides a convenient syntax for replacing some fields in a structure a la functional programing by using the `with` keyword in a structure initialization: + +```lean +def zeroX (p : Point) : Point := + { p with x := 0 } +``` + +
+ +* every structure has a constructor, that gathers the data to be stored in the newly-allocated data structure + - the constructor for a structure named S is named S.mk: S is a namespace qualifier, and mk is the name of the constructor itself + +
+ +---- + +### linked lists + +
+ +* Lean's standard library includes a canonical linked list datatype, `List` + +```lean +def primesUnder10 : List Nat := [2, 3, 5, 7] +``` + +
+ +* behind the scenes, List is an inductive datatype: + +```lean +inductive List (α : Type) where + | nil : List α + | cons : α → List α → List α +``` + +
+ +--- + ### universes
@@ -54,7 +122,7 @@ def is_empty {α : Type} (l : List α) : Prop :=
-* lean4's type theory is built upon a hierarchy of universes, which are types that contain other types (predicative) +* Lean 4's type theory is built upon a hierarchy of universes, which are types that contain other types (predicative) * this is a hierarchy of universes (Type 0, Type 1, Type 2, ...), where Type is an abbreviation for Type 0 * these universes contain "data" or computational types. * for instance, for a function type `(a : A) → B`, where `A : Type u` and `B : Type v`, the resulting function type itself resides in `Type (max u v)` @@ -73,11 +141,24 @@ def is_empty {α : Type} (l : List α) : Prop := ```lean inductive Nat where | zero : Nat - | succ : Nat → Nat + | succ (n : Nat) : Nat +``` + +or (with two constructors as well) + +```lean +inductive Bool where + | false : Bool + | true : Bool ```
+* datatypes that allow choices are called sum types and datatypes that can include instances of themselves are called recursive datatypes. + - recursive sum types are called inductive datatypes, because mathematical induction may be used to prove statements about them + - inductive datatypes are consumed through pattern matching and recursive functions + + ##### inductive predicative types
@@ -98,7 +179,6 @@ inductive MyList (α : Type u) : Type u where
---- #### `Prop` (propositions) @@ -106,3 +186,214 @@ inductive MyList (α : Type u) : Type u where * impredicative (can quantify over any type, including types in higher universes and even Prop itself) * one can define a proposition that makes a statement about all types (for logical connectives -like `And`, `Or` - and quantifiers - `forall`, `exists`) + +
+ +--- + +### options + +
+ +* not every list has a first entry—some lists are empty +* instead of equipping existing types with a special null value, Lean provides a datatype called `Option` that equips some other type with an indicator for missing values (for instance, a nullable `Int` is represented by `Option Int`) +* introducing a new type to represent nullability means that the type system ensures that checks for null cannot be forgotten +* `Option` has two constructors, some and none: + +```lean +inductive Option (α : Type) : Type where + | none : Option α + | some (val : α) : Option α +``` + +
+ +--- + +### product + +
+ +* the `Prod` structure is a generic way of joining two values together (e.g, Prod Nat String contains a Nat and a String) + +* the structure Prod is defined with two type arguments: + +```lean +structure Prod (α : Type) (β : Type) : Type where + fst : α + snd : β +``` + +* the type `Prod α β` is typically written `α × β` + +
+ +--- + +### sum + +
+ +* the `Sum` datatype is a generic way of allowing a choice between values of two different types (e.g., `Sum String Int` is either a `String` or an `Int`. + +```lean +inductive Sum (α : Type) (β : Type) : Type where + | inl : α → Sum α β + | inr : β → Sum α β +``` + +* these names are abbreviations for "left injection" and "right injection" + +
+ +--- + +## pattern matching + +
+ +```lean +def isZero (n : Nat) : Bool := + match n with + | Nat.zero => true + | Nat.succ k => false +``` + +
+ +* Lean 4 supports various types of patterns: + - literal: match exact literal values + +```lean +match false with +| true => "It's true!" +| false => "It's false!" +``` + - variable: a fresh identifier acts as a variable, matching any value and binding that value to the variable within the right-hand side + +```lean +def isPositive (n : Nat) : Bool := + match n with + | 0 => false + | _ => true +``` + - constructor: match values constructed by a specific constructor of an inductive type (central to working with algebraic data types) + +```lean +inductive Option (α : Type) where +| none : Option α +| some : α → Option α + +def unwrapOption (o : Option Nat) : Nat := + match o with + | Option.none => 0 + | Option.some n => n +``` +- disjunctive: allows a single right-hand side to apply to multiple patterns +```lean +def fib (n : Nat) : Nat := + match n with + | 0 | 1 => 1 + | n' + 2 => fib n' + fib (n' + 1) +``` + +
+ +--- + +## recursivity + +
+ +* inductive datatypes are allowed to be recursive (Nat is an example of such a datatype because succ demands another Nat) +* recursive datatypes can represent arbitrarily large data, limited only by technical factors like available memory +* Lean ensures that every recursive function will eventually reach a base case (ruling out accidental infinite loops - especially important when proving theorems, where infinite loops cause major difficulties + +
+ +---- + +## polymorphism + +
+ +* in functional programming, polymorphism refers to datatypes and definitions that take types as arguments (as opposed to object-oriented programming, where the term refers to subclasses that may override some behavior of their superclass) + +
+ +--- + +## anonymous functions + +
+ +* define functions inline without giving them a specific name +* the most common way to define an anonymous function in Lean 4 is using the fun keyword + +```lean +fun (parameter_name : Type) => expression +``` + +* Lean also supports the traditional lambda calculus notation using the λ + +```lean +#check λ (x : Nat) => x * x +-- Output: fun x => x * x : Nat → Nat +``` + +* pattern matching can be used within anonymous functions, particularly useful when the function's behavior depends on the structure of its input + +```lean +inductive Option (α : Type) where + | none : Option α + | some : α → Option α + +def unwrapOptionOrDefault (defaultVal : Nat) : Option Nat → Nat := + fun + | Option.none => defaultVal + | Option.some n => n + +#eval unwrapOptionOrDefault 0 (Option.some 5) -- 5 +#eval unwrapOptionOrDefault 0 Option.none -- 0 +``` + +* for very simple anonymous functions, Lean 4 provides the · (dot) character (often used for operations that involve an infix operator or a function application) + +```lean +def twice (f : Nat → Nat) (a : Nat) := f (f a) + +#eval twice (fun x => x + 2) 10 -- 14 +#eval twice (· + 2) 10 -- 14 (using shorthand) +#eval (· * 10) 5 -- 50 +``` + +
+ +--- + +## namespaces + +
+ +* each name in Lean occurs in a namespace, which is a collection of names +* names are placed in namespaces using . (e.g., `List.map` is the name map in the List namespace) +* names can be directly defined within a namespace: + +```lean +def Nat.double (x : Nat) : Nat := x + x +``` + +* because Nat is also the name of a type, dot notation is available to call Nat.double on expressions with type Nat: + +```lean +#eval (4 : Nat).double +8 +``` + +* namespaces may be opened, which allows the names in them to be used without explicit qualification + +```lean +open NewNamespace in +#check quadruple +NewNamespace.quadruple (x : Nat) : Nat +``` \ No newline at end of file From 59eb3bb2ce56b645b1e57a1347dcdf7ec11d369e Mon Sep 17 00:00:00 2001 From: von-steinkirch Date: Mon, 16 Jun 2025 18:47:06 -1000 Subject: [PATCH 3/3] add fermat last theorem to create theorems later --- README.md | 16 ++++++++++------ src/proofs/FermatLastTheorem.lean | 22 ++++++++++++++++++++++ 2 files changed, 32 insertions(+), 6 deletions(-) create mode 100644 src/proofs/FermatLastTheorem.lean diff --git a/README.md b/README.md index db1506c..e8813eb 100644 --- a/README.md +++ b/README.md @@ -49,7 +49,7 @@ lake --version - `src.lean`: the main entry point for the source code - `src/`: source code for concepts and `examples/` -- `lakefile.lean`: the lean package manager configuration file (TODO: replace with `toml`) +- `lakefile.lean`: the lean package manager configuration file - `lean-toolchain`: specifies the Lean version for the project (elan manages the compiler toolchains) - `Makefile`: specify all available commands @@ -84,17 +84,21 @@ run any other file inside `src/example/` following its command inside `Makefile` #### my notes -
- - [basics](docs/basic_concepts.md)
#### learning lean -- ✅[learn lean](https://lean-lang.org/documentation/0) -- [Lean 4 documentation](https://leanprover.github.io/lean4/doc/) -- [vscode/cursor plugin](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) +- ✅[learn Lean](https://lean-lang.org/documentation/0) +- 🟡[Lean 4 documentation](https://leanprover.github.io/lean4/doc/) +- 🟡[mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html) +- 🟡[theorem proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/) + + +#### useful + +- 🟡[vscode/cursor plugin](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4)
diff --git a/src/proofs/FermatLastTheorem.lean b/src/proofs/FermatLastTheorem.lean new file mode 100644 index 0000000..9edd28d --- /dev/null +++ b/src/proofs/FermatLastTheorem.lean @@ -0,0 +1,22 @@ +/- +## +## for the lolz +## +-/ + +#check 2 + 2 = 4 + +def FermatLastTheorem := + ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n + +#check FermatLastTheorem + +theorem easy : 2 + 2 = 4 := + rfl + +#check easy + +theorem hard : FermatLastTheorem := + sorry + +#check hard