Documentation out of dateLearn more

Catch-all case

When defining relations in non-empty contexts, it is often necessary to put a case of the relation in the LF context. In some circumstances, it is possible to avoid doing so by writing a catch-all case instead. This technique works when you can cover the space of the relation that would be covered by a context case without mentioning any variables from the context explicitly.

Using a catch-all case leads to simpler STELF code because it saves you from having to repeat the context case at a variety of context extension points.

As a motivating example, we use the theorem about the size of a STLC term from Proving metatheorems in non-empty contexts. For review, here are the relevant judgements:

%sort tp %.
%term unit tp %.
%term arrow %pi tp %-> tp %-> tp %.
%sort tm %.
%term empty tm %.
%term lam %pi tp %-> (%pi tm %-> tm) %-> tm %.
%term app %pi tm %-> tm %-> tm %.
%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%mode plus %in %in %out %.
%term plus-z plus z N2 N2 %.
%term plus-s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.
%worlds () (plus _ _ _) %.
%total N (plus N _ _) %.

(options removed from twelftag: hidden=“true”)

%sort plus-exists {N1} {N2} {_ plus N1 N2 N3} %.
%mode plus-exists %in %in %out %.
%term _ plus-exists z _ plus-z %.
%term _ %pi (plus-exists (s N1) N2 (plus-s D)) %<- (plus-exists N1 N2 D) %.
%worlds () (plus-exists _ _ _) %.
%total N1 (plus-exists N1 _ _) %.
%sort plus-z-rh {n nat} {_ plus n z n} %.
%mode plus-z-rh %in %out %.
%term _ plus-z-rh z plus-z %.
%term _ %pi (plus-z-rh (s N) (plus-s D)) %<- (plus-z-rh N (%the (plus N z N) D)) %.
%worlds () (plus-z-rh _ _) %.
%total N (plus-z-rh N _) %.
%sort plus-s-rh {_ plus N1 N2 N3} {_ plus N1 (s N2) (s N3)} %.
%mode plus-s-rh %in %out %.
%term _ plus-s-rh plus-z plus-z %.
%term _
  %pi (plus-s-rh (plus-s (%the (plus N1' N2 N3') D)) (plus-s D'))
  %<- (plus-s-rh D (%the (plus N1' (s N2) (s N3')) D')) %.
%worlds () (plus-s-rh _ _) %.
%total D (plus-s-rh D _) %.
%sort plus-commute {_ plus N1 N2 N3} {_ plus N2 N1 N3} %.
%mode plus-commute %in %out %.
%term _ %pi (plus-commute (%the (plus z N N) plus-z) D) %<- (plus-z-rh N D) %.
%term _
  %pi (plus-commute (%the (plus (s N1) N2 (s N3)) (plus-s D)) D'')
  %<- (plus-commute D (%the (plus N2 N1 N3) D'))
  %<- (plus-s-rh D' (%the (plus N2 (s N1) (s N3)) D'')) %.
%worlds () (plus-commute _ _) %.
%total D (plus-commute D _) %.
%sort id/nat {_ nat} {_ nat} %.
%term id/nat-refl id/nat N N %.
%sort id/nat-s-cong {_ id/nat N1 N2} {_ id/nat (s N1) (s N2)} %.
%mode id/nat-s-cong %in %out %.
%term _ id/nat-s-cong id/nat-refl id/nat-refl %.
%worlds () (id/nat-s-cong _ _) %.
%total {} (id/nat-s-cong _ _) %.
%sort plus-unique {_ plus N1 N2 N3} {_ plus N1 N2 N3'} {_ id/nat N3 N3'} %.
%mode plus-unique %in %in %out %.
%term _ plus-unique D D id/nat-refl %.
%term _
  %pi (plus-unique (plus-s D) (plus-s D') DidS)
  %<- (plus-unique D D' Did)
  %<- (id/nat-s-cong Did DidS) %.
%worlds () (plus-unique _ _ _) %.
%total D (plus-unique D _ _) %.
%sort plus-respects-id {_ plus N1 N2 N3} {_ id/nat N1 N1'} {_ id/nat N2 N2'} {_ id/nat N3 N3'} {_ plus N1' N2' N3'} %.
%mode plus-respects-id %in %in %in %in %out %.
%term _ plus-respects-id D id/nat-refl id/nat-refl id/nat-refl D %.
%worlds () (plus-respects-id _ _ _ _ _) %.
%total {} (plus-respects-id _ _ _ _ _) %.
%sort id/nat-sym {_ id/nat N1 N2} {_ id/nat N2 N1} %.
%mode id/nat-sym %in %out %.
%term _ id/nat-sym id/nat-refl id/nat-refl %.
%worlds () (id/nat-sym _ _) %.
%total {} (id/nat-sym _ _) %.
%sort plus-assoc {_ plus A B AB} {_ plus B C BC} {_ plus AB C ABC} {_ plus A BC ABC} %.
%mode plus-assoc %in %in %in %out %.
%term _
  %pi (plus-assoc plus-z DplusB-C DplusB-C' Dplus)
  %<- (plus-unique DplusB-C DplusB-C' Did)
  %<- (plus-respects-id plus-z id/nat-refl id/nat-refl Did Dplus) %.
%term _
  %pi (plus-assoc (plus-s DplusA'-B) DplusB-C (plus-s DplusA'B-C) (plus-s DplusA'-BC))
  %<- (plus-assoc DplusA'-B DplusB-C DplusA'B-C DplusA'-BC) %.
%worlds () (plus-assoc _ _ _ _) %.
%total D (plus-assoc D _ _ _) %.
%sort plus-assoc2 {_ plus A B AB} {_ plus B C BC} {_ plus AB C ABC} {_ plus A BC ABC} %.
%mode plus-assoc2 %in %in %out %in %.
%term _
  %pi (plus-assoc2 D1 D2 D3' D4)
  %<- (plus-exists _ _ D3)
  %<- (plus-assoc D1 D2 D3 D4')
  %<- (plus-unique D4 D4' Did)
  %<- (id/nat-sym Did Did')
  %<- (plus-respects-id D3 id/nat-refl id/nat-refl Did' D3') %.
%worlds () (plus-assoc2 _ _ _ _) %.
%total {} (plus-assoc2 _ _ _ _) %.
%sort lemma {_ plus N1 N2 Nsum} {_ plus Ndiff1 N1 N1'} {_ plus Ndiff2 N2 N2'} {_ plus N1' N2' Nsum'} {_ plus Ndiff Nsum Nsum'} %.
%mode lemma %in %in %in %in %out %.
%term _
  %pi (lemma (%the (plus N1 N2 Nsum) D) (%the (plus Ndiff1 N1 N1') D1pre) (%the (plus Ndiff2 N2 N2') D2pre) (%the (plus N1' N2' Nsum') D') Dres')
  %<- (plus-commute D1pre D1)
  %<- (plus-commute D2pre D2)
  %<- (plus-exists Ndiff1 N2' (%the (plus Ndiff1 N2' Ndiff1+2') Ddiff1+2'))
  %<- (plus-assoc D1 Ddiff1+2' D' (%the (plus N1 Ndiff1+2' Nsum') Dassoc))
  %<- (plus-commute D2 (%the (plus Ndiff2 N2 N2') D2'))
  %<- (plus-exists Ndiff1 Ndiff2 (%the (plus Ndiff1 Ndiff2 Ndiff1+2) Ddiff1+2))
  %<- (plus-assoc2 Ddiff1+2 D2' (%the (plus Ndiff1+2 N2 Ndiff1+2') Dassoc') Ddiff1+2')
  %<- (plus-commute Dassoc' (%the (plus N2 Ndiff1+2 Ndiff1+2') Dassoc''))
  %<- (plus-assoc2 D Dassoc'' Dres Dassoc)
  %<- (plus-commute Dres Dres') %.
%worlds () (lemma _ _ _ _ _) %.
%total {} (lemma _ _ _ _ _) %.

(options removed from twelftag: check=“true”)

%sort size {_ tm} {_ nat} %.
%mode size %in %out %.
%term size-empty size empty (s z) %.
%term size-lam %pi (size (lam _ E) (s N)) %<- ({x} {dx size x (s z)} size (E x) N) %.
%term size-app %pi (size (app E1 E2) (s N)) %<- (size E1 N1) %<- (size E2 N2) %<- (plus N1 N2 N) %.
%block size-block {x tm} {dx size x (s z)}%.
%worlds (size-block) (size _ _) %.
%total E (size E _) %.

Original proof

(options removed from twelftag: hidden=“true”)

%sort size-at-least-one {_ size E N} {_ plus (s z) N' N} %.
%mode size-at-least-one %in %out %.
%term _ size-at-least-one _ (plus-s plus-z) %.
%worlds (size-block) (size-at-least-one _ _) %.
%total {} (size-at-least-one _ _) %.

In Proving metatheorems in non-empty contexts, we proved the following theorem:

%sort subst-size {E' tm} {_ {x tm} %pi (size x (s z)) %-> (size (E x) N)} {_ size (E E') N'} {_ plus Ndiff N N'} %.
%mode subst-size %in %in %in %out %.
%block sdblock {y tm} {dy size y (s z)} {_ {E' tm} subst-size E' ([x] [dx] dy) dy plus-z}%.
%worlds (sdblock) (subst-size _ _ _ _) %.

The %block declaration includes a case of the theorem for the variable dy declared in the context.

Alternate proof using a catch-all case

In this instance, it is possible to avoid putting the theorem case in the context. How? We instead write a catch-all case that covers the context variable case without mentioning the context variable explicitly:

(options removed from twelftag: check=“true”)

%sort subst-size-ca {E' tm} {_ {x tm} %pi (size x (s z)) %-> (size (E x) N)} {_ size (E E') N'} {_ plus Ndiff N N'} %.
%mode subst-size-ca %in %in %in %out %.
%term _ subst-size-ca E' ([x] [dx] D) D plus-z %.

This case covers any first-argument derivation D that does not mention the bound variables x and dx, as long as the second argument is also that derivation D. Note that the context case in the previous proof has this form. To complete the proof for these inputs, we simply use plus-z : plus z N N to derive the result. This technique works because we do not actually need to use any reasoning specific to the variable from the context.

The remaining cases are the same as in the previous proof, except that

the catch-all case happens to cover the case for size-empty as well, so we can elide it.
the case for size-lam no longer adds the theorem case to the context.

(options removed from twelftag: check=“true”)

%term _
  %pi (subst-size-ca E' ([x] [dx] dx) D Dplus')
  %<- (size-at-least-one D Dplus)
  %<- (plus-commute Dplus Dplus') %.
%term _
  %pi (subst-size-ca E' ([x] [dx] %the (size (lam T _) _) (size-lam ([y] [dy] D x dx y dy))) (size-lam D') Dplus')
  %<- ({y tm} {dy size y (s z)} subst-size-ca E' ([x] [dx] D x dx y dy) (D' y dy) Dplus)
  %<- (plus-s-rh Dplus Dplus') %.
%term _
  %pi (subst-size-ca E' ([x] [dx] size-app (%the (plus N1 N2 Nsum) Dplus) (%the (size (E2 x) N2) (D2 x dx)) (%the (size (E1 x) N1) (D1 x dx))) (size-app (%the (plus N1' N2' Nsum') Dplus') (%the (size (E2 E') N2') D2') (%the (size (E1 E') N1') D1')) DplusRes')
  %<- (subst-size-ca E' D1 (%the (size (E1 E') N1') D1') (%the (plus Ndiff1 N1 N1') Dplus1))
  %<- (subst-size-ca E' D2 (%the (size (E2 E') N2') D2') (%the (plus Ndiff2 N2 N2') Dplus2))
  %<- (lemma Dplus Dplus1 Dplus2 Dplus' DplusRes)
  %<- (plus-s-rh DplusRes DplusRes') %.
%worlds (size-block) (subst-size-ca _ _ _ _) %.
%total D (subst-size-ca _ D _ _) %.