Lean
A guided introduction to Lean for theorem proving, formalization, and proof engineering.
Tag
Proof-Assistant
80 notes
Preface
This book is a working manual for the Lean proof assistant.
4.25 Common Pitfalls and Debugging
Rewriting failures in Lean usually come from a small set of recurring issues.
4.24 Rewriting Strategies and Heuristics
Rewriting is most effective when guided by a small set of consistent strategies.
4.23 Rewriting in Goals vs Hypotheses
Rewriting can target either the goal or the local context.
4.22 Rewriting with `conv`
The `conv` tactic provides fine-grained control over rewriting.
4.21 Rewriting in Pattern Matching
Pattern matching performs case analysis by selecting a branch based on the shape of a value.
4.20 Decidable Equality and Boolean Bridges
Reasoning often alternates between propositional equality `a = b` and boolean equality `a == b`.
4.19 Proof Irrelevance and Equality of Proofs
In Lean, propositions live in `Prop`, a universe where proof irrelevance holds.
4.18 Rewriting of Functions and Extensionality
Equality between functions requires a different treatment than equality between values.
4.17 Rewriting in Structures and Records
Structures package multiple fields into a single value.
4.16 Rewriting with Equivalences
Equalities are often too strict.
4.15 Avoiding Rewrite Loops and Nontermination
Rewriting systems can diverge if rules are poorly oriented or interact cyclically.
4.14 Dependent Rewriting and Transport
When types depend on values, rewriting affects both terms and their types.
4.13 Substitution and `subst`
Substitution is the direct elimination of equalities from the context.
4.12 Rewriting Under Binders
Rewriting becomes more subtle when the target term appears inside a binder.
4.11 Chained Rewriting and `calc`
Complex equalities are rarely achieved in a single step.
4.10 Rewriting with Lemmas
Lemmas provide reusable equalities that drive most rewriting.
4.9 Rewriting with Hypotheses
In most proofs, equalities come from the local context.
4.8 Case Analysis and Rewriting
Case analysis splits a goal according to the structure of a value.
4.7 Controlling the `simp` Set
The behavior of `simp` depends entirely on the set of rewrite rules it uses.
4.6 Simplification with `simp`
The tactic `simp` performs normalization by repeated rewriting using a curated set of lemmas.
4.5 Directed Rewriting with `rw`
Rewriting is the primary way to apply propositional equalities in Lean.
4.4 Congruence and Contextual Rewriting
Equality becomes useful when it propagates through larger expressions.
4.3 Reflexivity, Symmetry, and Transitivity
Propositional equality in Lean is generated from a small set of core operations.
4.2 Propositional Equality
Propositional equality is the explicit notion of equality in Lean.
4.1 Definitional Equality
Definitional equality is the built-in notion of equality used by the kernel of Lean.
Chapter 4. Equality and Rewriting
This chapter isolates the operational core of reasoning in Type Theory as implemented by Lean: equality and its use as a transport mechanism.
2.25 Common Proof Mistakes and Debugging
Lean proofs fail in predictable ways.
2.24 Simplification and Automation
Lean provides automation to reduce routine proof steps.
2.23 Rewriting Strategies
Rewriting with equality is one of the most frequent operations in Lean.
2.22 Backward Reasoning
Backward reasoning starts from the goal and reduces it to simpler subgoals.
2.21 Forward Reasoning
Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate.
2.20 Using Assumptions Effectively
An assumption is a local term that Lean may use to solve the current goal or produce another proof.
2.19 Local Context Management
The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof.
2.18 Naming Conventions
Names in Lean carry meaning.
2.17 Proof Structuring Patterns
A Lean proof should expose the shape of the argument.
2.16 Introduction and Elimination Rules
Every logical connective in Lean has two sides.
2.15 Case Analysis
Case analysis is the proof pattern for using data that has more than one possible constructor.
2.14 Proof by Contradiction
Proof by contradiction is a classical proof pattern.
2.13 Classical vs Constructive Logic
Lean is constructive by default.
2.12 Universal Quantifiers
A universal statement asserts that a property holds for every element of a type.
2.11 Existential Quantifiers
An existential statement says that some object exists with a given property.
2.10 Symmetry and Transitivity
Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity).
2.9 Rewriting with Equality
Rewriting is the main way to use equality in Lean.
2.8 Equality Basics
Equality expresses that two terms are identical.
2.7 True and Trivial Proofs
`True` is the proposition that always has a proof.
2.6 False and Contradiction
`False` is the proposition with no constructors.
2.5 Negation
Negation represents "not".
2.4 Disjunction
Disjunction represents "or".
2.3 Conjunction
Conjunction represents "and".
2.2 Implication and Functions
Implication is the first logical connective to understand in Lean because it is also the ordinary function type.
2.1 Propositions as Types
Lean identifies propositions with types and proofs with terms.
Chapter 2. Propositions and Proofs
This chapter introduces the proof layer of Lean.
1.25 Minimal Working Examples
A minimal working example is the smallest complete Lean fragment that demonstrates a definition, theorem, error, or technique.
1.24 Editor Integration
Lean is normally developed inside an editor with live feedback.
1.23 Interactive Development Workflow
Lean development is interactive.
1.22 Imports and Dependencies
Imports control what a Lean file can see.
1.21 Error Messages and Debugging
Lean’s error messages report failed constraints during elaboration.
1.20 Holes and Goals
Lean development is driven by goals.
1.19 Term Mode vs Tactic Mode
Lean proofs are terms.
1.18 Basic Tactic Mode
Tactic mode is an interactive way to build proofs.
1.17 Structures and Records
A structure is a type whose values are built from named fields.
1.16 Inductive Types Introduction
Inductive types define data by listing its constructors.
1.15 Pattern Matching Basics
Pattern matching defines functions by cases on the shape of their inputs.
1.14 Simple Rewriting
Rewriting replaces one expression with another using an equality.
1.13 Checking Types with `#check`
Type checking is the primary feedback mechanism in Lean.
1.12 Evaluation with `#eval`
Lean can execute many expressions during development.
1.11 Comments and Documentation
Lean files serve two readers at once: the compiler and the human maintainer.
1.10 Notation and Infix Operators
Lean notation is ordinary syntax attached to ordinary declarations.
1.9 Implicit and Explicit Arguments
Lean functions often contain arguments that the user does not write.
1.8 Functions and Lambda Abstraction
Functions are the main form of computation in Lean.
1.7 Types and Universes
Lean is a dependently typed system.
1.6 Theorems with `theorem` and `lemma`
Lean treats a theorem as a named proof.
1.5 Definitions with `def`
A definition introduces a named term together with its type.
1.4 Basic Syntax and Expressions
Lean code is built from expressions.
1.3 Files, Namespaces, and Modules
Lean organizes code as a hierarchy of modules.
1.2 Project Structure with Lean and Lake
Lean development is organized around projects.
1.1 Installation and Toolchain
Lean is distributed as a small toolchain rather than as a single editor plugin.
Chapter 1. Core Language and Environment
This chapter establishes the operational model of the Lean system.