Hints on Proving Theorems in Twelf
Andrew W. Appel
Princeton University, February 2000
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.
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.
6. Implication elimination and introduction; metalogic vs. object logic.
7. Or, false, not.
8. Twelf metalogic quantification.
9. Types in the object logic.
10. Creating object-logic functions and predicates.
11. Object logic quantification.
12. Equality and congruence
13. Forward proof using "cut"
14. Twelf Traps and pitfalls
15. Object-logic definitions
16. A case study
17. Coping with nonstrictness
18. A case study in strictness and type inference (by Kedar Swadi)
19. Extensionality & Equivalence Relations