Lecture 2.4: Functional Programming — Metaprogramming

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++)

Example applications

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

Advantages of metaprogramming

But see A Review of the Lean Theorem Prover by Thomas Hales, especially point 4 of "What's not so great about Lean?"

Metaconstants and tactics

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:

Expression type

Expressions may contain

We can create literal expressions conveniently using backticks (quotations)

Tactic monad

Tactics have access to

Tactics can also produce trace messages

The tactic monad is an alternative (with fail and <|>)



Newly introduced syntax


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

Tactic monad

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