Lean 4 Cheatsheet

Cheatsheet Content

### Basic Syntax - **Comments:** - Single line: `-- This is a comment` - Multi-line: `/- This is a multi-line comment -/` - **Variables:** `def x := 5` (immutable) - **Functions:** ```lean def add (a b : Nat) : Nat := a + b ``` - **Types:** `Nat`, `Int`, `Bool`, `Prop` (propositions), `Type` (types) - **Imports:** `import Mathlib.Data.Nat.Basic` ### Proof Basics - **Proposition:** `P : Prop` - **Theorem:** ```lean theorem my_theorem (hA : A) (hB : B) : A ∧ B := And.intro hA hB ``` - **Proof by `rfl`:** `a = a` - **Proof by `exact`:** `exact hP` (if `hP` is a proof of the goal) - **Proof by `apply`:** `apply f h_arg` (if goal is `B` and `f : A → B`) - **Proof by `intro`:** `intro h` (introduces hypothesis `h` for an implication `A → B`) - **Proof by `have`:** `have hC : C := by ...` (introduces a new hypothesis `hC` by proving `C`) - **Proof by `calc`:** For equational reasoning. ```lean example (a b c : Nat) : a + b + c = a + (b + c) := calc a + b + c = (a + b) + c := Nat.add_assoc a b c _ = a + (b + c) := rfl ``` ### Common Tactics - **`intro`:** Introduces hypotheses for implications (`A → B`). - **`apply`:** Applies a theorem or hypothesis (`A → B`) to prove `B`, generating `A` as a new goal. - **`exact`:** Closes the current goal if the term provided matches the goal exactly. - **`rfl`:** Proves equality goals `t = t`. - **`rw` (rewrite):** Rewrites an expression using an equality. `rw [h_eq]` or `rw [h_eq] at h_target`. - **`simp` (simplify):** Applies simplification lemmas to the goal. `simp [h_lemma]` - **`cases`:** Splits a goal based on a disjunction or an inductive type. `cases h_or with hL hR`. - **`induction`:** For proofs by induction on natural numbers or other inductive types. - **`specialize`:** Specializes a universal hypothesis. `specialize h_forall a`. - **`unfold`:** Unfolds definitions. `unfold my_def`. - **`dsimp`:** Simplifies definitions in hypotheses. - **`linarith`:** Solves linear arithmetic goals. - **`tauto`:** Solves propositional tautologies. ### Inductive Types - **Definition:** Creating new data types or propositions. ```lean inductive MyList (α : Type) : Type | nil : MyList α | cons (head : α) (tail : MyList α) : MyList α inductive MyOr (A B : Prop) : Prop | inl (hA : A) : MyOr A B | inr (hB : B) : MyOr A B ``` - **Pattern Matching:** ```lean def list_length (xs : MyList α) : Nat := match xs with | MyList.nil => 0 | MyList.cons _ tail => 1 + list_length tail ``` - **Recursion:** Defined using `match` or `rec`. ### Structures & Type Classes - **Structures:** Grouping data. ```lean structure Point where x : Float y : Float def origin : Point := { x := 0.0, y := 0.0 } ``` - **Type Classes:** Ad-hoc polymorphism. ```lean class Additive (α : Type) where add : α → α → α zero : α instance : Additive Nat where add := Nat.add zero := 0 #check (Additive.add Nat.additive 5 3) -- 8 ``` - **`instance`:** Provides an implementation for a type class for a specific type. - **`variable`:** Declares local variables that can be used in subsequent definitions/theorems. ### Metaprogramming (Macros) - **Macros:** Extending Lean's syntax. ```lean macro "my_macro!" t:term : term => `($t + 1) #eval my_macro! 5 -- 6 ``` - **`elab`:** More powerful elaboration for custom syntax. ### Useful Commands - **`#check`:** Displays the type of an expression. `#check 5 + 3` - **`#eval`:** Evaluates an expression. `#eval 5 + 3` - **`#print`:** Prints information about a declaration. `#print Nat.add` - **`#synth`:** Synthesizes a type class instance. `#synth Additive Nat` - **`#set_option pp.all true`:** Shows all implicit arguments and type class instances. - **`#guard_msgs`:** Ensures that specific messages are produced (useful for testing macros). - **`#reduce`:** Reduces an expression to its normal form. ### Mathlib Integration - **`import Mathlib.Data.Nat.Basic`:** Imports basic natural number definitions and theorems. - **`import Mathlib.Tactic.Linarith`:** Imports the `linarith` tactic. - **`import Mathlib.Algebra.Group.Basic`:** Imports group theory definitions. - **Navigating Mathlib:** Use VS Code's "Go to Definition" (F12) to explore library code.