Set Implicit Arguments.
Require Import Metatheory
STLC_Exn_Definitions
STLC_Exn_Infrastructure.
Lemma typing_weaken : forall G E F t T,
(E & G) |= t ~: T ->
ok (E & F & G) ->
(E & F & G) |= 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.
apply* typing_app.
apply* typing_raise.
apply* typing_catch.
Qed.
Lemma typing_subst : forall F E t T z u U,
(E & z ~ U & F) |= t ~: T ->
E |= u ~: U ->
(E & F) |= [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.
apply* typing_app.
apply* typing_raise.
apply* typing_catch.
Qed.
Lemma fails_to_exception : forall E t T e,
fails t e ->
E |= t ~: T ->
E |= e ~: typ_exn.
Proof.
introv Fail Typ. induction Typ; inversions* Fail.
Qed.
Lemma preservation_result : preservation.
Proof.
introv Typ. gen t'.
induction Typ; introv Red; inversions Red.
inversions Typ1. pick_fresh x. rewrite* (@subst_intro x).
apply_empty* typing_subst.
apply* typing_app.
apply* typing_app.
apply* typing_raise.
apply* typing_catch.
assumption.
apply* typing_app. apply* fails_to_exception.
Qed.
Lemma progress_result : progress.
Proof.
introv Typ. gen_eq (empty : env) as E. poses Typ' Typ.
induction Typ; intros; subst.
contradictions.
or_31*.
right. destruct~ IHTyp1 as [Val1 | [[e Fail] | [t1' Red1]]].
destruct~ IHTyp2 as [Val2 | [[e Fail2] | [t2' Red2]]].
right. inversions Typ1; inversions Val1. exists* (t0 ^^ t2).
left. exists* e.
right. exists* (trm_app t1 t2').
left. exists* e.
right. exists* (trm_app t1' t2).
right. destruct~ IHTyp as [Val1 | [[e Fail] | [t1' Red1]]].
left. exists* t1.
left. exists* e.
right. exists* (trm_raise t1').
or_33. destruct~ IHTyp2 as [Val2 | [[e Fail] | [t2' Red2]]].
exists* t2.
exists* (trm_app t1 e).
exists* (trm_catch t1 t2').
Qed.
|