4.25 Common Pitfalls and Debugging
Rewriting failures in Lean usually come from a small set of recurring issues.
Tag
Functional-Programming
50 notes
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.
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.