Introduction
The Lean theorem prover is one of several that supports constructing proofs using tactics - commands that allow users to build up proofs step-by-step interactively at a high level of abstraction, usually interspersed with automation (for a demonstration of tactics and an introduction to Lean in general, consult the Natural Number Game). One of the appealing aspects of Lean, especially Lean4, is that there is a robust framework in place for users to write custom tactics within the language, making Lean its own metaprogramming language.
In an attempt to familiarise myself with metaprogramming in Lean4, I have written a simple tactic findProof to construct functions, given their type. The type A -> A, for instance, is inhabited by the identity function, and the type A -> B -> A also has a natural candidate that returns the first parameter ignoring the second. One would ideally like to algorithmically construct such functions from their types, and perhaps even apply this algorithm to obtain constructions arising natually in mathematics such as the adjoint of a linear transformation, the pushforward map between the tangent spaces of manifolds, or the isomorphism in the Gelfand-Naimark theorem of functional analysis.
The rest of the post contains examples of the findProof tactic in action on all the above-mentioned types, followed by a detailed explanation of the algorithm behind the tactic. The code for the tactic is available at this link.
Examples
These are a few functions that were created using the findProof tactic. The name and type of the function are specified by the user, and the actual function body is produced by the tactic. The functions are written according to the usual parenthesis-free style of functional programming.
Identity
The identity function, one of the simplest examples of a function that can be produced from the type information alone.
def ident : {A : Type} → A → A :=
fun {A} a => aFirst projection
A function that projects onto the first input is the most natural candidate for a function of type A -> B -> A.
def proj₁ : {A B : Type} → A → B → A :=
fun {A B} a a_1 => aModus ponens
The rule of inference in propositional logic - modus ponens (if P -> Q as well as P are the premises, the conclusion is Q) - can also be expressed in terms of functions and types by the Curry-Howard correspondence between propositions and types. The types P and Q are of type Type rather than Prop as there are issues with displaying terms of types in the universe Prop.
def modusPonens : {P Q : Type} → (P → Q) → P → Q :=
fun {P Q} a a_1 => a a_1A convoluted example
This is an example demonstrating that the tactic is capable of handling reasonably large types.
def convolutedexample : String → Float → (Unit → Int) → (Int → Nat) → (String → Unit) → Nat :=
fun a a_1 a_2 a_3 a_4 => a_3 (a_2 (a_4 a))Adjoint of a linear transformation
Given a linear transformation $T: V \to W$, one can construct its adjoint $T^{*}: W^{*} \to V^{*}$ between the dual spaces as $T^{*}(w^{*})(v) := w^{*}(T(v))$.
The expression for the adjoint of a linear transformation between vector spaces has a particularly nice form that can be derived in a similar manner to the above examples purely based on the type information.
If the types V F W : Type below are replaced by P Q F : Prop, the type changes to the statement of contraposition of logical implication.
def adjoint : {V W F : Type} → (V → W) → (W → F) → V → F :=
fun {V W F} a a_1 a_2 => a_1 (a a_2)Gelfand-Naimark isomorphism
Another example is the Gelfand-Naimark theorem in functional analysis asserting a bijection between a $C^{*}$-algebra $A$ and $C(\hat{A})$, the ring of continuous complex-valued functions on the set of $C^{*}$-homomorphisms between $A$ and $\mathbb{C}$ (with a suitable topology).
def gelfand_naimark : {A ℂ : Type} → A → (A → ℂ) → ℂ :=
fun {A ℂ} a a_1 => a_1 aTODO The differential map between tangent spaces
If $f:M \to N$ is a map between manifolds, one can define a map $df_{p}$ taking $T_{p}(M)$, the tangent space at the point $p$ of $M$, to $T_{f(p)}(N)$. Here, tangent vectors are regarded as derivations.
Unlike the previous examples, this one requires some special care since there is potential for infinite looping during the proof search (explained in the next section).
The algorithm
A term of the function type A -> B in type theory is usually produced either by recursion (more technically, by applying the induction principle where the source is an inductive type), or by considering an arbitrary element a : A of type A and then producing an element of type B in its context. This algorithm considers only the latter method of constructing functions, since it is applicable even when nothing about the source and target types is known. Therefore, to construct a term of an arbitrary function type A_1 -> (A_2 -> ... (A_n -> B)), terms a_1 : A_1, a_2:A_2, ..., a_n:A_n must first be introduced into the context.
To now construct a term of type B from just the available terms, a good strategy is to scan the context for functions that eventually return B, i.e., terms of type C_1 -> (C_2 -> ... (C_m -> B)), where m is possibly zero. The B at the end must be "unlocked" to use such a term; in other words, terms of all types C_1, C_2, ..., C_m must first be produced to use such a function to construct a term of type B. The problem of generating terms of types C_1, C_2, ..., C_m in the given context is similar to the original one, making a recursive strategy viable.
The tactic succeeds if all terms of types C_1, C_2, ..., C_m can be constructed, and otherwise it moves to the next term in the context that eventually returns B. If the type B cannot be constructed from any of the relevant terms in the context, the tactic fails.
An illustration of the algorithm
Consider the problem of finding an expression for the adjoint of a linear transformation. The corresponding type to be inhabited is (V -> W) -> ((W -> F) -> (V -> F)), where V, W, F are types meant to represent two vector spaces and the underlying field respectively.
Following the algorithm, we first introduce all the relevant variables in the context, so that it becomes V F W : Type, f : V -> W, w* : W -> F, v : V, with the goal now being to construct a term of type F. The term w* : W -> F in the context eventually returns F, but only when given a term of type W. Recursively calling the algorithm changes the goal to W, and f : V -> W is a term that returns W when given a term of type V. However, a term v : V is present in the context.
Chaining these together gives w*(f v), the expression for the adjoint.
—