We learned in lecture 2.3 how to use monads to program with implicit state and failure
Users can extend Lean with custom monadic tactics and tools
Metaprogramming: Program the prover in its own language, using a monadic language
Abstract syntax trees reflect internal data structures, e.g. for expressions (terms)
The prover's C++ internals are exposed through Lean interfaces, which we can use for accessing the current context and goal, unifying expressions, querying and modifying the environment, and setting attributes (e.g. @[simp])
Most of Lean's predefined tactics are implemented in this way (and not in C++)
Proof goal transformations (e.g. apply all safe introduction rules for connectives, put the goal in negation normal form)
Heuristic proof search (e.g. apply unsafe introduction rules for connectives and hypotheses but with backtracking)
Decision procedures (e.g. for propositional logic, linear arithmetic)
Definition generators (e.g. Haskell-style derive for inductive types)
Advisor tools (e.g. lemma finders, counterexample generators)
Exporters (e.g. documentation generators)
Ad hoc automation (to avoid boilerplate or duplication)
In principle, we could do everything with copy-paste, proof terms and predefined tactics, and grep (or Ctrl+P/Cmd+P, #... in Visual Studio Code), but
Users (e.g. mathematicians) do not need to learn another programming language to write metaprograms; they can work with the same constructs and notation used to define ordinary objects in the prover's library
Everything in that library is available for metaprogramming purposes (e.g. ℤ, list, algebraic structures)
Metaprograms can be written and debugged in the same interactive environment, encouraging a style where formal libraries and supporting automation are developed at the same time
But see A Review of the Lean Theorem Prover by Thomas Hales, especially point 4 of "What's not so great about Lean?"
Any executable (i.e. not defined using noncomputable) Lean definition can be used as a metaprogram
In addition, we can put meta in front of a definition to indicate that is a metadefinition; these need not terminate but cannot be used in non-meta contexts
Metaprograms (whether defined with meta or not) can communicate with Lean through metaconstants, which are implemented in C++ and have no logical meaning (i.e. they are opaque names)
Important types:
name: hierarchical names
expr: terms, types, proofs are represented as abstract syntax trees
tactic: the tactic monad, which contains the proof state, the environment, etc.
Expressions may contain
metavariables, correponding to holes in expressions (e.g. _, ? variables, subgoals)
local constants, corresponding to the hypotheses
bound variables, which refer variables bound by λ and Π (∀), using De Bruijn indices (in its locally nameless variant)
We can create literal expressions conveniently using backticks (quotations)
Tactics have access to
the list of goals as metavariables (each metavariables has a type and a local context (hypothesis); they can optionally be instantiated)
the elaborator (to elaborate expressions and compute their type)
the attributes (e.g. the list of simp-rules)
the environment, containing all declarations and inductive types
Tactics can also produce trace messages
The tactic monad is an alternative (with fail and <|>)
| Syntax | Description |
|---|---|
meta |
prefix for declarations in meta Lean; constant cannot be used in proofs. |
run_cmd |
executes a tactic on the top level, without a proof context |
| Syntax | Description |
|---|---|
`h |
quotation: literal syntax for check names |
``h |
quotation: literal syntax for un-checked names |
`(e) |
quotation: fully elaborated expressions, without holes |
``(e) |
quotation: pre-expressions with checked names |
```(e) |
quotation: pre-expressions without checked names |
%%e |
antiquotation to insert a expression into a quotation |
| Name | Description |
|---|---|
expr |
Represents expression, i.e. terms, types and proofs |
name |
Represents names, i.e. hierarchical identifiers |
parser |
Describes the syntax of interactive tactics |
tactic |
Provides the tactic monad and a namespace for most tactics |
| Function | Description |
|---|---|
trace |
Outputs a debug string |
get_local |
Finds a local constant (i.e. expression) by name |
local_context |
Gives the list of all local constants, i.e. all assumptions in the proof |
infer_type |
Computes the type of an expression |
to_expr |
Elaborates a pre-expression |
target |
Gives the current statement to prove |
get_goals |
Gives the list of all proof holes to fill in |
Further reading:
These notes are partly inspired by Gabriel Ebner et al.'s article A Metaprogramming Framework for Formal Verification