Metatheorems

This page is part of the introduction to proving metatheorems with STELF.

In the previous section, we saw how to ask STELF to verify totality assertions, which are a particular form of statement one can make about a deductive system. However, not all that many metatheorems are totality assertions about the judgements of an object language. Moreover, even if a judgement does in fact satisfy a total assertion, the judgement often will not be written in the particular form that allows STELF to automatically check mode, worlds, termination, and coverage. So why are totality assertions so important?

nat : type.
z   : nat.
s   : nat -> nat.

even   : nat -> type.
even-z : even z.
even-s : even (s (s N))
    <- even N.

plus   : nat -> nat -> nat -> type.
plus-z : plus z N2 N2.
plus-s : plus (s N1) N2 (s N3)
    <- plus N1 N2 N3.

How to prove metatheorems

The reason is that we can use STELF’s ability to prove totality assertions to check proofs of more general metatheorems. Let’s illustrate this with an example. Say we want to prove that the sum of two even numbers is even. More precisely, let’s prove the following statement:

If $\mathsf{even}(N_1)$ and $\mathsf{even}(N_2)$ and $\mathsf{plus}(N_1,N_2,N_3)$ then $\mathsf{even}(N_3)$.

We can prove this statement by rule induction on the first premise, the derivation that $\mathsf{even}(N_1)$. The computational content of this proof will be a function that transforms the derivations of the premises into a derivation of the conclusion.

Now, let’s recast this informal theorem statement as a statement about LF terms. By the adequacy of our LF representations as discussed in a previous section, this informal statement is equivalent to a statement about the canonical forms of the corresponding types:

For all DevenN1 : even N1 and DevenN2 : even N2 and Dplus : plus N1 N2 N3 there exists a DevenN3 : even N3.

We can recast the informal proof by rule induction on the derivation of $\mathsf{even}(N_1)$ as a proof by induction on the canonical forms of type even N1. The computational content of this proof will be a transformation from LF terms of type even N1, even N2, and plus N1 N2 N3 to an LF term of type even N3.

The key to the way we use STELF to prove general metatheorems is that we can represent this transformation within LF itself. Specifically, we represent the theorem statement as a type family, which defines a relation on the subjects of the theorem. Then, we represent the proof as LF constants inhabiting that type family. A proof is correct iff it defines a total relation (because the original metatheorem is implied by the totality assertion for the relation). So we deploy STELF’s ability to verify totality assertions in order to check the proof of the metatheorem. Thus, you already have all the tools you need to prove metatheorems with STELF; you just need to use them in the right way.

Our first metatheorem

This will all be clearer once we do an example.

Representing the theorem statement

We represent the above theorem statement in STELF as a type family relating the appropriate derivations:

sum-evens : even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type.
%mode sum-evens +D1 +D2 +Dplus -D3.

The kind of sum-evens is dependent, unlike all the kinds we have seen so far. The dependency ensures that the sum-evens relation relates derivations of the appropriate facts.

The mode declaration for this type family makes the “for all” theorem subjects into inputs, and the “there exists” theorem subject into an output. Intuitively, this is the right thing to do because then the relation defined by sum-evens will transform these three “for all” derivations into the “there exists” derivation. More formally, observe that the mode and worlds declarations declare the following totality assertion:

For all D1 : even N1 and D2 : even N2 and Dplus : plus N1 N2 N3 there exist D3 : even N3 and D : sum-evens D1 D2 Dplus D3.

The above metatheorem statement is clearly a corollary of this totality assertion.

Informally describing the proof

Before we transcribe the informal proof of the metatheorem as LF constants of the appropriate types, let’s review the informal proof.

The proof is by induction over the derivation of $\mathsf{even}(N_1)$.

Case for $\overline{\mathsf{even}(\mathsf{zero})}$:

In this case, $N_1$ is $\mathsf{zero}$, so by inversion the derivation of $\mathsf{plus}(N_1,N_2,N_3)$ must derive $\mathsf{plus}(\mathsf{zero},N_2,N_2)$. Then the assumption of $\mathsf{even}(N_2)$ gives the result.

Case for $\mathsf{even}(N_1’) \over \mathsf{even}(\mathsf{succ}(\mathsf{succ}(N_1’)))$:

In this case, $N_1$ is $\mathsf{succ}(\mathsf{succ}(N_1’))$, so we have a derivation of $\mathsf{plus}(\mathsf{succ}(\mathsf{succ}(N_1’)),N_2,N_3)$. By inversion on this derivation, $N_3$ is $\mathsf{succ}(\mathsf{succ}(N_3’))$ and we have a derivation of $\mathsf{plus}(N_1’,N_2,N_3’)$. Then the inductive hypothesis applied to this derivation and the derivation of $\mathsf{even}(N_2)$ yields a derivation of $\mathsf{even}(N_3’)$. So we can derive

$$\mathsf{even}(N_3’) \over \mathsf{even}(\mathsf{succ}(\mathsf{succ}(N_3’))$$

to finish the case.

LF Representation of the proof

We represent this informal proof as LF constants inhabiting the type family sum-evens. We use the implicit-arguments versions of the definitions from Proving_metatheorems:Full_LF. There will be one constant for each case of the informal proof. The constant corresponding to the first case is:

sez : sum-evens
       even-z
       (DevenN2 : even N2)
       (plus-z : plus z N2 N2)
       DevenN2.

We can read the type of this constant as the above case: when the term of type even N1 is even-z, then N1 is z and the term of type plus N1 N2 N3 must be plus-z. Then the assumed term of type even N2 has the appropriate type for the result.

The constant corresponding to the second case is:

ses : sum-evens
       ( (even-s DevenN1') : even (s (s N1')))
       (DevenN2 : even N2)
       ( (plus-s (plus-s Dplus)) : plus (s (s N1')) N2 (s (s N3')))
       (even-s DevenN3')
       <- sum-evens DevenN1' DevenN2 Dplus DevenN3'.

We invert the derivation of plus by pattern-matching it as two applications of the constant plus-s. The inductive call to the theorem is represented as a premise of type sum-evens on a term DevenN1' that is a subterm of the input term (even-s DevenN1'). The result of the case is created by applying the constant even-s, which corresponds to the rule used in the informal case, to the result of the inductive call.

You should try to get used to the three equivalent ways of thinking about these constants:

• Informal proof: They are a direct transcription of the cases of the informal proof.
• Type inhabitation: They define the relation sum-evens by type inhabitation, in such a way that STELF can prove that the family is inhabited for all inputs.
• Logic programming: They define a total logic program from the inputs to the outputs.

Now that we have represented the proof, all that’s left is to ask STELF to verify this proof by induction on the first argument:

%worlds () (sum-evens _ _ _ _).
%total D (sum-evens D _ _ _).

We call attention to a few of STELF’s checks:

• Termination: In the premise of the constant even-s, the term DevenN1' is a subterm of the input derivation, so the termination check succeeds. In this case, it happens that the term Dplus is also smaller, so we could have checked termination on this argument instead.
• Input Coverage: Because STELF separates termination checking from coverage checking, the constants defining a type family may case-analyze more arguments than just the induction one. This subsidiary case-analyses correspond to inversion steps in an informal proof. If an inversion is not justified (e.g., if in sez there were another way to derive plus z N2 N3 besides plus-z), STELF reports an input coverage error—not all possible input terms are covered.

What metatheorems can we prove this way?

The metatheorems that can be proved in STELF have the form

For all LF terms of some input types, there exist LF terms of some output types.

These metatheorems are called $\forall\exists$-statements, and they are the theorems whose proofs consist of total relations between the input types and the output types.

This means that there are many theorems that cannot be mechanized in STELF (e.g., theorems requiring higher quantifier complexity). However, in practice, $\forall\exists$-statements have been shown to be a useful class of metatheorems about programming languages (for example, they are enough to prove type safety for all of Standard ML).

It is important to recognize that the restriction to $\forall\exists$-statements is a consequence of representing proofs of metatheorems as total relations among LF types. It is not a consequence of representing object languages in LF. Any on-paper proof about an informal description of an object language can be translated into an on-paper proof about the associated adequate LF representation. But only some of these proofs can be mechanically verified in STELF using the techniques presented above.