Lambda calculus terms have a size

In this example we will discuss schema subsumption, a capability in Adelfa which allows one to "transport" a formula with a context variable typed by one context schema to a different context schema. This becomes especially useful when using lemmas.

The complete developments are provided here for reference:

• Signature: size.lf
• Proof development without transport: size-no-transport.ath
• Proof development with transport: size-transport.ath

Problem Statement

To show the usefulness of schema subsumption, we formalize a specification for the size of lambda calculus terms and prove that every term has a size. The informal rules for the size of terms are:

Where $e$ ranges over terms and $x$ denotes a variable.

The proof is by induction on terms. Variables have size $1$ by definition. For $\lambda x. e'$, the inductive hypothesis gives some $n'= |e'|$, so $|\lambda x. e'| = 1 + n'$. For $e_1\ e_2$, the inductive hypothesis gives $n_1 = |e_1|$ and $n_2 = |e_2|$, so $|e_1\ e_2| = 1 + n_1 + n_2$.

Formalizing the Proof

Specification

Before we can specify the size judgements in LF, we have to specify natural numbers and addition. We have seen these specified in first order examples so will limit the discussion here to a presentation of the specification.

nat : type.
z : nat.
s : {x:nat} nat.

plus : {x1:nat}{x2:nat}{x3:nat} type.
plus-z : {x: nat} plus z x x.
plus-s : {x1:nat}{x2:nat}{x3:nat}
         {D: plus x1 x2 x3}
         plus (s x1) x2 (s x3).

With natural numbers and addition defined, we can specify our $\lambda$-calculus terms and their size. Their specification is a straightforward translation from our informal rules.

app : {E1:tm}{E2:tm} tm.
lam : {E: {x:tm} tm} tm.

size : {E:tm}{x:nat} type.
size-lam : {E: {y:tm} tm}{X:nat}
           {D:{x:tm} {dx: size x (s z)} size (E x) X}
           size (lam ([x] E x)) (s X).
size-app : {E1:tm}{E2:tm}{X1:nat}{X2:nat}{X3:nat}
           {D1: size E1 X1}
           {D2: size E2 X2}
           {D3: plus X1 X2 X3}
           size (app E1 E2) (s X3).

Natural numbers and addition are common enough relations that we would want to have a standard library¹ which defines them along with its properties. Foreseeing our eventual proof, we introduce a single theorem which states "for any two natural numbers, there exists a natural number which is their sum."

Theorem plus-exist : forall N1 N2,
  {N1: nat} => {N2:nat} => exists N3 D, {D: plus N1 N2 N3}.
induction on 1.
intros.
case H1.
apply IH to H3 H2.
exists s N3.
exists plus-s x N2 N3 D.
search.
exists N2.
exists plus-z N2. search.

Proof Attempt

When proving this in Adelfa, we must be more precise about our statement. We permit open terms in our informal proof and categorize all variables as having a size of $1$. This doesn't suffice in a formal setting, so we limit ourselves to closed terms and prove our statement for terms under a context which forces the size of terms to be assessed under a context with variables of size 1. This is encoded within the size-lam term constructor. Reasoning inductively over derivations of size then results in a regular shape for contexts:

We specify such a shape in adelfa by defining a context schema C, with which we lay out the entries of a single repetition.

Schema C := (x: tm, y: size x (s z)).

Our proof in Adelfa aligns closely with our informal proof. We begin by performing induction on the derivation of the of E, introducing the eigenvariables, context variable, and implication as hypotheses, then performing case analysis on the derivation of E. Our first proof obligation is that of an abstraction. To keep this example concise, we will skip the proof of the abstraction and move into the more interesting case of an application.

Theorem tm-has-size : ctx G:C, forall E,
  {G |- E : tm} => exists N D, {G |- D: size E N}.
  induction on 1. intros.
  case H1 (keep). skip.

The Context Mismatch Problem

To complete the application case, we apply the inductive hypothesis to the assumptions {G |- E1 : tm} and {G |- E2 : tm}.

apply IH to H2. apply IH to H3.

We want to instantiate the existentially quantified N with the successor of the sum for N and N1, but we are missing a derivation for the sum. In our library, we have a proof of this plus-exist. Let's get derivations for these natural numbers and attempt to utilize this lemma.

assert { G |- N : nat }.
assert { G |- N1 : nat }.
apply plus-exist to H6 H7.

The resulting error "Error: could not match context variables" arises because plus-exist was proven for LF derivations without any context variable. As such, Adelfa cannot verify the proof still holds in the presence of this context variable. In the next section we'll walk through, step by step, how one may attempt to fix this situation and discuss them.

Without Transport

In this section, we will discuss two ways to continue this proof without utilizing the transport rule and see where approaches differ and where they fall short.

Removing context dependencies

The first solution one may try is to prove that the natural numbers do not rely on entries in the schema C to use this lemma. Such a proof is fairly routine by induction and case analysis on the derivation for natural numbers.

Theorem nat-ind : ctx G:C, forall N,
  { G |- N : nat } => { N : nat }.
induction on 1. intros.
case H1. apply IH to H2. search. search.

Let's back up to when we tried to use plus-exist and try to complete the proof after removing the context variables. This time, the application of plus-exist is allowed, and now have an assumption for {D2 : plus N N1 N3}.

assert { G |- N : nat }. apply nat-ind to H6.
assert { G |- N1 : nat }. apply nat-ind to H8.
apply plus-exist to H7 H9.

Given N3 is the sum of the sizes for E1 and E2, the goal's existentially quantified variables can now be instantiated with N as (s N3) and D as a term constructor for size-app. This time, we cannot complete the case since adelfa cannot find a derivation for:

exists (s N3).
exists size-app E1 E2 N N1 N3 D D1 D2.
search.

In order to utilize size-app we must have N3 under the same context variable as the other terms. Yet, our only occurrence of N3 in our assumption set is within the formula {D2 : plus N N1 N3}. The best Adelfa can deduce is therefore {N3 : nat}. One may try to prove a lemma of the sort:

Theorem nat-wk : ctx G:C, forall N, { N : nat } => { G |- N : nat}.

But this will not work. The instantiations for G are not limited to well-formed ones, and therefore this statement is false. Therefore, the state we are in within our proof of tm-has-size has reached a dead end, and we must reevaluate how to proceed.

Reproving lemmas

The second approach one may attempt is to reprove necessary lemmas under a context variable.

Theorem plus-exist-context : ctx G:C, forall N1 N2,
  {G |- N1: nat} => {G |- N2:nat} => exists N3 D, {G |- D: plus N1 N2 N3}.
induction on 1.
intros.
case H1.
apply IH to H3 H2.
exists s N3.
exists plus-s x N2 N3 D.
search.
exists N2.
exists plus-z N2. search.

Notice that there is no difference in the proof compared to the one without the context variable. This makes sense, because nat and plus do not depend on anything within G.

Using this reproved lemma within our proof of tm-has-size will succeed this time.

assert { G |- N : nat }.
assert { G |- N1 : nat }.
apply plus-exist-context to H6 H7.

Having an assumption formula {G |- D2 : plus N N1 N3} allows us to properly instantiate the existentially quantified variables with N as s N3 and D as the term constructor size-app. This case can then be completed and we can move on to the next proof obligation. Our previous issue where we could not show that N3 is a wellformed term of type nat in the context G. This is no longer an issue now that we have the assumption {G |- D2 : plus N N1 N3}, which implies {G |- N3 : nat}.

exists (s N3).
exists size-app E1 E2 N N1 N3 D D1 D2.

With Transport

With schema subsumption, when Adelfa encounters a usage of the apply tactic which would fail due to a mismatch in context schemas, it will automatically try to transport the proof into the new context schema. In our case, transporting the proof of plus-exist into one of plus-exist-context automatically.

The proof for tm-has-size then requires no extra lemmas and can directly utilize the library's theorem without worrying about reproving routine properties under a new context schema.

assert { G |- N : nat }.
assert { G |- N1 : nat }.
apply plus-exist to H6 H7.
exists (s N3).
exists size-app E1 E2 N N1 N3 D D1 D2.
search.

With transport, the entire proof is:

Theorem tm-has-size : ctx G:C, forall E,
  {G |- E : tm} => exists N D, {G |- D: size E N}.
induction on 1. intros.
case H1 (keep).
weaken H2 with size n (s z).
apply IH to H3 with (G = G, n1:tm, n:size n1 (s z)).
assert { G, n1:tm, n:size n1 (s z) |- N n1 n : nat }.
prune H5. strengthen H5. strengthen H6.
exists (s N). exists size-lam ([x] E1 x) N D.
search.
apply IH to H2. apply IH to H3.
assert { G |- N : nat }. assert { G |- N1 : nat }.
apply plus-exist to H6 H7.
exists (s N3). exists size-app E1 E2 N N1 N3 D D1 D2. search.
exists (s z). exists n1. search.