Set Implicit Arguments.
Require Import Metatheory STLC_Ref_Definitions STLC_Ref_Infrastructure.
Hint Constructors typing.
Lemma typing_weaken : forall G E F P t T,
(E & G) ! P |= t ~: T ->
ok (E & F & G) ->
(E & F & G) ! P |= t ~: T.
Proof.
introv Typ. gen_eq (E & G) as H. gen G.
induction Typ; introv EQ Ok; subst.
apply* typing_var. apply* binds_weaken.
apply_fresh* typing_abs as y. apply_ih_bind* H0.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
Qed.
Lemma typing_subst : forall F E P t T z u U,
(E & z ~ U & F) ! P |= t ~: T ->
E ! P |= u ~: U ->
(E & F) ! P |= [z ~> u]t ~: T.
Proof.
introv Typt Typu. gen_eq (E & z ~ U & F) as G. gen F.
induction Typt; introv Equ; subst; simpl subst.
case_var.
binds_get H0. apply_empty* typing_weaken.
binds_cases H0; apply* typing_var.
apply_fresh typing_abs as y.
rewrite* subst_open_var. apply_ih_bind* H0.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
Qed.
Lemma typing_stability : forall P E P' t T,
E ! P |= t ~: T ->
extends P P' ->
E ! P' |= t ~: T.
Proof.
introv Typ Ext. induction* Typ.
Qed.
Hint Resolve typing_stability.
Lemma sto_typing_push : forall P mu l t T,
P |== mu ->
empty ! P |= t ~: T ->
l # mu -> l # P ->
(P & l ~ T) |== (mu & l ~ t).
Proof.
unfold sto_typing. introv [StoOk [Dom Ext]]. split3.
auto.
intros l0 Fr. simpls. puts (Dom l0).
asserts* Fr2 (l <> l0). asserts* Fr3 (l0 # P). auto.
intros l' T' Has. binds_cases Has.
destruct (Ext _ _ B) as [t' [Hast' Typt']].
exists* t'.
subst. exists* t.
Qed.
Ltac pres H t' mu' :=
let P' := fresh "P'" in
let Ext := fresh "Ext" in
let Typt' := fresh "Typt'" in
let TypSto' := fresh "TypSto'" in
destruct~ (H (@refl_equal env empty) t' mu')
as [P' [Ext [Typt' TypSto']]].
Lemma preservation_result : preservation.
Proof.
introv Typ. gen t' mu'. gen_eq (empty : env) as E.
induction Typ; intros EQ t' mu' Red TypSto; subst;
inversions Red; env_fix.
exists P. inversions Typ1. split3~.
pick_fresh x. rewrite* (@subst_intro x).
apply_empty* typing_subst.
pres IHTyp1 t1' mu'. exists* P'.
pres IHTyp2 t2' mu'. exists* P'.
exists (P & l ~ T).
asserts Fr (l # P). use (proj32 TypSto).
split3~. apply* sto_typing_push.
pres IHTyp t1' mu'. exists* P'.
exists P. split3~.
inversions Typ.
destruct~ ((proj33 TypSto) l T) as [t [Hast Typt]].
rewrite~ (binds_inj H4 Hast).
pres IHTyp t1' mu'. exists* P'.
exists P. inversions Typ1. split3~.
destruct TypSto as [StoOk [Dom Map]]. split3~.
intros. unfold binds. simpl. case_var.
exists t2. split~. rewrite~ (binds_inj H H6).
destruct (Map _ _ H) as [t [Has Typ]]. exists* t.
pres IHTyp1 t1' mu'. exists* P'.
pres IHTyp2 t2' mu'. exists* P'.
Qed.
Lemma progress_result : progress.
Proof.
introv Typ. gen_eq (empty : env) as E. poses Typ' Typ.
induction Typ; intros; subst.
contradictions.
left*.
right. destruct~ IHTyp1 as [Val1 | [t1' [mu' Red1]]].
destruct~ IHTyp2 as [Val2 | [t2' [mu' Red2]]].
inversions Typ1; inversions Val1. exists* (t0 ^^ t2) mu.
exists* (trm_app t1 t2') mu'.
exists* (trm_app t1' t2).
left*.
left*.
right. destruct~ IHTyp as [Val1 | [t1' [mu' Red1]]].
destruct (var_fresh (dom mu)) as [l Fr].
exists* (trm_loc l) (mu & l ~ t1).
exists* (trm_ref t1') mu'.
right. destruct~ IHTyp as [Val1 | [t1' [mu' Red1]]].
inversions Val1; inversions Typ.
destruct ((proj33 H0) _ _ H5) as [t' [Has' Typt']].
exists* t' mu.
exists* (trm_get t1') mu'.
right. destruct~ IHTyp1 as [Val1 | [t1' [mu' Red1]]].
destruct~ IHTyp2 as [Val2 | [t2' [mu' Red2]]].
inversions Val1; inversions Typ1.
destruct ((proj33 H0) _ _ H5) as [t' [Has' Typt']].
exists* trm_unit (mu & l ~ t2).
exists* (trm_set t1 t2') mu'.
exists* (trm_set t1' t2) mu'.
Qed.