# 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
_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
* **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_
## Advantages of metaprogramming
* 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](https://jiggerwit.wordpress.com/2018/09/18/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:
* `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.
## Expression type
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)
## Tactic monad
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 `<|>`)
## Demo
[`24_lecture.lean`](24_lecture.lean)
## Newly introduced syntax
### Declarations
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
### Notations
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
### Metatypes
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
## References
* [_Programming in Lean_](https://leanprover.github.io/programming_in_lean/), Chapters 8 and 9
Further reading:
* [A Metaprogramming Framework for Formal Verification](https://leanprover.github.io/papers/tactic.pdf) by Gabriel Ebner et al. (slightly outdated)
## Acnkowledgment
These notes are partly inspired by Gabriel Ebner et al.'s article [A Metaprogramming Framework for Formal Verification](https://leanprover.github.io/papers/tactic.pdf)