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