Set Implicit Arguments.
Require Import List Metatheory ML_Definitions ML_Infrastructure.
Lemma factorize_map : forall Z U xs Us,
iter_push xs (List.map (Sch 0) (List.map (typ_subst Z U) Us))
= (map (sch_subst Z U) (iter_push xs (List.map (Sch 0) Us))).
Proof.
induction xs; simpl; intros.
auto. destruct Us. auto. simpl.
do 2 rewrite iter_push_cons.
rewrite map_concat. f_equal*.
Qed.
Definition has_scheme_vars L E P t M := forall Xs,
fresh L (sch_arity M) Xs ->
E ! P |= t ~: (M ^ Xs).
Definition has_scheme E P t M := forall Vs,
types (sch_arity M) Vs ->
E ! P |= t ~: (M ^^ Vs).
Lemma pat_typing_typ_subst : forall Z U Us p T,
Us \= p ~: T ->
List.map (typ_subst Z U) Us \= p ~: typ_subst Z U T.
Proof.
induction 1; simpl*. rewrite* map_app.
Qed.
Lemma typing_typ_subst : forall F P Z U E t T,
Z \notin (env_fv E) -> Z \notin (phi_fv P) ->
type U ->
E & F ! P |= t ~: T ->
E & (map (sch_subst Z U) F) ! P |= t ~: (typ_subst Z U T).
Proof.
introv. intros Fr1 Fr2 WVs Typ. gen_eq (E & F) as G. gen F.
induction Typ; intros F EQ; subst; simpls typ_subst.
rewrite~ sch_subst_open. apply* typing_var.
binds_cases H1.
apply* binds_concat_fresh.
rewrite* sch_subst_fresh. use (fv_in_spec sch_fv B).
auto*.
rewrite~ sch_subst_arity. apply* typ_subst_type_list.
apply_fresh* typing_abs. intros y Fr.
rewrite sch_subst_fold.
apply_ih_map_bind* H1.
apply_fresh* typing_fix. intros f y Fr.
replace (E & (map (sch_subst Z U) F) &
f ~ Sch 0 (typ_arrow (typ_subst Z U U0) (typ_subst Z U T)) &
y ~ Sch 0 (typ_subst Z U U0))
with (E & map (sch_subst Z U) (F &
f ~ Sch 0 (typ_arrow U0 T) &
y ~ (Sch 0 U0))); [|auto].
apply* H1.
apply_fresh* (@typing_let (sch_subst Z U M) (L1 \u {{Z}})).
simpl. intros Ys Fr. rewrite* <- sch_subst_open_vars.
intros y Fr. apply_ih_map_bind* H4.
apply_fresh* (@typing_match (typ_subst Z U T)
(List.map (typ_subst Z U) Us)).
apply* pat_typing_typ_subst.
intros xs Fr.
rewrite factorize_map. rewrite concat_assoc.
rewrite <- map_concat. apply* H1. rewrite* <- concat_assoc.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
apply* typing_loc.
rewrite* typ_subst_fresh.
use (fv_in_spec typ_fv H1).
auto*.
auto*.
apply* typing_set.
apply* typing_raise.
rewrite* <- (@typ_subst_fresh Z U typ_exn).
apply* typing_catch.
rewrite* <- (@typ_subst_fresh Z U typ_exn).
Qed.
Lemma typing_typ_substs : forall Zs Us E P t T,
fresh (env_fv E \u phi_fv P) (length Zs) Zs ->
types (length Zs) Us ->
E ! P |= t ~: T ->
E ! P |= t ~: (typ_substs Zs Us T).
Proof.
induction Zs; destruct Us; simpl; introv Fr WU Tt;
destruct Fr; inversions WU;
simpls; try solve [ auto | contradictions* ].
inversions H2. inversions H1. clear H2 H1.
apply* IHZs. apply_empty* typing_typ_subst.
Qed.
Lemma has_scheme_from_vars : forall L E P t M,
has_scheme_vars L E P t M ->
has_scheme E P t M.
Proof.
intros L E P t [n T] H Vs TV. unfold sch_open. simpls.
pick_freshes n Xs.
rewrite (fresh_length _ _ _ Fr) in TV, H.
rewrite~ (@typ_substs_intro Xs Vs T).
unfolds has_scheme_vars sch_open_vars. simpls.
apply* typing_typ_substs.
Qed.
Lemma has_scheme_from_typ : forall E P t T,
E ! P |= t ~: T ->
has_scheme E P t (Sch 0 T).
Proof.
introz. unfold sch_open. simpls.
rewrite* <- typ_open_type.
Qed.
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; intros G EQ Ok; subst.
apply* typing_var. apply* binds_weaken.
apply_fresh* typing_abs. intros y Fr.
do_rew* concat_assoc (apply* H1).
apply_fresh* typing_fix. intros f y Fr2.
do_rew_2* concat_assoc (apply* H1).
apply_fresh* (@typing_let M L1). intros y Fr.
do_rew* concat_assoc (apply* H4).
apply_fresh* (@typing_match T Us). intros xs Fr.
do_rew* concat_assoc (apply* H1).
apply* (@ok_iter_push sch (pat_arity p)). simpl_env. auto.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
Qed.
Lemma value_fv : forall z u t,
value u -> value t -> value ([z ~> u]t).
Proof.
introv Valu Valt. induction Valt; simpl*.
Qed.
Lemma typing_trm_subst : forall F M E P t T z u,
E & z ~ M & F ! P |= t ~: T ->
has_scheme E P u M ->
value u ->
E & F ! P |= (trm_subst z u t) ~: T.
Proof.
introv Typt. intros Typu Valu.
gen_eq (E & z ~ M & F) as G. gen F.
induction Typt; intros G EQ; subst; simpl trm_subst.
case_var.
binds_get H1. apply_empty* typing_weaken.
binds_cases H1; apply* typing_var.
apply_fresh* typing_abs. intros y Fr.
rewrite* subst_open_vars.
do_rew concat_assoc (apply* H1).
apply_fresh* typing_fix. intros f y Fr.
rewrite* subst_open_vars.
do_rew_2 concat_assoc (apply* H1).
apply_fresh* (@typing_let M0 L1); try intros y Fr.
apply* value_fv.
rewrite* subst_open_vars. do_rew concat_assoc (apply* H4).
apply_fresh* (@typing_match T Us). intros xs Fr.
rewrite* subst_open_vars.
do_rew* concat_assoc (apply* H1).
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
auto*.
Qed.
Lemma typing_trm_substs : forall Us E P xs ts t T,
length xs = length ts ->
typings E P ts Us ->
(E & (iter_push xs (List.map (Sch 0) Us))) ! P |= t ~: T ->
list_forall value ts ->
E ! P |= substs xs ts t ~: T.
Proof.
intros Us E P xs. gen Us E.
induction xs; simpl; introv Le Typts Typt Val. auto.
destruct ts; simpls; inversions Le.
inversions Typts. inversions Val.
simpl in Typt.
rewrite iter_push_cons in Typt.
rewrite <- concat_assoc in Typt.
apply* (@IHxs Us0).
apply* typing_trm_subst.
apply* has_scheme_from_typ.
Qed.
Lemma typing_pattern_match : forall p t T E P ts Us,
Some ts = pat_match p t ->
E ! P |= t ~: T ->
Us \= p ~: T ->
typings E P ts Us.
Proof.
induction p; introv H1 H2 H0; destruct t;
inversion H0; inversion H1; auto; subst; inversions H2; auto*.
remember (pat_match p1 t1) as K1.
remember (pat_match p2 t2) as K2.
destruct K1 as [ts1|]; destruct K2 as [ts2|]; try discriminate.
inversions H9. apply* typings_concat.
Qed.
Lemma pattern_match_values : forall p t ts,
Some ts = pat_match p t ->
value t ->
list_forall value ts.
Proof.
induction p; introv EQ Val;
destruct t; simpl in EQ; inversion EQ; auto; inversions Val; auto*.
remember (pat_match p1 t1) as K1.
remember (pat_match p2 t2) as K2.
destruct K1 as [ts1|]; destruct K2 as [ts2|]; try discriminate.
inversions EQ. apply* list_forall_concat.
Qed.
Lemma typing_stability : forall P E P' t T,
E ! P |= t ~: T ->
extends P P' ->
phi_ok 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 [PhiOk [StoOk [Dom Ext]]]. split4.
auto.
auto.
intros l0 Fr. simpls. puts (Dom l0).
asserts* Frl0 (l0 # P). auto.
intros l' T' Has. binds_cases Has.
destruct (Ext _ _ B) as [t' [Hast' Typt']].
exists* t'.
subst. exists* t.
Qed.
Lemma fails_to_exception : forall E P t T e,
fails t e ->
E ! P |= t ~: T ->
E ! P |= e ~: typ_exn.
Proof.
introv Fail Typ. induction Typ; inversions* Fail.
pick_freshes (sch_arity M) Xs. forward~ (H2 Xs).
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. split3~.
pick_fresh x. forward~ (H3 x) as K. clear H2 H3 H4.
rewrite~ (@substs_intro (x::nil)). simpl.
apply_empty* typing_trm_subst.
apply* (@has_scheme_from_vars L1).
exists P. split3~. clear H1 IHTyp1 IHTyp2.
forward~ (@pat_match_terms _ _ _ H13) as Wts.
pick_freshes (pat_arity p) xs.
rewrite~ (@substs_intro xs);
[| rewrite~ <- (fresh_length _ _ _ Fr)].
forward~ (H0 xs) as K.
rewrite (proj1 Wts) in Fr, Wts.
apply_empty* (@typing_trm_substs Us).
rewrite* (fresh_length _ _ _ Fr).
apply* typing_pattern_match.
apply* pattern_match_values.
exists P. split3~.
pres IHTyp1 t1' mu'. exists* P'.
exists P. split3~.
inversions Typ1.
pick_fresh x. forward~ (H8 x) as K. clear H8 IHTyp1 IHTyp2.
rewrite~ (@substs_intro (x::nil)). simpl.
apply_empty* typing_trm_subst.
apply* has_scheme_from_typ.
exists P. split3~.
inversions Typ1.
pick_fresh f. pick_fresh x. forward~ (H8 f x) as K. clear H8.
rewrite~ (@substs_intro (f::x::nil)).
apply_empty* (@typing_trm_substs ((typ_arrow S T)::S::nil)).
exists P. split3~. inversions Typ1. inversions* H4.
pres IHTyp1 t1' mu'. exists* P'.
pres IHTyp2 t2' mu'. exists* P'.
pres IHTyp1 t1' mu'. exists* P'.
pres IHTyp2 t2' mu'. exists* P'.
pres IHTyp t1' mu'. exists* P'.
pres IHTyp t1' mu'. exists* P'.
exists (P & l ~ T). puts (proj43 TypSto).
split3~. apply* sto_typing_push.
pres IHTyp t1' mu'. exists* P'.
exists P. split3~.
inversions Typ.
destruct~ ((proj44 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 [PhiOk [StoOk [Dom Map]]]. split4~.
intros. unfold binds. simpl. case_var.
exists t2. split~. rewrite~ (binds_inj H H7).
destruct (Map _ _ H) as [t [Has Typ]]. exists* t.
pres IHTyp1 t1' mu'. exists* P'.
pres IHTyp2 t2' mu'. exists* P'.
pres IHTyp t1' mu'. exists* P'.
exists* P.
exists P. split3~.
apply* typing_app. apply* fails_to_exception.
pres IHTyp2 t2' mu'. exists* P'.
Qed.
Lemma red_value_false : forall t, value t ->
forall t' mu mu', (t, mu) --> (t', mu') -> False.
Proof.
induction 1; introv Red; inversions* Red.
inversions H5. inversions H5.
Qed.
Hint Constructors fails.
Lemma progress_result : progress.
Proof.
introv Typ. gen_eq (empty:env) as E. poses Typ' Typ.
induction Typ; intros; subst.
contradictions.
or_31*.
or_31*.
asserts* K (empty ! P |= (trm_let t1 t2) ~: T2).
pick_freshes (sch_arity M) Ys.
forward~ (@H2 Ys) as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
or_33. exists* (t2 ^^ (t1::nil)) mu.
or_32. exists* e.
contradictions. apply* (red_value_false H Red1).
destruct~ IHTyp1 as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
or_33. remember (pat_match p t1) as K. destruct K as [ts|].
exists* (b ^^ ts) mu.
exists* t2 mu.
or_32. exists* e.
or_33. exists* (trm_match t1' p b t2) mu'.
destruct~ IHTyp1 as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
destruct~ IHTyp2 as [Val2 | [[e Fail] | [t2' [mu' Red2]]]].
inversions Typ1; inversion Val1.
or_33. exists* (t0 ^^ (t2::nil)) mu.
or_33. exists* (t0 ^^ ((trm_fix t0)::t2::nil)) mu.
or_33. subst. inversions H. inversions Val2; inversions Typ2.
exists* (trm_nat (n + n0)) mu.
inversions H6.
or_31. inversions Val2; inversions Typ2.
auto*.
inversions H4.
or_32. exists* e.
or_33. exists* (trm_app t1 t2') mu'.
or_32. exists* e.
or_33. exists* (trm_app t1' t2) mu'.
or_31*.
or_31*.
or_31*.
destruct~ IHTyp1 as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
destruct~ IHTyp2 as [Val2 | [[e Fail] | [t2' [mu' Red2]]]].
or_32. exists* e.
or_33. exists* (trm_pair t1 t2').
or_32. exists* e.
or_33. exists* (trm_pair t1' t2).
destruct~ IHTyp as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
or_32. exists* e.
or_33. exists* (trm_inj1 t1') mu'.
destruct~ IHTyp as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
or_32. exists* e.
or_33. exists* (trm_inj2 t1') mu'.
or_31*.
destruct~ IHTyp as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
destruct (var_fresh (dom mu)) as [l Fr].
or_33. exists* (trm_loc l) (mu & l ~ t1).
or_32. exists* e.
or_33. exists* (trm_ref t1') mu'.
destruct~ IHTyp as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
inversions Val1; inversions Typ.
inversion H4.
destruct ((proj44 H0) _ _ H6) as [t' [Has' Typt']].
or_33. exists* t' mu.
or_32. exists* e.
or_33. exists* (trm_get t1') mu'.
destruct~ IHTyp1 as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
destruct~ IHTyp2 as [Val2 | [[e Fail] | [t2' [mu' Red2]]]].
inversions Val1; inversions Typ1.
inversion H4.
destruct ((proj44 H0) _ _ H6) as [t' [Has' Typt']].
or_33. exists* trm_unit (mu & l ~ t2).
or_32. exists* e.
or_33. exists* (trm_set t1 t2') mu'.
or_32. exists* e.
or_33. exists* (trm_set t1' t2) mu'.
destruct~ IHTyp as [Val1 | [[e Fail] | [t1' [mu' Red1]]]].
or_32. exists* t1.
or_32. exists* e.
or_33. exists* (trm_raise t1') mu'.
destruct~ IHTyp2 as [Val2 | [[e Fail] | [t2' [mu' Red2]]]].
or_33. exists* t2 mu.
or_33. exists* (trm_app t1 e) mu.
or_33. exists* (trm_catch t1 t2') mu'.
Qed.