7. Tactic Proofs
The tactic language is a special-purpose programming language for constructing proofs. In Lean, propositions are represented by types, and proofs are terms that inhabit these types. The section on propositions describes propositions in more detail. While terms are designed to make it convenient to indicate a specific inhabitant of a type, tactics are designed to make it convenient to demonstrate that a type is inhabited. This distinction exists because it's important that definitions pick out the precise objects of interest and that programs return the intended results, but proof irrelevance means that there's no technical reason to prefer one proof term over another. For example, given two assumptions of a given type, a program must be carefully written to use the correct one, while a proof may use either without consequence.
Tactics are imperative programs that modify a proof state.
A proof state consists of an ordered sequence of goals, which are contexts of local assumptions together with types to be inhabited; a tactic may either succeed with a possibly-empty sequence of further goals (called subgoals) or fail if it cannot make progress.
If tactic succeeds with no subgoals, then the proof is complete.
If it succeeds with one or more subgoals, then its goal or goals will be proved when those subgoals have been proved.
The first goal in the proof state is called the main goal.
While most tactics affect only the main goal, operators such as <;>
and all_goals
can be used to apply a tactic to many goals, and operators such as bullets, next
or case
can narrow the focus of subsequent tactics to only a single goal in the proof state.
Behind the scenes, tactics construct proof terms. Proof terms are independently checkable evidence of a theorem's truth, written in Lean's type theory. Each proof is checked in the kernel, and can be verified with independently-implemented external checkers, so the worst outcome from a bug in a tactic is a confusing error message, rather than an incorrect proof. Each goal in a tactic proof corresponds to an incomplete portion of a proof term.
- 7.1. Running Tactics
- 7.2. Reading Proof States
- 7.3. The Tactic Language
- 7.4. Options
-
7.5. Tactic Reference
- 7.5.1. Assumptions
- 7.5.2. Quantifiers
- 7.5.3. Relations
- 7.5.4. Lemmas
- 7.5.5. Falsehood
- 7.5.6. Goal Management
- 7.5.7. Cast Management
- 7.5.8. Extensionality
- 7.5.9. Simplification
- 7.5.10. Rewriting
- 7.5.11. Inductive Types
- 7.5.12. Library Search
- 7.5.13. Case Analysis
- 7.5.14. Decision Procedures
- 7.5.15. Control Flow
- 7.5.16. Term Elaboration Backends
- 7.5.17. Debugging Utilities
- 7.5.18. Other
-
7.6. Targeted Rewriting with
conv
- 7.7. Custom Tactics