Summary

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

Take-aways

The three things to remember from this section are:

• Object-language syntax and judgements are represented as LF terms of corresponding types. These representations are adequate iff they are isomorphic to the original description of the object language.
• An LF type family defines a relation on its indices. STELF has the ability to verify that a type family represents a total relation.
• Proofs of $\forall\exists$-statements can be mechanized and verified in STELF by representing them as LF type families.

At a high level, that’s all there is to know about proving metatheorems with STELF.

What’s next?

So far, we have used only first-order LF representations (we haven’t used LF variables or lambdas for anything yet). That’s reasonable, since the natural numbers and the judgements we defined about them are first-order things.

However, one of the main benefits of LF is that the above methodology scales gracefully to programming languages with binding structure. This is the subject of the next section.

Test yourself

Before going on to the next section, you may wish to test yourself with the following exercises.

1. State and prove a metatheorem showing that plus is commutative. (Solution)
2. Define the odd numbers with a judgement analogous to the even judgement defined above. (Solution)
3. State and prove a theorem succ-even that shows that the successor of an even number is an odd number. After that, state and prove a theorem succ-odd that shows that the successor of an odd number is an even number. (Solution)
4. Prove remaining properties of how evenness and oddness interacts with addition. (Hint: some of the most straightforward solutions to these exercises reuse one or more results from previous exercises.) (Solution):
   • State and prove the theorem sum-even-odd that shows that the sum of an even and an odd number results in an odd number
   • State and prove a theorem sum-odd-even that shows that the sum of an odd plus an even number produces an odd number
   • Finally, state and prove a theorem sum-odds that shows that the sum of two odd numbers produces an even number