Catch-all case

From The Twelf Project
Jump to: navigation, search

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 Twelf 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 in the tutorial Proving metatheorems with Twelf. For review, here are the relevant judgements:

tp    : type.
unit  : tp.
arrow : tp -> tp -> tp.

tm    : type.
empty : tm.
lam   : tp -> (tm -> tm) -> tm.
app   : tm -> tm -> tm.

nat : type.
z   : nat.
s   : nat -> nat.

plus   : nat -> nat -> nat -> type.
%mode plus +X1 +X2 -X3.

plus-z : plus z N2 N2.
plus-s : plus (s N1) N2 (s N3)
	  <- plus N1 N2 N3.

%worlds () (plus _ _ _).
%total N (plus N _ _).
size       : tm -> nat -> type.
%mode size +E -N.

size-empty : size empty (s z). 
size-lam   : size (lam _ E) (s N)
		<- ({x} {dx : size x (s z)}
		      size (E x) N).
size-app   : size (app E1 E2) (s N)
		<- size E1 N1
		<- size E2 N2 
		<- plus N1 N2 N.

%block size-block : block {x : tm} {dx : size x (s z)}.

%worlds (size-block) (size _ _).
%total E (size E _).
See Twelf's output

Original proof


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

subst-size : {E' : tm}
	       ({x : tm} size x (s z) -> size (E x) N)
	       -> size (E E') N'
	       -> plus Ndiff N N'
	       -> type.
%mode subst-size +E' +D1 +D2 -DL.

%block sdblock : block {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:

subst-size-ca : {E' : tm}
		  ({x : tm} size x (s z) -> size (E x) N)
		  -> size (E E') N'
		  -> plus Ndiff N N'
		  -> type.
%mode subst-size-ca +E' +D1 +D2 -DL.

- : subst-size-ca E'
     ([x] [dx] D)
     D
     plus-z.
See Twelf's output

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.
- : subst-size-ca E'
     ([x] [dx] dx)
     D
     Dplus'
     <- size-at-least-one D Dplus
     <- plus-commute Dplus Dplus'.
     
- : subst-size-ca E'
     ([x] [dx] 
	(size-lam ([y] [dy] D x dx y dy)
	   %% tell reconstruction that T doesn't depend on x
	   : size (lam T _) _))
     (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'.

- : subst-size-ca E'
     ([x] [dx] 
	size-app 
	(Dplus : plus N1 N2 Nsum)
	((D2 x dx) : size (E2 x) N2)
	((D1 x dx) : size (E1 x) N1)
	)
     (size-app 
	(Dplus' : plus N1' N2' Nsum')
	(D2' : size (E2 E') N2')
	(D1' : size (E1 E') N1'))
     DplusRes'
     <- subst-size-ca E' D1 
	(D1' : size (E1 E') N1')
	(Dplus1 : plus Ndiff1 N1 N1')
     <- subst-size-ca E' D2 
	(D2' : size (E2 E') N2')
	(Dplus2 : plus Ndiff2 N2 N2')
     <- lemma Dplus Dplus1 Dplus2 Dplus' DplusRes
     <- plus-s-rh DplusRes DplusRes'.
%worlds (size-block) (subst-size-ca _ _ _ _).
%total D (subst-size-ca _ D _ _).
See Twelf's output

Read more Twelf tutorials and other Twelf documentation.