Tutorials

⚠️ All the tutorials on this page assume some familiarity with STELF. If you are just getting started, check out Proving metatheorems with STELF or one of the other introductions to STELF. ⚠️

Proof techniques

These tutorials cover helpful and common STELF devices. Many of these proof techniques are also demonstrated by various case studies.

Beginner

• Reformulating languages to use hypothetical judgements - how to present judgements in a way that’s easy to encode in LF.
• Holes in metatheorems - how to assume lemmas while developing proofs.
• Equality - how to represent equality of LF terms as a type family.
• Respects lemmas - how to prove that other families and constants respect equality and other relations.
• Uniqueness lemmas - how to prove that the inputs to a relation determine an output uniquely.
• Effectiveness lemmas - how to prove totality assertions explicitly.
• Output factoring - how to reason from a disjunction. Illustrates proving the progress theorem for a programming language.
• Reasoning from false - how to do proofs by contradiction.
• Catch-all cases - how to avoid putting a theorem case in the LF context.
• Mutual induction - how to prove mutually inductive theorems
• Converting between implicit and explicit parameters - how to convert between implicit and explicit quantification of the parameters of a type family.

Advanced

• Strengthening - how to convince STELF that a term does not depend on some assumptions.
• Explicit termination metrics - how to use a termination metric other than the subderivation ordering.
  • Numeric termination metrics - how to use numbers to induct on the size of some argument.
  • Structural termination metrics - how to use fancier termination metrics that capture the structure of an argument directly.
• Simplifying dynamic clauses - how to streamline certain proofs about relations that introduce hypotheses.
• Canonical forms lemma for a progress theorem - how to get this lemma for free when you can, and how to prove it explicitly using equality when you can’t.
• Structural properties of a hypothetical judgement - how to get structural properties for free when you can, and how to prove them explicitly when you can’t.
  • Weakening
  • Exchange
  • Substitution
• Evaluation contexts - how to represent evaluation contexts as LF functions
• User-defined constraint domains - how to make encodings more intrinsic by replacing predicates with indexing, and how to use Church-encodings to create special index types that are similar to constraint domains in that they admit non-trivial equations on their elements. For larger examples of STELF in action, see see the case studies.

Troubleshooting

These tutorials cover diagnosing and fixing STELF errors.

• Error messages - brief explanations of (and remedies for) common STELF error messages.
• Troubleshooting mode checking errors
• Understanding output freeness - understanding a subtle part of output coverage checking.
• Debugging coverage errors - techniques for finding coverage errors.
• Constraint domains and coverage checking - in general, you can’t use them in the same signature.