Transporting Theorems Across Context Schemas
Prior to reading the discussion within this page, it’s necessary to have a rough understanding of the syntax of Adelfa and tactics of Adelfa. An explanation of these can be found in the Reference Guide. One may also search using the search bar in the top right to look up terms.
We discuss a series of examples which utilize schema subsumption in Adelfa, a capability in Adelfa which allows one to transport the validity of a formula into one with the context variable typed by a different context schema. When in the scope of Adelfa, this amounts to taking a theorem with a context variable quantification which has been proven, such as one of the form:
Schema C := ...
Theorem transport-ex : ctx G:C, ...and determining when the same proof can be used to complete the same theorem under a different context schema:
Schema C' := ...
Theorem transport-ex' : ctx G:C', ...These examples are intended to be complementary to the paper “Transporting Theorems about Typeability in LF Across Schematically Defined Contexts” but aim to be as self-contained as possible. We suggest reading the following examples in the order presented below as they are intended to build on each other.
- Every lambda calculus terms has a size displays a straightforward use of theorem transport and discusses alternatives as well as their downsides.
- Size of lambda calculus terms does not decrease after substitution shows the use of transport in a larger development order to bring out how avoiding transport causes more work as one’s development grows.
- ORBI completes a standardized benchmark for what is referred to as “Non-Linear Context Extensions,” which schema subsumption permits.