diff --git a/README.md b/README.md
index 8b673c8..e8813eb 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)*
@@ -49,9 +49,9 @@ 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
+- `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)
-- [lean4 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/docs/basic_concepts.md b/docs/basic_concepts.md
index f95f09f..f600ae2 100644
--- a/docs/basic_concepts.md
+++ b/docs/basic_concepts.md
@@ -1,16 +1,93 @@
-## basic concepts
+# basic concepts
-### tl; dr
+## tl; dr
+* 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`
+* 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
+ - `#reduce`: see the normal form of an expression
+
+
+
+---
+
+## 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 α
+```
@@ -45,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)`
@@ -64,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
@@ -89,7 +179,6 @@ inductive MyList (α : Type u) : Type u where
----
#### `Prop` (propositions)
@@ -97,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
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/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
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