strong-normalization.slf

/* 
 * A Formalization of the Simply Typed Lambda Calculus in SASyLF
 *
 * Author: Jonathan Aldrich
 * 
 * This file defines the simply typed lambda calculus with an implicit representation of
 * contexts, and proves type safety.  As we go along, we illustrate the SASyLF language
 * in tutorial style.
 */


/** The package declaration is similar to Java;
 * it must match what directory the proof file is in.
 */
package examples;

/** SASyLF programs explicitly declare terminals that are
 * used to parse expressions.  This helps the SASyLF parser
 * detect problems in the input grammar--anything that is not
 * a declared terminal, non-terminal, or variable must be an error.
 * The user should declare all identifiers used in syntax and judgment
 * that do not themselves denote syntactic classes.  Symbols like
 * + or |- do not need to be declared, even if they are terminals.
 */
terminals fn unit in value stepsorvalue


/************************ SYNTAX **************************************/

/** The syntax section declares the syntax of the formal
 * system, in this case of the lambda calculus.  Syntax is
 * given using an ordinary BNF grammar.
 */
syntax

/** This declaration declares e as a nonterminal.  e and variants of e
 * (e', e'', e1, e2, etc.--you can add primes or numbers) are used as
 * metavariables for this syntactic category, as commonly used in the
 * PL research literature.
 *
 * We use the notation e[x] to denote that the variable x is bound in e.
 * Any uses of the same variable in a binding, such as fn "x" : ... are
 * treated as the binding occurence where the name of the variable is
 * defined.
 */
e ::= fn x : tau => e[x]

/** To what syntactic class does the variable x refer?  We specify that
 * by including a case "x" in the grammar for e.
 */

 | x
 | e e
 
 /** Parentheses are special in SASyLF, thus to use them in
  * the object language being defined requires quotes.
  */
 
 | "(" ")" 				


/** Here we define the syntax of types */

tau ::= unit
 | tau -> tau


/** The form of contexts.  Judgments that use this as a variable
 * context will say "assumes Gamma."  SASyLF uses built-in semantics for
 * these contexts, allowing properties like substitution, weakening, and
 * exchange.  We require that contexts that are understood using these
 * built-in semantics have a recursive structure that binds exactly one
 * variable at each level.
 */ 

Gamma ::= *
      |   Gamma, x : tau


/************************ JUDGMENTS **************************************/

/** We declare a judgment with a name ("value") and a form ("e value").
 * The judgment is then followed by a series of inference rules that define
 * the judgment's semantics.
 */

judgment value: e value

--------------- val-unit
"(" ")" value

--------------------------- val-fn
fn x : tau => e1[x] value


/** The reduction judgment.  Rules are defined with the premises above the line
 * and the conclusion below the line.
 */

judgment reduce: e -> e

e1 -> e1'
------------------- c-app-l
e1 e2 -> e1' e2

e1 value
e2 -> e2'
------------------- c-app-r
(e1 e2) -> (e1 e2')			// the parentheses are not necessary here, but can be used to disambiguate
							// expressions that otherwise can be parsed more than one way 

/** Substitution is built into SASyLF.  Here, we see that e has the variable x bound in it.
 * We substitute e2 for x in e using the notation e[e2].
 */

e2 value
---------------------------------- r-app
(fn x : tau => e[x]) e2 -> e[e2]



/** The typing judgment uses a list of assumptions for variable types.
 * This is just like the LF context in Twelf.  More details on how this works will
 * come later, but the gist is that it gives us a bunch of theorems for free,
 * including substitution, weakening, contraction, and exchange.
 */

judgment has-type: Gamma |- e : tau
assumes Gamma


-------------------------- t-unit
Gamma |- "("")" : unit

/** This rule shows how to use an assumption in Gamma to determine that a variable
 * is well-typed.  These assumption-using rules have a special form: no premises are
 * allowed, exactly one variable must be free in Gamma, and one variable free in the
 * main judgment.
 */

------------------------- t-var
Gamma, x:tau |- x : tau


/** we can replace x with x1 because it's a bound variable */

Gamma, x1:tau |- e[x1] : tau'
--------------------------------------------- t-fn
Gamma |- fn x : tau => e[x] : tau -> tau'


Gamma |- e1 : tau' -> tau
Gamma |- e2 : tau'
---------------------------------- t-app
Gamma |- e1 e2 : tau


/** We don't have logical and or or operators built-in, so we define the logical
 * or used in progress (steps OR is a value) using its own judgment, with one
 * rule for each disjunct.  Twelf uses the same trick for encoding "or."
 */

judgment stepsorvalue: e stepsorvalue

e value
--------------- stepsorvalue-value
e stepsorvalue

e -> e'
--------------- stepsorvalue-steps
e stepsorvalue


/************************ THEOREMS **************************************/

/** Warm-up theorem: the identity function really is the identity.
 *
 * Theorems consist of the keyword theorem (or lemma), a name, a :,
 * a list of foralls, and a single exists.  The foralls may be syntax
 * like "e" or judgments like "e1 -> e2" -- in the latter case, the
 * derivation of the judgment itself must be named ("dv" below).
 * We can assume derivations are available for all the facts in the forall
 * part; we are trying to construct a derivation for the exists part.
 */ 

theorem identity-behavior : forall dv : e value exists (fn x : tau => x) e -> e.


/** The actual proof is a series of statements of the form:
 *
 * name : judge			by justification
 *
 * Here name is an identifier that is used to refer to each fact, in case we need it
 * later.  judge is the judgment we've proved.  And the justification is the reason
 * we believe it's true (SASyLF will make sure we're right by checking that the
 * justification actually proves the judgment).
 *
 * The most common justification is "by rule <rule-name> on <name1>, <name2>, ..., <name_k>"
 * This means that we conclude the judgment on the left by applying rule <rule-name> to the
 * (ordered) list of premises <name1>, <name2>, ..., <name_k>.  Each <name> must be either
 * one of the foralls (we don't have any for this theorem) or one of the earlier things we
 * concluded.  If the rule has no premises (i.e. it's an axiom) we leave out the "on <name1>..."
 * part.
 */

d1 : (fn x : tau => x) e -> e by rule r-app on dv

end theorem


/** Note: we'd usually define substitution here, and maybe weakening and other basic
 * properties.  But in this case, we don't need to, because the underlying LF type theory
 * gives us substitution for free!
 */


/************************ PROGRESS **************************************/


theorem progress : forall dt : * |- e : tau exists e stepsorvalue.

/** Now the real fun begins--a proof by induction.  We use a "by induction on X :"
 * justification, where X is the derivation or syntax that we are doing induction
 * over.
 */

dsv : e stepsorvalue by induction on dt :

/** Inside the induction proof, we do a case analysis, with one case for each rule
 * that could have been used to produce the indicated judgment.  If we are doing
 * induction over syntax, then we will have cases for each case in the BNF
 * definition.
 *
 * A rule case is of the form "case rule <rule> is <derivation>"
 * Here <rule> is a rule defined above, but instantiated with actual
 * expressions as appropriate for the judgment we are doing case analysis over.
 * Any fresh variables in <rule> are bound for the derivation and can be used there.
 * SASyLF checks to make sure you don't get the case analysis wrong, for example, by
 * assuming more than is justified about the premises of the rule.
 */

case rule

	-------------------------- t-unit
	dut : * |- "("")" : unit

is

	dv : e value by rule val-unit
	dsv : "("")" stepsorvalue by rule stepsorvalue-value on dv

end case

// case t-var impossible - conclusion doesn't unify with dt


case rule

	dext: *, x:tau'' |- e'[x] : tau'
	------------------------------------------------- t-fn
	dfnt: * |- fn x : tau'' => e'[x] : tau'' -> tau'

is

	dv : fn x : tau'' => e'[x] value by rule val-fn
	dsv : fn x : tau'' => e'[x] stepsorvalue by rule stepsorvalue-value on dv

end case

case rule

	dp1t: (*) |- e1 : tau' -> tau
	dp2t: (*) |- e2 : tau'
	---------------------------------- t-app
	dappt: (*) |- (e1 e2) : tau

is

/** This example shows how we can use the induction hypothesis.
 * Note that this is only legal because dp1t is a subderivation of dt.
 */

	dp1sv: e1 stepsorvalue by induction hypothesis on dp1t
	dp2sv: e2 stepsorvalue by induction hypothesis on dp2t
	
	dsv : e stepsorvalue by case analysis on dp1sv :

	case rule

		dp1v : e1 value
		---------------------- stepsorvalue-value
		dp1sv' : e1 stepsorvalue

	is
	
		dsv : e stepsorvalue by case analysis on dp2sv :
	
		case rule
		
			dp2v : e2 value
			---------------------- stepsorvalue-value
			dp2sv' : e2 stepsorvalue
		
		is
		
			dsv : e stepsorvalue by case analysis on dp1t :
			
			case rule
			
				dpp1t' : *, x:tau' |- e1'[x] : tau
				---------------------------------------------------- t-fn
				dp1t' : * |- fn x : tau' => e1'[x] : tau' -> tau
			is
				ds : (fn x : tau' => e1'[x]) e2 -> e1'[e2] by rule r-app on dp2v
				dsv : e stepsorvalue by rule stepsorvalue-steps on ds
				
			end case
			
			case rule
			
				dp1t1' : (*) |- e11 : tau'' -> (tau' -> tau)
				dp1t2' : (*) |- e12 : tau''
				--------------------------------------------- t-app
				tp1t' : (*) |- e11 e12 : tau' -> tau
			
			is
				dsv : e stepsorvalue by case analysis on dp1v :
				
				end case analysis
								
			end case
			
			// other cases don't unify with conclusion
			
			end case analysis

		end case
		
		case rule
		
			dp2s : e2 -> e2'
			---------------- stepsorvalue-steps
			dp2sv' :  e2 stepsorvalue
		
		is
			ds : e1 e2 -> e1 e2' by rule c-app-r on dp1v, dp2s
			dsv : e1 e2 stepsorvalue by rule stepsorvalue-steps on ds
		end case
		end case analysis
	end case
	
	case rule
	
		dp1s : e1 -> e1'
		-------------------------- stepsorvalue-steps
		dp1sv' :  e1 stepsorvalue
	
	is
	
		ds : e1 e2 -> e1' e2 by rule c-app-l on dp1s
		dsv : e1 e2 stepsorvalue by rule stepsorvalue-steps on ds
	
	end case
	end case analysis
end case
end induction
end theorem


/************************ PRESERVATION **************************************/


theorem preservation: forall dt: * |- e : tau forall ds: e -> e' exists * |- e' : tau.

dt' : * |- e' : tau by induction on ds:

case rule

	d1 : e1 -> e1'
	----------------------- c-app-l
	d2 : e1 e2 -> e1' e2

is

	dt' : * |- e' : tau by case analysis on dt :
	
	case rule
	
		d3 : * |- e1 : tau' -> tau
		d4 : * |- e2 : tau'
		---------------------------------- t-app
		d5 : * |- (e1 e2) : tau
	
	is
	
		d6 : * |- e1' : tau' -> tau by induction hypothesis on d3, d1
		dt' : * |- e1' e2 : tau by rule t-app on d6, d4
	
	end case
	// other cases do not unify with form of e = (e1 e2)
	end case analysis

end case

case rule

	d1 : e1 value
	d2 : e2 -> e2'
	----------------------- c-app-r
	d3 : e1 e2 -> e1 e2'

is

	dt' : * |- e' : tau by case analysis on dt :

	case rule
	
		d4 : * |- e1 : tau' -> tau
		d5 : * |- e2 : tau'
		---------------------------------- t-app
		d6 : * |- e1 e2 : tau
	
	is
	
		d7 : * |- e2' : tau' by induction hypothesis on d5, d2
		dt' : * |- e1 e2' : tau by rule t-app on d4, d7
	
	end case
	// other cases do not unify with form of e = (e1 e2)
	end case analysis

end case

case rule

	d1 : e2 value
	------------------------------------------- r-app
	d2 : (fn x : tau' => e1[x]) e2 -> e1[e2]

is

	dt' : * |- e' : tau by case analysis on dt :

	case rule

		d4 : * |- fn x : tau' => e1[x] : tau'' -> tau
		d5 : * |- e2 : tau''
		---------------------------------------------------------- t-app
		d6 : * |- (fn x : tau' => e1[x]) e2 : tau
	
	is
	
		dt' : * |- e' : tau by case analysis on d4 :
	
		case rule
		
			d7: *, x:tau' |- e1[x] : tau
			------------------------------------------------- t-fn
			d8: * |- fn x : tau' => e1[x] : tau' -> tau  
		
		is
		
			/** Substitution preserves typing!  No lemma to prove.
			 */ 
			
 			d9: * |- e1[e2] : tau by substitution on d7, d5
		
		end case
		// other cases do not unify with fn expression
		end case analysis
	
	end case
	// other cases do not unify with form of e = (e1 e2)
	end case analysis

end case
end induction
end theorem


/************************ SUBSTITUTION **********************************/

/* Just for fun, we prove a substitution lemma.  Note that this is
 * UNNECESSARY in SASyLF and in fact is NOT USED in the proof above--instead,
 * the proof above uses the built-in substitution mechanism that is justified
 * by the LF type theory behind SASyLF.  However, sometimes one may have to
 * prove substitution explicitly, and this example shows how it can be done.
 *
 * Additionally, some instructors may find it pedagogically useful to ask
 * students to prove substitution explicitly even though it is built into the
 * type theory of the tool.
 */

theorem subst : assumes Gamma forall dt : (Gamma, x:tau') |- e[x] : tau  forall dt' : Gamma |- e' : tau' exists Gamma |- e[e'] : tau.

d1 : Gamma |- e[e'] : tau by induction on dt :

	case rule

		------------------------------------ t-unit
		d2 : (Gamma, x:tau') |- ("("")") : (unit)

		is
	
		d3 : Gamma |- ("("")") : (unit)		by rule t-unit

	end case
	
	case rule
	
		------------------------- t-var
		d2 : (Gamma, x:tau) |- x : tau

		is
		
	d3 : Gamma |- e' : tau  by dt'

	end case
	
	case rule
	
		-------------------------------------------- t-var
		_ : (Gamma', x1:tau, x:tau') |- x1 : tau

		is
		
		d3 : Gamma', x1:tau |- x1 : tau		by rule t-var

	end case
	
	case rule
		d2: ((Gamma, x:tau'), x1:tau'') |- e1[x][x1] : tau'''
		------------------------------------------------------------------------ t-fn
		d3: (Gamma, x:tau') |- (fn x1 : tau'' => e1[x][x1]) : (tau'' -> tau''')

		is
		
		d2': ((Gamma, x1:tau''), x:tau') |- e1[x][x1] : tau''' by exchange on d2
		dt'': (Gamma, x1:tau'') |- e' : tau' by weakening on dt'
		d4 : (Gamma, x1:tau'') |- e1[e'][x1] : tau'''	by induction hypothesis on d2', dt''
		d5 : Gamma |- (fn x1 : tau'' => e1[e'][x1]) : (tau'' -> tau''') by rule t-fn on d4

	end case 
	
	case rule

		d2: (Gamma, x:tau') |- e1[x] : (tau'' -> tau)
		d3: (Gamma, x:tau') |- e2[x] : tau''
		-------------------------------------- t-app
		d4: (Gamma, x:tau') |- (e1[x] e2[x]) : tau
		
		is
		
		d5 : Gamma |- e1[e'] : (tau'' -> tau)	by induction hypothesis on d2, dt'
		d6 : Gamma |- e2[e'] : tau''			by induction hypothesis on d3, dt'
		d7 : Gamma |- (e1[e'] e2[e']) : tau	by rule t-app on d5, d6
		
	end case
end induction
end theorem