Skip to Content

Substitution Size of λ\lambda-calculus Terms

Our usage of the transport rule in term has size motivated our usage of transport in a simple theorem. A solution without using the transport rule was to reprove a routine lemma under a new context variable. This worked well for our small example, but does not scale to larger developments. We will continue our reasoning about the size of lambda calculus terms, which is based on the same definition as the term has size example, reiterated here:

∣x∣=1∣λx.e∣=1+∣e∣∣e1 e2∣=1+∣e1∣+∣e2∣|x| = 1 \qquad |\lambda x. e| = 1 + |e| \qquad |e_1\ e_2| = 1 + |e_1| + |e_2|

Our goal is to show that the size of a lambda term does not decrease after substitution, modified from an example in Twelf .

The complete developments are provided here for reference:

Theorem: For any λ\lambda-calculus terms ee and e′e', ∣e∣≤∣{e′/x}e∣|e| \leq |\{e'/x\}e|.

To specify this statement in LF, we will extend the one specification presented in term has size to include rules for less than or equal to. Our library of theorems will also be expanded to include properties about less than or equal to.

Logonat.lf
leq : {x1:nat}{x2:nat} type.
leq-z : {x:nat} leq z x.
leq-s : {x1:nat}{x2:nat}{D: leq x1 x2} leq (s x1) (s x2).

Library theorems

Logonat.ath
Theorem plus-s-rhs : forall N1 N2 N3 D1,
  {D1: plus N1 N2 N3} =>
  exists D2, {D2: plus N1 (s N2) (s N3)}.
induction on 1.
intros.
case H1.
apply IH to H5.
exists plus-s x1 (s N2) (s x3) D2. search.
exists plus-z (s N3). search.
 
Theorem ident-rhs : forall x1,
  {x1: nat} => exists D, {D: plus x1 z x1}.
induction on 1.
intros.
case H1 (keep).
apply IH to H2.
exists plus-s x z x D. search.
exists plus-z z. search.
 
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.
 
Theorem plus-comm : forall N1 N2 N3 D1,
  {D1: plus N1 N2 N3} =>
  exists D2, {D2: plus N2 N1 N3}.
induction on 1.
intros.
case H1.
apply IH to H5.
apply plus-s-rhs to H6.
exists D1. search.
apply ident-rhs to H2.
exists D. search.
 
Theorem leq-transitive : forall x1 x2 x3 D1 D2,
  {D1: leq x1 x2} => {D2: leq x2 x3} =>
  exists D3, {D3: leq x1 x3}.
induction on 1.
intros.
case H1.
case H2.
apply IH to H5 H8.
exists leq-s x4 x7 D1.
search.
case H2.
exists leq-z (s x5).
search.
exists leq-z x3.
search.
 
Theorem leq-monotonic-plus-r : forall x1 x2 x3 x12 x13 D1 D2 D3,
  {D2: plus x1 x2 x12} => {D1: leq x2 x3} =>
  {D3: plus x1 x3 x13} =>
  exists D4, {D4: leq x12 x13}.
induction on 1.
intros.
case H1.
case H3.
apply IH to H7 H2 H11.
exists leq-s x6 x8 D2.
search.
case H3.
exists D1.
search.
 
Theorem leq-monotonic-plus-l : forall x1 x2 x3 x13 x23 D1 D2 D3,
  {D1: leq x1 x2} => {D2: plus x1 x3 x13} => {D3: plus x2 x3 x23} =>
  exists D4, {D4: leq x13 x23}.
intros.
apply plus-comm to H2.
apply plus-comm to H3.
apply leq-monotonic-plus-r to H4 H1 H5.
exists D6.
search.
 
Theorem leq-monotonic-plus : forall x1 x2 x3 x4 x13 x24 D1 D2 D3 D4,
  {D1: leq x1 x2} => {D2: leq x3 x4} =>
  {D3: plus x1 x3 x13} => { D4: plus x2 x4 x24} =>
  exists D6, {D6: leq x13 x24}.
intros.
assert { x2 : nat }.
assert { x3 : nat }.
apply plus-exist to H5 H6.
apply leq-monotonic-plus-l to H1 H3 H7.
apply leq-monotonic-plus-r to H7 H2 H4.
apply leq-transitive to H8 H9.
exists D7.
search.

Our informal theorem and proof is as follows, which implicitly utilizes several properties about less than or equal to.

Proof: By induction on the structure of ee followed by case analysis on ee.

  • If ee is a variable yy:
    • If x=yx = y, ∣x∣=1|x| = 1, ∣{e′/x}x∣=∣e′∣|\{e'/x\}x| = |e'|, by a routine lemma, the size of a term must be at least one.1
    • If x≠yx \ne y, then this follows since {e′/x}y=y\{e'/x\}y = y and ≤\leq is a reflexive relation.
  • If ee is an application, then ∣(e1 e2)∣=1+n1+n2|(e_1\ e_2)| = 1 + n_1 + n_2 by definition. By application of the inductive hypothesis on the component terms, there is some n1′n'_1 and n2′n'_2 such that ∣{e′/x}e1∣=n1′|\{e'/x\}e_1| = n'_1, ∣{e′/x}e2∣=n2′|\{e'/x\}e_2| = n'_2, n1≤n1′n_1 \leq n'_1 and n2≤n2′n_2 \leq n'_2 hold. Addition is monotonic with respect to ≤\leq, so n1+n2≤n1′+n2′n_1 + n_2 \leq n'_1 + n'_2. Then 1+n1+n2≤1+n1′+n2′1 + n_1 + n_2 \leq 1 + n'_1 + n'_2 follows.
  • If ee is an abstraction, ∣λy.e∣=1+n|\lambda y. e| = 1 + n such that yy does not occur freely within ee, then this follows inductive hypothesis with ee.

Q.E.D

Like our last theorem statement about λ\lambda-calculus terms have a size, we will need to modify our theorem statement to be within a context. We can reuse the same shape for the context here:

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

For pedagogical purposes, we present two ways of proving this statement. We will strategically choose our theorem statement(s) in order to complete or simplify the proof.

  1. Immediately proved without context dependency
    Logosubst-size.ath
    Theorem size-subst : ctx G:C, forall E' E: o -> o T-size D1: o -> o -> o,
  {G |- [x][dx] D1 x dx: {x:tm}{dx: size x (s z)} size (E x) T-size} =>
  {G |- E' : tm} =>
  exists D2 Sub-size D3, {G |- D2 : size (E E') Sub-size} /\
  {D3: leq T-size Sub-size}.
  2. Proved with context dependency, then shown to be independent
    Logosubst-size.ath
    Theorem size-subst' : ctx G:C, forall E' E: o -> o T-size D1: o -> o -> o,
  {G |- [x][dx] D1 x dx: {x:tm}{dx: size x (s z)} size (E x) T-size} =>
  {G |- E' : tm} =>
  exists D2 Sub-size D3, {G |- D2 : size (E E') Sub-size} /\
  {G |- D3: leq T-size Sub-size}.
 
Theorem size-subst : ctx G:C, forall E' E: o -> o T-size D1: o -> o -> o,
  {G |- [x][dx] D1 x dx: {x:tm}{dx: size x (s z)} size (E x) T-size} =>
  {G |- E' : tm} =>
  exists D2 Sub-size D3, {G |- D2 : size (E E') Sub-size} /\
  {D3: leq T-size Sub-size}.

Proof Without Transport

In this section, we will discuss a “hybrid” approach which utilizes both work in our previous example since we needed the result of the lemma application to be under a context variable. In our first theorem statement of size-subst, we do not have the same problem. The issue presented with the size of an application still arises, but we can reprove one lemma in order to complete that case. This, in conjunction with independence lemmas for natural numbers, addition, and less than or equal to, allows us to complete the proof.

Logosubst-size.ath
Theorem nat-independent : ctx G:C, forall N,
  {G |- N : nat } => {N : nat}
induction on 1 intros case H1
apply IH to H2 search search
 
Theorem plus-independent : ctx G:C, forall N1 N2 N3 D,
  {G |- D : plus N1 N2 N3} => {D : plus N1 N2 N3}
induction on 1 intros case H1
apply IH to H5 search apply nat-independent to H2 search
 
Theorem leq-independent : ctx G:C, forall N1 N2 D,
  {G |- D : leq N1 N2} => {D : leq N1 N2}
induction on 1 intros case H1
apply IH to H4 apply nat-independent to H2
apply nat-independent to H3 search
apply nat-independent to H2 search
 
% Reprove `plus-exist` but with context shape `C`
Theorem plus-exist-ind : 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

We’ll now walk through the proof, and show the general pattern one must use to properly utilize these proofs. Starting with the application case, we follow our informal proof by applying the inductive hypothesis to the component terms.

Logosubst-size.ath
Theorem size-subst : ctx G:C, forall E' E: o -> o T-size D1: o -> o -> o,
  {G |- [x][dx] D1 x dx: {x:tm}{dx: size x (s z)} size (E x) T-size} =>
  {G |- E' : tm} =>
    exists D2 Sub-size D3,
      {G |- D2 : size (E E') Sub-size} /\
      {D3: leq T-size Sub-size}
induction on 1
intros
case H1
% app case
  prune H6 prune H5 prune H10
  apply IH to H8 H2 apply IH to H9 H2
  case H11 prune H13 prune H14
  case H12 prune H15 prune H16

Let us first try to get the total size of the application, to instantiate the Sub-size variable in our consequent. We will utilize our lifted version of plus-exist with Sub-size and Sub-size1 to accomplish this. We have to do some intermediate assertions to get assumption formulas for the natural numbers, then invoke our plus-exist'.

Logosubst-size
assert {G |- Sub-size n1 n : nat} prune H17
assert {G |- Sub-size1 n1 n : nat} prune H18
apply plus-exist' to H17 H18 prune H19

The next step is to ensure that the substitution size is less than the term’s size prior to substitution. This will require the monotonicity property for addition with respect to less than or equal to. This property being in the empty context will require us to apply our independence lemmas.

Logosubst-size
assert { G |- N3 n1 n : nat } prune H20
assert { G |- D4 : plus X1 X2 T-size1 }* strengthen H10 strengthen H21 search
apply plus-independent to H21 apply plus-independent to H19
apply leq-monotonic-plus to H14 H16 H22 H23

The remainder of the theorem follows a similar pattern. One will strengthen the necessary assumptions then invoke the relevant lemma. We include the proof in its entirety here, but omit state to reduce the page’s size.

Logosubst-size.ath
Theorem size-subst : ctx G:C, forall E' E: o -> o T-size D1: o -> o -> o,
  {G |- [x][dx] D1 x dx: {x:tm}{dx: size x (s z)} size (E x) T-size} =>
  {G |- E' : tm} =>
    exists D2 Sub-size D3,
      {G |- D2 : size (E E') Sub-size} /\
      {D3: leq T-size Sub-size}.
induction on 1.
intros.
case H1.
% app case
  prune H6. prune H5. prune H10.
  apply IH to H8 H2. apply IH to H9 H2.
  case H11. prune H13. prune H14.
  case H12. prune H15. prune H16.
  assert {G |- Sub-size n1 n : nat}. prune H17.
  assert {G |- Sub-size1 n1 n : nat}. prune H18.
  apply plus-exist-independent to H17 H18. prune H19.
  assert { G |- N3 n1 n : nat }. prune H20.
  assert { G |- D4 : plus X1 X2 T-size1 }*. strengthen H10. strengthen H21. search.
  apply plus-independent to H21. apply plus-independent to H19.
  apply leq-monotonic-plus to H14 H16 H22 H23.
  exists size-app (E1 E') (E2 E') Sub-size Sub-size1 N3 D1 D6 D.
  exists (s N3). exists leq-s T-size1 N3 (D8 n1 n). split. search. search.
  % lam
  weaken H2 with tm. weaken H6 with size n5 (s z).
  ctxpermute H5 to G, n3:tm, n4: size n3 (s z), n:tm, n1:size n (s z).
  apply IH to H8 H7 with (G = G, n1:tm, n:size n1 (s z)).
  case H9.
  prune H10. prune H11.
  assert {G, n1:tm, n:size n1 (s z) |- Sub-size n6 n5 n4 n3 n2 n1 n : nat}. prune H12.
  inst H3 with n = E'. strengthen H13.
  ctxpermute H13 to G, n2:tm, n1: size E' (s z). strengthen H14.
  exists size-lam ([x] E1 E' x) Sub-size D2. exists (s Sub-size). strengthen H12. strengthen H16.
  exists leq-s T-size1 Sub-size (D3 n6 n5 n4 n3 n2 n1 n). split. search. search.
  % var1
  apply tm-has-size to H2. prune H3. assert {G |- N n1 n : nat}. prune H4.
  exists D. exists N. apply size-at-least-one to H3. prune H5. 
  exists D' n1 n. split. search. search.
  % var2
  exists n3. exists (s z). exists leq-s z z (leq-z z). split. search. search.

Proof with Transport

Our proof with transport will utilize our second presentation of the theorem, where we prove the property within the context and then later prove that the desired judgements are independent of the context. This leads to a more straightforward version of the proof, with no uses of independence lemmas in the proof of size-subst. For example, the application case is:

Logosubst-size.ath
Theorem size-subst : ctx G:C, forall E' E: o -> o T-size D1: o -> o -> o,
  {G |- [x][dx] D1 x dx: {x:tm}{dx: size x (s z)} size (E x) T-size} =>
  {G |- E' : tm} =>
    exists D2 Sub-size D3,
      {G |- D2 : size (E E') Sub-size} /\
      {G |- D3: leq T-size Sub-size}.
induction on 1.
intros.
case H1.
% app case
  prune H6. prune H5. prune H10.
  apply IH to H8 H2. apply IH to H9 H2.
  case H11. prune H13. prune H14.
  case H12. prune H15. prune H16.
  assert {G |- Sub-size n1 n : nat}. prune H17.
  assert {G |- Sub-size1 n1 n : nat}. prune H18.
  apply plus-exist-independent to H17 H18. prune H19.
  assert { G |- N3 n1 n : nat }. prune H20.
  assert { G |- D4 : plus X1 X2 T-size1 }*. strengthen H10. strengthen H21. search.
  apply leq-monotonic-plus to H14 H16 H21 H19.
  exists size-app (E1 E') (E2 E') Sub-size Sub-size1 N3 D1 D6 D.
  exists (s N3). exists leq-s T-size1 N3 (D8 n1 n). split. search. search.

Summary

The theorem we have laid out above can be proven without utilizing the transport rule or reproving any library lemmas. We accomplished this by proving a series of independence lemmas to show that our encoding of natural numbers, addition, and “less than or equal to” do not depend on any entries within the context schema C. While this works, this approach results in a more complex proof structure.

When using library lemmas with this approach, the relevant assumptions must first be shown to be independent of the context variable via the relevant independence lemma.

For example, invoking the monotonicity property discussed earlier is accomplished with three uses of the apply tactic.

apply plus-independent to H21.
apply plus-independent to H19.
apply leq-monotonic-plus to H14 H16 H22 H23.

In contrast, the version which utilizes transport allows for the monotonicity property to be utilized directly, with only one use of the apply tactic.

Footnotes

  1. The proof of this follows by observing all judgements for size have an occurrence of 1 directly or 1 as the component of an addition. ↩

Last updated on
Download