Proving metatheorems:Summary: the natural numbers

From The Twelf Project

Jump to: navigation, search

Previous:
Proving metatheorems

Proving metatheorems with Twelf

Next:
Higher-order representation of syntax

[edit] 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. Twelf has the ability to verify that a type family represents a total relation.
Proofs of $\forall\exists$ -statements can be mechanized and verified in Twelf by representing them as LF type families.

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

[edit] 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.

[edit] Test yourself

This section is under development. If you try other examples at this point, please add them here. If you try more advanced examples, add them to the next section.

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