Transporting Theorems Across Context Schemas

Prior to reading the discussion within this page, it’s necessary to have a rough understanding of the syntax and tactics of Adelfa. We recommend the reader explore the provided walkthrough or have the reference guide at hand. You may also search using the search bar in the top right to look up terms.

If you’d like to install Adelfa and try things out for yourself, you must install this pre-release version which implements the transport rule.

Some code blocks in the examples show the proof state after each command if the terminating symbol (.) is hovered over or clicked. The latter method allows easier scrolling in larger outputs. Try hovering over the following commands to see the output:

Theorem hover-example : false => true.
intros. case H1.

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 $\Pi \Gamma{:}\mathcal{C}.F$ 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.

Adelfa will always transport a proof if it’s able to by default. If you would like to follow along with the examples, we recommend using Set schema_sub false. in sections are discussing how the proof would proceed without using the transport rule.

1. Every lambda calculus term has a size displays a straightforward use of theorem transport and discusses alternatives as well as their downsides.
2. 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.
3. ORBI completes a standardized benchmark for what is referred to as “Non-Linear Context Extensions,” which schema subsumption permits.