9. 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.

  1. 9.1. Running Tactics
  2. 9.2. Reading Proof States
    1. 9.2.1. Hiding Proofs and Large Terms
    2. 9.2.2. Metavariables
  3. 9.3. The Tactic Language
    1. 9.3.1. Control Structures
      1. 9.3.1.1. Success and Failure
      2. 9.3.1.2. Branching
      3. 9.3.1.3. Goal Selection
        1. 9.3.1.3.1. Sequencing
        2. 9.3.1.3.2. Working on Multiple Goals
      4. 9.3.1.4. Focusing
      5. 9.3.1.5. Repetition and Iteration
    2. 9.3.2. Names and Hygiene
      1. 9.3.2.1. Accessing Assumptions
    3. 9.3.3. Assumption Management
    4. 9.3.4. Local Definitions and Proofs
    5. 9.3.5. Configuration
    6. 9.3.6. Namespace and Option Management
      1. 9.3.6.1. Controlling Unfolding
  4. 9.4. Options
  5. 9.5. Tactic Reference
    1. 9.5.1. Assumptions
    2. 9.5.2. Quantifiers
    3. 9.5.3. Relations
      1. 9.5.3.1. Equality
    4. 9.5.4. Lemmas
    5. 9.5.5. Falsehood
    6. 9.5.6. Goal Management
    7. 9.5.7. Cast Management
    8. 9.5.8. Extensionality
    9. 9.5.9. Simplification
    10. 9.5.10. Rewriting
    11. 9.5.11. Inductive Types
      1. 9.5.11.1. Introduction
      2. 9.5.11.2. Elimination
    12. 9.5.12. Library Search
    13. 9.5.13. Case Analysis
    14. 9.5.14. Decision Procedures
      1. 9.5.14.1. SAT Solver Integration
    15. 9.5.15. Control Flow
    16. 9.5.16. Term Elaboration Backends
    17. 9.5.17. Debugging Utilities
    18. 9.5.18. Other
  6. 9.6. Targeted Rewriting with conv
    1. 9.6.1. Control Structures
    2. 9.6.2. Goal Selection
    3. 9.6.3. Navigation
    4. 9.6.4. Changing the Goal
      1. 9.6.4.1. Reduction
      2. 9.6.4.2. Simplification
      3. 9.6.4.3. Rewriting
    5. 9.6.5. Nested Tactics
    6. 9.6.6. Debugging Utilities
    7. 9.6.7. Other
  7. 9.7. Custom Tactics
    1. 9.7.1. Tactic Macros
      1. 9.7.1.1. Extensible Tactic Macros
    2. 9.7.2. The Tactic Monad
      1. 9.7.2.1. Control
      2. 9.7.2.2. Expressions
      3. 9.7.2.3. Source Locations
      4. 9.7.2.4. Goals
      5. 9.7.2.5. Term Elaboration
      6. 9.7.2.6. Low-Level Operations
        1. 9.7.2.6.1. Monad Class Implementations
        2. 9.7.2.6.2. Macro Expansion
        3. 9.7.2.6.3. Case Analysis
        4. 9.7.2.6.4. Simplifier
        5. 9.7.2.6.5. Attributes