Desugaring
Require Export Coq.Program.Equality.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Require Export Blame Safety.
Fixpoint typ_of_ityp C :=
match C with
| ityp_base ⇒ typ_null dtyp_base
| ityp_arrow A B ⇒ typ_null (dtyp_arrow (typ_of_ityp A) (typ_of_ityp B))
end.
Definition elvis L M := (t_case L M (t_var_b 0)).
Definition elvis_blame L p := elvis L (t_blame (label_name p)).
Definition blame_label_op := 0.
Definition blame_label_deref := 1.
Definition blame_label_ei := 2.
Definition blame_label_ie := 3.
Fixpoint trm_of_itrm N :=
match N with
| itrm_var_b n ⇒ t_var_b n
| itrm_var_f x ⇒ t_var_f x
| itrm_const c ⇒ t_lift (t_const c)
| itrm_binop M N ⇒ t_lift (t_binop
(elvis_blame (trm_of_itrm M) blame_label_op)
(elvis_blame (trm_of_itrm N) blame_label_op))
| itrm_abs A N ⇒ t_lift (t_abs (typ_of_ityp A) (trm_of_itrm N))
| itrm_app L M ⇒ t_app
(elvis_blame (trm_of_itrm L) blame_label_deref)
(trm_of_itrm M)
| itrm_null ⇒ t_null
end.
Definition ictx := list ( atom × ityp ).
Definition ctx_of_ictx (G:ictx) : ctx := map typ_of_ityp G.
Lemma ctx_of_ictx_binds_ityp:
∀ (G:ictx) x (A:ityp),
binds x A G →
binds x (typ_of_ityp A) (ctx_of_ictx G).
Proof.
intros.
eapply binds_map_2; eauto.
Qed.
Lemma uniq_ctx:
∀ G,
uniq G →
uniq (ctx_of_ictx G).
Proof.
intros.
eapply uniq_map_2; eauto.
Qed.
Lemma open_trm_of_itrm :
∀ N M k,
trm_of_itrm (open_itrm_wrt_itrm_rec k M N) =
open_trm_wrt_trm_rec k (trm_of_itrm M) (trm_of_itrm N).
Proof.
intros.
dependent induction N; default_simp.
- unfold elvis_blame, elvis. f_equal. eauto.
- unfold elvis_blame, elvis. f_equal. eauto.
- unfold elvis_blame, elvis. f_equal. eauto.
Qed.
Hint Resolve ctx_of_ictx_binds_ityp uniq_ctx : core.
Lemma open_trm_of_itrm_rec_var :
∀ N x k,
trm_of_itrm (open_itrm_wrt_itrm_rec k (itrm_var_f x) N) =
open_trm_wrt_trm_rec k (t_var_f x) (trm_of_itrm N).
Proof.
intros.
assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
eapply open_trm_of_itrm.
Qed.
Lemma open_trm_of_itrm_var:
∀ N x,
trm_of_itrm (open_itrm_wrt_itrm N (itrm_var_f x)) =
open_trm_wrt_trm (trm_of_itrm N) (t_var_f x).
Proof.
intros. eapply open_trm_of_itrm_rec_var.
Qed.
Lemma desugaring_typing:
∀ iG iN iA,
ityping iG iN iA →
typing (ctx_of_ictx iG) (trm_of_itrm iN) (typ_of_ityp iA).
Proof.
intros.
induction H; intros; pose (ctx_of_ictx iG) as G'; default_simp; eauto.
- constructor.
constructor;
unfold elvis_blame, elvis;
pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
- constructor.
pick fresh x and apply typing_abs; eauto.
rewrite <- open_trm_of_itrm_var.
eapply H0; eauto.
- eapply typing_app; eauto.
unfold elvis_blame, elvis.
pick fresh x and apply typing_case; eauto.
constructor;
try eapply uniq_cons_3; eauto.
- induction iA; default_simp; eauto.
Qed.
Lemma blame_eq_dec:
∀ (p q:label),
p = q ∨ p ≠ q.
Proof.
intros.
destruct p; destruct q;
destruct (eq_nat_dec bl bl0); eauto; right;
inversion 1; auto.
Qed.
Lemma close_pres_safe:
∀ N x k p,
safe (open_trm_wrt_trm_rec k (t_var_f x) N) p →
safe N p.
Proof.
intros.
dependent induction N; eauto; inversion H; subst; eauto.
Qed.
Hint Resolve close_pres_safe : core.
Fixpoint typ_of_ityp_naive A :=
match A with
| ityp_base ⇒ typ_def dtyp_base
| ityp_arrow B C ⇒ typ_def (dtyp_arrow (typ_of_ityp_naive B) (typ_of_ityp_naive C))
end.
Lemma imp_naive_subtyp A :
subtyp_n (typ_of_ityp_naive A) (typ_of_ityp A).
Proof.
induction A; simpl; eauto.
Qed.
Fixpoint ityp_of_typ A : ityp :=
match A with
| typ_null dtyp_base ⇒ ityp_base
| typ_null (dtyp_arrow A B) ⇒ ityp_arrow (ityp_of_typ A) (ityp_of_typ B)
| typ_def dtyp_base ⇒ ityp_base
| typ_def (dtyp_arrow A B) ⇒ ityp_arrow (ityp_of_typ A) (ityp_of_typ B)
end.
Lemma exp_naive_subtyp :
(∀ A, subtyp_n A (typ_of_ityp (ityp_of_typ A))) ∧
(∀ D, subtyp_n (typ_def D) (typ_of_ityp (ityp_of_typ (typ_def D))) ∧
subtyp_n (typ_null D) (typ_of_ityp (ityp_of_typ (typ_null D))))
.
Proof.
apply_mutual_ind typ_dtyp_mutind; default_simp.
Qed.
Lemma compat_naive_subtyp A B :
subtyp_n A B → compat A B.
Proof.
induction 1; eauto.
Qed.
Lemma compat_typ_ityp A:
compat A (typ_of_ityp (ityp_of_typ A)).
Proof.
apply compat_naive_subtyp. apply exp_naive_subtyp.
Qed.
Definition ctrm_elvis_blame CL p := (ctrm_case_scrutinee CL (t_blame (label_name p)) (t_var_b 0)).
Fixpoint ctrm_of_ictrm iC :=
match iC with
| ictrm_hole ⇒ ctrm_hole
| ictrm_binop_left iC N ⇒ ctrm_lift (ctrm_binop_left
(ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_op)
(elvis_blame (trm_of_itrm N) blame_label_op))
| ictrm_binop_right N iC ⇒ ctrm_lift (ctrm_binop_right
(elvis_blame (trm_of_itrm N) blame_label_op)
(ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_op))
| ictrm_abs A iC ⇒ ctrm_lift (ctrm_abs (typ_of_ityp A) (ctrm_of_ictrm iC))
| ictrm_app_left iC N ⇒ ctrm_app_left
(ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_deref)
(trm_of_itrm N)
| ictrm_app_right N iC ⇒ ctrm_app_right
(elvis_blame (trm_of_itrm N) blame_label_deref)
(ctrm_of_ictrm iC)
end.
Lemma open_ctrm_of_ictrm :
∀ N M k,
ctrm_of_ictrm (open_ictrm_wrt_itrm_rec k M N) =
open_ctrm_wrt_trm_rec k (trm_of_itrm M) (ctrm_of_ictrm N).
Proof.
intros.
dependent induction N; default_simp;
unfold ctrm_elvis_blame, elvis_blame, elvis;
try f_equal; eauto; eapply open_trm_of_itrm.
Qed.
Lemma open_ctrm_of_itrm_rec_var :
∀ N x k,
ctrm_of_ictrm (open_ictrm_wrt_itrm_rec k (itrm_var_f x) N) =
open_ctrm_wrt_trm_rec k (t_var_f x) (ctrm_of_ictrm N).
Proof.
intros.
assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
eapply open_ctrm_of_ictrm.
Qed.
Lemma open_ctrm_of_itrm_var:
∀ N x,
ctrm_of_ictrm (open_ictrm_wrt_itrm N (itrm_var_f x)) =
open_ctrm_wrt_trm (ctrm_of_ictrm N) (t_var_f x).
Proof.
intros. eapply open_ctrm_of_itrm_rec_var.
Qed.
Ltac desugar_ityping :=
match goal with
| [ H : ityping _ _ _ |- _ ] ⇒
pose proof (desugaring_typing _ _ _ H) end.
Lemma ictrm_desugaring_typing:
∀ iG' iA' iG iCN iA,
ictyping iG' iA' iG iCN iA →
ctyping (ctx_of_ictx iG') (typ_of_ityp iA') (ctx_of_ictx iG) (ctrm_of_ictrm iCN) (typ_of_ityp iA).
Proof.
intros.
dependent induction H; intros; pose (ctx_of_ictx iG) as G'; default_simp; try desugar_ityping; eauto.
- constructor. apply ctyping_binop_left.
+ pick fresh x and apply ctyping_case_scrutinee; eauto;
constructor; try eapply uniq_cons_3; eauto.
+ pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
- constructor. apply ctyping_binop_right.
+ pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
+ pick fresh x and apply ctyping_case_scrutinee; eauto;
constructor; try eapply uniq_cons_3; eauto.
- constructor.
pick fresh x and apply ctyping_abs; eauto.
assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
rewrite <- open_ctrm_of_itrm_var.
eapply H0; eauto.
- eapply ctyping_app_left; eauto.
pick fresh x and apply ctyping_case_scrutinee; eauto;
constructor; try eapply uniq_cons_3; eauto.
- eapply ctyping_app_right; eauto.
pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
Qed.
Inductive plug_ctrm : ctrm → trm → trm → Prop :=
| plug_ctrm_hole M : plug_ctrm ctrm_hole M M
| plug_ctrm_binop_left CM M' M N : plug_ctrm CM M' M → plug_ctrm (ctrm_binop_left CM N) M' (t_binop M N)
| plug_ctrm_binop_right CN M N' N : plug_ctrm CN N' N → plug_ctrm (ctrm_binop_right M CN) N' (t_binop M N)
| plug_ctrm_abs L CM A M' M :
( ∀ x , x \notin L →
plug_ctrm
(open_ctrm_wrt_trm CM (t_var_f x))
(open_trm_wrt_trm M' (t_var_f x))
(open_trm_wrt_trm M (t_var_f x))) →
plug_ctrm (ctrm_abs A CM) M' (t_abs A M)
| plug_ctrm_app_left CM M' M N : plug_ctrm CM M' M → plug_ctrm (ctrm_app_left CM N) M' (t_app M N)
| plug_ctrm_app_right CN M N' N : plug_ctrm CN N' N → plug_ctrm (ctrm_app_right M CN) N' (t_app M N)
| plug_ctrm_lift CM M' M : plug_ctrm CM M' M → plug_ctrm (ctrm_lift CM) M' (t_lift M)
| plug_ctrm_case_scrutinee CL L' L M N : plug_ctrm CL L' L → plug_ctrm (ctrm_case_scrutinee CL M N) L' (t_case L M N)
| plug_ctrm_case_null CM L M' M N : plug_ctrm CM M' M → plug_ctrm (ctrm_case_null L CM N) M' (t_case L M N)
| plug_ctrm_case_nonnull L CN LL M N' N :
( ∀ x , x \notin L →
plug_ctrm
(open_ctrm_wrt_trm CN (t_var_f x))
(open_trm_wrt_trm N' (t_var_f x))
(open_trm_wrt_trm N (t_var_f x))) →
plug_ctrm (ctrm_case_nonnull LL M CN) N' (t_case LL M N)
| plug_ctrm_cast CM M' M A B p : plug_ctrm CM M' M → plug_ctrm (ctrm_cast CM A B p) M' (t_cast M A B p).
Lemma typing_plugged:
∀ G' A' G C A,
ctyping G' A' G C A →
∀ M',
typing G' M' A' →
∀ M,
plug_ctrm C M' M →
typing G M A.
Proof.
intros × CTyp.
dependent induction CTyp; intros × Typ × PG; inversion PG; subst; eauto.
- pick fresh x and apply typing_abs; eauto.
assert (open_trm_wrt_trm M' (t_var_f x) = M') by eauto with lngen.
eapply H0; eauto.
rewrite <- H1.
eapply H5. eauto.
- pick fresh x and apply typing_case; eauto.
assert (open_trm_wrt_trm M' (t_var_f x) = M') by eauto with lngen.
eapply H2; eauto.
rewrite <- H3.
eapply H8. eauto.
Qed.
Lemma nest_trm_in_ictx:
∀ iG' M' A' iG iC iA M,
ictyping iG' (ityp_of_typ A') iG iC iA →
typing (ctx_of_ictx iG') M' A' →
plug_ctrm (ctrm_of_ictrm iC)
(M' ⦂ A' ⇒ (typ_of_ityp (ityp_of_typ A')) @@ (label_name blame_label_ei))
M →
typing
(ctx_of_ictx iG)
M
(typ_of_ityp iA).
Proof.
intros.
apply typing_plugged with
(G':=(ctx_of_ictx iG'))
(A':=(typ_of_ityp (ityp_of_typ A')))
(C:=(ctrm_of_ictrm iC))
(M':=(M' ⦂ A' ⇒ (typ_of_ityp (ityp_of_typ A')) @@ (label_name blame_label_ei)))
; eauto.
- apply ictrm_desugaring_typing; eauto.
- apply typing_cast; eauto.
apply compat_typ_ityp; eauto.
Qed.
Inductive plug_ictrm : ictrm → itrm → itrm → Prop :=
| plug_ictrm_hole M : plug_ictrm ictrm_hole M M
| plug_ictrm_binop_left CM M' M N : plug_ictrm CM M' M → plug_ictrm (ictrm_binop_left CM N) M' (itrm_binop M N)
| plug_ictrm_binop_right CN M N' N : plug_ictrm CN N' N → plug_ictrm (ictrm_binop_right M CN) N' (itrm_binop M N)
| plug_ictrm_abs L CM A M' M :
( ∀ x , x \notin L →
plug_ictrm
(open_ictrm_wrt_itrm CM (itrm_var_f x))
(open_itrm_wrt_itrm M' (itrm_var_f x))
(open_itrm_wrt_itrm M (itrm_var_f x))) →
plug_ictrm (ictrm_abs A CM) M' (itrm_abs A M)
| plug_ictrm_app_left CM M' M N : plug_ictrm CM M' M → plug_ictrm (ictrm_app_left CM N) M' (itrm_app M N)
| plug_ictrm_app_right CN M N' N : plug_ictrm CN N' N → plug_ictrm (ictrm_app_right M CN) N' (itrm_app M N).
Lemma ityping_to_lc_itrm : ∀ G N A,
ityping G N A → lc_itrm N.
Proof.
intros G N A H. induction H; eauto.
Qed.
Hint Resolve ityping_to_lc_itrm : core.
Lemma ityping_plugged:
∀ G' A' G C A,
ictyping G' A' G C A →
∀ M',
ityping G' M' A' →
∀ M,
plug_ictrm C M' M →
ityping G M A.
Proof.
intros × CTyp.
dependent induction CTyp; intros × Typ × PG; inversion PG; subst; eauto.
- pick fresh x and apply ityping_abs; eauto.
assert (open_itrm_wrt_itrm M' (itrm_var_f x) = M') by eauto with lngen.
eapply H0; eauto.
rewrite <- H1.
eapply H5. eauto.
Qed.
Definition ictx_of_ctx (G:ctx) : ictx := map ityp_of_typ G.
Lemma nest_itrm_in_ctx:
∀ G' iM' iA' G C A M,
ctyping (ctx_of_ictx (ictx_of_ctx G')) (typ_of_ityp_naive iA') G C A →
ityping (ictx_of_ctx G') iM' iA' →
plug_ctrm C
((trm_of_itrm iM') ⦂ (typ_of_ityp iA') ⇒ (typ_of_ityp_naive iA') @@ (label_name blame_label_ie))
M →
typing G M A.
Proof.
intros.
eapply typing_plugged; eauto.
desugar_ityping.
apply typing_cast; eauto.
apply compat_sym. apply compat_naive_subtyp. apply imp_naive_subtyp.
Qed.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Require Export Blame Safety.
Fixpoint typ_of_ityp C :=
match C with
| ityp_base ⇒ typ_null dtyp_base
| ityp_arrow A B ⇒ typ_null (dtyp_arrow (typ_of_ityp A) (typ_of_ityp B))
end.
Definition elvis L M := (t_case L M (t_var_b 0)).
Definition elvis_blame L p := elvis L (t_blame (label_name p)).
Definition blame_label_op := 0.
Definition blame_label_deref := 1.
Definition blame_label_ei := 2.
Definition blame_label_ie := 3.
Fixpoint trm_of_itrm N :=
match N with
| itrm_var_b n ⇒ t_var_b n
| itrm_var_f x ⇒ t_var_f x
| itrm_const c ⇒ t_lift (t_const c)
| itrm_binop M N ⇒ t_lift (t_binop
(elvis_blame (trm_of_itrm M) blame_label_op)
(elvis_blame (trm_of_itrm N) blame_label_op))
| itrm_abs A N ⇒ t_lift (t_abs (typ_of_ityp A) (trm_of_itrm N))
| itrm_app L M ⇒ t_app
(elvis_blame (trm_of_itrm L) blame_label_deref)
(trm_of_itrm M)
| itrm_null ⇒ t_null
end.
Definition ictx := list ( atom × ityp ).
Definition ctx_of_ictx (G:ictx) : ctx := map typ_of_ityp G.
Lemma ctx_of_ictx_binds_ityp:
∀ (G:ictx) x (A:ityp),
binds x A G →
binds x (typ_of_ityp A) (ctx_of_ictx G).
Proof.
intros.
eapply binds_map_2; eauto.
Qed.
Lemma uniq_ctx:
∀ G,
uniq G →
uniq (ctx_of_ictx G).
Proof.
intros.
eapply uniq_map_2; eauto.
Qed.
Lemma open_trm_of_itrm :
∀ N M k,
trm_of_itrm (open_itrm_wrt_itrm_rec k M N) =
open_trm_wrt_trm_rec k (trm_of_itrm M) (trm_of_itrm N).
Proof.
intros.
dependent induction N; default_simp.
- unfold elvis_blame, elvis. f_equal. eauto.
- unfold elvis_blame, elvis. f_equal. eauto.
- unfold elvis_blame, elvis. f_equal. eauto.
Qed.
Hint Resolve ctx_of_ictx_binds_ityp uniq_ctx : core.
Lemma open_trm_of_itrm_rec_var :
∀ N x k,
trm_of_itrm (open_itrm_wrt_itrm_rec k (itrm_var_f x) N) =
open_trm_wrt_trm_rec k (t_var_f x) (trm_of_itrm N).
Proof.
intros.
assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
eapply open_trm_of_itrm.
Qed.
Lemma open_trm_of_itrm_var:
∀ N x,
trm_of_itrm (open_itrm_wrt_itrm N (itrm_var_f x)) =
open_trm_wrt_trm (trm_of_itrm N) (t_var_f x).
Proof.
intros. eapply open_trm_of_itrm_rec_var.
Qed.
Lemma desugaring_typing:
∀ iG iN iA,
ityping iG iN iA →
typing (ctx_of_ictx iG) (trm_of_itrm iN) (typ_of_ityp iA).
Proof.
intros.
induction H; intros; pose (ctx_of_ictx iG) as G'; default_simp; eauto.
- constructor.
constructor;
unfold elvis_blame, elvis;
pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
- constructor.
pick fresh x and apply typing_abs; eauto.
rewrite <- open_trm_of_itrm_var.
eapply H0; eauto.
- eapply typing_app; eauto.
unfold elvis_blame, elvis.
pick fresh x and apply typing_case; eauto.
constructor;
try eapply uniq_cons_3; eauto.
- induction iA; default_simp; eauto.
Qed.
Lemma blame_eq_dec:
∀ (p q:label),
p = q ∨ p ≠ q.
Proof.
intros.
destruct p; destruct q;
destruct (eq_nat_dec bl bl0); eauto; right;
inversion 1; auto.
Qed.
Lemma close_pres_safe:
∀ N x k p,
safe (open_trm_wrt_trm_rec k (t_var_f x) N) p →
safe N p.
Proof.
intros.
dependent induction N; eauto; inversion H; subst; eauto.
Qed.
Hint Resolve close_pres_safe : core.
Fixpoint typ_of_ityp_naive A :=
match A with
| ityp_base ⇒ typ_def dtyp_base
| ityp_arrow B C ⇒ typ_def (dtyp_arrow (typ_of_ityp_naive B) (typ_of_ityp_naive C))
end.
Lemma imp_naive_subtyp A :
subtyp_n (typ_of_ityp_naive A) (typ_of_ityp A).
Proof.
induction A; simpl; eauto.
Qed.
Fixpoint ityp_of_typ A : ityp :=
match A with
| typ_null dtyp_base ⇒ ityp_base
| typ_null (dtyp_arrow A B) ⇒ ityp_arrow (ityp_of_typ A) (ityp_of_typ B)
| typ_def dtyp_base ⇒ ityp_base
| typ_def (dtyp_arrow A B) ⇒ ityp_arrow (ityp_of_typ A) (ityp_of_typ B)
end.
Lemma exp_naive_subtyp :
(∀ A, subtyp_n A (typ_of_ityp (ityp_of_typ A))) ∧
(∀ D, subtyp_n (typ_def D) (typ_of_ityp (ityp_of_typ (typ_def D))) ∧
subtyp_n (typ_null D) (typ_of_ityp (ityp_of_typ (typ_null D))))
.
Proof.
apply_mutual_ind typ_dtyp_mutind; default_simp.
Qed.
Lemma compat_naive_subtyp A B :
subtyp_n A B → compat A B.
Proof.
induction 1; eauto.
Qed.
Lemma compat_typ_ityp A:
compat A (typ_of_ityp (ityp_of_typ A)).
Proof.
apply compat_naive_subtyp. apply exp_naive_subtyp.
Qed.
Definition ctrm_elvis_blame CL p := (ctrm_case_scrutinee CL (t_blame (label_name p)) (t_var_b 0)).
Fixpoint ctrm_of_ictrm iC :=
match iC with
| ictrm_hole ⇒ ctrm_hole
| ictrm_binop_left iC N ⇒ ctrm_lift (ctrm_binop_left
(ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_op)
(elvis_blame (trm_of_itrm N) blame_label_op))
| ictrm_binop_right N iC ⇒ ctrm_lift (ctrm_binop_right
(elvis_blame (trm_of_itrm N) blame_label_op)
(ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_op))
| ictrm_abs A iC ⇒ ctrm_lift (ctrm_abs (typ_of_ityp A) (ctrm_of_ictrm iC))
| ictrm_app_left iC N ⇒ ctrm_app_left
(ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_deref)
(trm_of_itrm N)
| ictrm_app_right N iC ⇒ ctrm_app_right
(elvis_blame (trm_of_itrm N) blame_label_deref)
(ctrm_of_ictrm iC)
end.
Lemma open_ctrm_of_ictrm :
∀ N M k,
ctrm_of_ictrm (open_ictrm_wrt_itrm_rec k M N) =
open_ctrm_wrt_trm_rec k (trm_of_itrm M) (ctrm_of_ictrm N).
Proof.
intros.
dependent induction N; default_simp;
unfold ctrm_elvis_blame, elvis_blame, elvis;
try f_equal; eauto; eapply open_trm_of_itrm.
Qed.
Lemma open_ctrm_of_itrm_rec_var :
∀ N x k,
ctrm_of_ictrm (open_ictrm_wrt_itrm_rec k (itrm_var_f x) N) =
open_ctrm_wrt_trm_rec k (t_var_f x) (ctrm_of_ictrm N).
Proof.
intros.
assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
eapply open_ctrm_of_ictrm.
Qed.
Lemma open_ctrm_of_itrm_var:
∀ N x,
ctrm_of_ictrm (open_ictrm_wrt_itrm N (itrm_var_f x)) =
open_ctrm_wrt_trm (ctrm_of_ictrm N) (t_var_f x).
Proof.
intros. eapply open_ctrm_of_itrm_rec_var.
Qed.
Ltac desugar_ityping :=
match goal with
| [ H : ityping _ _ _ |- _ ] ⇒
pose proof (desugaring_typing _ _ _ H) end.
Lemma ictrm_desugaring_typing:
∀ iG' iA' iG iCN iA,
ictyping iG' iA' iG iCN iA →
ctyping (ctx_of_ictx iG') (typ_of_ityp iA') (ctx_of_ictx iG) (ctrm_of_ictrm iCN) (typ_of_ityp iA).
Proof.
intros.
dependent induction H; intros; pose (ctx_of_ictx iG) as G'; default_simp; try desugar_ityping; eauto.
- constructor. apply ctyping_binop_left.
+ pick fresh x and apply ctyping_case_scrutinee; eauto;
constructor; try eapply uniq_cons_3; eauto.
+ pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
- constructor. apply ctyping_binop_right.
+ pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
+ pick fresh x and apply ctyping_case_scrutinee; eauto;
constructor; try eapply uniq_cons_3; eauto.
- constructor.
pick fresh x and apply ctyping_abs; eauto.
assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
rewrite <- open_ctrm_of_itrm_var.
eapply H0; eauto.
- eapply ctyping_app_left; eauto.
pick fresh x and apply ctyping_case_scrutinee; eauto;
constructor; try eapply uniq_cons_3; eauto.
- eapply ctyping_app_right; eauto.
pick fresh x and apply typing_case; eauto;
constructor; try eapply uniq_cons_3; eauto.
Qed.
Inductive plug_ctrm : ctrm → trm → trm → Prop :=
| plug_ctrm_hole M : plug_ctrm ctrm_hole M M
| plug_ctrm_binop_left CM M' M N : plug_ctrm CM M' M → plug_ctrm (ctrm_binop_left CM N) M' (t_binop M N)
| plug_ctrm_binop_right CN M N' N : plug_ctrm CN N' N → plug_ctrm (ctrm_binop_right M CN) N' (t_binop M N)
| plug_ctrm_abs L CM A M' M :
( ∀ x , x \notin L →
plug_ctrm
(open_ctrm_wrt_trm CM (t_var_f x))
(open_trm_wrt_trm M' (t_var_f x))
(open_trm_wrt_trm M (t_var_f x))) →
plug_ctrm (ctrm_abs A CM) M' (t_abs A M)
| plug_ctrm_app_left CM M' M N : plug_ctrm CM M' M → plug_ctrm (ctrm_app_left CM N) M' (t_app M N)
| plug_ctrm_app_right CN M N' N : plug_ctrm CN N' N → plug_ctrm (ctrm_app_right M CN) N' (t_app M N)
| plug_ctrm_lift CM M' M : plug_ctrm CM M' M → plug_ctrm (ctrm_lift CM) M' (t_lift M)
| plug_ctrm_case_scrutinee CL L' L M N : plug_ctrm CL L' L → plug_ctrm (ctrm_case_scrutinee CL M N) L' (t_case L M N)
| plug_ctrm_case_null CM L M' M N : plug_ctrm CM M' M → plug_ctrm (ctrm_case_null L CM N) M' (t_case L M N)
| plug_ctrm_case_nonnull L CN LL M N' N :
( ∀ x , x \notin L →
plug_ctrm
(open_ctrm_wrt_trm CN (t_var_f x))
(open_trm_wrt_trm N' (t_var_f x))
(open_trm_wrt_trm N (t_var_f x))) →
plug_ctrm (ctrm_case_nonnull LL M CN) N' (t_case LL M N)
| plug_ctrm_cast CM M' M A B p : plug_ctrm CM M' M → plug_ctrm (ctrm_cast CM A B p) M' (t_cast M A B p).
Lemma typing_plugged:
∀ G' A' G C A,
ctyping G' A' G C A →
∀ M',
typing G' M' A' →
∀ M,
plug_ctrm C M' M →
typing G M A.
Proof.
intros × CTyp.
dependent induction CTyp; intros × Typ × PG; inversion PG; subst; eauto.
- pick fresh x and apply typing_abs; eauto.
assert (open_trm_wrt_trm M' (t_var_f x) = M') by eauto with lngen.
eapply H0; eauto.
rewrite <- H1.
eapply H5. eauto.
- pick fresh x and apply typing_case; eauto.
assert (open_trm_wrt_trm M' (t_var_f x) = M') by eauto with lngen.
eapply H2; eauto.
rewrite <- H3.
eapply H8. eauto.
Qed.
Lemma nest_trm_in_ictx:
∀ iG' M' A' iG iC iA M,
ictyping iG' (ityp_of_typ A') iG iC iA →
typing (ctx_of_ictx iG') M' A' →
plug_ctrm (ctrm_of_ictrm iC)
(M' ⦂ A' ⇒ (typ_of_ityp (ityp_of_typ A')) @@ (label_name blame_label_ei))
M →
typing
(ctx_of_ictx iG)
M
(typ_of_ityp iA).
Proof.
intros.
apply typing_plugged with
(G':=(ctx_of_ictx iG'))
(A':=(typ_of_ityp (ityp_of_typ A')))
(C:=(ctrm_of_ictrm iC))
(M':=(M' ⦂ A' ⇒ (typ_of_ityp (ityp_of_typ A')) @@ (label_name blame_label_ei)))
; eauto.
- apply ictrm_desugaring_typing; eauto.
- apply typing_cast; eauto.
apply compat_typ_ityp; eauto.
Qed.
Inductive plug_ictrm : ictrm → itrm → itrm → Prop :=
| plug_ictrm_hole M : plug_ictrm ictrm_hole M M
| plug_ictrm_binop_left CM M' M N : plug_ictrm CM M' M → plug_ictrm (ictrm_binop_left CM N) M' (itrm_binop M N)
| plug_ictrm_binop_right CN M N' N : plug_ictrm CN N' N → plug_ictrm (ictrm_binop_right M CN) N' (itrm_binop M N)
| plug_ictrm_abs L CM A M' M :
( ∀ x , x \notin L →
plug_ictrm
(open_ictrm_wrt_itrm CM (itrm_var_f x))
(open_itrm_wrt_itrm M' (itrm_var_f x))
(open_itrm_wrt_itrm M (itrm_var_f x))) →
plug_ictrm (ictrm_abs A CM) M' (itrm_abs A M)
| plug_ictrm_app_left CM M' M N : plug_ictrm CM M' M → plug_ictrm (ictrm_app_left CM N) M' (itrm_app M N)
| plug_ictrm_app_right CN M N' N : plug_ictrm CN N' N → plug_ictrm (ictrm_app_right M CN) N' (itrm_app M N).
Lemma ityping_to_lc_itrm : ∀ G N A,
ityping G N A → lc_itrm N.
Proof.
intros G N A H. induction H; eauto.
Qed.
Hint Resolve ityping_to_lc_itrm : core.
Lemma ityping_plugged:
∀ G' A' G C A,
ictyping G' A' G C A →
∀ M',
ityping G' M' A' →
∀ M,
plug_ictrm C M' M →
ityping G M A.
Proof.
intros × CTyp.
dependent induction CTyp; intros × Typ × PG; inversion PG; subst; eauto.
- pick fresh x and apply ityping_abs; eauto.
assert (open_itrm_wrt_itrm M' (itrm_var_f x) = M') by eauto with lngen.
eapply H0; eauto.
rewrite <- H1.
eapply H5. eauto.
Qed.
Definition ictx_of_ctx (G:ctx) : ictx := map ityp_of_typ G.
Lemma nest_itrm_in_ctx:
∀ G' iM' iA' G C A M,
ctyping (ctx_of_ictx (ictx_of_ctx G')) (typ_of_ityp_naive iA') G C A →
ityping (ictx_of_ctx G') iM' iA' →
plug_ctrm C
((trm_of_itrm iM') ⦂ (typ_of_ityp iA') ⇒ (typ_of_ityp_naive iA') @@ (label_name blame_label_ie))
M →
typing G M A.
Proof.
intros.
eapply typing_plugged; eauto.
desugar_ityping.
apply typing_cast; eauto.
apply compat_sym. apply compat_naive_subtyp. apply imp_naive_subtyp.
Qed.