/* * Annotated solution to POPLMark Challenge 2a * * Author: Jonathan Aldrich * * This file defines System F_sub and proves type safety as specified in POPLMark * challenge problem 2a. */ /** The package declaration is currently a placeholder, but * will eventually support a module system for SASyLF */ package edu.cmu.cs.sasylf.poplmark; /** 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 lambda all Top 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. t and variants of t * (t', t'', t1, t2, 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 t[x] to denote that the variable x is bound in t. * Any uses of the same variable in a binding, such as lam "x" : ... are * treated as the binding occurence where the name of the variable is * defined. */ t ::= lambda x:T => t[x] /** To what syntactic class does the variable x refer? We specify that * by including a case "x" in the grammar for t. */ | x | t t | lambda X <: T => t[X] /** Brackets are special in SASyLF, so we use quotes to turn them into * terminals. */ | t "[" T "]" /** Here we define the syntax of types */ T ::= X | Top | T -> T | all X <: T => T[X] /** 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 : T | Gamma, X <: T /************************ JUDGMENTS **************************************/ /** We declare a judgment with a name ("value") and a form ("t value"). * The judgment is then followed by a series of inference rules that define * the judgment's semantics. * * With respect to POPLMark, this is not quite as syntactically nice as * defining values using a grammar that happens to be a subset of the term * grammar. We hope this can be implemented as syntactic sugar in the * future. */ judgment value: t value ----------------------- V-Abs lambda x:T => t[x] value -------------------------- V-Tabs lambda X <: T => t[X] value /** The evaluation judgment. Rules are defined with the premises above the line * and the conclusion below the line. * * With respect to POPLMark, we are using context evaluation rules rather than * explicit evaluation contexts. I'm guessing it would be possible to encode * things using explicit evaluation contexts, but unless we "built in" contexts * I think the metatheory would be extremely complicated. The best solution in * SASyLF is thus probably the one below, but investigating better support for * the "explicit context style" could be useful future work. */ judgment reduce: t -> t t1 -> t1' ------------------- E-CtxApp1 t1 t2 -> t1' t2 t1 -> t1' ------------------------------- E-CtxTapp t1 "[" T2 "]" -> t1' "[" T2 "]" t1 value t2 -> t2' ------------------- E-CtxApp2 (t1 t2) -> (t1 t2') // 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 t has the variable x bound in it. * We substitute t2 for x in t12 using the notation t12[t2]. */ t2 value ------------------------------------- E-AppAbs (lambda x:T11 => t12[x]) t2 -> t12[t2] ------------------------------------------------ E-TappTabs (lambda X <: T11 => t12[X]) "[" T2 "]" -> t12[T2] /** 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 |- t : T assumes Gamma /** 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:T |- x : T Gamma, x:T1 |- t2[x] : T2 --------------------------------------- T-Abs Gamma |- lambda x:T1 => t2[x] : T1 -> T2 Gamma |- t1 : T11 -> T12 Gamma |- t2 : T11 ---------------------------------- T-App Gamma |- t1 t2 : T12 Gamma, X <: T1 |- t2[X] : T2[X] ------------------------------------------------------- T-Tabs Gamma |- lambda X <: T1 => t2[X] : all X <: T1 => T2[X] Gamma |- t1 : all X <: T11 => T12[X] Gamma |- T2 <: T11 ----------------------------------- T-Tapp Gamma |- t1 "[" T2 "]" : T12[T2] // In this rule we use T' rather than S as SASyLF doesn't currently support // more than one metavariable per syntactic category. Gamma |- t : T' Gamma |- T' <: T ---------------- T-Sub Gamma |- t : T /** The subtyping judgment */ judgment subtyping: Gamma |- T <: T' assumes Gamma ----------------- SA-Top Gamma |- T <: Top /** As in the Twelf solution, we provide standard variable, reflexivity, and * transitivity rules rather than their algorithmic variants. I believe * the algorithmic rules could be encoded at some cost to the metatheory, * but it would be awkward because we wouldn't be able to use the built-in * variable rule, and would instead have to have the variable use come from * a different judgment. */ ----------------------- SA-Var Gamma, X <: T |- X <: T ----------------------- SA-Refl Gamma |- T <: T Gamma |- T1 <: T2 Gamma |- T2 <: T3 ----------------------- SA-Trans Gamma |- T1 <: T3 Gamma |- T1 <: T1' Gamma |- T2' <: T2 ------------------------------- SA-Arrow Gamma |- T1' -> T2' <: T1 -> T2 Gamma |- T1 <: T1' Gamma, X <: T1 |- T2'[X] <: T2[X] ------------------------------------------------------- SA-All Gamma |- all X' <: T1' => T2'[X'] <: all X <: T1 => T2[X] /** 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: t stepsorvalue t value --------------- stepsorvalue-value t stepsorvalue t -> t' --------------- stepsorvalue-steps t stepsorvalue /** equality judgment, used in canonical forms lemma */ judgment equality: t == t ------ equality t == t judgment type-equality: T == T ------ type-equality T == T judgment arrow-sub: T == T1' -> T2 <: T1 -> T2 * |- T1 <: T1' * |- T2' <: T2 -------------------------------------- arrow-sub (T1' -> T2') == T1' -> T2' <: T1 -> T2 judgment Tarrow-sub: T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] * |- T11'' <: T11' *, X <: T11'' |- T12'[X] <: T12[X] ---------------------------------------------------------------------------------- Tarrow-sub (all X <: T11' => T12'[X]) == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] judgment app-sub: t : T t : T -> T <: T * |- t2 : T2 * |- t1 : T2 -> T1 * |- T1 <: T -------------------------- app-sub t2 : T2 t1 : T2 -> T1 <: T /************************ 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 : t value exists (lambda x : T => x) t -> t. /** 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 on , , ..., " * This means that we conclude the judgment on the left by applying rule to the * (ordered) list of premises , , ..., . Each 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 ..." * part. */ d1 : (lambda x : T => x) t -> t by rule E-AppAbs 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 **************************************/ lemma arrow-sub-arrow: forall dsub: * |- T <: T1 -> T2 exists T == T1' -> T2'' <: T1 -> T2. // T == T1' -> T2', T1 <: T1', and T2' <: T2 deq: T == T1' -> T2'' <: T1 -> T2 by induction on dsub: case rule ------------------- SA-Refl d1: Gamma |- T <: T is dsub1: * |- T1 <: T1 by rule SA-Refl dsub2: * |- T2 <: T2 by rule SA-Refl deq: T == T1 -> T2 <: T1 -> T2 by rule arrow-sub on dsub1, dsub2 end case case rule d1: Gamma |- T <: T2' d2: Gamma |- T2' <: T1 -> T2 ---------------------------- SA-Trans d3: Gamma |- T <: T1 -> T2 is d4: T2' == T21' -> T22' <: T1 -> T2 by induction hypothesis on d2 deq: T == T1' -> T2'' <: T1 -> T2 by case analysis on d4: case rule d5: * |- T1 <: T21' d6: * |- T22' <: T2 ----------------------------------- arrow-sub d7: T21' -> T22' == T21' -> T22' <: T1 -> T2 is d8: T == T1'' -> T3 <: T21' -> T22' by induction hypothesis on d1 deq: T == T1' -> T2'' <: T1 -> T2 by case analysis on d8: case rule d9: * |- T21' <: T1'' d10: * |- T3 <: T22' ----------------------------------------------- arrow-sub d11: (T1'' -> T3) == T1'' -> T3 <: T21' -> T22' is d12: * |- T1 <: T1'' by rule SA-Trans on d5, d9 d13: * |- T3 <: T2 by rule SA-Trans on d10, d6 deq: T == T1'' -> T3 <: T1 -> T2 by rule arrow-sub on d12, d13 end case end case analysis end case end case analysis end case case rule d1: Gamma |- T1 <: T1' d2: Gamma |- T2' <: T2 ----------------------------------- SA-Arrow d3: Gamma |- T1' -> T2' <: T1 -> T2 is deq: T == T1' -> T2' <: T1 -> T2 by rule arrow-sub on d1, d2 end case end induction end lemma theorem canonical-form-lambda : forall dtv : t value forall dtt: * |- t : T1 -> T2 exists t == lambda x : T1' => t'[x]. deq : t == lambda x : T1' => t'[x] by induction on dtt : /** ugh--problem with SASyLF here. We'd like to case analyze on dtv first, but * we built case analysis in to induction. TODO: revisit this decision! */ case rule dtt'' : *, x:T1 |- t'[x] : T2 --------------------------------------------- T-Abs dtt' : * |- lambda x : T1 => t'[x] : T1 -> T2 is deq : t == lambda x : T1 => t'[x] by rule equality end case case rule dtt1' : (*) |- t1 : T'' -> (T1 -> T2) dtt2' : (*) |- t2 : T'' --------------------------------------------- T-App dtt' : (*) |- t1 t2 : T1 -> T2 is deq : t == lambda x : T1' => t'[x] by case analysis on dtv : end case analysis end case case rule dp1t1': * |- t' : all X <: T'' => T'''[X] dp1t2': * |- T' <: T'' ---------------------------------------- T-Tapp dp1t': * |- t' "[" T' "]" : T'''[T'] is deq : t == lambda x : T1' => t'[x] by case analysis on dtv : end case analysis end case case rule d1': * |- t : T' d2': * |- T' <: T1 -> T2 ------------------------ T-Sub d3': * |- t : T1 -> T2 is d4: T' == T1'' -> T2' <: T1 -> T2 by lemma arrow-sub-arrow on d2' deq : t == lambda x : T1' => t'[x] by case analysis on d4: case rule d5: * |- T1 <: T1'' d6: * |- T2' <: T2 ------------------------------------------- arrow-sub d7: (T1'' -> T2') == T1'' -> T2' <: T1 -> T2 is d8: t == lambda x : T1''' => t''[x] by induction hypothesis on dtv, d1' end case end case analysis end case // other cases don't unify with conclusion end induction end theorem lemma narrow-subtype: forall dsub: Gamma, X <: T |- T1[X] <: T2[X] forall dsub': Gamma |- T' <: T exists Gamma, X <: T' |- T1[X] <: T2[X]. dres: Gamma, X <: T' |- T1[X] <: T2[X] by induction on dsub: case rule ----------------------------- SA-Top d1: Gamma, X <: T |- T1[X] <: Top is d2: Gamma, X <: T' |- T1[X] <: Top by rule SA-Top end case case rule ----------------------- SA-Var d1: Gamma, X <: T |- X <: T is d2: Gamma, X <: T' |- X <: T' by rule SA-Var d3: Gamma, X <: T' |- T' <: T by weakening on dsub' d4: Gamma, X <: T' |- X <: T by rule SA-Trans on d2, d3 end case case rule ----------------------------------------- SA-Var d1: Gamma, X' <: T'', X <: T |- X' <: T'' is d2: Gamma, X' <: T'' |- X' <: T'' by rule SA-Var d3: Gamma, X' <: T'', X <: T' |- X' <: T'' by weakening on d2 end case case rule ----------------------------------- SA-Refl d1: Gamma, X <: T |- T1[X] <: T1[X] is d2: Gamma, X <: T' |- T1[X] <: T1[X] by rule SA-Refl end case case rule d1: Gamma, X <: T |- T1[X] <: T3[X] d2: Gamma, X <: T |- T3[X] <: T2[X] ----------------------------------- SA-Trans d3: Gamma, X <: T |- T1[X] <: T2[X] is d4: Gamma, X <: T' |- T1[X] <: T3[X] by induction hypothesis on d1, dsub' d5: Gamma, X <: T' |- T3[X] <: T2[X] by induction hypothesis on d2, dsub' d6: Gamma, X <: T' |- T1[X] <: T2[X] by rule SA-Trans on d4, d5 end case case rule d1: Gamma, X <: T |- T2'[X] <: T1'[X] d2: Gamma, X <: T |- T1''[X] <: T2''[X] ----------------------------------------------------------- SA-Arrow d3: Gamma, X <: T |- T1'[X] -> T1''[X] <: T2'[X] -> T2''[X] is d4: Gamma, X <: T' |- T2'[X] <: T1'[X] by induction hypothesis on d1, dsub' d5: Gamma, X <: T' |- T1''[X] <: T2''[X] by induction hypothesis on d2, dsub' d6: Gamma, X <: T' |- T1'[X] -> T1''[X] <: T2'[X] -> T2''[X] by rule SA-Arrow on d4, d5 end case case rule d1: Gamma, X <: T |- T2'[X] <: T1'[X] d2: Gamma, X <: T, X' <: T2'[X] |- T1''[X][X'] <: T2''[X][X'] --------------------------------------------------------------------------------------- SA-All d3: Gamma, X <: T |- all X' <: T1'[X] => T1''[X][X'] <: all X' <: T2'[X] => T2''[X][X'] is d4: Gamma, X <: T' |- T2'[X] <: T1'[X] by induction hypothesis on d1, dsub' //d8: Gamma, X <: T', X' <: T2'[X] |- T1''[X][X'] <: T2''[X][X'] by induction hypothesis on d2, dsub' // limitation: not yet supported d9: Gamma, X <: T', X' <: T2'[X] |- T1''[X][X'] <: T2''[X][X'] by unproved // should be the text above! d10: Gamma, X <: T' |- T1[X] <: T2[X] by rule SA-All on d4, d9 end case end induction end lemma lemma Tarrow-sub-Tarrow: forall dsub: * |- T'' <: all X <: T11'' => T12[X] exists T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X]. deq: T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] by induction on dsub: case rule ----------------------------------------------------------------- SA-Refl d1: * |- all X <: T11'' => T12[X] <: all X <: T11'' => T12[X] is dsub1: * |- T11'' <: T11'' by rule SA-Refl dsub2: *, X <: T11'' |- T12[X] <: T12[X] by rule SA-Refl deq: all X <: T11'' => T12[X] == all X <: T11'' => T12[X] <: all X <: T11'' => T12[X] by rule Tarrow-sub on dsub1, dsub2 end case case rule d1: * |- T'' <: T2' d2: * |- T2' <: all X <: T11'' => T12[X] ---------------------------------------- SA-Trans d3: * |- T'' <: all X <: T11'' => T12[X] is d4: T2' == all X <: T21' => T22[X] <: all X <: T11'' => T12[X] by induction hypothesis on d2 deq: T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] by case analysis on d4: case rule d5: * |- T11'' <: T21' d6: *, X <: T11'' |- T22[X] <: T12[X] ---------------------------------------------------------------------------------- Tarrow-sub d7: all X <: T21' => T22[X] == all X <: T21' => T22[X] <: all X <: T11'' => T12[X] is d8: T'' == all X <: T11''' => T12''[X] <: all X <: T21' => T22[X] by induction hypothesis on d1 deq: T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] by case analysis on d8: case rule d9: * |- T21' <: T11''' d10: *, X <: T21' |- T12''[X] <: T22[X] ------------------------------------------------------------------------------------- Tarrow-sub d11: all X <: T11''' => T12''[X] == all X <: T11''' => T12''[X] <: all X <: T21' => T22[X] is d12: * |- T11'' <: T11''' by rule SA-Trans on d5, d9 d13: *, X <: T11'' |- T12''[X] <: T22[X] by lemma narrow-subtype on d10, d5 d14: *, X <: T11'' |- T12''[X] <: T12[X] by rule SA-Trans on d13, d6 deq: T'' == all X <: T11''' => T12''[X] <: all X <: T11'' => T12[X] by rule Tarrow-sub on d12, d14 end case end case analysis end case end case analysis end case case rule d1: * |- T11'' <: T11' d2: *, X <: T11'' |- T12'[X] <: T12[X] ----------------------------------------------------------------- SA-All d3: * |- all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] is deq: T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] by rule Tarrow-sub on d1, d2 end case end induction end lemma theorem canonical-form-Lambda : forall dtv : t value forall dtt: * |- t : all X <: T1 => T2[X] exists t == lambda X <: T1' => t2[X]. deq : t == lambda X <: T1' => t2[X] by induction on dtt : /** ugh--problem with SASyLF here. We'd like to case analyze on dtv first, but * we built case analysis in to induction. TODO: revisit this decision! */ case rule d1: *, X <: T1 |- t2[X] : T2[X] --------------------------------------------------- T-Tabs d2: * |- lambda X <: T1 => t2[X] : all X <: T1 => T2[X] is deq : t == lambda X <: T1 => t2[X] by rule equality end case case rule dtt1' : (*) |- t1 : T'' -> (all X <: T1 => T2[X]) dtt2' : (*) |- t2 : T'' --------------------------------------------- T-App dtt' : (*) |- t1 t2 : all X <: T1 => T2[X] is deq : t == lambda X <: T1' => t2[X] by case analysis on dtv : end case analysis end case case rule dp1t1': * |- t' : all X <: T'' => T'''[X] dp1t2': * |- T' <: T'' ---------------------------------------- T-Tapp dp1t': * |- t' "[" T' "]" : T'''[T'] is deq : t == lambda X <: T1' => t2[X] by case analysis on dtv : end case analysis end case case rule d1': * |- t : T' d2': * |- T' <: all X <: T1 => T2[X] ------------------------------------ T-Sub d3': * |- t : all X <: T1 => T2[X] is d4: T' == all X <: T1'' => T2'[X] <: all X <: T1 => T2[X] by lemma Tarrow-sub-Tarrow on d2' deq : t == lambda X <: T1' => t2[X] by case analysis on d4: case rule d5: * |- T1 <: T1'' d6: *, X <: T1 |- T2'[X] <: T2[X] ------------------------------------------------------------------------------------- Tarrow-sub d7: all X <: T1'' => T2'[X] == all X <: T1'' => T2'[X] <: all X <: T1 => T2[X] is deq : t == lambda X <: T1''' => t2'[X] by induction hypothesis on dtv, d1' end case end case analysis end case // other cases don't unify with conclusion end induction end theorem theorem progress : forall dt : * |- t : T exists t 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 : t 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 is " * Here 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 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. */ // variable case is impossible since Gamma must be * case rule d1: *, x:T1 |- t2[x] : T2 --------------------------------------- T-Abs d2: * |- lambda x:T1 => t2[x] : T1 -> T2 is d3 : lambda x:T1 => t2[x] value by rule V-Abs d4 : lambda x:T1 => t2[x] stepsorvalue by rule stepsorvalue-value on d3 end case case rule dp1t: * |- t1 : T11 -> T12 dp2t: * |- t2 : T11 ---------------------------------- T-App d3: * |- t1 t2 : T12 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: t1 stepsorvalue by induction hypothesis on dp1t dp2sv: t2 stepsorvalue by induction hypothesis on dp2t dsv : t stepsorvalue by case analysis on dp1sv : case rule dp1s : t1 -> t1' ---------------------- stepsorvalue-steps dp1sv' : t1 stepsorvalue is ds : t1 t2 -> t1' t2 by rule E-CtxApp1 on dp1s dsv : t1 t2 stepsorvalue by rule stepsorvalue-steps on ds end case case rule dp1v : t1 value ---------------------- stepsorvalue-value dp1sv' : t1 stepsorvalue is dsv : t stepsorvalue by case analysis on dp2sv : case rule dp2v : t2 value ---------------------- stepsorvalue-value dp2sv' : t2 stepsorvalue is deq : t1 == lambda x : T11' => t1'[x] by lemma canonical-form-lambda on dp1v, dp1t dsv : t stepsorvalue by case analysis on deq : case rule ------------------------------------- equality deq' : lambda x : T11' => t1'[x] == lambda x : T11' => t1'[x] is dsteps : t1 t2 -> t1'[t2] by rule E-AppAbs on dp2v dsv : t stepsorvalue by rule stepsorvalue-steps on dsteps end case end case analysis end case case rule dp2s : t2 -> t2' ------------------------- stepsorvalue-steps dp2sv' : t2 stepsorvalue is ds : t1 t2 -> t1 t2' by rule E-CtxApp2 on dp1v, dp2s dsv : t1 t2 stepsorvalue by rule stepsorvalue-steps on ds end case end case analysis end case end case analysis end case case rule d1: *, X <: T1 |- t2[X] : T2[X] ------------------------------------------------------- T-Tabs d2: * |- lambda X <: T1 => t2[X] : all X <: T1 => T2[X] is d3 : lambda X <: T1 => t2[X] value by rule V-Tabs d4 : lambda X <: T1 => t2[X] stepsorvalue by rule stepsorvalue-value on d3 end case case rule d1: * |- t1 : all X <: T11 => T12[X] d2: * |- T2 <: T11 ----------------------------------- T-Tapp d3: * |- t1 "[" T2 "]" : T12[T2] is d1sv: t1 stepsorvalue by induction hypothesis on d1 dsv : t stepsorvalue by case analysis on d1sv : case rule d1s : t1 -> t1' ----------------------- stepsorvalue-steps d1sv' : t1 stepsorvalue is ds : t1 "[" T2 "]" -> t1' "[" T2 "]" by rule E-CtxTapp on d1s dsv : t1 "[" T2 "]" stepsorvalue by rule stepsorvalue-steps on ds end case case rule d1v : t1 value ----------------------- stepsorvalue-value d1sv' : t1 stepsorvalue is deq : t1 == lambda X <: T11' => t1'[X] by lemma canonical-form-Lambda on d1v, d1 dsv : t stepsorvalue by case analysis on deq : case rule ------------------------------------------------------------- equality deq' : lambda X <: T11' => t1'[X] == lambda X <: T11' => t1'[X] is dsteps : t1 "[" T2 "]" -> t1'[T2] by rule E-TappTabs dsv : t stepsorvalue by rule stepsorvalue-steps on dsteps end case end case analysis end case end case analysis end case case rule d1: * |- t : T' d2: * |- T' <: T ---------------- T-Sub d3: * |- t : T is dsv : t stepsorvalue by induction hypothesis on d1 end case end induction end theorem /************************ PRESERVATION **************************************/ lemma invert-lambda: forall dt: * |- lambda x:T11 => t12[x] : T1 -> T forall dt2: * |- t2 : T2 forall dsub: * |- T2 <: T1 exists * |- t12[t2] : T. dt12: * |- t12[t2] : T by induction on dt: case rule d1: *, x:T1 |- t12[x] : T --------------------------------------- T-Abs d2: * |- lambda x:T1 => t12[x] : T1 -> T is dt12: * |- t12[t2] : T by substitution on dt2, d1 end case case rule d1: * |- lambda x:T11 => t12[x] : T'' d2: * |- T'' <: T1 -> T ----------------------------------------- T-Sub d3: * |- lambda x:T11 => t12[x] : T1 -> T is d4: T'' == T1' -> T' <: T1 -> T by lemma arrow-sub-arrow on d2 dt12: * |- t12[t2] : T by case analysis on d4: case rule d5: * |- T1 <: T1' d6: * |- T' <: T -------------------------------- arrow-sub d7: T1' -> T' == T1' -> T' <: T1 -> T is d8: * |- T2 <: T1' by rule SA-Trans on dsub, d5 d9: * |- t12[t2] : T' by induction hypothesis on d1, dt2, d8 dt12: * |- t12[t2] : T by rule T-Sub on d9, d6 end case end case analysis end case end induction end lemma lemma invert-lambda2: forall dt: * |- lambda X <: T11 => t12[X] : all X <: T11'' => T12[X] forall dsub1: * |- T2 <: T11'' exists * |- t12[T2] : T12[T2]. dt2: * |- t12[T2] : T12[T2] by induction on dt: case rule d1: *, X <: T11 |- t12[X] : T12[X] ----------------------------------------------------------- T-Tabs d2: * |- lambda X <: T11 => t12[X] : all X <: T11 => T12[X] is d3: * |- t12[T2] : T12[T2] by substitution on d1, dsub1 end case case rule d1: * |- lambda X <: T11 => t12[X] : T'' d2: * |- T'' <: all X <: T11'' => T12[X] ----------------------------------------------------------- T-Sub d3: * |- lambda X <: T11 => t12[X] : all X <: T11'' => T12[X] is d4: T'' == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] by lemma Tarrow-sub-Tarrow on d2 dt12: * |- t12[T2] : T12[T2] by case analysis on d4: case rule d5: * |- T11'' <: T11' d6: *, X <: T11'' |- T12'[X] <: T12[X] --------------------------------------------------------------- Tarrow-sub d7: all X <: T11' => T12'[X] == all X <: T11' => T12'[X] <: all X <: T11'' => T12[X] is d8: * |- T2 <: T11' by rule SA-Trans on dsub1, d5 d9: * |- t12[T2] : T12'[T2] by induction hypothesis on d1, d8 d11: * |- T12'[T2] <: T12[T2] by substitution on d6, dsub1 dt12: * |- t12[T2] : T12[T2] by rule T-Sub on d9, d11 end case end case analysis end case end induction end lemma // Note: we prove preservation, as usual, with an empty Gamma. // Was the non-empty Gamma in the POPLMark challenge a mistake? theorem preservation: forall dt: * |- t : T forall ds: t -> t' exists * |- t' : T. dt' : * |- t' : T by induction on dt: // variable case is impossible since Gamma must be * case rule d1: *, x:T1 |- t2[x] : T2 --------------------------------------- T-Abs d2: * |- lambda x:T1 => t2[x] : T1 -> T2 is dt' : * |- t' : T by case analysis on ds: end case analysis end case case rule d1: * |- t1 : T1 -> T d2: * |- t2 : T1 ---------------------------------- T-App d3: * |- t1 t2 : T is dt' : * |- t' : T by case analysis on ds: case rule d4: t1 -> t1' ------------------- E-CtxApp1 d5: t1 t2 -> t1' t2 is d6: * |- t1' : T1 -> T by induction hypothesis on d1, d4 d7: * |- t' : T by rule T-App on d6, d2 end case case rule d4: t1 value d5: t2 -> t2' ------------------- E-CtxApp2 d6: t1 t2 -> t1 t2' is d7: * |- t2' : T1 by induction hypothesis on d2, d5 d8: * |- t' : T by rule T-App on d1, d7 end case case rule d4: t2 value ------------------------------------- E-AppAbs d5: (lambda x:T11 => t12[x]) t2 -> t12[t2] is //d6: *, x:T1 |- t12[x] : T by lemma invert-lambda on d1 d6: * |- T1 <: T1 by rule SA-Refl d7: * |- t12[t2] : T by lemma invert-lambda on d1, d2, d6 end case end case analysis end case case rule d1: *, X <: T1 |- t2[X] : T2[X] ------------------------------------------------------- T-Tabs d2: * |- lambda X <: T1 => t2[X] : all X <: T1 => T2[X] is dt' : * |- t' : T by case analysis on ds: end case analysis end case case rule d1: * |- t1 : all X <: T11'' => T12[X] d2: * |- T2 <: T11'' ----------------------------------- T-Tapp d3: * |- t1 "[" T2 "]" : T12[T2] is dt' : * |- t' : T by case analysis on ds: case rule d4: t1 -> t1' ----------------------------------- E-CtxTapp d5: t1 "[" T2 "]" -> t1' "[" T2 "]" is d6: * |- t1' : all X <: T11'' => T12[X] by induction hypothesis on d1, d4 d7: * |- t' : T by rule T-Tapp on d6, d2 end case case rule ----------------------------------------------------- E-TappTabs d5: (lambda X <: T11 => t12[X]) "[" T2 "]" -> t12[T2] is d7: * |- t12[T2] : T12[T2] by lemma invert-lambda2 on d1, d2 end case end case analysis end case case rule d1: * |- t : T' d2: * |- T' <: T ---------------- T-Sub d3: * |- t : T is dtT' : * |- t' : T' by induction hypothesis on d1, ds dt' : * |- t' : T by rule T-Sub on dtT', d2 end case end induction end theorem