Hints on Proving Theorems in Twelf

Andrew W. Appel

To run this tutorial, unpack the tar file, and use Emacs to visit the README file.

You may browse the tutorial on the web by clicking the links below, but that is a poor substitute for the interactive problem-solving you get by running it in Emacs.

Contents:

proving.elf

1. The mechanics of running Twelf.
2. Proving a theorem.
3. Organization of the object logic.
4. Examples using and, and_i, and_l.
5. Proof style.

proving2.elf

6. Implication elimination and introduction; metalogic vs. object logic.
7. Or, false, not.

proving3.elf

8. Twelf metalogic quantification.
9. Types in the object logic.
10. Creating object-logic functions and predicates.
11. Object logic quantification.

proving4.elf

12. Equality and congruence
13. Forward proof using "cut"
14. Twelf Traps and pitfalls
15. Object-logic definitions

proving5.elf

16. A case study

proving6.elf

17. Coping with nonstrictness
18. A case study in strictness and type inference (by Kedar Swadi)

proving7.elf

19. Extensionality & Equivalence Relations