MoreStlcMore on the Simply Typed Lambda-Calculus
Require Import SfLib.
Require Import Maps.
Require Import Types.
Require Import Smallstep.
Require Import Stlc.
Simple Extensions to STLC
Numbers
let-bindings
t ::= Terms | ... (other terms same as before) | let x=t in t let-binding
t1 ⇒ t1' | (ST_Let1) |
let x=t1 in t2 ⇒ let x=t1' in t2 |
(ST_LetValue) | |
let x=v1 in t2 ⇒ [x:=v1]t2 |
Γ ⊢ t1 : T1 Γ , x:T1 ⊢ t2 : T2 | (T_Let) |
Γ ⊢ let x=t1 in t2 : T2 |
Pairs
λx:Nat*Nat. let sum = x.fst + x.snd in let diff = x.fst - x.snd in (sum,diff)
t ::= Terms | ... | (t,t) pair | t.fst first projection | t.snd second projection v ::= Values | ... | (v,v) pair value T ::= Types | ... | T * T product type
t1 ⇒ t1' | (ST_Pair1) |
(t1,t2) ⇒ (t1',t2) |
t2 ⇒ t2' | (ST_Pair2) |
(v1,t2) ⇒ (v1,t2') |
t1 ⇒ t1' | (ST_Fst1) |
t1.fst ⇒ t1'.fst |
(ST_FstPair) | |
(v1,v2).fst ⇒ v1 |
t1 ⇒ t1' | (ST_Snd1) |
t1.snd ⇒ t1'.snd |
(ST_SndPair) | |
(v1,v2).snd ⇒ v2 |
Γ ⊢ t1 : T1 Γ ⊢ t2 : T2 | (T_Pair) |
Γ ⊢ (t1,t2) : T1*T2 |
Γ ⊢ t1 : T11*T12 | (T_Fst) |
Γ ⊢ t1.fst : T11 |
Γ ⊢ t1 : T11*T12 | (T_Snd) |
Γ ⊢ t1.snd : T12 |
Unit
t ::= Terms | ... | unit unit value v ::= Values | ... | unit unit T ::= Types | ... | Unit Unit typeTyping:
(T_Unit) | |
Γ ⊢ unit : Unit |
Sums
Nat + Bool
inl : Nat -> Nat + Bool inr : Bool -> Nat + Bool
div : Nat -> Nat -> (Nat + Unit) = div = λx:Nat. λy:Nat. if iszero y then inr unit else inl ...The type Nat + Unit above is in fact isomorphic to option nat in Coq, and we've already seen how to signal errors with options.
getNat = λx:Nat+Bool. case x of inl n => n | inr b => if b then 1 else 0
t ::= Terms | ... | inl T t tagging (left) | inr T t tagging (right) | case t of case inl x => t | inr x => t v ::= Values | ... | inl T v tagged value (left) | inr T v tagged value (right) T ::= Types | ... | T + T sum type
t1 ⇒ t1' | (ST_Inl) |
inl T t1 ⇒ inl T t1' |
t1 ⇒ t1' | (ST_Inr) |
inr T t1 ⇒ inr T t1' |
t0 ⇒ t0' | (ST_Case) |
case t0 of inl x1 ⇒ t1 | inr x2 ⇒ t2 ⇒ | |
case t0' of inl x1 ⇒ t1 | inr x2 ⇒ t2 |
(ST_CaseInl) | |
case (inl T v0) of inl x1 ⇒ t1 | inr x2 ⇒ t2 | |
⇒ [x1:=v0]t1 |
(ST_CaseInr) | |
case (inr T v0) of inl x1 ⇒ t1 | inr x2 ⇒ t2 | |
⇒ [x2:=v0]t2 |
Γ ⊢ t1 : T1 | (T_Inl) |
Γ ⊢ inl T2 t1 : T1 + T2 |
Γ ⊢ t1 : T2 | (T_Inr) |
Γ ⊢ inr T1 t1 : T1 + T2 |
Γ ⊢ t0 : T1+T2 | |
Γ , x1:T1 ⊢ t1 : T | |
Γ , x2:T2 ⊢ t2 : T | (T_Case) |
Γ ⊢ case t0 of inl x1 ⇒ t1 | inr x2 ⇒ t2 : T |
Lists
λx:List Nat. lcase x of nil -> 0 | a::x' -> lcase x' of nil -> a | b::x'' -> a+b
t ::= Terms | ... | nil T | cons t t | lcase t of nil -> t | x::x -> t v ::= Values | ... | nil T nil value | cons v v cons value T ::= Types | ... | List T list of Ts
t1 ⇒ t1' | (ST_Cons1) |
cons t1 t2 ⇒ cons t1' t2 |
t2 ⇒ t2' | (ST_Cons2) |
cons v1 t2 ⇒ cons v1 t2' |
t1 ⇒ t1' | (ST_Lcase1) |
(lcase t1 of nil → t2 | xh::xt → t3) ⇒ | |
(lcase t1' of nil → t2 | xh::xt → t3) |
(ST_LcaseNil) | |
(lcase nil T of nil → t2 | xh::xt → t3) | |
⇒ t2 |
(ST_LcaseCons) | |
(lcase (cons vh vt) of nil → t2 | xh::xt → t3) | |
⇒ [xh:=vh,xt:=vt]t3 |
(T_Nil) | |
Γ ⊢ nil T : List T |
Γ ⊢ t1 : T Γ ⊢ t2 : List T | (T_Cons) |
Γ ⊢ cons t1 t2: List T |
Γ ⊢ t1 : List T1 | |
Γ ⊢ t2 : T | |
Γ , h:T1, t:List T1 ⊢ t3 : T | (T_Lcase) |
Γ ⊢ (lcase t1 of nil → t2 | h::t → t3) : T |
General Recursion
fact = λx:Nat. if x=0 then 1 else x * (fact (pred x)))But this would require quite a bit of work to formalize: we'd have to introduce a notion of "function definitions" and carry around an "environment" of such definitions in the definition of the step relation.
fact = fix (\f:Nat->Nat. λx:Nat. if x=0 then 1 else x * (f (pred x)))
t ::= Terms | ... | fix t fixed-point operatorReduction:
t1 ⇒ t1' | (ST_Fix1) |
fix t1 ⇒ fix t1' |
F = \xf:T1.t2 | (ST_FixAbs) |
fix F ⇒ [xf:=fix F]t2 |
Γ ⊢ t1 : T1->T1 | (T_Fix) |
Γ ⊢ fix t1 : T1 |
fix F 3⇒ ST_FixAbs
(\x. if x=0 then 1 else x * (fix F (pred x))) 3⇒ ST_AppAbs
if 3=0 then 1 else 3 * (fix F (pred 3))⇒ ST_If0_Nonzero
3 * (fix F (pred 3))⇒ ST_FixAbs + ST_Mult2
3 * ((\x. if x=0 then 1 else x * (fix F (pred x))) (pred 3))⇒ ST_PredNat + ST_Mult2 + ST_App2
3 * ((\x. if x=0 then 1 else x * (fix F (pred x))) 2)⇒ ST_AppAbs + ST_Mult2
3 * (if 2=0 then 1 else 2 * (fix F (pred 2)))⇒ ST_If0_Nonzero + ST_Mult2
3 * (2 * (fix F (pred 2)))⇒ ST_FixAbs + 2 x ST_Mult2
3 * (2 * ((\x. if x=0 then 1 else x * (fix F (pred x))) (pred 2)))⇒ ST_PredNat + 2 x ST_Mult2 + ST_App2
3 * (2 * ((\x. if x=0 then 1 else x * (fix F (pred x))) 1))⇒ ST_AppAbs + 2 x ST_Mult2
3 * (2 * (if 1=0 then 1 else 1 * (fix F (pred 1))))⇒ ST_If0_Nonzero + 2 x ST_Mult2
3 * (2 * (1 * (fix F (pred 1))))⇒ ST_FixAbs + 3 x ST_Mult2
3 * (2 * (1 * ((\x. if x=0 then 1 else x * (fix F (pred x))) (pred 1))))⇒ ST_PredNat + 3 x ST_Mult2 + ST_App2
3 * (2 * (1 * ((\x. if x=0 then 1 else x * (fix F (pred x))) 0)))⇒ ST_AppAbs + 3 x ST_Mult2
3 * (2 * (1 * (if 0=0 then 1 else 0 * (fix F (pred 0)))))⇒ ST_If0Zero + 3 x ST_Mult2
3 * (2 * (1 * 1))⇒ ST_MultNats + 2 x ST_Mult2
3 * (2 * 1)⇒ ST_MultNats + ST_Mult2
3 * 2⇒ ST_MultNats
6
Exercise: 1 star, optional (halve_fix)
Translate this informal recursive definition into one using fix:halve = λx:Nat. if x=0 then 0 else if (pred x)=0 then 0 else 1 + (halve (pred (pred x))))(* FILL IN HERE *)
☐
Exercise: 1 star, optional (fact_steps)
Write down the sequence of steps that the term fact 1 goes through to reduce to a normal form (assuming the usual reduction rules for arithmetic operations).☐
fix (\x:T.x)
By T_Fix and T_Abs, this term has type T. By ST_FixAbs
it reduces to itself, over and over again. Thus it is an
undefined element of T.
equal = fix (\eq:Nat->Nat->Bool. λm:Nat. λn:Nat. if m=0 then iszero n else if n=0 then false else eq (pred m) (pred n))
evenodd = fix (\eo: (Nat->Bool * Nat->Bool). let e = λn:Nat. if n=0 then true else eo.snd (pred n) in let o = λn:Nat. if n=0 then false else eo.fst (pred n) in (e,o)) even = evenodd.fst odd = evenodd.snd
Records
t ::= Terms | ... | {i1=t1, ..., in=tn} record | t.i projection v ::= Values | ... | {i1=v1, ..., in=vn} record value T ::= Types | ... | {i1:T1, ..., in:Tn} record typeIntuitively, the generalization is pretty obvious. But it's worth noticing that what we've actually written is rather informal: in particular, we've written "..." in several places to mean "any number of these," and we've omitted explicit mention of the usual side-condition that the labels of a record should not contain repetitions.
ti ⇒ ti' | (ST_Rcd) |
{i1=v1, ..., im=vm, in=ti, ...} | |
⇒ {i1=v1, ..., im=vm, in=ti', ...} |
t1 ⇒ t1' | (ST_Proj1) |
t1.i ⇒ t1'.i |
(ST_ProjRcd) | |
{..., i=vi, ...}.i ⇒ vi |
Γ ⊢ t1 : T1 ... Γ ⊢ tn : Tn | (T_Rcd) |
Γ ⊢ {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn} |
Γ ⊢ t : {..., i:Ti, ...} | (T_Proj) |
Γ ⊢ t.i : Ti |
Encoding Records (Optional)
- We can directly formalize the syntactic forms and inference
rules, staying as close as possible to the form we've given
them above. This is conceptually straightforward, and it's
probably what we'd want to do if we were building a real
compiler — in particular, it will allow us to print error
messages in the form that programmers will find easy to
understand. But the formal versions of the rules will not be
pretty at all!
- We could look for a smoother way of presenting records — for
example, a binary presentation with one constructor for the
empty record and another constructor for adding a single field
to an existing record, instead of a single monolithic
constructor that builds a whole record at once. This is the
right way to go if we are primarily interested in studying the
metatheory of the calculi with records, since it leads to
clean and elegant definitions and proofs. Chapter Records
shows how this can be done.
- Alternatively, if we like, we can avoid formalizing records altogether, by stipulating that record notations are just informal shorthands for more complex expressions involving pairs and product types. We sketch this approach here.
{} ----> unit {t1, t2, ..., tn} ----> (t1, trest) where {t2, ..., tn} ----> trestSimilarly, we can encode tuple types using nested product types:
{} ----> Unit {T1, T2, ..., Tn} ----> T1 * TRest where {T2, ..., Tn} ----> TRestThe operation of projecting a field from a tuple can be encoded using a sequence of second projections followed by a first projection:
t.0 ----> t.fst t.(n+1) ----> (t.snd).n
LABEL POSITION a 0 b 1 c 2 ... ... foo 1004 ... ... bar 10562 ... ...
{a=5, b=6} ----> {5,6} {a=5, c=7} ----> {5,unit,7} {c=7, a=5} ----> {5,unit,7} {c=5, b=3} ----> {unit,3,5} {f=8,c=5,a=7} ----> {7,unit,5,unit,unit,8} {f=8,c=5} ----> {unit,unit,5,unit,unit,8}Note that each field appears in the position associated with its label, that the size of the tuple is determined by the label with the highest position, and that we fill in unused positions with unit.
{a:Nat, b:Nat} ----> {Nat,Nat} {c:Nat, a:Nat} ----> {Nat,Unit,Nat} {f:Nat,c:Nat} ----> {Unit,Unit,Nat,Unit,Unit,Nat}
t.l ----> t.(position of l)
Variants (Optional Reading)
Exercise: Formalizing the Extensions
Exercise: 4 stars, optional (STLC_extensions)
In this problem you will formalize a couple of the extensions described above. We've provided the necessary additions to the syntax of terms and types, and we've included a few examples that you can test your definitions with to make sure they are working as expected. You'll fill in the rest of the definitions and extend all the proofs accordingly.- numbers
- pairs and units
- sums
- lists
- let (which involves binding)
- fix
Inductive ty : Type :=
| TArrow : ty → ty → ty
| TNat : ty
| TUnit : ty
| TProd : ty → ty → ty
| TSum : ty → ty → ty
| TList : ty → ty.
Inductive tm : Type :=
(* pure STLC *)
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
(* numbers *)
| tnat : nat → tm
| tsucc : tm → tm
| tpred : tm → tm
| tmult : tm → tm → tm
| tif0 : tm → tm → tm → tm
(* pairs *)
| tpair : tm → tm → tm
| tfst : tm → tm
| tsnd : tm → tm
(* units *)
| tunit : tm
(* let *)
| tlet : id → tm → tm → tm
(* i.e., let x = t1 in t2 *)
(* sums *)
| tinl : ty → tm → tm
| tinr : ty → tm → tm
| tcase : tm → id → tm → id → tm → tm
(* i.e., case t0 of inl x1 ⇒ t1 | inr x2 ⇒ t2 *)
(* lists *)
| tnil : ty → tm
| tcons : tm → tm → tm
| tlcase : tm → tm → id → id → tm → tm
(* i.e., lcase t1 of | nil → t2 | x::y → t3 *)
(* fix *)
| tfix : tm → tm.
Note that, for brevity, we've omitted booleans and instead
provided a single if0 form combining a zero test and a
conditional. That is, instead of writing
if x = 0 then ... else ...we'll write this:
if0 x then ... else ...
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar y ⇒
if beq_id x y then s else t
| tabs y T t1 ⇒
tabs y T (if beq_id x y then t1 else (subst x s t1))
| tapp t1 t2 ⇒
tapp (subst x s t1) (subst x s t2)
| tnat n ⇒
tnat n
| tsucc t1 ⇒
tsucc (subst x s t1)
| tpred t1 ⇒
tpred (subst x s t1)
| tmult t1 t2 ⇒
tmult (subst x s t1) (subst x s t2)
| tif0 t1 t2 t3 ⇒
tif0 (subst x s t1) (subst x s t2) (subst x s t3)
| tpair t1 t2 ⇒
tpair (subst x s t1) (subst x s t2)
| tfst t1 ⇒
tfst (subst x s t1)
| tsnd t1 ⇒
tsnd (subst x s t1)
| tunit ⇒ tunit
(* FILL IN HERE *)
| tinl T t1 ⇒
tinl T (subst x s t1)
| tinr T t1 ⇒
tinr T (subst x s t1)
| tcase t0 y1 t1 y2 t2 ⇒
tcase (subst x s t0)
y1 (if beq_id x y1 then t1 else (subst x s t1))
y2 (if beq_id x y2 then t2 else (subst x s t2))
| tnil T ⇒
tnil T
| tcons t1 t2 ⇒
tcons (subst x s t1) (subst x s t2)
| tlcase t1 t2 y1 y2 t3 ⇒
tlcase (subst x s t1) (subst x s t2) y1 y2
(if beq_id x y1 then
t3
else if beq_id x y2 then t3
else (subst x s t3))
(* FILL IN HERE *)
| _ ⇒ t (* ... and delete this line *)
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
Inductive value : tm → Prop :=
| v_abs : ∀x T11 t12,
value (tabs x T11 t12)
(* Numbers are values: *)
| v_nat : ∀n1,
value (tnat n1)
(* A pair is a value if both components are: *)
| v_pair : ∀v1 v2,
value v1 →
value v2 →
value (tpair v1 v2)
(* A unit is always a value *)
| v_unit : value tunit
(* A tagged value is a value: *)
| v_inl : ∀v T,
value v →
value (tinl T v)
| v_inr : ∀v T,
value v →
value (tinr T v)
(* A list is a value iff its head and tail are values: *)
| v_lnil : ∀T, value (tnil T)
| v_lcons : ∀v1 vl,
value v1 →
value vl →
value (tcons v1 vl)
.
Hint Constructors value.
Reserved Notation "t1 '⇒' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T11 t12 v2,
value v2 →
(tapp (tabs x T11 t12) v2) ⇒ [x:=v2]t12
| ST_App1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tapp t1 t2) ⇒ (tapp t1' t2)
| ST_App2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tapp v1 t2) ⇒ (tapp v1 t2')
(* nats *)
| ST_Succ1 : ∀t1 t1',
t1 ⇒ t1' →
(tsucc t1) ⇒ (tsucc t1')
| ST_SuccNat : ∀n1,
(tsucc (tnat n1)) ⇒ (tnat (S n1))
| ST_Pred : ∀t1 t1',
t1 ⇒ t1' →
(tpred t1) ⇒ (tpred t1')
| ST_PredNat : ∀n1,
(tpred (tnat n1)) ⇒ (tnat (pred n1))
| ST_Mult1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tmult t1 t2) ⇒ (tmult t1' t2)
| ST_Mult2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tmult v1 t2) ⇒ (tmult v1 t2')
| ST_MultNats : ∀n1 n2,
(tmult (tnat n1) (tnat n2)) ⇒ (tnat (mult n1 n2))
| ST_If01 : ∀t1 t1' t2 t3,
t1 ⇒ t1' →
(tif0 t1 t2 t3) ⇒ (tif0 t1' t2 t3)
| ST_If0Zero : ∀t2 t3,
(tif0 (tnat 0) t2 t3) ⇒ t2
| ST_If0Nonzero : ∀n t2 t3,
(tif0 (tnat (S n)) t2 t3) ⇒ t3
(* pairs *)
| ST_Pair1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tpair t1 t2) ⇒ (tpair t1' t2)
| ST_Pair2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tpair v1 t2) ⇒ (tpair v1 t2')
| ST_Fst1 : ∀t1 t1',
t1 ⇒ t1' →
(tfst t1) ⇒ (tfst t1')
| ST_FstPair : ∀v1 v2,
value v1 →
value v2 →
(tfst (tpair v1 v2)) ⇒ v1
| ST_Snd1 : ∀t1 t1',
t1 ⇒ t1' →
(tsnd t1) ⇒ (tsnd t1')
| ST_SndPair : ∀v1 v2,
value v1 →
value v2 →
(tsnd (tpair v1 v2)) ⇒ v2
(* let *)
(* FILL IN HERE *)
(* sums *)
| ST_Inl : ∀t1 t1' T,
t1 ⇒ t1' →
(tinl T t1) ⇒ (tinl T t1')
| ST_Inr : ∀t1 t1' T,
t1 ⇒ t1' →
(tinr T t1) ⇒ (tinr T t1')
| ST_Case : ∀t0 t0' x1 t1 x2 t2,
t0 ⇒ t0' →
(tcase t0 x1 t1 x2 t2) ⇒ (tcase t0' x1 t1 x2 t2)
| ST_CaseInl : ∀v0 x1 t1 x2 t2 T,
value v0 →
(tcase (tinl T v0) x1 t1 x2 t2) ⇒ [x1:=v0]t1
| ST_CaseInr : ∀v0 x1 t1 x2 t2 T,
value v0 →
(tcase (tinr T v0) x1 t1 x2 t2) ⇒ [x2:=v0]t2
(* lists *)
| ST_Cons1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tcons t1 t2) ⇒ (tcons t1' t2)
| ST_Cons2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tcons v1 t2) ⇒ (tcons v1 t2')
| ST_Lcase1 : ∀t1 t1' t2 x1 x2 t3,
t1 ⇒ t1' →
(tlcase t1 t2 x1 x2 t3) ⇒ (tlcase t1' t2 x1 x2 t3)
| ST_LcaseNil : ∀T t2 x1 x2 t3,
(tlcase (tnil T) t2 x1 x2 t3) ⇒ t2
| ST_LcaseCons : ∀v1 vl t2 x1 x2 t3,
value v1 →
value vl →
(tlcase (tcons v1 vl) t2 x1 x2 t3) ⇒ (subst x2 vl (subst x1 v1 t3))
(* fix *)
(* FILL IN HERE *)
where "t1 '⇒' t2" := (step t1 t2).
Notation multistep := (multi step).
Notation "t1 '⇒*' t2" := (multistep t1 t2) (at level 40).
Hint Constructors step.
Next we define the typing rules. These are nearly direct
transcriptions of the inference rules shown above.
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
(* Typing rules for proper terms *)
| T_Var : ∀Γ x T,
Γ x = Some T →
Γ ⊢ (tvar x) ∈ T
| T_Abs : ∀Γ x T11 T12 t12,
(update Γ x T11) ⊢ t12 ∈ T12 →
Γ ⊢ (tabs x T11 t12) ∈ (TArrow T11 T12)
| T_App : ∀T1 T2 Γ t1 t2,
Γ ⊢ t1 ∈ (TArrow T1 T2) →
Γ ⊢ t2 ∈ T1 →
Γ ⊢ (tapp t1 t2) ∈ T2
(* nats *)
| T_Nat : ∀Γ n1,
Γ ⊢ (tnat n1) ∈ TNat
| T_Succ : ∀Γ t1,
Γ ⊢ t1 ∈ TNat →
Γ ⊢ (tsucc t1) ∈ TNat
| T_Pred : ∀Γ t1,
Γ ⊢ t1 ∈ TNat →
Γ ⊢ (tpred t1) ∈ TNat
| T_Mult : ∀Γ t1 t2,
Γ ⊢ t1 ∈ TNat →
Γ ⊢ t2 ∈ TNat →
Γ ⊢ (tmult t1 t2) ∈ TNat
| T_If0 : ∀Γ t1 t2 t3 T1,
Γ ⊢ t1 ∈ TNat →
Γ ⊢ t2 ∈ T1 →
Γ ⊢ t3 ∈ T1 →
Γ ⊢ (tif0 t1 t2 t3) ∈ T1
(* pairs *)
| T_Pair : ∀Γ t1 t2 T1 T2,
Γ ⊢ t1 ∈ T1 →
Γ ⊢ t2 ∈ T2 →
Γ ⊢ (tpair t1 t2) ∈ (TProd T1 T2)
| T_Fst : ∀Γ t T1 T2,
Γ ⊢ t ∈ (TProd T1 T2) →
Γ ⊢ (tfst t) ∈ T1
| T_Snd : ∀Γ t T1 T2,
Γ ⊢ t ∈ (TProd T1 T2) →
Γ ⊢ (tsnd t) ∈ T2
(* unit *)
| T_Unit : ∀Γ,
Γ ⊢ tunit ∈ TUnit
(* let *)
(* FILL IN HERE *)
(* sums *)
| T_Inl : ∀Γ t1 T1 T2,
Γ ⊢ t1 ∈ T1 →
Γ ⊢ (tinl T2 t1) ∈ (TSum T1 T2)
| T_Inr : ∀Γ t2 T1 T2,
Γ ⊢ t2 ∈ T2 →
Γ ⊢ (tinr T1 t2) ∈ (TSum T1 T2)
| T_Case : ∀Γ t0 x1 T1 t1 x2 T2 t2 T,
Γ ⊢ t0 ∈ (TSum T1 T2) →
(update Γ x1 T1) ⊢ t1 ∈ T →
(update Γ x2 T2) ⊢ t2 ∈ T →
Γ ⊢ (tcase t0 x1 t1 x2 t2) ∈ T
(* lists *)
| T_Nil : ∀Γ T,
Γ ⊢ (tnil T) ∈ (TList T)
| T_Cons : ∀Γ t1 t2 T1,
Γ ⊢ t1 ∈ T1 →
Γ ⊢ t2 ∈ (TList T1) →
Γ ⊢ (tcons t1 t2) ∈ (TList T1)
| T_Lcase : ∀Γ t1 T1 t2 x1 x2 t3 T2,
Γ ⊢ t1 ∈ (TList T1) →
Γ ⊢ t2 ∈ T2 →
(update (update Γ x2 (TList T1)) x1 T1) ⊢ t3 ∈ T2 →
Γ ⊢ (tlcase t1 t2 x1 x2 t3) ∈ T2
(* fix *)
(* FILL IN HERE *)
where "Gamma '⊢' t '∈' T" := (has_type Γ t T).
Hint Constructors has_type.
Examples
Notation a := (Id 0).
Notation f := (Id 1).
Notation g := (Id 2).
Notation l := (Id 3).
Notation k := (Id 6).
Notation i1 := (Id 7).
Notation i2 := (Id 8).
Notation x := (Id 9).
Notation y := (Id 10).
Notation processSum := (Id 11).
Notation n := (Id 12).
Notation eq := (Id 13).
Notation m := (Id 14).
Notation evenodd := (Id 15).
Notation even := (Id 16).
Notation odd := (Id 17).
Notation eo := (Id 18).
Next, a bit of Coq hackery to automate searching for typing
derivations. You don't need to understand this bit in detail —
just have a look over it so that you'll know what to look for if
you ever find yourself needing to make custom extensions to
auto.
The following Hint declarations say that, whenever auto
arrives at a goal of the form (Γ ⊢ (tapp e1 e1) ∈ T), it
should consider eapply T_App, leaving an existential variable
for the middle type T1, and similar for lcase. That variable
will then be filled in during the search for type derivations for
e1 and e2. We also include a hint to "try harder" when
solving equality goals; this is useful to automate uses of
T_Var (which includes an equality as a precondition).
Hint Extern 2 (has_type _ (tapp _ _) _) ⇒
eapply T_App; auto.
(* You'll want to uncomment the following line once
you've defined the T_Lcase constructor for the typing
relation: *)
(*
Hint Extern 2 (has_type _ (tlcase _ _ _ _ _) _) =>
eapply T_Lcase; auto.
*)
Hint Extern 2 (_ = _) ⇒ compute; reflexivity.
Module Numtest.
(* if0 (pred (succ (pred (2 * 0))) then 5 else 6 *)
Definition test :=
tif0
(tpred
(tsucc
(tpred
(tmult
(tnat 2)
(tnat 0)))))
(tnat 5)
(tnat 6).
Remove the comment braces once you've implemented enough of the
definitions that you think this should work.
(*
Example typechecks :
(@empty ty) |- test ∈ TNat.
Proof.
unfold test.
(* This typing derivation is quite deep, so we need to increase the
max search depth of auto from the default 5 to 10. *)
auto 10.
Qed.
Example numtest_reduces :
test ==>* tnat 5.
Proof.
unfold test. normalize.
Qed.
*)
End Numtest.
Module Prodtest.
(* ((5,6),7).fst.snd *)
Definition test :=
tsnd
(tfst
(tpair
(tpair
(tnat 5)
(tnat 6))
(tnat 7))).
(*
Example typechecks :
(@empty ty) |- test ∈ TNat.
Proof. unfold test. eauto 15. Qed.
Example reduces :
test ==>* tnat 6.
Proof. unfold test. normalize. Qed.
*)
End Prodtest.
Module LetTest.
(* let x = pred 6 in succ x *)
Definition test :=
tlet
x
(tpred (tnat 6))
(tsucc (tvar x)).
(*
Example typechecks :
(@empty ty) |- test ∈ TNat.
Proof. unfold test. eauto 15. Qed.
Example reduces :
test ==>* tnat 6.
Proof. unfold test. normalize. Qed.
*)
End LetTest.
Module Sumtest1.
(* case (inl Nat 5) of
inl x => x
| inr y => y *)
Definition test :=
tcase (tinl TNat (tnat 5))
x (tvar x)
y (tvar y).
(*
Example typechecks :
(@empty ty) |- test ∈ TNat.
Proof. unfold test. eauto 15. Qed.
Example reduces :
test ==>* (tnat 5).
Proof. unfold test. normalize. Qed.
*)
End Sumtest1.
Module Sumtest2.
(* let processSum =
\x:Nat+Nat.
case x of
inl n => n
inr n => if0 n then 1 else 0 in
(processSum (inl Nat 5), processSum (inr Nat 5)) *)
Definition test :=
tlet
processSum
(tabs x (TSum TNat TNat)
(tcase (tvar x)
n (tvar n)
n (tif0 (tvar n) (tnat 1) (tnat 0))))
(tpair
(tapp (tvar processSum) (tinl TNat (tnat 5)))
(tapp (tvar processSum) (tinr TNat (tnat 5)))).
(*
Example typechecks :
(@empty ty) |- test ∈ (TProd TNat TNat).
Proof. unfold test. eauto 15. Qed.
Example reduces :
test ==>* (tpair (tnat 5) (tnat 0)).
Proof. unfold test. normalize. Qed.
*)
End Sumtest2.
Module ListTest.
(* let l = cons 5 (cons 6 (nil Nat)) in
lcase l of
nil => 0
| x::y => x*x *)
Definition test :=
tlet l
(tcons (tnat 5) (tcons (tnat 6) (tnil TNat)))
(tlcase (tvar l)
(tnat 0)
x y (tmult (tvar x) (tvar x))).
(*
Example typechecks :
(@empty ty) |- test ∈ TNat.
Proof. unfold test. eauto 20. Qed.
Example reduces :
test ==>* (tnat 25).
Proof. unfold test. normalize. Qed.
*)
End ListTest.
Module FixTest1.
(* fact := fix
(\f:nat->nat.
\a:nat.
if a=0 then 1 else a * (f (pred a))) *)
Definition fact :=
tfix
(tabs f (TArrow TNat TNat)
(tabs a TNat
(tif0
(tvar a)
(tnat 1)
(tmult
(tvar a)
(tapp (tvar f) (tpred (tvar a))))))).
(Warning: you may be able to typecheck fact but still have some
rules wrong!)
(*
Example fact_typechecks :
(@empty ty) |- fact ∈ (TArrow TNat TNat).
Proof. unfold fact. auto 10.
Qed.
*)
(*
Example fact_example:
(tapp fact (tnat 4)) ==>* (tnat 24).
Proof. unfold fact. normalize. Qed.
*)
End FixTest1.
Module FixTest2.
(* map :=
\g:nat->nat.
fix
(\f:nat->nat.
\l:nat.
case l of
| ->
| x::l -> (g x)::(f l)) *)
Definition map :=
tabs g (TArrow TNat TNat)
(tfix
(tabs f (TArrow (TList TNat) (TList TNat))
(tabs l (TList TNat)
(tlcase (tvar l)
(tnil TNat)
a l (tcons (tapp (tvar g) (tvar a))
(tapp (tvar f) (tvar l))))))).
(*
(* Make sure you've uncommented the last Hint Extern above... *)
Example map_typechecks :
empty |- map ∈
(TArrow (TArrow TNat TNat)
(TArrow (TList TNat)
(TList TNat))).
Proof. unfold map. auto 10. Qed.
Example map_example :
tapp (tapp map (tabs a TNat (tsucc (tvar a))))
(tcons (tnat 1) (tcons (tnat 2) (tnil TNat)))
==>* (tcons (tnat 2) (tcons (tnat 3) (tnil TNat))).
Proof. unfold map. normalize. Qed.
*)
End FixTest2.
Module FixTest3.
(* equal =
fix
(\eq:Nat->Nat->Bool.
\m:Nat. \n:Nat.
if0 m then (if0 n then 1 else 0)
else if0 n then 0
else eq (pred m) (pred n)) *)
Definition equal :=
tfix
(tabs eq (TArrow TNat (TArrow TNat TNat))
(tabs m TNat
(tabs n TNat
(tif0 (tvar m)
(tif0 (tvar n) (tnat 1) (tnat 0))
(tif0 (tvar n)
(tnat 0)
(tapp (tapp (tvar eq)
(tpred (tvar m)))
(tpred (tvar n)))))))).
(*
Example equal_typechecks :
(@empty ty) |- equal ∈ (TArrow TNat (TArrow TNat TNat)).
Proof. unfold equal. auto 10.
Qed.
*)
(*
Example equal_example1:
(tapp (tapp equal (tnat 4)) (tnat 4)) ==>* (tnat 1).
Proof. unfold equal. normalize. Qed.
*)
(*
Example equal_example2:
(tapp (tapp equal (tnat 4)) (tnat 5)) ==>* (tnat 0).
Proof. unfold equal. normalize. Qed.
*)
End FixTest3.
Module FixTest4.
(* let evenodd =
fix
(\eo: (Nat->Nat * Nat->Nat).
let e = \n:Nat. if0 n then 1 else eo.snd (pred n) in
let o = \n:Nat. if0 n then 0 else eo.fst (pred n) in
(e,o)) in
let even = evenodd.fst in
let odd = evenodd.snd in
(even 3, even 4)
*)
Definition eotest :=
tlet evenodd
(tfix
(tabs eo (TProd (TArrow TNat TNat) (TArrow TNat TNat))
(tpair
(tabs n TNat
(tif0 (tvar n)
(tnat 1)
(tapp (tsnd (tvar eo)) (tpred (tvar n)))))
(tabs n TNat
(tif0 (tvar n)
(tnat 0)
(tapp (tfst (tvar eo)) (tpred (tvar n))))))))
(tlet even (tfst (tvar evenodd))
(tlet odd (tsnd (tvar evenodd))
(tpair
(tapp (tvar even) (tnat 3))
(tapp (tvar even) (tnat 4))))).
(*
Example eotest_typechecks :
(@empty ty) |- eotest ∈ (TProd TNat TNat).
Proof. unfold eotest. eauto 30.
Qed.
*)
(*
Example eotest_example1:
eotest ==>* (tpair (tnat 0) (tnat 1)).
Proof. unfold eotest. normalize. Qed.
*)
End FixTest4.
End Examples.
Properties of Typing
Theorem progress : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t ⇒ t'.
Proof with eauto.
(* Theorem: Suppose empty |- t : T. Then either
1. t is a value, or
2. t ==> t' for some t'.
Proof: By induction on the given typing derivation. *)
intros t T Ht.
remember (@empty ty) as Γ.
generalize dependent HeqGamma.
induction Ht; intros HeqGamma; subst.
- (* T_Var *)
(* The final rule in the given typing derivation cannot be T_Var,
since it can never be the case that empty ⊢ x : T (since the
context is empty). *)
inversion H.
- (* T_Abs *)
(* If the T_Abs rule was the last used, then t = tabs x T11 t12,
which is a value. *)
left...
- (* T_App *)
(* If the last rule applied was T_App, then t = t1 t2, and we know
from the form of the rule that
empty ⊢ t1 : T1 → T2
empty ⊢ t2 : T1
By the induction hypothesis, each of t1 and t2 either is a value
or can take a step. *)
right.
destruct IHHt1; subst...
+ (* t1 is a value *)
destruct IHHt2; subst...
× (* t2 is a value *)
(* If both t1 and t2 are values, then we know that
t1 = tabs x T11 t12, since abstractions are the only values
that can have an arrow type. But
(tabs x T11 t12) t2 ⇒ [x:=t2]t12 by ST_AppAbs. *)
inversion H; subst; try (solve by inversion).
∃(subst x t2 t12)...
× (* t2 steps *)
(* If t1 is a value and t2 ⇒ t2', then t1 t2 ⇒ t1 t2'
by ST_App2. *)
inversion H0 as [t2' Hstp]. ∃(tapp t1 t2')...
+ (* t1 steps *)
(* Finally, If t1 ⇒ t1', then t1 t2 ⇒ t1' t2 by ST_App1. *)
inversion H as [t1' Hstp]. ∃(tapp t1' t2)...
- (* T_Nat *)
left...
- (* T_Succ *)
right.
destruct IHHt...
+ (* t1 is a value *)
inversion H; subst; try solve by inversion.
∃(tnat (S n1))...
+ (* t1 steps *)
inversion H as [t1' Hstp].
∃(tsucc t1')...
- (* T_Pred *)
right.
destruct IHHt...
+ (* t1 is a value *)
inversion H; subst; try solve by inversion.
∃(tnat (pred n1))...
+ (* t1 steps *)
inversion H as [t1' Hstp].
∃(tpred t1')...
- (* T_Mult *)
right.
destruct IHHt1...
+ (* t1 is a value *)
destruct IHHt2...
× (* t2 is a value *)
inversion H; subst; try solve by inversion.
inversion H0; subst; try solve by inversion.
∃(tnat (mult n1 n0))...
× (* t2 steps *)
inversion H0 as [t2' Hstp].
∃(tmult t1 t2')...
+ (* t1 steps *)
inversion H as [t1' Hstp].
∃(tmult t1' t2)...
- (* T_If0 *)
right.
destruct IHHt1...
+ (* t1 is a value *)
inversion H; subst; try solve by inversion.
destruct n1 as [|n1'].
× (* n1=0 *)
∃t2...
× (* n1<>0 *)
∃t3...
+ (* t1 steps *)
inversion H as [t1' H0].
∃(tif0 t1' t2 t3)...
- (* T_Pair *)
destruct IHHt1...
+ (* t1 is a value *)
destruct IHHt2...
× (* t2 steps *)
right. inversion H0 as [t2' Hstp].
∃(tpair t1 t2')...
+ (* t1 steps *)
right. inversion H as [t1' Hstp].
∃(tpair t1' t2)...
- (* T_Fst *)
right.
destruct IHHt...
+ (* t1 is a value *)
inversion H; subst; try solve by inversion.
∃v1...
+ (* t1 steps *)
inversion H as [t1' Hstp].
∃(tfst t1')...
- (* T_Snd *)
right.
destruct IHHt...
+ (* t1 is a value *)
inversion H; subst; try solve by inversion.
∃v2...
+ (* t1 steps *)
inversion H as [t1' Hstp].
∃(tsnd t1')...
- (* T_Unit *)
left...
(* let *)
(* FILL IN HERE *)
- (* T_Inl *)
destruct IHHt...
+ (* t1 steps *)
right. inversion H as [t1' Hstp]...
(* exists (tinl _ t1')... *)
- (* T_Inr *)
destruct IHHt...
+ (* t1 steps *)
right. inversion H as [t1' Hstp]...
(* exists (tinr _ t1')... *)
- (* T_Case *)
right.
destruct IHHt1...
+ (* t0 is a value *)
inversion H; subst; try solve by inversion.
× (* t0 is inl *)
∃([x1:=v]t1)...
× (* t0 is inr *)
∃([x2:=v]t2)...
+ (* t0 steps *)
inversion H as [t0' Hstp].
∃(tcase t0' x1 t1 x2 t2)...
- (* T_Nil *)
left...
- (* T_Cons *)
destruct IHHt1...
+ (* head is a value *)
destruct IHHt2...
× (* tail steps *)
right. inversion H0 as [t2' Hstp].
∃(tcons t1 t2')...
+ (* head steps *)
right. inversion H as [t1' Hstp].
∃(tcons t1' t2)...
- (* T_Lcase *)
right.
destruct IHHt1...
+ (* t1 is a value *)
inversion H; subst; try solve by inversion.
× (* t1=tnil *)
∃t2...
× (* t1=tcons v1 vl *)
∃([x2:=vl]([x1:=v1]t3))...
+ (* t1 steps *)
inversion H as [t1' Hstp].
∃(tlcase t1' t2 x1 x2 t3)...
(* fix *)
(* FILL IN HERE *)
Qed.
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (tvar x)
| afi_app1 : ∀x t1 t2,
appears_free_in x t1 → appears_free_in x (tapp t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 → appears_free_in x (tapp t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (tabs y T11 t12)
(* nats *)
| afi_succ : ∀x t,
appears_free_in x t →
appears_free_in x (tsucc t)
| afi_pred : ∀x t,
appears_free_in x t →
appears_free_in x (tpred t)
| afi_mult1 : ∀x t1 t2,
appears_free_in x t1 →
appears_free_in x (tmult t1 t2)
| afi_mult2 : ∀x t1 t2,
appears_free_in x t2 →
appears_free_in x (tmult t1 t2)
| afi_if01 : ∀x t1 t2 t3,
appears_free_in x t1 →
appears_free_in x (tif0 t1 t2 t3)
| afi_if02 : ∀x t1 t2 t3,
appears_free_in x t2 →
appears_free_in x (tif0 t1 t2 t3)
| afi_if03 : ∀x t1 t2 t3,
appears_free_in x t3 →
appears_free_in x (tif0 t1 t2 t3)
(* pairs *)
| afi_pair1 : ∀x t1 t2,
appears_free_in x t1 →
appears_free_in x (tpair t1 t2)
| afi_pair2 : ∀x t1 t2,
appears_free_in x t2 →
appears_free_in x (tpair t1 t2)
| afi_fst : ∀x t,
appears_free_in x t →
appears_free_in x (tfst t)
| afi_snd : ∀x t,
appears_free_in x t →
appears_free_in x (tsnd t)
(* let *)
(* FILL IN HERE *)
(* sums *)
| afi_inl : ∀x t T,
appears_free_in x t →
appears_free_in x (tinl T t)
| afi_inr : ∀x t T,
appears_free_in x t →
appears_free_in x (tinr T t)
| afi_case0 : ∀x t0 x1 t1 x2 t2,
appears_free_in x t0 →
appears_free_in x (tcase t0 x1 t1 x2 t2)
| afi_case1 : ∀x t0 x1 t1 x2 t2,
x1 ≠ x →
appears_free_in x t1 →
appears_free_in x (tcase t0 x1 t1 x2 t2)
| afi_case2 : ∀x t0 x1 t1 x2 t2,
x2 ≠ x →
appears_free_in x t2 →
appears_free_in x (tcase t0 x1 t1 x2 t2)
(* lists *)
| afi_cons1 : ∀x t1 t2,
appears_free_in x t1 →
appears_free_in x (tcons t1 t2)
| afi_cons2 : ∀x t1 t2,
appears_free_in x t2 →
appears_free_in x (tcons t1 t2)
| afi_lcase1 : ∀x t1 t2 y1 y2 t3,
appears_free_in x t1 →
appears_free_in x (tlcase t1 t2 y1 y2 t3)
| afi_lcase2 : ∀x t1 t2 y1 y2 t3,
appears_free_in x t2 →
appears_free_in x (tlcase t1 t2 y1 y2 t3)
| afi_lcase3 : ∀x t1 t2 y1 y2 t3,
y1 ≠ x →
y2 ≠ x →
appears_free_in x t3 →
appears_free_in x (tlcase t1 t2 y1 y2 t3)
(* fix *)
(* FILL IN HERE *)
.
Hint Constructors appears_free_in.
Lemma context_invariance : ∀Γ Γ' t S,
Γ ⊢ t ∈ S →
(∀x, appears_free_in x t → Γ x = Γ' x) →
Γ' ⊢ t ∈ S.
Proof with eauto.
intros. generalize dependent Γ'.
induction H;
intros Γ' Heqv...
- (* T_Var *)
apply T_Var... rewrite ← Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros y Hafi.
unfold update, t_update.
destruct (beq_idP x y)...
- (* T_Mult *)
apply T_Mult...
- (* T_If0 *)
apply T_If0...
- (* T_Pair *)
apply T_Pair...
(* let *)
(* FILL IN HERE *)
- (* T_Case *)
eapply T_Case...
+ apply IHhas_type2. intros y Hafi.
unfold update, t_update.
destruct (beq_idP x1 y)...
+ apply IHhas_type3. intros y Hafi.
unfold update, t_update.
destruct (beq_idP x2 y)...
- (* T_Cons *)
apply T_Cons...
- (* T_Lcase *)
eapply T_Lcase... apply IHhas_type3. intros y Hafi.
unfold update, t_update.
destruct (beq_idP x1 y)...
destruct (beq_idP x2 y)...
Qed.
Lemma free_in_context : ∀x t T Γ,
appears_free_in x t →
Γ ⊢ t ∈ T →
∃T', Γ x = Some T'.
Proof with eauto.
intros x t T Γ Hafi Htyp.
induction Htyp; inversion Hafi; subst...
- (* T_Abs *)
destruct IHHtyp as [T' Hctx]... ∃T'.
unfold update, t_update in Hctx.
rewrite false_beq_id in Hctx...
(* let *)
(* FILL IN HERE *)
(* T_Case *)
- (* left *)
destruct IHHtyp2 as [T' Hctx]... ∃T'.
unfold update, t_update in Hctx. rewrite false_beq_id in Hctx...
- (* right *)
destruct IHHtyp3 as [T' Hctx]... ∃T'.
unfold update, t_update in Hctx. rewrite false_beq_id in Hctx...
- (* T_Lcase *)
clear Htyp1 IHHtyp1 Htyp2 IHHtyp2.
destruct IHHtyp3 as [T' Hctx]... ∃T'.
unfold update, t_update in Hctx.
rewrite false_beq_id in Hctx...
rewrite false_beq_id in Hctx...
Qed.
Lemma substitution_preserves_typing : ∀Γ x U v t S,
(update Γ x U) ⊢ t ∈ S →
empty ⊢ v ∈ U →
Γ ⊢ ([x:=v]t) ∈ S.
Proof with eauto.
(* Theorem: If Gamma,x:U |- t : S and empty |- v : U, then
Gamma |- x:=vt : S. *)
intros Γ x U v t S Htypt Htypv.
generalize dependent Γ. generalize dependent S.
(* Proof: By induction on the term t. Most cases follow directly
from the IH, with the exception of tvar and tabs.
The former aren't automatic because we must reason about how the
variables interact. *)
induction t;
intros S Γ Htypt; simpl; inversion Htypt; subst...
- (* tvar *)
simpl. rename i into y.
(* If t = y, we know that
empty ⊢ v : U and
Γ,x:U ⊢ y : S
and, by inversion, update Γ x U y = Some S. We want to
show that Γ ⊢ [x:=v]y : S.
There are two cases to consider: either x=y or x≠y. *)
unfold update, t_update in H1.
destruct (beq_idP x y).
+ (* x=y *)
(* If x = y, then we know that U = S, and that [x:=v]y = v.
So what we really must show is that if empty ⊢ v : U then
Γ ⊢ v : U. We have already proven a more general version
of this theorem, called context invariance. *)
subst.
inversion H1; subst. clear H1.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
inversion HT'.
+ (* x<>y *)
(* If x ≠ y, then Γ y = Some S and the substitution has no
effect. We can show that Γ ⊢ y : S by T_Var. *)
apply T_Var...
- (* tabs *)
rename i into y. rename t into T11.
(* If t = tabs y T11 t0, then we know that
Γ,x:U ⊢ tabs y T11 t0 : T11→T12
Γ,x:U,y:T11 ⊢ t0 : T12
empty ⊢ v : U
As our IH, we know that forall S Gamma,
Γ,x:U ⊢ t0 : S → Γ ⊢ [x:=v]t0 : S.
We can calculate that
x:=vt = tabs y T11 (if beq_id x y then t0 else x:=vt0)
And we must show that Γ ⊢ [x:=v]t : T11→T12. We know
we will do so using T_Abs, so it remains to be shown that:
Γ,y:T11 ⊢ if beq_id x y then t0 else [x:=v]t0 : T12
We consider two cases: x = y and x ≠ y.
*)
apply T_Abs...
destruct (beq_idP x y) as [Hxy|Hxy].
+ (* x=y *)
(* If x = y, then the substitution has no effect. Context
invariance shows that Γ,y:U,y:T11 and Γ,y:T11 are
equivalent. Since the former context shows that t0 : T12, so
does the latter. *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_id y x)...
+ (* x<>y *)
(* If x ≠ y, then the IH and context invariance allow us to show that
Γ,x:U,y:T11 ⊢ t0 : T12 =>
Γ,y:T11,x:U ⊢ t0 : T12 =>
Γ,y:T11 ⊢ [x:=v]t0 : T12 *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP y z) as [Hyz|Hyz]...
subst.
rewrite false_beq_id...
(* let *)
(* FILL IN HERE *)
- (* tcase *)
rename i into x1. rename i0 into x2.
eapply T_Case...
+ (* left arm *)
destruct (beq_idP x x1) as [Hxx1|Hxx1].
× (* x = x1 *)
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (beq_id x1 z)...
× (* x <> x1 *)
apply IHt2. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP x1 z) as [Hx1z|Hx1z]...
subst. rewrite false_beq_id...
+ (* right arm *)
destruct (beq_idP x x2) as [Hxx2|Hxx2].
× (* x = x2 *)
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (beq_id x2 z)...
× (* x <> x2 *)
apply IHt3. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP x2 z)...
subst. rewrite false_beq_id...
- (* tlcase *)
rename i into y1. rename i0 into y2.
eapply T_Lcase...
destruct (beq_idP x y1).
+ (* x=y1 *)
simpl.
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (beq_idP y1 z)...
+ (* x<>y1 *)
destruct (beq_idP x y2).
× (* x=y2 *)
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (beq_idP y2 z)...
× (* x<>y2 *)
apply IHt3. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP y1 z)...
subst. rewrite false_beq_id...
destruct (beq_idP y2 z)...
subst. rewrite false_beq_id...
Qed.
Theorem preservation : ∀t t' T,
empty ⊢ t ∈ T →
t ⇒ t' →
empty ⊢ t' ∈ T.
Proof with eauto.
intros t t' T HT.
(* Theorem: If empty ⊢ t : T and t ⇒ t', then empty ⊢ t' : T. *)
remember (@empty ty) as Γ. generalize dependent HeqGamma.
generalize dependent t'.
(* Proof: By induction on the given typing derivation. Many cases are
contradictory (T_Var, T_Abs). We show just the interesting ones. *)
induction HT;
intros t' HeqGamma HE; subst; inversion HE; subst...
- (* T_App *)
(* If the last rule used was T_App, then t = t1 t2, and three rules
could have been used to show t ⇒ t': ST_App1, ST_App2, and
ST_AppAbs. In the first two cases, the result follows directly from
the IH. *)
inversion HE; subst...
+ (* ST_AppAbs *)
(* For the third case, suppose
t1 = tabs x T11 t12
and
t2 = v2.
We must show that empty ⊢ [x:=v2]t12 : T2.
We know by assumption that
empty ⊢ tabs x T11 t12 : T1→T2
and by inversion
x:T1 ⊢ t12 : T2
We have already proven that substitution_preserves_typing and
empty ⊢ v2 : T1
by assumption, so we are done. *)
apply substitution_preserves_typing with T1...
inversion HT1...
- (* T_Fst *)
inversion HT...
- (* T_Snd *)
inversion HT...
(* let *)
(* FILL IN HERE *)
(* T_Case *)
- (* ST_CaseInl *)
inversion HT1; subst.
eapply substitution_preserves_typing...
- (* ST_CaseInr *)
inversion HT1; subst.
eapply substitution_preserves_typing...
- (* T_Lcase *)
+ (* ST_LcaseCons *)
inversion HT1; subst.
apply substitution_preserves_typing with (TList T1)...
apply substitution_preserves_typing with T1...
(* fix *)
(* FILL IN HERE *)
Qed.
☐