Fsub.CaptureTrack.Fsub_LetSum_Soundness
Type-safety proofs for Fsub.CaptureTrack.
Authors: Brian Aydemir and Arthur Chargu\'eraud, with help from
Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
In parentheses are given the label of the corresponding lemma in
the appendix (informal proofs) of the POPLmark Challenge.
Table of contents:
Require Import Fsub.CaptureTrack.Tactics.
Require Import Coq.Program.Equality.
Require Export Fsub.CaptureTrack.Fsub_LetSum_Lemmas.
(* ********************************************************************** *)
Require Import Coq.Program.Equality.
Require Export Fsub.CaptureTrack.Fsub_LetSum_Lemmas.
(* ********************************************************************** *)
(* ********************************************************************** *)
Lemma subqual_reflexivity : forall E T,
wf_env E ->
wf_qua E T ->
subqual E T T.
Proof with eauto 6.
intros E T Ok Wf.
induction Wf...
Qed.
Lemma sub_reflexivity : forall E T,
wf_env E ->
wf_typ E T ->
sub E T T
with subqtype_reflexivity : forall E T,
wf_env E ->
wf_qtyp E T ->
subqtype E T T.
Proof with eauto using subqual_reflexivity.
------
clear sub_reflexivity.
intros E T Ok Wf.
induction Wf...
pick fresh y and apply sub_arrow...
pick fresh Y and apply sub_all...
pick fresh Y and apply sub_qall...
------
clear subqtype_reflexivity.
intros E T Ok Wf.
induction Wf...
Qed.
(* ********************************************************************** *)
wf_env E ->
wf_qua E T ->
subqual E T T.
Proof with eauto 6.
intros E T Ok Wf.
induction Wf...
Qed.
Lemma sub_reflexivity : forall E T,
wf_env E ->
wf_typ E T ->
sub E T T
with subqtype_reflexivity : forall E T,
wf_env E ->
wf_qtyp E T ->
subqtype E T T.
Proof with eauto using subqual_reflexivity.
------
clear sub_reflexivity.
intros E T Ok Wf.
induction Wf...
pick fresh y and apply sub_arrow...
pick fresh Y and apply sub_all...
pick fresh Y and apply sub_qall...
------
clear subqtype_reflexivity.
intros E T Ok Wf.
induction Wf...
Qed.
(* ********************************************************************** *)
Lemma subqual_weakening : forall E F G S T,
subqual (G ++ E) S T ->
wf_env (G ++ F ++ E) ->
subqual (G ++ F ++ E) S T.
Proof with simpl_env; auto 6 using wf_qua_weakening.
intros E F G S T Sub Ok.
remember (G ++ E) as H.
generalize dependent G.
induction Sub; intros G Ok EQ; subst...
Case "subqual_trans_qvar".
apply (subqual_trans_qvar R)...
Case "subqual_trans_term_qvar".
apply (subqual_trans_term_qvar R) with (T := T)...
Qed.
Lemma sub_weakening : forall E F G S T,
sub (G ++ E) S T ->
wf_env (G ++ F ++ E) ->
sub (G ++ F ++ E) S T
with subqtype_weakening : forall E F G S T,
subqtype (G ++ E) S T ->
wf_env (G ++ F ++ E) ->
subqtype (G ++ F ++ E) S T.
Proof with simpl_env; auto using wf_typ_weakening, subqual_weakening,
wf_qtyp_weakening, wf_qua_weakening.
------
clear sub_weakening.
intros E F G S T Sub Ok.
remember (G ++ E) as H.
generalize dependent G.
induction Sub; intros G Ok EQ; subst...
Case "sub_trans_tvar".
apply (sub_trans_tvar U)...
Case "sub_arrow".
pick fresh y and apply sub_arrow...
rewrite <- app_assoc.
apply subqtype_weakening...
Case "sub_all".
pick fresh Y and apply sub_all...
rewrite <- app_assoc.
apply subqtype_weakening...
Case "sub_qall".
pick fresh Y and apply sub_qall...
rewrite <- app_assoc.
apply subqtype_weakening...
------
clear subqtype_weakening.
intros E F G S T Sub Ok.
remember (G ++ E) as H.
generalize dependent G.
induction Sub; intros G Ok EQ; subst...
Qed.
(* ********************************************************************** *)
Definition transitivity_on_sub Q := forall E S T,
sub E S Q -> sub E Q T -> sub E S T.
Definition transitivity_on_subqtype Q := forall E S T,
subqtype E S Q -> subqtype E Q T -> subqtype E S T.
Definition transitivity_on_subqual Q := forall E S T,
subqual E S Q -> subqual E Q T -> subqual E S T.
Lemma subqual_join_split : forall E R1 R2 T,
subqual E (qua_join R1 R2) T ->
subqual E R1 T /\ subqual E R2 T.
Proof with eauto.
intros * Sub.
dependent induction Sub; try solve [intuition eauto]...
- edestruct IHSub...
- edestruct IHSub...
- edestruct IHSub1...
edestruct IHSub2...
Qed.
Lemma subqual_transitivity : forall Q,
transitivity_on_subqual Q.
Proof with simpl_env; auto.
unfold transitivity_on_subqual.
intros Q E S T SsubQ QsubT.
generalize dependent T.
induction SsubQ; intros Tq QsubT...
* dependent induction QsubT...
* eapply subqual_trans_qvar with (R := R)...
* eapply subqual_trans_term_qvar with (R := R) (T := T)...
* eapply subqual_join_split in QsubT as [SubL SubR]...
* eapply subqual_join_split in QsubT as [SubL SubR]...
* remember (qua_meet R1 R2) as R.
induction QsubT; inversion HeqR; subst...
Qed.
Lemma subqual_narrowing_qua_aux : forall Q F E Z P S T,
transitivity_on_subqual Q ->
subqual (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual E P Q ->
subqual (F ++ Z ~ bind_qua P ++ E) S T.
Proof with simpl_env; eauto using wf_qua_narrowing_qua,
wf_env_narrowing_qua.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
apply (subqual_trans_qvar P); [ eauto using fresh_mid_head | ].
apply TransQ.
SSCase "P <: Q".
rewrite_env (empty ++ (F ++ Z ~ bind_qua P) ++ E).
apply subqual_weakening...
SSCase "Q <: T".
analyze_binds_uniq H.
injection BindsTacVal; intros; subst...
SCase "X <> Z".
apply (subqual_trans_qvar R)...
Case "sub_trans_term_tvar".
destruct (X == Z); subst...
exfalso. analyze_binds_uniq H.
Qed.
Lemma subqual_narrowing_sub_aux : forall Q F E Z P S T,
transitivity_on_sub Q ->
subqual (F ++ Z ~ bind_sub Q ++ E) S T ->
sub E P Q ->
subqual (F ++ Z ~ bind_sub P ++ E) S T.
Proof with simpl_env; eauto using wf_qua_narrowing_sub,
wf_env_narrowing_sub.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
destruct (X == Z); subst...
exfalso. analyze_binds_uniq H.
Case "sub_trans_term_tvar".
destruct (X == Z); subst...
exfalso. analyze_binds_uniq H.
Qed.
Lemma subqual_narrowing_typ_aux : forall Q F E Z P S T,
transitivity_on_subqtype Q ->
subqual (F ++ Z ~ bind_typ Q ++ E) S T ->
subqtype E P Q ->
subqual (F ++ Z ~ bind_typ P ++ E) S T.
Proof with simpl_env; eauto using wf_qua_narrowing_typ,
wf_env_narrowing_typ.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_typ Q ++ E) as G.
generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
destruct (X == Z); subst...
exfalso. analyze_binds_uniq H.
Case "sub_trans_term_tvar".
destruct (X == Z); subst...
destruct P as [R2 T2].
apply subqual_trans_term_qvar with (R := R2) (T := T2)...
inversion PsubQ; analyze_binds_uniq H; subst...
inversion BindsTacVal; subst...
eapply (subqual_transitivity Q2)...
rewrite_env (empty ++ (F ++ Z ~ bind_typ (qtyp_qtyp R2 T2)) ++ E).
apply subqual_weakening...
Qed.
Lemma sub_narrowing_sub_aux : forall Q F E Z P S T,
transitivity_on_sub Q ->
sub (F ++ Z ~ bind_sub Q ++ E) S T ->
sub E P Q ->
sub (F ++ Z ~ bind_sub P ++ E) S T
with subqtype_narrowing_sub_aux : forall Q F E Z P S T,
transitivity_on_sub Q ->
subqtype (F ++ Z ~ bind_sub Q ++ E) S T ->
sub E P Q ->
subqtype (F ++ Z ~ bind_sub P ++ E) S T.
Proof with simpl_env; eauto using wf_typ_narrowing_sub, wf_env_narrowing_sub,
subqual_narrowing_sub_aux.
------
clear sub_narrowing_sub_aux.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
apply (sub_trans_tvar P); [ eauto using fresh_mid_head | ].
apply TransQ.
SSCase "P <: Q".
rewrite_env (empty ++ (F ++ Z ~ bind_sub P) ++ E).
apply sub_weakening...
SSCase "Q <: T".
analyze_binds_uniq H.
injection BindsTacVal; intros; subst...
SCase "X <> Z".
apply (sub_trans_tvar U)...
Case "sub_arrow".
pick fresh Y and apply sub_arrow...
rewrite <- app_assoc.
eapply subqtype_narrowing_sub_aux...
Case "sub_all".
pick fresh Y and apply sub_all...
rewrite <- app_assoc.
eapply subqtype_narrowing_sub_aux...
Case "sub_qall".
pick fresh Y and apply sub_qall...
rewrite <- app_assoc.
eapply subqtype_narrowing_sub_aux...
------
clear subqtype_narrowing_sub_aux.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Qed.
Lemma sub_narrowing_qua_aux : forall Q F E Z P S T,
transitivity_on_subqual Q ->
sub (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual E P Q ->
sub (F ++ Z ~ bind_qua P ++ E) S T
with subqtype_narrowing_qua_aux : forall Q F E Z P S T,
transitivity_on_subqual Q ->
subqtype (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual E P Q ->
subqtype (F ++ Z ~ bind_qua P ++ E) S T.
Proof with simpl_env; eauto using wf_typ_narrowing_qua, wf_env_narrowing_qua,
subqual_narrowing_qua_aux.
------
clear sub_narrowing_qua_aux.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
exfalso. analyze_binds_uniq H...
SCase "X <> Z".
apply (sub_trans_tvar U)...
Case "sub_arrow".
pick fresh Y and apply sub_arrow...
rewrite <- app_assoc.
eapply subqtype_narrowing_qua_aux...
Case "sub_all".
pick fresh Y and apply sub_all...
rewrite <- app_assoc.
eapply subqtype_narrowing_qua_aux...
Case "sub_qall".
pick fresh Y and apply sub_qall...
rewrite <- app_assoc.
eapply subqtype_narrowing_qua_aux...
------
clear subqtype_narrowing_qua_aux.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Qed.
Lemma sub_narrowing_typ_aux : forall Q F E Z P S T,
transitivity_on_subqtype Q ->
sub (F ++ Z ~ bind_typ Q ++ E) S T ->
subqtype E P Q ->
sub (F ++ Z ~ bind_typ P ++ E) S T
with subqtype_narrowing_typ_aux : forall Q F E Z P S T,
transitivity_on_subqtype Q ->
subqtype (F ++ Z ~ bind_typ Q ++ E) S T ->
subqtype E P Q ->
subqtype (F ++ Z ~ bind_typ P ++ E) S T.
Proof with simpl_env; eauto using wf_typ_narrowing_typ, wf_env_narrowing_typ,
subqual_narrowing_typ_aux.
------
clear sub_narrowing_typ_aux.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_typ Q ++ E) as G.
generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
analyze_binds_uniq H...
SCase "X <> Z".
apply (sub_trans_tvar U)...
Case "sub_arrow".
pick fresh Y and apply sub_arrow...
rewrite <- app_assoc.
eapply subqtype_narrowing_typ_aux...
Case "sub_all".
pick fresh Y and apply sub_all...
rewrite <- app_assoc.
eapply subqtype_narrowing_typ_aux...
Case "sub_qall".
pick fresh Y and apply sub_qall...
rewrite <- app_assoc.
eapply subqtype_narrowing_typ_aux...
------
clear subqtype_narrowing_typ_aux.
intros Q F E Z P S T TransQ SsubT PsubQ.
remember (F ++ Z ~ bind_typ Q ++ E) as G. generalize dependent F.
induction SsubT; intros F EQ; subst...
Qed.
Lemma sub_transitivity_rec : forall Q,
type Q -> transitivity_on_sub Q
with subqtype_transitivity_rec : forall Q,
qtype Q -> transitivity_on_subqtype Q.
Proof with simpl_env; auto.
------
clear sub_transitivity_rec.
unfold transitivity_on_sub.
intros Q W E S T SsubQ QsubT.
generalize dependent T.
generalize dependent S.
generalize dependent E.
remember Q as Q' in |- *.
generalize dependent Q'.
induction W;
intros Q' EQ E S SsubQ;
induction SsubQ; try discriminate; inversion EQ; subst;
intros T' QsubT;
inversion QsubT; subst; eauto 4 using sub_trans_tvar.
Case "sub_arrow / sub_top".
assert (sub E (typ_arrow S1 S2) (typ_arrow T1 T2)).
SCase "proof of assertion".
pick fresh y and apply sub_arrow...
auto.
Case "sub_arrow / sub_arrow".
pick fresh Y and apply sub_arrow...
SCase "bounds".
eapply subqtype_transitivity_rec with (Q := T1)...
SCase "bodies".
lapply (H2 Y); [ intros K | auto ].
lapply (H8 Y); [ intros K2 | auto ].
eapply subqtype_transitivity_rec...
rewrite_env (empty ++ Y ~ bind_typ T0 ++ E).
eapply (subqtype_narrowing_typ_aux T1)...
Case "sub_all / sub_top".
assert (sub E (typ_all S1 S2) (typ_all T1 T2)).
SCase "proof of assertion".
pick fresh y and apply sub_all...
auto.
Case "sub_all / sub_all".
pick fresh Y and apply sub_all.
SCase "bounds".
eauto.
SCase "bodies".
lapply (H0 Y); [ intros K | auto ].
lapply (H6 Y); [ intros K2 | auto ].
eapply subqtype_transitivity_rec with (Q := (open_tqt T2 Y))...
rewrite_env (empty ++ Y ~ bind_sub T0 ++ E).
eapply (subqtype_narrowing_sub_aux T1)...
unshelve epose proof (IHW T1 _) as TransT1...
unfold transitivity_on_sub; eauto using TransT1...
Case "sub_qall / sub_top".
assert (sub E (typ_qall S1 S2) (typ_qall Q T)).
SCase "proof of assertion".
pick fresh y and apply sub_qall...
auto.
Case "sub_qall / sub_qall".
pick fresh Y and apply sub_qall...
SCase "bounds".
eapply subqual_transitivity with (Q := Q)...
SCase "bodies".
lapply (H2 Y); [ intros K | auto ].
lapply (H8 Y); [ intros K2 | auto ].
eapply subqtype_transitivity_rec...
rewrite_env (empty ++ Y ~ bind_qua T1 ++ E).
eapply subqtype_narrowing_qua_aux ...
apply subqual_transitivity.
Case "sub_sum / sub_sum".
eapply sub_sum...
eapply subqtype_transitivity_rec with (Q := T1)...
eapply subqtype_transitivity_rec with (Q := T2)...
Case "sub_pair / sub_pair".
eapply sub_pair...
eapply subqtype_transitivity_rec with (Q := T1)...
eapply subqtype_transitivity_rec with (Q := T2)...
------
clear subqtype_transitivity_rec.
unfold transitivity_on_subqtype.
intros Q W E S T SsubQ QsubT.
generalize dependent T.
generalize dependent S.
generalize dependent E.
remember Q as Q' in |- *.
generalize dependent Q'.
induction W;
intros Q' EQ E S SsubQ;
induction SsubQ; try discriminate; inversion EQ; subst;
intros T' QsubT;
inversion QsubT; subst; eauto 4 using sub_trans_tvar.
eapply sub_qtyp_qtyp...
eapply subqual_transitivity with (Q := Q)...
eapply sub_transitivity_rec with (Q := T)...
Qed.
Lemma sub_transitivity : forall Q,
transitivity_on_sub Q.
Proof with simpl_env; auto.
unfold transitivity_on_sub.
intros.
eapply sub_transitivity_rec with (Q := Q)...
Qed.
Lemma subqtype_transitivity : forall Q,
transitivity_on_subqtype Q.
Proof with simpl_env; auto.
unfold transitivity_on_subqtype.
intros.
eapply subqtype_transitivity_rec with (Q := Q)...
Qed.
Lemma sub_narrowing_sub : forall Q E F Z P S T,
sub E P Q ->
sub (F ++ Z ~ bind_sub Q ++ E) S T ->
sub (F ++ Z ~ bind_sub P ++ E) S T.
Proof.
intros.
eapply sub_narrowing_sub_aux; eauto.
apply sub_transitivity.
Qed.
Lemma subqtype_narrowing_sub : forall Q E F Z P S T,
sub E P Q ->
subqtype (F ++ Z ~ bind_sub Q ++ E) S T ->
subqtype (F ++ Z ~ bind_sub P ++ E) S T.
Proof.
intros.
eapply subqtype_narrowing_sub_aux; eauto.
apply sub_transitivity.
Qed.
Lemma subqual_narrowing_sub : forall Q E F Z P S T,
sub E P Q ->
subqual (F ++ Z ~ bind_sub Q ++ E) S T ->
subqual (F ++ Z ~ bind_sub P ++ E) S T.
Proof.
intros.
eapply subqual_narrowing_sub_aux; eauto.
apply sub_transitivity.
Qed.
Lemma sub_narrowing_qua : forall Q E F Z P S T,
subqual E P Q ->
sub (F ++ Z ~ bind_qua Q ++ E) S T ->
sub (F ++ Z ~ bind_qua P ++ E) S T.
Proof.
intros.
eapply sub_narrowing_qua_aux; eauto.
apply subqual_transitivity.
Qed.
Lemma subqtype_narrowing_qua : forall Q E F Z P S T,
subqual E P Q ->
subqtype (F ++ Z ~ bind_qua Q ++ E) S T ->
subqtype (F ++ Z ~ bind_qua P ++ E) S T.
Proof.
intros.
eapply subqtype_narrowing_qua_aux; eauto.
apply subqual_transitivity.
Qed.
Lemma subqual_narrowing_qua : forall Q E F Z P S T,
subqual E P Q ->
subqual (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual (F ++ Z ~ bind_qua P ++ E) S T.
Proof.
intros.
eapply subqual_narrowing_qua_aux; eauto.
apply subqual_transitivity.
Qed.
Lemma sub_narrowing_typ : forall Q E F Z P S T,
subqtype E P Q ->
sub (F ++ Z ~ bind_typ Q ++ E) S T ->
sub (F ++ Z ~ bind_typ P ++ E) S T.
Proof.
intros.
eapply sub_narrowing_typ_aux; eauto.
apply subqtype_transitivity.
Qed.
Lemma subqtype_narrowing_typ : forall Q E F Z P S T,
subqtype E P Q ->
subqtype (F ++ Z ~ bind_typ Q ++ E) S T ->
subqtype (F ++ Z ~ bind_typ P ++ E) S T.
Proof.
intros.
eapply subqtype_narrowing_typ_aux; eauto.
apply subqtype_transitivity.
Qed.
Lemma subqual_narrowing_typ : forall Q E F Z P S T,
subqtype E P Q ->
subqual (F ++ Z ~ bind_typ Q ++ E) S T ->
subqual (F ++ Z ~ bind_typ P ++ E) S T.
Proof.
intros.
eapply subqual_narrowing_typ_aux; eauto.
apply subqtype_transitivity.
Qed.
(* ********************************************************************** *)
Lemma subqual_through_subst_qq : forall Q E F Z S T P,
subqual (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual E P Q ->
subqual (map (subst_qb Z P) F ++ E) (subst_qq Z P S) (subst_qq Z P T).
Proof with simpl_env;
eauto 4 using wf_qua_subst_qb, wf_env_subst_qb, wf_qua_weaken_head.
intros Q E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_qq...
Case "subqual_top".
eapply subqual_top...
Case "subqual_bot".
eapply subqual_bot...
Case "subqual_refl_fvar".
destruct (X == Z); subst.
SCase "X = Z".
apply subqual_reflexivity...
SCase "X <> Z".
apply subqual_reflexivity...
inversion H0; subst; analyze_binds H3...
apply (wf_qua_fvar (subst_qq Z P R))...
apply (wf_qua_term_fvar (subst_qqt Z P T))...
Case "subqual_trans_qvar".
destruct (X == Z); subst.
SCase "X = Z".
apply (subqual_transitivity Q).
SSCase "left branch".
rewrite_env (empty ++ map (subst_qb Z P) G ++ E).
apply subqual_weakening...
SSCase "right branch".
rewrite (subst_qq_fresh Z P Q).
analyze_binds_uniq H.
inversion BindsTacVal; subst...
apply (notin_fv_qq_wf_qua E); eauto using fresh_mid_tail.
SCase "X <> Z".
apply (subqual_trans_qvar (subst_qq Z P R))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H...
Case "subqual_trans_term_qvar".
destruct (X == Z); subst.
SCase "X = Z".
apply (subqual_transitivity Q).
SSCase "left branch".
rewrite_env (empty ++ map (subst_qb Z P) G ++ E).
apply subqual_weakening...
SSCase "right branch".
rewrite (subst_qq_fresh Z P Q).
analyze_binds_uniq H.
apply (notin_fv_qq_wf_qua E); eauto using fresh_mid_tail.
SCase "X <> Z".
apply (subqual_trans_term_qvar (subst_qq Z P R) _ (subst_qt Z P T))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
replace (bind_typ (qtyp_qtyp (subst_qq Z P R) (subst_qt Z P T)))
with (subst_qb Z P (bind_typ (qtyp_qtyp R T)))...
analyze_binds H...
Case "subqual_join_inl".
apply subqual_join_inl...
Case "subqual_join_inr".
apply subqual_join_inr...
Case "subqual_meet_eliml".
apply subqual_meet_eliml...
Case "subqual_meet_elimr".
apply subqual_meet_elimr...
Qed.
Lemma subqual_through_subst_tt : forall Q E F Z S T P,
subqual (F ++ Z ~ bind_sub Q ++ E) S T ->
sub E P Q ->
subqual (map (subst_tb Z P) F ++ E) S T.
Proof with simpl_env;
eauto 4 using wf_qua_subst_tb, wf_env_subst_tb, wf_qua_weaken_head.
intros Q E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl...
Case "subqual_top".
apply subqual_top...
Case "subqual_bot".
eapply subqual_bot...
Case "subqual_refl_fvar".
apply subqual_reflexivity...
Case "subqual_trans_qvar".
apply (subqual_trans_qvar R)...
analyze_binds H...
unsimpl (subst_tb Z P (bind_qua R))...
Case "subqual_trans_term_qvar".
apply (subqual_trans_term_qvar R _ (subst_tt Z P T))...
analyze_binds H;
unsimpl (subst_tb Z P (bind_typ (qtyp_qtyp R T)))...
rewrite (map_subst_tb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ]...
Case "subqual_join_inl".
apply subqual_join_inl...
Case "subqual_join_inr".
apply subqual_join_inr...
Case "subqual_meet_eliml".
apply subqual_meet_eliml...
Case "subqual_meet_elimr".
apply subqual_meet_elimr...
Qed.
Lemma subqual_through_subst_qq_var : forall Q R E F Z S T P,
subqual (F ++ Z ~ bind_typ (qtyp_qtyp Q R) ++ E) S T ->
subqual E P Q ->
subqual (map (subst_qb Z P) F ++ E) (subst_qq Z P S) (subst_qq Z P T).
Proof with simpl_env;
eauto 4 using wf_qua_subst_qb_var, wf_env_subst_qb_var, wf_qua_weaken_head.
intros Q R E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_typ (qtyp_qtyp Q R) ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_qq...
Case "subqual_top".
eapply subqual_top...
Case "subqual_bot".
eapply subqual_bot...
Case "subqual_refl_fvar".
destruct (X == Z); subst.
SCase "X = Z".
apply subqual_reflexivity...
SCase "X <> Z".
apply subqual_reflexivity...
inversion H0; subst; analyze_binds H3...
apply (wf_qua_fvar (subst_qq Z P R0))...
apply (wf_qua_term_fvar (subst_qqt Z P T))...
Case "subqual_trans_qvar".
destruct (X == Z); subst.
SCase "X = Z".
exfalso.
analyze_binds_uniq H...
SCase "X <> Z".
apply (subqual_trans_qvar (subst_qq Z P R0))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H...
Case "subqual_trans_term_qvar".
destruct (X == Z); subst.
SCase "X = Z".
apply (subqual_transitivity Q).
SSCase "left branch".
rewrite_env (empty ++ map (subst_qb Z P) G ++ E).
apply subqual_weakening...
SSCase "right branch".
rewrite (subst_qq_fresh Z P Q).
analyze_binds_uniq H.
inversion BindsTacVal; subst...
apply (notin_fv_qq_wf_qua E); eauto using fresh_mid_tail.
SCase "X <> Z".
apply (subqual_trans_term_qvar (subst_qq Z P R0) _ (subst_qt Z P T))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
unsimpl (subst_qqt Z P (qtyp_qtyp R0 T)).
replace (bind_typ (subst_qqt Z P (qtyp_qtyp R0 T)))
with (subst_qb Z P (bind_typ (qtyp_qtyp R0 T))); [ | auto].
analyze_binds_uniq H...
Case "subqual_join_inl".
apply subqual_join_inl...
Case "subqual_join_inr".
apply subqual_join_inr...
Case "subqual_meet_eliml".
apply subqual_meet_eliml...
Case "subqual_meet_elimr".
apply subqual_meet_elimr...
Qed.
Lemma sub_through_subst_tt : forall Q E F Z S T P,
sub (F ++ Z ~ bind_sub Q ++ E) S T ->
sub E P Q ->
sub (map (subst_tb Z P) F ++ E) (subst_tt Z P S) (subst_tt Z P T)
with subqtype_through_subst_tqt : forall Q E F Z S T P,
subqtype (F ++ Z ~ bind_sub Q ++ E) S T ->
sub E P Q ->
subqtype (map (subst_tb Z P) F ++ E) (subst_tqt Z P S) (subst_tqt Z P T).
Proof with
simpl_env;
eauto 4 using wf_typ_subst_tb, wf_env_subst_tb, wf_typ_weaken_head.
------
clear sub_through_subst_tt.
intros Q E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_tt...
Case "sub_top".
apply sub_top...
Case "sub_refl_tvar".
destruct (X == Z); subst.
SCase "X = Z".
apply sub_reflexivity...
SCase "X <> Z".
apply sub_reflexivity...
inversion H0; subst.
analyze_binds H3...
apply (wf_typ_var (subst_tt Z P U))...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
apply (sub_transitivity Q).
SSCase "left branch".
rewrite_env (empty ++ map (subst_tb Z P) G ++ E).
apply sub_weakening...
SSCase "right branch".
rewrite (subst_tt_fresh Z P Q).
analyze_binds_uniq H.
inversion BindsTacVal; subst...
apply (notin_fv_tt_wf_typ E); eauto using fresh_mid_tail.
SCase "X <> Z".
apply (sub_trans_tvar (subst_tt Z P U))...
rewrite (map_subst_tb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H...
Case "sub_arrow".
pick fresh x and apply sub_arrow...
rewrite subst_tqt_open_qqt_var...
rewrite subst_tqt_open_qqt_var...
rewrite_env (map (subst_tb Z P) (x ~ bind_typ T1 ++ G) ++ E).
eapply subqtype_through_subst_tqt...
Case "sub_all".
pick fresh X and apply sub_all...
rewrite subst_tqt_open_tqt_var...
rewrite subst_tqt_open_tqt_var...
rewrite_env (map (subst_tb Z P) (X ~ bind_sub T1 ++ G) ++ E).
eapply subqtype_through_subst_tqt...
Case "sub_qall".
apply (sub_qall L)...
eapply subqual_through_subst_tt...
intros.
rewrite <- subst_tqt_open_qqt...
rewrite <- subst_tqt_open_qqt...
rewrite_env (map (subst_tb Z P) (X ~ bind_qua T1 ++ G) ++ E).
eapply subqtype_through_subst_tqt...
------
clear subqtype_through_subst_tqt.
intros Q E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_tt...
econstructor; eauto using subqual_through_subst_tt...
Qed.
Lemma sub_through_subst_qt : forall Q E F Z S T P,
sub (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual E P Q ->
sub (map (subst_qb Z P) F ++ E) (subst_qt Z P S) (subst_qt Z P T)
with subqtype_through_subst_qqt : forall Q E F Z S T P,
subqtype (F ++ Z ~ bind_qua Q ++ E) S T ->
subqual E P Q ->
subqtype (map (subst_qb Z P) F ++ E) (subst_qqt Z P S) (subst_qqt Z P T).
Proof with
simpl_env;
eauto 4 using wf_typ_subst_qb, wf_env_subst_qb, wf_typ_weaken_head,
subqual_through_subst_qq.
------
clear sub_through_subst_qt.
intros Q E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_qt...
Case "sub_top".
apply sub_top...
Case "sub_refl_tvar".
apply sub_reflexivity...
unsimpl (subst_qt Z P X)...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
exfalso. analyze_binds_uniq H.
SCase "X <> Z".
apply (sub_trans_tvar (subst_qt Z P U))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H...
Case "sub_arrow".
pick fresh x and apply sub_arrow...
rewrite subst_qqt_open_qqt_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb Z P) (x ~ bind_typ T1 ++ G) ++ E).
eapply subqtype_through_subst_qqt...
Case "sub_all".
pick fresh X and apply sub_all...
rewrite subst_qqt_open_tqt_var...
rewrite subst_qqt_open_tqt_var...
rewrite_env (map (subst_qb Z P) (X ~ bind_sub T1 ++ G) ++ E).
eapply subqtype_through_subst_qqt...
Case "sub_qall".
pick fresh X and apply sub_qall...
rewrite subst_qqt_open_qqt_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb Z P) (X ~ bind_qua T1 ++ G) ++ E).
eapply subqtype_through_subst_qqt...
------
clear subqtype_through_subst_qqt.
intros Q E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_qt...
econstructor; eauto using subqual_through_subst_qq...
Qed.
Lemma sub_through_subst_qt_var : forall Q R E F Z S T P,
sub (F ++ Z ~ bind_typ (qtyp_qtyp Q R) ++ E) S T ->
subqual E P Q ->
sub (map (subst_qb Z P) F ++ E) (subst_qt Z P S) (subst_qt Z P T)
with subqtype_through_subst_qqt_var : forall Q R E F Z S T P,
subqtype (F ++ Z ~ bind_typ (qtyp_qtyp Q R) ++ E) S T ->
subqual E P Q ->
subqtype (map (subst_qb Z P) F ++ E) (subst_qqt Z P S) (subst_qqt Z P T).
Proof with
simpl_env;
eauto 4 using wf_typ_subst_qb_var, wf_env_subst_qb_var, wf_typ_weaken_head,
subqual_through_subst_qq_var.
------
clear sub_through_subst_qt_var.
intros Q R E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_typ (qtyp_qtyp Q R) ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_qt...
Case "sub_top".
apply sub_top...
Case "sub_refl_tvar".
apply sub_reflexivity...
unsimpl (subst_qt Z P X)...
Case "sub_trans_tvar".
destruct (X == Z); subst.
SCase "X = Z".
exfalso. analyze_binds_uniq H.
SCase "X <> Z".
apply (sub_trans_tvar (subst_qt Z P U))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H...
Case "sub_arrow".
pick fresh x and apply sub_arrow...
rewrite subst_qqt_open_qqt_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb Z P) (x ~ bind_typ T1 ++ G) ++ E).
eapply subqtype_through_subst_qqt_var...
Case "sub_all".
pick fresh X and apply sub_all...
rewrite subst_qqt_open_tqt_var...
rewrite subst_qqt_open_tqt_var...
rewrite_env (map (subst_qb Z P) (X ~ bind_sub T1 ++ G) ++ E).
eapply subqtype_through_subst_qqt_var...
Case "sub_qall".
pick fresh X and apply sub_qall...
rewrite subst_qqt_open_qqt_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb Z P) (X ~ bind_qua T1 ++ G) ++ E).
eapply subqtype_through_subst_qqt_var...
------
clear subqtype_through_subst_qqt_var.
intros Q R E F Z S T P SsubT PsubQ.
remember (F ++ Z ~ bind_typ (qtyp_qtyp Q R) ++ E) as G.
generalize dependent F.
induction SsubT; intros G EQ; subst; simpl subst_qt...
econstructor; eauto using subqual_through_subst_qq_var...
Qed.
(* ********************************************************************** *)
(* ********************************************************************** *)
Lemma typing_weakening : forall E F G e T,
typing (G ++ E) e T ->
wf_env (G ++ F ++ E) ->
typing (G ++ F ++ E) e T.
Proof with simpl_env;
eauto using wf_typ_weakening,
wf_qtyp_weakening,
wf_qua_weakening,
wf_qtyp_from_wf_env_typ,
wf_typ_from_wf_env_sub,
wf_qua_from_wf_env_qua,
sub_weakening,
subqual_weakening,
subqtype_weakening.
intros E F G e T Typ.
remember (G ++ E) as H.
generalize dependent G.
induction Typ; intros G EQ Ok; subst...
Case "typing_abs".
pick fresh x and apply typing_abs...
lapply (H0 x); [intros K | auto].
rewrite <- app_assoc.
apply (H1 x)...
Case "typing_tabs".
pick fresh X and apply typing_tabs...
lapply (H0 X); [intros K | auto].
rewrite <- app_assoc.
apply (H1 X)...
Case "typing_qabs".
pick fresh X and apply typing_qabs...
lapply (H0 X); [intros K | auto].
rewrite <- app_assoc.
apply (H1 X)...
Case "typing_let".
pick fresh x and apply typing_let...
lapply (H0 x); [intros K | auto].
rewrite <- app_assoc.
eapply H1...
Case "typing_inl".
apply typing_inl...
Case "typing_inr".
apply typing_inr...
Case "typing_case".
pick fresh x and apply typing_case...
SCase "inl branch".
lapply (H0 x); [intros K | auto].
rewrite <- app_assoc.
apply H1...
eassert (M : wf_qtyp (G ++ F ++ E) (qtyp_qtyp _ (typ_sum (qtyp_qtyp Q1 S1) (qtyp_qtyp Q2 S2))))...
assert (J : wf_typ (G ++ F ++ E) (typ_sum (qtyp_qtyp Q1 S1) (qtyp_qtyp Q2 S2)))...
inversion J...
SCase "inr branch".
lapply (H2 x); [intros K | auto].
rewrite <- app_assoc.
apply H3...
Qed.
(* ********************************************************************** *)
Strengthening (6)
Narrowing for typing (7)
Lemma typing_narrowing_sub : forall Q E F X P e T,
sub E P Q ->
typing (F ++ X ~ bind_sub Q ++ E) e T ->
typing (F ++ X ~ bind_sub P ++ E) e T.
Proof with eauto 6 using wf_env_narrowing_sub,
wf_typ_narrowing_sub, wf_qtyp_narrowing_sub, wf_qua_narrowing_sub,
sub_narrowing_sub, subqual_narrowing_sub, subqtype_narrowing_sub.
intros Q E F X P e T PsubQ Typ.
remember (F ++ X ~ bind_sub Q ++ E) as E'.
generalize dependent F.
induction Typ; intros F EQ; subst...
Case "typing_var".
analyze_binds H0...
Case "typing_abs".
pick fresh y and apply typing_abs...
rewrite <- app_assoc.
apply H1...
Case "typing_tabs".
pick fresh y and apply typing_tabs...
rewrite <- app_assoc.
apply H1...
Case "typing_qabs".
pick fresh y and apply typing_qabs...
rewrite <- app_assoc.
apply H1...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite <- app_assoc.
apply H1...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite <- app_assoc.
apply H1...
SCase "inr branch".
rewrite <- app_assoc.
apply H3...
Qed.
Lemma typing_narrowing_qua : forall Q E F X P e T,
subqual E P Q ->
typing (F ++ X ~ bind_qua Q ++ E) e T ->
typing (F ++ X ~ bind_qua P ++ E) e T.
Proof with eauto 6 using wf_env_narrowing_qua,
wf_typ_narrowing_qua, wf_qtyp_narrowing_qua, wf_qua_narrowing_qua,
sub_narrowing_qua, subqual_narrowing_qua, subqtype_narrowing_qua.
intros Q E F X P e T PsubQ Typ.
remember (F ++ X ~ bind_qua Q ++ E) as E'.
generalize dependent F.
induction Typ; intros F EQ; subst...
Case "typing_var".
analyze_binds H0...
Case "typing_abs".
pick fresh y and apply typing_abs...
rewrite <- app_assoc.
apply H1...
Case "typing_tabs".
pick fresh Y and apply typing_tabs...
rewrite <- app_assoc.
apply H1...
Case "typing_qabs".
pick fresh Y and apply typing_qabs...
rewrite <- app_assoc.
apply H1...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite <- app_assoc.
apply H1...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite <- app_assoc.
apply H1...
SCase "inr branch".
rewrite <- app_assoc.
apply H3...
Qed.
Lemma typing_narrowing_typ : forall Q E F X P e T,
subqtype E P Q ->
typing (F ++ X ~ bind_typ Q ++ E) e T ->
typing (F ++ X ~ bind_typ P ++ E) e T.
Proof with eauto 6 using wf_env_narrowing_typ,
wf_typ_narrowing_typ, wf_qtyp_narrowing_typ, wf_qua_narrowing_typ,
sub_narrowing_typ, subqual_narrowing_typ, subqtype_narrowing_typ.
intros Q E F X P e T PsubQ Typ.
remember (F ++ X ~ bind_typ Q ++ E) as E'.
generalize dependent F.
induction Typ; intros F EQ; subst...
Case "typing_var".
analyze_binds H0...
inversion BindsTacVal; subst...
assert (wf_qtyp E P) as WfP... inversion WfP; subst...
eapply typing_sub with (S := (qtyp_qtyp X T))...
econstructor... eapply subqual_reflexivity...
inversion PsubQ; subst.
rewrite_env (empty ++ (F ++ X ~ bind_typ (qtyp_qtyp Q T)) ++ E).
eapply sub_weakening...
simpl_env...
Case "typing_abs".
pick fresh y and apply typing_abs.
eapply subqual_narrowing_typ...
rewrite <- app_assoc.
apply H1...
Case "typing_tabs".
pick fresh Y and apply typing_tabs.
eapply subqual_narrowing_typ...
rewrite <- app_assoc.
apply H1...
Case "typing_qabs".
pick fresh Y and apply typing_qabs.
eapply subqual_narrowing_typ...
rewrite <- app_assoc.
apply H1...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite <- app_assoc.
apply H1...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite <- app_assoc.
apply H1...
SCase "inr branch".
rewrite <- app_assoc.
apply H3...
Qed.
(************************************************************************ *)
Substitution preserves typing (8)
Lemma capture_prediction : forall E u Q U,
value u ->
typing E u (qtyp_qtyp Q U) ->
subqual E (fv_exp_for_qua u) Q.
Proof with eauto using subqual_reflexivity; try discriminate.
intros * Val Typ.
assert (wf_qua E Q) as WfCap.
eapply wf_qua_from_wf_qtyp with (T := U)...
assert (wf_env E) as WfEnv...
dependent induction Typ; try inversion Val; subst; simpl...
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* unshelve epose proof (IHTyp Q1 S1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* unshelve epose proof (IHTyp Q2 S2 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* unshelve epose proof (subqual_regular _ _ _ H) as [? [? ?]]...
unshelve epose proof (IHTyp1 Q1 S1 _ _ _ _)...
unshelve epose proof (IHTyp2 Q2 S2 _ _ _ _)...
eapply subqual_join_split in H as [Sub1 Sub2]...
eapply subqual_join_elim; eapply subqual_transitivity...
Qed.
Lemma subqual_through_subst_qt_covariant : forall Q E F Z R P T,
wf_env (F ++ Z ~ bind_typ T ++ E) ->
wf_qua (F ++ Z ~ bind_typ T ++ E) R ->
subqual E P Q ->
subqual (map (subst_qb Z Q) F ++ E) (subst_qq Z P R) (subst_qq Z Q R).
Proof with eauto 4 using
wf_typ_subst_qb,
wf_typ_subst_tb,
wf_env_subst_qb,
wf_env_subst_tb,
wf_typ_weaken_head,
subqual_reflexivity,
wf_typ_subst_qb_var,
wf_env_subst_qb_var,
wf_qua_subst_qb_var,
wf_qua_strengthening_sub.
intros Q E F Z R P T WfEnv WfR PsubQ.
destruct T as [Qt St]; subst.
dependent induction WfR; simpl...
* destruct (X == Z); subst...
exfalso. analyze_binds_uniq H.
eapply subqual_reflexivity...
replace (qua_fvar X) with (subst_qq Z Q X).
eapply wf_qua_subst_qb_var...
simpl; destruct (X == Z); subst...
intuition.
* destruct (x == Z); subst...
- rewrite_env (empty ++ map (subst_qb Z Q) F ++ E).
eapply subqual_weakening...
- eapply subqual_reflexivity...
analyze_binds H...
destruct T as [Qt' St'].
eapply wf_qua_term_fvar with (T := subst_qqt Z Q (qtyp_qtyp Qt' St')); simpl...
unsimpl (subst_qb Z Q (bind_typ (qtyp_qtyp Qt' St')))...
* eapply subqual_meet_intro...
- eapply subqual_meet_eliml...
eapply wf_qua_subst_qb_var_indep...
- eapply subqual_meet_elimr...
eapply wf_qua_subst_qb_var_indep...
* eapply subqual_join_elim...
- eapply subqual_join_inl...
- eapply subqual_join_inr...
Qed.
Lemma subqual_through_subst_qq_covariant : forall Q E F Z R P T,
wf_env (F ++ Z ~ bind_qua T ++ E) ->
wf_qua (F ++ Z ~ bind_qua T ++ E) R ->
subqual E P Q ->
subqual (map (subst_qb Z Q) F ++ E) (subst_qq Z P R) (subst_qq Z Q R).
Proof with eauto 4 using
wf_typ_subst_qb,
wf_typ_subst_qb_var,
wf_env_subst_qb_var,
wf_qua_subst_qb_var,
wf_typ_subst_qb,
wf_env_subst_qb,
wf_qua_subst_qb,
wf_env_subst_qb,
wf_env_subst_tb,
wf_typ_weaken_head,
subqual_reflexivity,
wf_qua_strengthening_sub.
intros Q E F Z R P T WfEnv WfR PsubQ.
dependent induction WfR; simpl...
* destruct (X == Z); subst...
- rewrite_env (empty ++ map (subst_qb Z Q) F ++ E).
eapply subqual_weakening...
- eapply subqual_reflexivity...
analyze_binds H...
eapply wf_qua_fvar with (R := subst_qq Z Q R)...
* destruct (x == Z); subst...
exfalso. analyze_binds_uniq H.
eapply subqual_reflexivity...
analyze_binds H...
eapply wf_qua_term_fvar with (T := subst_qqt Z Q T0)...
* eapply subqual_meet_intro...
- eapply subqual_meet_eliml...
eapply wf_qua_subst_qb_indep...
- eapply subqual_meet_elimr...
eapply wf_qua_subst_qb_indep...
* eapply subqual_join_elim...
- eapply subqual_join_inl...
- eapply subqual_join_inr...
Qed.
Lemma typing_through_subst_ee : forall Q U E F x T e u,
typing (F ++ x ~ bind_typ (qtyp_qtyp Q U) ++ E) e T ->
typing E u (qtyp_qtyp Q U) ->
value u ->
typing (map (subst_qb x Q) F ++ E) (subst_ee x u Q e) (subst_qqt x Q T).
value u ->
typing E u (qtyp_qtyp Q U) ->
subqual E (fv_exp_for_qua u) Q.
Proof with eauto using subqual_reflexivity; try discriminate.
intros * Val Typ.
assert (wf_qua E Q) as WfCap.
eapply wf_qua_from_wf_qtyp with (T := U)...
assert (wf_env E) as WfEnv...
dependent induction Typ; try inversion Val; subst; simpl...
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* dependent induction H; subst... unshelve epose proof (IHTyp Q1 T1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* unshelve epose proof (IHTyp Q1 S1 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* unshelve epose proof (IHTyp Q2 S2 _ _ _ _)...
eapply subqual_transitivity. eassumption. eauto.
* unshelve epose proof (subqual_regular _ _ _ H) as [? [? ?]]...
unshelve epose proof (IHTyp1 Q1 S1 _ _ _ _)...
unshelve epose proof (IHTyp2 Q2 S2 _ _ _ _)...
eapply subqual_join_split in H as [Sub1 Sub2]...
eapply subqual_join_elim; eapply subqual_transitivity...
Qed.
Lemma subqual_through_subst_qt_covariant : forall Q E F Z R P T,
wf_env (F ++ Z ~ bind_typ T ++ E) ->
wf_qua (F ++ Z ~ bind_typ T ++ E) R ->
subqual E P Q ->
subqual (map (subst_qb Z Q) F ++ E) (subst_qq Z P R) (subst_qq Z Q R).
Proof with eauto 4 using
wf_typ_subst_qb,
wf_typ_subst_tb,
wf_env_subst_qb,
wf_env_subst_tb,
wf_typ_weaken_head,
subqual_reflexivity,
wf_typ_subst_qb_var,
wf_env_subst_qb_var,
wf_qua_subst_qb_var,
wf_qua_strengthening_sub.
intros Q E F Z R P T WfEnv WfR PsubQ.
destruct T as [Qt St]; subst.
dependent induction WfR; simpl...
* destruct (X == Z); subst...
exfalso. analyze_binds_uniq H.
eapply subqual_reflexivity...
replace (qua_fvar X) with (subst_qq Z Q X).
eapply wf_qua_subst_qb_var...
simpl; destruct (X == Z); subst...
intuition.
* destruct (x == Z); subst...
- rewrite_env (empty ++ map (subst_qb Z Q) F ++ E).
eapply subqual_weakening...
- eapply subqual_reflexivity...
analyze_binds H...
destruct T as [Qt' St'].
eapply wf_qua_term_fvar with (T := subst_qqt Z Q (qtyp_qtyp Qt' St')); simpl...
unsimpl (subst_qb Z Q (bind_typ (qtyp_qtyp Qt' St')))...
* eapply subqual_meet_intro...
- eapply subqual_meet_eliml...
eapply wf_qua_subst_qb_var_indep...
- eapply subqual_meet_elimr...
eapply wf_qua_subst_qb_var_indep...
* eapply subqual_join_elim...
- eapply subqual_join_inl...
- eapply subqual_join_inr...
Qed.
Lemma subqual_through_subst_qq_covariant : forall Q E F Z R P T,
wf_env (F ++ Z ~ bind_qua T ++ E) ->
wf_qua (F ++ Z ~ bind_qua T ++ E) R ->
subqual E P Q ->
subqual (map (subst_qb Z Q) F ++ E) (subst_qq Z P R) (subst_qq Z Q R).
Proof with eauto 4 using
wf_typ_subst_qb,
wf_typ_subst_qb_var,
wf_env_subst_qb_var,
wf_qua_subst_qb_var,
wf_typ_subst_qb,
wf_env_subst_qb,
wf_qua_subst_qb,
wf_env_subst_qb,
wf_env_subst_tb,
wf_typ_weaken_head,
subqual_reflexivity,
wf_qua_strengthening_sub.
intros Q E F Z R P T WfEnv WfR PsubQ.
dependent induction WfR; simpl...
* destruct (X == Z); subst...
- rewrite_env (empty ++ map (subst_qb Z Q) F ++ E).
eapply subqual_weakening...
- eapply subqual_reflexivity...
analyze_binds H...
eapply wf_qua_fvar with (R := subst_qq Z Q R)...
* destruct (x == Z); subst...
exfalso. analyze_binds_uniq H.
eapply subqual_reflexivity...
analyze_binds H...
eapply wf_qua_term_fvar with (T := subst_qqt Z Q T0)...
* eapply subqual_meet_intro...
- eapply subqual_meet_eliml...
eapply wf_qua_subst_qb_indep...
- eapply subqual_meet_elimr...
eapply wf_qua_subst_qb_indep...
* eapply subqual_join_elim...
- eapply subqual_join_inl...
- eapply subqual_join_inr...
Qed.
Lemma typing_through_subst_ee : forall Q U E F x T e u,
typing (F ++ x ~ bind_typ (qtyp_qtyp Q U) ++ E) e T ->
typing E u (qtyp_qtyp Q U) ->
value u ->
typing (map (subst_qb x Q) F ++ E) (subst_ee x u Q e) (subst_qqt x Q T).
We provide detailed comments for the following proof, mainly to
point out several useful tactics and proof techniques.
Starting a proof with "Proof with <some tactic>" allows us to
specify a default tactic that should be used to solve goals. To
invoke this default tactic at the end of a proof step, we signal
the end of the step with three periods instead of a single one,
e.g., "apply typing_weakening...".
Proof with simpl_env;
eauto 4 using
wf_env_subst_qb_var,
qual_from_wf_qua,
qual_from_typing_qtyp,
subqual_reflexivity,
wf_qua_weakening,
wf_qua_narrowing_qua,
wf_qua_narrowing_sub,
wf_qua_narrowing_typ,
wf_qtyp_subst_qb_var,
wf_typ_weakening,
wf_typ_narrowing_qua,
wf_typ_narrowing_sub,
wf_typ_narrowing_typ,
wf_qtyp_weakening,
wf_qtyp_narrowing_qua,
wf_qtyp_narrowing_sub,
wf_qtyp_narrowing_typ,
wf_env_narrowing_qua,
wf_env_narrowing_sub,
wf_env_narrowing_typ,
subqual_weakening,
subqual_narrowing_qua,
subqual_narrowing_sub,
subqual_narrowing_typ,
sub_weakening,
sub_narrowing_qua,
sub_narrowing_sub,
sub_narrowing_typ,
subqtype_weakening,
subqtype_narrowing_qua,
subqtype_narrowing_sub,
subqtype_narrowing_typ,
typing_weakening,
typing_narrowing_qua,
typing_narrowing_sub,
typing_narrowing_typ,
typing_regular;
try discriminate.
intros Q U E F x T e u TypT TypU ValueU.
remember (F ++ x ~ bind_typ (qtyp_qtyp Q U) ++ E) as E'.
assert (wf_qtyp E (qtyp_qtyp Q U)) as WfQT...
assert (wf_qua E Q) as WfQ...
assert (typing E' e T) as TypT'...
assert (wf_env E') as WfEnv...
generalize dependent F.
induction TypT; intros F EQ; subst; simpl subst_ee...
Case "typing_var".
destruct (x0 == x); try subst x0.
SCase "x0 = x".
analyze_binds_uniq H0.
injection BindsTacVal; intros; subst.
assert (x `notin` fv_qq Q).
eapply (notin_fv_qq_wf_qua) with (E := E);
destruct (typing_regular E u (qtyp_qtyp Q U))
as [_ [?]]...
assert (x `notin` fv_qt U).
eapply (notin_fv_qt_wf_typ) with (E := E);
destruct (typing_regular E u (qtyp_qtyp Q U))
as [_ [?]]...
simpl subst_qqt...
rewrite <- subst_qt_fresh...
rewrite_env (empty ++ (map (subst_qb x Q) F ++ E)).
apply typing_weakening...
destruct (x == x)...
exfalso...
SCase "x0 <> x".
analyze_binds H0; simpl subst_qqt;
destruct (x0 == x); subst;
try contradiction.
eapply typing_var with (Q := (subst_qq x Q Q0))...
destruct (typing_regular E u (qtyp_qtyp Q U))
as [_ [?]]...
unsimpl (subst_qb x Q (bind_typ (qtyp_qtyp Q0 S)))...
eapply typing_var with (Q := (subst_qq x Q Q0))...
destruct (typing_regular E u (qtyp_qtyp Q U))
as [_ [?]]...
unsimpl (subst_qb x Q (bind_typ (qtyp_qtyp Q0 S)))...
rewrite (map_subst_qb_id E x Q);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds_uniq BindsTac0...
Case "typing_abs".
simpl subst_qqt...
pick fresh y and apply typing_abs.
unshelve epose proof (capture_prediction _ _ _ _ _ TypU)
as CapU...
rewrite fv_exp_for_qua_through_subst_ee at 1.
eapply subqual_transitivity with (Q := subst_qq x Q (fv_exp_for_qua e1))...
eapply subqual_through_subst_qt_covariant with (T := qtyp_qtyp Q U)...
eapply subqual_through_subst_qq_var...
rewrite subst_ee_open_ee_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb x Q) (y ~ bind_typ V ++ F) ++ E).
apply H1...
econstructor...
destruct (typing_regular _ _ _ TypT') as [? [? WfQT']]...
inversion WfQT'; subst...
inversion H8...
Case "typing_app".
unshelve epose proof (IHTypT1 _ _) as IHTypT3...
simpl in IHTypT3.
rewrite subst_qqt_open_qqt...
Case "typing_tabs".
simpl subst_qqt...
simpl; pick fresh Y and apply typing_tabs.
unshelve epose proof (capture_prediction _ _ _ _ _ TypU)
as CapU...
rewrite fv_exp_for_qua_through_subst_ee at 1.
eapply subqual_transitivity with (Q := subst_qq x Q (fv_exp_for_qua e1))...
eapply subqual_through_subst_qt_covariant with (T := qtyp_qtyp Q U)...
eapply subqual_through_subst_qq_var...
rewrite subst_ee_open_te_var...
rewrite subst_qqt_open_tqt_var...
rewrite_env (map (subst_qb x Q) (Y ~ bind_sub V ++ F) ++E).
apply H1...
econstructor...
destruct (typing_regular _ _ _ TypT') as [? [? WfQT']]...
inversion WfQT'; subst...
inversion H8...
Case "typing_tapp".
rewrite subst_qqt_open_tqt...
eapply typing_tapp with (T1 := (subst_qt x Q T1))...
eapply sub_through_subst_qt_var...
Case "typing_qabs".
simpl subst_qqt...
simpl; pick fresh Y and apply typing_qabs.
unshelve epose proof (capture_prediction _ _ _ _ _ TypU)
as CapU...
rewrite fv_exp_for_qua_through_subst_ee at 1.
eapply subqual_transitivity with (Q := subst_qq x Q (fv_exp_for_qua e1))...
eapply subqual_through_subst_qt_covariant with (T := qtyp_qtyp Q U)...
eapply subqual_through_subst_qq_var...
rewrite subst_ee_open_qe_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb x Q) (Y ~ bind_qua Q0 ++ F) ++ E).
apply H1...
econstructor...
destruct (typing_regular _ _ _ TypT') as [? [? WfQT']]...
inversion WfQT'; subst...
inversion H8...
Case "typing_qapp".
rewrite subst_qqt_open_qqt...
eapply typing_qapp with (Q1 := (subst_qq x Q Q1))...
eapply subqual_through_subst_qq_var...
Case "typing_sub".
econstructor...
eapply subqtype_through_subst_qqt_var...
Case "typing_let".
unshelve epose proof (IHTypT _ _) as IHTypT2...
pick fresh y and apply typing_let...
repeat (fold subst_qt; fold subst_qqt)...
rewrite subst_ee_open_ee_var...
rewrite_env (map (subst_qb x Q) (y ~ bind_typ (qtyp_qtyp Q0 S) ++ F) ++ E).
apply H1...
Case "typing_inl".
unshelve epose proof (IHTypT _ _) as IHTypT2...
simpl.
apply typing_inl...
eapply subqual_through_subst_qq_var...
Case "typing_inr".
unshelve epose proof (IHTypT _ _) as IHTypT2...
simpl.
apply typing_inr...
eapply subqual_through_subst_qq_var...
Case "typing_case".
unshelve epose proof (IHTypT _ _) as IHTypT2...
pick fresh y and apply typing_case.
eapply IHTypT...
eapply wf_qtyp_subst_qb_var...
repeat (fold subst_qt; fold subst_qqt).
rewrite subst_ee_open_ee_var...
rewrite_env (map (subst_qb x Q) (y ~ bind_typ (qtyp_qtyp Q1 S1) ++ F) ++ E).
eapply H1...
econstructor...
destruct (typing_regular _ _ _ TypT) as [? [? WfQT']]...
inversion WfQT'; subst...
inversion H10...
repeat (fold subst_qt; fold subst_qqt).
rewrite subst_ee_open_ee_var...
rewrite_env (map (subst_qb x Q) (y ~ bind_typ (qtyp_qtyp Q2 S2) ++ F) ++ E).
eapply H3...
econstructor...
destruct (typing_regular _ _ _ TypT) as [? [? WfQT']]...
inversion WfQT'; subst...
inversion H10...
Case "typing_pair".
unshelve epose proof (IHTypT1 _ _) as IHTypT3...
eassert (wf_qtyp _ (qtyp_qtyp Q2 S2))...
eassert (wf_qua _ Q2)...
eassert (wf_qtyp _ (qtyp_qtyp Q1 S1))...
eassert (wf_qua _ Q1)...
simpl... eapply typing_pair...
unsimpl (subst_qq x Q (qua_join Q1 Q2)).
eapply subqual_through_subst_qq_var...
Case "typing_first".
simpl; eapply typing_first with (T2 := (subst_qqt x Q T2))...
Case "typing_second".
simpl; eapply typing_second with (T1 := (subst_qqt x Q T1))...
Case "typing_upqual".
simpl; eapply typing_upqual...
eapply subqual_through_subst_qq_var...
Case "typing_check".
simpl; eapply typing_check...
eapply subqual_through_subst_qq_var...
Qed.
(************************************************************************ *)
Lemma typing_through_subst_te : forall Q E F Z e T P,
typing (F ++ Z ~ bind_sub Q ++ E) e T ->
sub E P Q ->
typing (map (subst_tb Z P) F ++ E) (subst_te Z P e) (subst_tqt Z P T).
Proof with simpl_env;
eauto 6 using wf_env_subst_tb,
wf_typ_subst_tb,
wf_qua_subst_tb,
wf_qtyp_subst_tb,
sub_through_subst_tt,
subqtype_through_subst_tqt,
subqual_through_subst_tt.
intros Q E F Z e T P Typ PsubQ.
remember (F ++ Z ~ bind_sub Q ++ E) as G.
generalize dependent F.
assert (wf_env G) as WfEnv...
induction Typ; intros F EQ; subst;
simpl subst_te in *; simpl subst_tt in *;
simpl subst_tqt in *...
Case "typing_var".
eapply typing_var with (Q := Q0)...
rewrite (map_subst_tb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
unsimpl (subst_tb Z P (bind_typ (qtyp_qtyp Q0 S))).
analyze_binds H0...
Case "typing_abs".
pick fresh y and apply typing_abs.
rewrite <- (fv_exp_for_qua_subst_te_intro Z P e1)...
rewrite subst_te_open_ee_var...
rewrite subst_tqt_open_qqt_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_typ V ++ F) ++ E).
apply H1...
unshelve epose proof (H0 y _)...
Case "typing_app".
rewrite subst_tqt_open_qqt...
Case "typing_tabs".
pick fresh y and apply typing_tabs.
rewrite <- (fv_exp_for_qua_subst_te_intro Z P e1)...
rewrite subst_te_open_te_var...
rewrite subst_tqt_open_tqt_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_sub V ++ F) ++ E).
apply H1...
unshelve epose proof (H0 y _)...
Case "typing_tapp".
rewrite subst_tqt_open_tqt...
Case "typing_qabs".
pick fresh y and apply typing_qabs.
rewrite <- (fv_exp_for_qua_subst_te_intro Z P e1)...
rewrite subst_te_open_qe_var...
rewrite subst_tqt_open_qqt_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_qua Q0 ++ F) ++ E).
apply H1...
unshelve epose proof (H0 y _)...
Case "typing_qapp".
rewrite subst_tqt_open_qqt...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite subst_te_open_ee_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_typ (qtyp_qtyp Q0 S) ++ F) ++ E).
apply H1...
Case "typing_inl".
eapply typing_inl...
Case "typing_inr".
eapply typing_inr...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite subst_te_open_ee_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_typ (qtyp_qtyp Q1 S1) ++ F) ++ E).
apply H1...
unshelve epose proof (H0 y _)...
SCase "inr branch".
rewrite subst_te_open_ee_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_typ (qtyp_qtyp Q2 S2) ++ F) ++ E).
apply H3...
unshelve epose proof (H2 y _)...
Qed.
Lemma fv_exp_for_qua_through_subst_qq : forall X Q e,
X `notin` fv_qq (fv_exp_for_qua e) ->
(fv_exp_for_qua (subst_qe X Q e)) = (subst_qq X Q (fv_exp_for_qua e)).
Proof with eauto;
intros.
(*** this proof is cursed ****)
dependent induction e; simpl in *...
* destruct (a == X); subst...
exfalso. fsetdec.
* f_equal...
* f_equal...
* f_equal; simpl...
rewrite IHe2... rewrite IHe3...
* f_equal; simpl...
* f_equal...
Qed.
Lemma notin_fv_exp_qua_open_ee : forall Z e k x,
Z <> x ->
Z `notin` fv_qq (fv_exp_for_qua (open_ee_rec k x x e)) ->
Z `notin` fv_qq (fv_exp_for_qua e).
Proof with eauto.
intros. generalize dependent k.
induction e; simpl...
Qed.
Lemma notin_fv_exp_qua_open_te : forall Z e k X,
Z `notin` fv_qq (fv_exp_for_qua (open_te_rec k X e)) ->
Z `notin` fv_qq (fv_exp_for_qua e).
Proof with eauto.
intros. generalize dependent k.
induction e; simpl...
Qed.
Lemma notin_fv_exp_qua_open_qe : forall Z e k X,
Z <> X ->
Z `notin` fv_qq (fv_exp_for_qua (open_qe_rec k X e)) ->
Z `notin` fv_qq (fv_exp_for_qua e).
Proof with eauto.
intros. generalize dependent k.
induction e; simpl...
Qed.
Lemma qualifier_variables_are_not_term_variables : forall Z Q E e T,
typing E e T ->
binds Z (bind_qua Q) E ->
Z `notin` fv_qq (fv_exp_for_qua e).
Proof with eauto.
intros * Typ Binds.
induction Typ; simpl...
* destruct (x == Z); subst...
exfalso. eapply binds_unique in H0...
inversion H0...
* (* needs notin_fv lemma *)
pick fresh x.
eapply notin_fv_exp_qua_open_ee with (k := 0) (x := x)...
* (* needs notin_fv lemma *)
pick fresh X.
eapply notin_fv_exp_qua_open_te with (k := 0) (X := X)...
* (* needs notin_fv lemma *)
pick fresh X.
eapply notin_fv_exp_qua_open_qe with (k := 0) (X := X)...
* (* needs notin_fv lemma *)
pick fresh x.
unshelve epose proof (notin_fv_exp_qua_open_ee Z e2 0 x _ _).
fsetdec.
apply H1...
unshelve epose proof (IHTyp _)...
* (* needs notin_fv lemma *)
pick fresh x.
unshelve epose proof (notin_fv_exp_qua_open_ee Z e2 0 x _ _).
fsetdec.
apply H1...
unshelve epose proof (notin_fv_exp_qua_open_ee Z e3 0 x _ _).
clear H4. fsetdec.
apply H3...
unshelve epose proof (IHTyp _)...
Qed.
Lemma typing_through_subst_qe : forall Q E F Z e T P,
typing (F ++ Z ~ bind_qua Q ++ E) e T ->
subqual E P Q ->
typing (map (subst_qb Z P) F ++ E) (subst_qe Z P e) (subst_qqt Z P T).
Proof with simpl_env;
eauto 6 using wf_env_subst_qb,
wf_typ_subst_qb,
wf_qua_subst_qb,
wf_qtyp_subst_qb,
sub_through_subst_qt,
subqtype_through_subst_qqt,
subqual_through_subst_qq.
intros Q E F Z e T P Typ PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as E'.
assert (wf_qua E Q) as WfQ...
assert (typing E' e T) as TypT'...
assert (wf_env E') as WfEnv...
generalize dependent F.
induction Typ; intros F EQ; subst;
simpl subst_qe in *; simpl subst_qt in *;
simpl subst_qqt in *...
Case "typing_var".
destruct (x == Z); subst.
SCase "x = Z".
analyze_binds_uniq H0.
SCase "x <> Z".
eapply typing_var with (Q := (subst_qq Z P Q0))...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
unsimpl (subst_qb Z P (bind_typ (qtyp_qtyp Q0 S))).
analyze_binds H0...
Case "typing_abs".
pick fresh y and apply typing_abs.
destruct (typing_regular _ _ _ TypT') as [? [? ?]]...
rewrite (fv_exp_for_qua_through_subst_qq Z P e1)...
replace (fv_exp_for_qua e1) with (fv_exp_for_qua (exp_abs P0 V e1))...
eapply qualifier_variables_are_not_term_variables...
rewrite subst_qe_open_ee_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb Z P) (y ~ bind_typ V ++ F) ++ E).
apply H1...
unshelve epose proof (H0 y _)...
Case "typing_app".
rewrite subst_qqt_open_qqt...
Case "typing_tabs".
pick fresh Y and apply typing_tabs.
destruct (typing_regular _ _ _ TypT') as [? [? ?]]...
rewrite (fv_exp_for_qua_through_subst_qq Z P e1)...
replace (fv_exp_for_qua e1) with (fv_exp_for_qua (exp_tabs P0 V e1))...
eapply qualifier_variables_are_not_term_variables...
rewrite subst_qe_open_te_var...
rewrite subst_qqt_open_tqt_var...
rewrite_env (map (subst_qb Z P) (Y ~ bind_sub V ++ F) ++ E).
apply H1...
unshelve epose proof (H0 Y _)...
Case "typing_tapp".
rewrite subst_qqt_open_tqt...
Case "typing_qabs".
pick fresh Y and apply typing_qabs.
destruct (typing_regular _ _ _ TypT') as [? [? ?]]...
rewrite (fv_exp_for_qua_through_subst_qq Z P e1)...
replace (fv_exp_for_qua e1) with (fv_exp_for_qua (exp_qabs P0 Q0 e1))...
eapply qualifier_variables_are_not_term_variables...
rewrite subst_qe_open_qe_var...
rewrite subst_qqt_open_qqt_var...
rewrite_env (map (subst_qb Z P) (Y ~ bind_qua Q0 ++ F) ++ E).
apply H1...
unshelve epose proof (H0 Y _)...
Case "typing_qapp".
rewrite subst_qqt_open_qqt...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite subst_qe_open_ee_var...
rewrite_env (map (subst_qb Z P) (y ~ bind_typ (qtyp_qtyp Q0 S) ++ F) ++ E).
apply H1...
Case "typing_inl".
eapply typing_inl...
Case "typing_inr".
eapply typing_inr...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite subst_qe_open_ee_var...
rewrite_env (map (subst_qb Z P) (y ~ bind_typ (qtyp_qtyp Q1 S1) ++ F) ++ E).
apply H1...
unshelve epose proof (H0 y _)...
SCase "inr branch".
rewrite subst_qe_open_ee_var...
rewrite_env (map (subst_qb Z P) (y ~ bind_typ (qtyp_qtyp Q2 S2) ++ F) ++ E).
apply H3...
unshelve epose proof (H2 y _)...
Case "typing_pair".
apply typing_pair...
unsimpl (subst_qq Z P (qua_join Q1 Q2))...
Qed.
(* ********************************************************************** *)
(* ********************************************************************** *)
Lemma typing_inv_abs : forall E P S1 e1 T,
typing E (exp_abs P S1 e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_arrow U1 U2)) ->
subqtype E U1 S1
/\ exists S2, exists L, forall x, x `notin` L ->
typing (x ~ bind_typ S1 ++ E) (open_ee e1 x x) (open_qqt S2 x)
/\ subqtype (x ~ bind_typ U1 ++ E) (open_qqt S2 x) (open_qqt U2 x)
/\ subqual E P Q.
Proof with auto.
intros E P S1 e1 T Typ.
remember (exp_abs P S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1' b1 EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_abs".
inversion Sub; subst.
inversion select (sub _ (typ_arrow _ _) (typ_arrow _ _)); subst.
split...
exists T1. exists (L `union` L0)...
Case "typing_sub".
eapply IHTyp with (Q := Q')...
auto using (subqtype_transitivity T).
Qed.
Lemma typing_canonical_abs_rec : forall E P V e1 Qt Q T,
typing E (exp_abs P V e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E (exp_abs P V e1) (qtyp_qtyp P (typ_arrow U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_arrow U1 U2)) Qt /\
subqual E (fv_exp_for_qua e1) P.
Proof with eauto using subqtype_reflexivity.
intros * Typ Sub.
assert (wf_env E)...
dependent induction Typ...
Case "typing_abs".
inversion Sub; subst...
exists V. exists T1; split...
econstructor...
Case "typing_sub".
destruct (IHTyp P V e1) as [U1 [U2 [Typ' [Sub' SubQ']]]]...
eapply subqtype_transitivity...
exists U1. exists U2; repeat split...
eapply subqtype_transitivity...
Qed.
Lemma typing_canonical_abs : forall E P V e1 Q T,
typing E (exp_abs P V e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E (exp_abs P V e1) (qtyp_qtyp P (typ_arrow U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_arrow U1 U2)) (qtyp_qtyp Q T) /\
subqual E (fv_exp_for_qua e1) P.
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_abs_rec...
Qed.
Lemma typing_inv_tabs : forall E P S1 e1 T,
typing E (exp_tabs P S1 e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_all U1 U2)) ->
sub E U1 S1
/\ exists S2, exists L, forall X, X `notin` L ->
typing (X ~ bind_sub U1 ++ E) (open_te e1 X) (open_tqt S2 X)
/\ subqtype (X ~ bind_sub U1 ++ E) (open_tqt S2 X) (open_tqt U2 X)
/\ subqual E P Q.
Proof with simpl_env; auto.
intros E P S1 e1 T Typ.
remember (exp_tabs P S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1' e0 EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_tabs".
inversion Sub; subst.
inversion select (sub _ (typ_all _ _) (typ_all _ _)); subst.
split...
exists T1.
exists (L0 `union` L).
intros Y Fr.
split...
rewrite_env (empty ++ Y ~ bind_sub U1 ++ E).
apply (typing_narrowing_sub S1')...
Case "typing_sub".
eapply IHTyp with (Q := Q')...
auto using (subqtype_transitivity T).
Qed.
Lemma typing_inv_tabs_wide : forall E P S1 e1 T,
typing E (exp_tabs P S1 e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_all U1 U2)) ->
sub E U1 S1
/\ exists S2, exists L, forall X, X `notin` L ->
typing (X ~ bind_sub S1 ++ E) (open_te e1 X) (open_tqt S2 X)
/\ subqtype (X ~ bind_sub U1 ++ E) (open_tqt S2 X) (open_tqt U2 X)
/\ subqual E P Q.
Proof with simpl_env; auto.
intros E P S1 e1 T Typ.
remember (exp_tabs P S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1' e0 EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_tabs".
inversion Sub; subst.
inversion select (sub _ (typ_all _ _) (typ_all _ _)); subst.
split...
exists T1.
exists (L0 `union` L).
intros Y Fr.
split...
Case "typing_sub".
eapply IHTyp with (Q := Q')...
auto using (subqtype_transitivity T).
Qed.
Lemma typing_canonical_tabs_rec : forall E P S1 e1 Qt Q T,
typing E (exp_tabs P S1 e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E (exp_tabs P S1 e1) (qtyp_qtyp P (typ_all U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_all U1 U2)) Qt /\
subqual E (fv_exp_for_qua e1) P.
Proof with eauto using subqtype_reflexivity.
intros * Typ Sub.
assert (wf_env E)...
dependent induction Typ...
Case "typing_abs".
inversion Sub; subst...
exists S1. exists T1; split...
econstructor...
Case "typing_sub".
destruct (IHTyp P S1 e1) as [U1 [U2 [Typ' [Sub' SubQ']]]]...
eapply subqtype_transitivity...
exists U1. exists U2; repeat split...
eapply subqtype_transitivity...
Qed.
Lemma typing_canonical_tabs : forall E P S1 e1 Q T,
typing E (exp_tabs P S1 e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E (exp_tabs P S1 e1) (qtyp_qtyp P (typ_all U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_all U1 U2)) (qtyp_qtyp Q T) /\
subqual E (fv_exp_for_qua e1) P.
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_tabs_rec...
Qed.
Lemma typing_inv_qabs : forall E P S1 e1 T,
typing E (exp_qabs P S1 e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_qall U1 U2)) ->
subqual E U1 S1
/\ exists S2, exists L, forall X, X `notin` L ->
typing (X ~ bind_qua U1 ++ E) (open_qe e1 X) (open_qqt S2 X)
/\ subqtype (X ~ bind_qua U1 ++ E) (open_qqt S2 X) (open_qqt U2 X)
/\ subqual E P Q.
Proof with simpl_env; auto.
intros E P S1 e1 T Typ.
remember (exp_qabs P S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1' e0 EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_qabs".
inversion Sub; subst.
inversion select (sub _ (typ_qall _ _) (typ_qall _ _)); subst.
split...
exists T1.
exists (L0 `union` L).
intros Y Fr.
split...
rewrite_env (empty ++ Y ~ bind_qua U1 ++ E).
apply (typing_narrowing_qua S1')...
Case "typing_sub".
eapply IHTyp with (Q := Q')...
auto using (subqtype_transitivity T).
Qed.
Lemma typing_inv_qabs_wide : forall E P S1 e1 T,
typing E (exp_qabs P S1 e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_qall U1 U2)) ->
subqual E U1 S1
/\ exists S2, exists L, forall X, X `notin` L ->
typing (X ~ bind_qua S1 ++ E) (open_qe e1 X) (open_qqt S2 X)
/\ subqtype (X ~ bind_qua U1 ++ E) (open_qqt S2 X) (open_qqt U2 X)
/\ subqual E P Q.
Proof with simpl_env; auto.
intros E P S1 e1 T Typ.
remember (exp_qabs P S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
induction Typ; intros S1' e0 EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_qabs".
inversion Sub; subst.
inversion select (sub _ (typ_qall _ _) (typ_qall _ _)); subst.
split...
exists T1.
exists (L0 `union` L).
intros Y Fr.
split...
Case "typing_sub".
eapply IHTyp with (Q := Q')...
auto using (subqtype_transitivity T).
Qed.
Lemma typing_canonical_qabs_rec : forall E P S1 e1 Qt Q T,
typing E (exp_qabs P S1 e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E (exp_qabs P S1 e1) (qtyp_qtyp P (typ_qall U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_qall U1 U2)) Qt /\
subqual E (fv_exp_for_qua e1) P.
Proof with eauto using subqtype_reflexivity.
intros * Typ Sub.
assert (wf_env E)...
dependent induction Typ...
Case "typing_abs".
inversion Sub; subst...
exists S1. exists T1; split...
econstructor...
Case "typing_sub".
destruct (IHTyp P S1 e1) as [U1 [U2 [Typ' [Sub' SubQ']]]]...
eapply subqtype_transitivity...
exists U1. exists U2; repeat split...
eapply subqtype_transitivity...
Qed.
Lemma typing_canonical_qabs : forall E P S1 e1 Q T,
typing E (exp_qabs P S1 e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E (exp_qabs P S1 e1) (qtyp_qtyp P (typ_qall U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_qall U1 U2)) (qtyp_qtyp Q T) /\
subqual E (fv_exp_for_qua e1) P.
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_qabs_rec...
Qed.
Lemma typing_inv_inl : forall E P e1 T,
typing E (exp_inl P e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_sum U1 U2)) ->
exists S1, typing E e1 S1 /\ subqtype E S1 U1 /\ subqual E P Q.
Proof with eauto.
intros E P e1 T Typ.
remember (exp_inl P e1) as e. generalize dependent e1.
induction Typ; intros e' EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_sub".
eauto using (subqtype_transitivity T).
Case "typing_inl".
inversion Sub; subst...
inversion select (sub _ (typ_sum _ _) (typ_sum _ _))...
Qed.
Lemma typing_canonical_inl_rec : forall E P e1 Qt Q T,
typing E (exp_inl P e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2 U3,
typing E (exp_inl P e1) (qtyp_qtyp P (typ_sum (qtyp_qtyp U3 U1) U2)) /\
subqtype E (qtyp_qtyp P (typ_sum (qtyp_qtyp U3 U1) U2)) Qt /\
subqual E U3 P.
Proof with eauto using subqtype_reflexivity.
intros * Typ Sub.
assert (wf_env E)...
dependent induction Typ...
Case "typing_sub".
destruct (IHTyp P e1) as [U1 [U2 [U3 [Typ' [Sub' SubQ]]]]]...
eapply subqtype_transitivity...
exists U1. exists U2. exists U3. repeat split...
eapply subqtype_transitivity...
Case "typing_inl".
inversion Sub; subst...
exists S1. exists T2. exists Q1. split...
Qed.
Lemma typing_canonical_inl : forall E P e1 Q T,
typing E (exp_inl P e1) (qtyp_qtyp Q T) ->
exists U1 U2 U3,
typing E (exp_inl P e1) (qtyp_qtyp P (typ_sum (qtyp_qtyp U3 U1) U2)) /\
subqtype E (qtyp_qtyp P (typ_sum (qtyp_qtyp U3 U1) U2)) (qtyp_qtyp Q T) /\
subqual E U3 P.
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_inl_rec...
Qed.
Lemma typing_inv_inr : forall E P e1 T,
typing E (exp_inr P e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_sum U1 U2)) ->
exists S1, typing E e1 S1 /\ subqtype E S1 U2 /\ subqual E P Q.
Proof with eauto.
intros E P e1 T Typ.
remember (exp_inr P e1) as e. generalize dependent e1.
induction Typ; intros e' EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_sub".
eauto using (subqtype_transitivity T).
Case "typing_inr".
inversion Sub; subst...
inversion select (sub _ (typ_sum _ _) (typ_sum _ _))...
Qed.
Lemma typing_canonical_inr_rec : forall E P e1 Qt Q T,
typing E (exp_inr P e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2 U3,
typing E (exp_inr P e1) (qtyp_qtyp P (typ_sum U1 (qtyp_qtyp U3 U2))) /\
subqtype E (qtyp_qtyp P (typ_sum U1 (qtyp_qtyp U3 U2))) Qt /\
subqual E U3 P.
Proof with eauto using subqtype_reflexivity.
intros * Typ Sub.
assert (wf_env E)...
dependent induction Typ...
Case "typing_sub".
destruct (IHTyp P e1) as [U1 [U2 [U3 [Typ' [Sub' SubQ]]]]]...
eapply subqtype_transitivity...
exists U1. exists U2. exists U3. repeat split...
eapply subqtype_transitivity...
Case "typing_inr".
inversion Sub; subst...
exists T1. exists S2. exists Q2. repeat split...
eapply subqual_reflexivity...
Qed.
Lemma typing_canonical_inr : forall E P e1 Q T,
typing E (exp_inr P e1) (qtyp_qtyp Q T) ->
exists U1 U2 U3,
typing E (exp_inr P e1) (qtyp_qtyp P (typ_sum U1 (qtyp_qtyp U3 U2))) /\
subqtype E (qtyp_qtyp P (typ_sum U1 (qtyp_qtyp U3 U2))) (qtyp_qtyp Q T) /\
subqual E U3 P.
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_inr_rec...
Qed.
Lemma typing_inv_pair : forall E P e1 e2 T,
typing E (exp_pair P e1 e2) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_pair U1 U2)) ->
exists S1 S2, typing E e1 S1 /\ subqtype E S1 U1 /\
typing E e2 S2 /\ subqtype E S2 U2 /\ subqual E P Q.
Proof with eauto.
intros E P e1 e2 T Typ.
remember (exp_pair P e1 e2) as e. generalize dependent e1. generalize dependent e2.
induction Typ; intros e2' e1' EQ Q' U1 U2 Sub; inversion EQ; subst.
Case "typing_sub".
eauto using (subqtype_transitivity T).
Case "typing_inr".
inversion Sub; subst...
inversion select (sub _ (typ_pair _ _) (typ_pair _ _)); subst...
exists (qtyp_qtyp Q1 S1). exists (qtyp_qtyp Q2 S2) ...
Qed.
Lemma typing_canonical_pair_rec : forall E P e1 e2 Qt Q T,
typing E (exp_pair P e1 e2) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2 U3 U4,
typing E (exp_pair P e1 e2) (qtyp_qtyp P (typ_pair (qtyp_qtyp U3 U1) (qtyp_qtyp U4 U2)))
/\
subqtype E (qtyp_qtyp P (typ_pair (qtyp_qtyp U3 U1) (qtyp_qtyp U4 U2))) Qt
/\
subqual E (qua_join U3 U4) P.
Proof with eauto using subqtype_reflexivity.
intros * Typ Sub.
assert (wf_env E)...
dependent induction Typ...
Case "typing_sub".
destruct (IHTyp P e1 e2) as [U1 [U2 [U3 [U4 [Typ' [Sub' SubQ]]]]]]...
eapply subqtype_transitivity...
exists U1. exists U2. exists U3. exists U4. repeat split...
eapply subqtype_transitivity...
Case "typing_pair".
inversion Sub; subst...
exists S1. exists S2. exists Q1. exists Q2.
repeat split...
eapply subqual_reflexivity...
Qed.
Lemma typing_canonical_pair : forall E P e1 e2 Q T,
typing E (exp_pair P e1 e2) (qtyp_qtyp Q T) ->
exists U1 U2 U3 U4,
typing E (exp_pair P e1 e2) (qtyp_qtyp P (typ_pair (qtyp_qtyp U3 U1) (qtyp_qtyp U4 U2)))
/\
subqtype E (qtyp_qtyp P (typ_pair (qtyp_qtyp U3 U1) (qtyp_qtyp U4 U2))) (qtyp_qtyp Q T)
/\
subqual E (qua_join U3 U4) P.
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_pair_rec...
Qed.
(* ********************************************************************** *)
Lemma concrete_sub_qualifier : forall E Q s,
concretize Q = Some s ->
wf_env E ->
wf_qua E Q ->
subqual E (abstractize s) Q.
Proof with eauto.
intros * Eq WfE WfQ.
induction WfQ; simpl in *;
try inversion select (Some _ = Some _); subst; simpl in *...
- exfalso. inversion Eq.
- exfalso. inversion Eq.
- destruct (concretize Q1) eqn:HQ1;
destruct (concretize Q2) eqn:HQ2;
simpl in *;
try destruct c eqn:Hs0; subst; simpl in *;
try destruct c0 eqn:Hs1; subst; simpl in *;
inversion Eq; subst; simpl in *...
- destruct (concretize Q1) eqn:HQ1;
destruct (concretize Q2) eqn:HQ2;
simpl in *;
try destruct c eqn:Hs0; subst; simpl in *;
try destruct c0 eqn:Hs1; subst; simpl in *;
inversion Eq; subst; simpl in *...
Qed.
Lemma qualifier_sub_concrete : forall E Q s,
concretize Q = Some s ->
wf_env E ->
wf_qua E Q ->
subqual E Q (abstractize s).
Proof with eauto.
intros * Eq WfE WfQ.
induction WfQ; simpl in *;
try inversion select (Some _ = Some _); subst; simpl in *...
- exfalso. inversion Eq.
- exfalso. inversion Eq.
- destruct (concretize Q1) eqn:HQ1;
destruct (concretize Q2) eqn:HQ2;
simpl in *;
try destruct c eqn:Hs0; subst; simpl in *;
try destruct c0 eqn:Hs1; subst; simpl in *;
inversion Eq; subst; simpl in *...
- destruct (concretize Q1) eqn:HQ1;
destruct (concretize Q2) eqn:HQ2;
simpl in *;
try destruct c eqn:Hs0; subst; simpl in *;
try destruct c0 eqn:Hs1; subst; simpl in *;
inversion Eq; subst; simpl in *...
Qed.
Lemma subqual_compatible : forall s t,
subqual empty (abstractize s) (abstractize t) ->
s ≤ t.
Proof with eauto.
intros.
destruct s; destruct t...
simpl in *. dependent induction H...
Qed.
Lemma subqual_implies_compatible : forall P Q c d,
subqual empty P Q ->
concretize P = Some c ->
concretize Q = Some d ->
cqua_compatible c d.
Proof with eauto.
intros * Sub EqP EqQ.
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P).
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := Q)...
eapply qualifier_sub_concrete...
Qed.
(* ********************************************************************** *)
Lemma preservation : forall E e e' T,
typing E e T ->
red e e' ->
typing E e' T.
Proof with simpl_env; eauto.
intros E e e' T Typ. generalize dependent e'.
induction Typ; intros e' Red; try solve [ inversion Red; subst; eauto ].
Case "typing_app".
inversion Red; subst...
SCase "red_abs".
destruct (typing_inv_abs _ _ _ _ _ Typ1 Q (qtyp_qtyp R T1) T2) as [P1 [S2 [L P2]]].
apply subqtype_reflexivity...
pick fresh x.
destruct (P2 x) as [? [? ?]]...
rewrite (subst_ee_intro x)...
rewrite (subst_qqt_intro x)...
rewrite_env (empty ++ E).
rewrite_env ((map (subst_qb x R)) empty ++ E).
destruct T as [Tq Tt].
eapply typing_through_subst_ee with (U := T1).
apply (typing_sub (open_qqt S2 x))...
rewrite_env (empty ++ x ~ bind_typ (qtyp_qtyp R T1) ++ E).
apply typing_narrowing_typ with (Q := (qtyp_qtyp Tq Tt))...
eauto.
auto.
Case "typing_tapp".
inversion Red; subst...
SCase "red_tabs".
destruct (typing_inv_tabs _ _ _ _ _ Typ Q T1 T2) as [P1 [S2 [L P2]]].
apply subqtype_reflexivity...
pick fresh X.
destruct (P2 X) as [? [? ?]]...
rewrite (subst_te_intro X)...
rewrite (subst_tqt_intro X)...
rewrite_env (map (subst_tb X T) empty ++ E).
apply (typing_through_subst_te T1)...
Case "typing_qapp".
inversion Red; subst...
SCase "red_qabs".
destruct (typing_inv_qabs _ _ _ _ _ Typ R Q1 T) as [P1 [S2 [L P2]]].
apply subqtype_reflexivity...
pick fresh X.
destruct (P2 X) as [? [? ?]]...
rewrite (subst_qe_intro X)...
rewrite (subst_qqt_intro X)...
rewrite_env (map (subst_qb X Q) empty ++ E).
apply (typing_through_subst_qe Q1)...
Case "typing_let".
inversion Red; subst.
SCase "red_let_1".
eapply typing_let; eauto.
SCase "red_let".
pick fresh x.
rewrite (subst_ee_intro x)...
rewrite (subst_qqt_fresh x Q)...
rewrite_env ((map (subst_qb x Q)) empty ++ E).
eapply typing_through_subst_ee with (Q := Q)...
Case "typing_case".
inversion Red; subst.
SCase "red_case_1".
eapply typing_case; eauto.
SCase "red_case_inl".
destruct (typing_inv_inl _ _ _ _ Typ R (qtyp_qtyp Q1 S1) (qtyp_qtyp Q2 S2)) as [S1' [J2 [J3 J4]]].
apply subqtype_reflexivity...
pick fresh x.
rewrite (subst_ee_intro x)...
rewrite (subst_qqt_fresh x Q1)...
rewrite_env (map (subst_qb x Q1) empty ++ E).
eapply typing_through_subst_ee with (Q := Q1)...
SCase "red_case_inr".
destruct (typing_inv_inr _ _ _ _ Typ R (qtyp_qtyp Q1 S1) (qtyp_qtyp Q2 S2)) as [S1' [J2 [J3 J4]]].
apply subqtype_reflexivity...
pick fresh x.
rewrite (subst_ee_intro x)...
rewrite (subst_qqt_fresh x Q2)...
rewrite_env (map (subst_qb x Q2) empty ++ E).
eapply typing_through_subst_ee with (Q := Q2)...
Case "typing_first".
inversion Red; subst.
SCase "red_pair_first_1".
eapply typing_first...
SCase "red_pair_first_2".
destruct (typing_inv_pair _ _ _ _ _ Typ Q T1 T2)
as [S1 [S2 [Typ1 [Sub1 [Typ2 [Sub2 SubQ]]]]]]...
apply subqtype_reflexivity...
Case "typing_second".
inversion Red; subst.
SCase "red_pair_second_1".
eapply typing_second...
SCase "red_pair_second_2".
destruct (typing_inv_pair _ _ _ _ _ Typ Q T1 T2)
as [S1 [S2 [Typ1 [Sub1 [Typ2 [Sub2 SubQ]]]]]]...
apply subqtype_reflexivity...
Case "typing_upqual".
inversion Red; subst...
SCase "red_upqual_abs".
unshelve epose proof (typing_canonical_abs _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 [SubU1U2 SubPQ]]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_arrow U1 U2))...
destruct (typing_inv_abs _ _ _ _ _ TypU1U2 Q0 U1 U2) as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
eapply typing_sub with (S := qtyp_qtyp P (typ_arrow V S2))...
eapply typing_abs with (L := L)...
eapply subqual_transitivity with (Q := Q0)...
eapply subqual_transitivity with (Q := Q)...
eapply P2...
econstructor; eauto using subqual_reflexivity...
pick fresh x and apply sub_arrow... eapply (P2 x)...
econstructor; eauto using subqual_reflexivity...
SCase "red_upqual_tabs".
unshelve epose proof (typing_canonical_tabs _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 [SubU1U2 SubQ]]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_all U1 U2))...
destruct (typing_inv_tabs_wide _ _ _ _ _ TypU1U2 Q0 U1 U2) as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
eapply typing_sub with (S := qtyp_qtyp P (typ_all V S2))...
eapply typing_tabs with (L := L)...
eapply subqual_transitivity with (Q := Q0)...
eapply subqual_transitivity with (Q := Q)...
eapply P2...
econstructor; eauto using subqual_reflexivity...
econstructor... pick fresh X. eapply P2...
econstructor; eauto using subqual_reflexivity...
SCase "red_upqual_qabs".
unshelve epose proof (typing_canonical_qabs _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 [SubU1U2 SubQ]]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_qall U1 U2))...
destruct (typing_inv_qabs_wide _ _ _ _ _ TypU1U2 Q0 U1 U2) as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
eapply typing_sub with (S := qtyp_qtyp P (typ_qall V S2))...
eapply typing_qabs with (L := L)...
eapply subqual_transitivity with (Q := Q0)...
eapply subqual_transitivity with (Q := Q)...
eapply P2...
econstructor; eauto using subqual_reflexivity...
econstructor... pick fresh X. eapply P2...
econstructor; eauto using subqual_reflexivity...
SCase "red_upqual_inl".
unshelve epose proof (typing_canonical_inl _ _ _ _ _ Typ)
as [U1 [U2 [U3 [TypU1U2 [SubU1U2 SubQ]]]]].
assert (wf_qtyp E U2)...
apply subqtype_regular in SubU1U2 as [? [WfU1U2 ?]]...
inversion WfU1U2; subst...
inversion select (wf_typ _ (typ_sum _ _))...
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_sum (qtyp_qtyp U3 U1) U2))...
destruct (typing_inv_inl _ _ _ _ TypU1U2 Q0 (qtyp_qtyp U3 U1) U2) as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
eapply typing_inl...
eapply subqual_transitivity with (Q := Q0)...
eapply subqual_transitivity with (Q := Q)...
econstructor... eapply subqual_reflexivity...
SCase "red_upqual_inr".
unshelve epose proof (typing_canonical_inr _ _ _ _ _ Typ)
as [U1 [U2 [U3 [TypU1U2 [SubU1U2 SubQ]]]]].
assert (wf_qtyp E U1)...
apply subqtype_regular in SubU1U2 as [? [WfU1U2 ?]]...
inversion WfU1U2; subst...
inversion select (wf_typ _ (typ_sum _ _))...
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_sum U1 (qtyp_qtyp U3 U2)))...
destruct (typing_inv_inr _ _ _ _ TypU1U2 Q0 U1 (qtyp_qtyp U3 U2)) as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
eapply typing_inr...
eapply subqual_transitivity with (Q := Q0)...
eapply subqual_transitivity with (Q := Q)...
econstructor... eapply subqual_reflexivity...
SCase "red_upqual_pair".
unshelve epose proof (typing_canonical_pair _ _ _ _ _ _ Typ)
as [U1 [U2 [U3 [U4 [TypU1U2 [SubU1U2 SubQ]]]]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_pair (qtyp_qtyp U3 U1) (qtyp_qtyp U4 U2)))...
destruct (typing_inv_pair _ _ _ _ _ TypU1U2 Q0 (qtyp_qtyp U3 U1) (qtyp_qtyp U4 U2)) as [P1 [P2 [TypP1 [SubP1 [TypP2 [SubP2 SubQual]]]]]]...
eapply subqtype_reflexivity...
eapply typing_pair...
eapply subqual_transitivity with (Q := Q0)...
eapply subqual_transitivity with (Q := Q)...
econstructor... eapply subqual_reflexivity...
Qed.
(* ********************************************************************** *)
(* ********************************************************************** *)
Lemma canonical_form_abs : forall e Q U1 U2,
value e ->
typing empty e (qtyp_qtyp Q (typ_arrow U1 U2)) ->
exists P, exists V, exists e1, e = exp_abs P V e1.
Proof.
intros e Q U1 U2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Q (typ_arrow U1 U2)) as T.
revert Q U1 U2 HeqT HeqE.
induction Typ; intros Q' U1 U2 EQT EQE; subst;
try solve [ inversion Val | inversion EQT | eauto ].
Case "typing_sub".
inversion H; subst; eauto.
inversion select (sub _ _ _); subst...
inversion H0.
eapply IHTyp with (Q := Q1) (U1 := S1) (U2 := S2); auto.
Qed.
Lemma canonical_form_tabs : forall e Q U1 U2,
value e ->
typing empty e (qtyp_qtyp Q (typ_all U1 U2)) ->
exists P, exists V, exists e1, e = exp_tabs P V e1.
Proof.
intros e Q U1 U2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Q (typ_all U1 U2)) as T.
revert Q U1 U2 HeqT HeqT.
induction Typ; intros Q' U1 U2 EQT EQE; subst;
try solve [ inversion Val | inversion EQT | eauto ].
Case "typing_sub".
inversion H; subst; eauto.
inversion select (sub _ _ _); subst...
inversion H0.
eapply IHTyp with (Q := Q1) (U1 := S1) (U2 := S2); auto.
Qed.
Lemma canonical_form_qabs : forall e Q U1 U2,
value e ->
typing empty e (qtyp_qtyp Q (typ_qall U1 U2)) ->
exists P, exists V, exists e1, e = exp_qabs P V e1.
Proof.
intros e Q U1 U2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Q (typ_qall U1 U2)) as T.
revert Q U1 U2 HeqT HeqT.
induction Typ; intros Q' U1 U2 EQT EQE; subst;
try solve [ inversion Val | inversion EQT | eauto ].
Case "typing_sub".
inversion H; subst; eauto.
inversion select (sub _ _ _); subst...
inversion H0.
eapply IHTyp with (Q := Q1) (U1 := S1) (U2 := S2); auto.
Qed.
Lemma canonical_form_sum : forall e Q T1 T2,
value e ->
typing empty e (qtyp_qtyp Q (typ_sum T1 T2)) ->
exists P e1, e = exp_inl P e1 \/ e = exp_inr P e1.
Proof.
intros e Q T1 T2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Q (typ_sum T1 T2)) as T.
revert Q T1 T2 HeqE HeqT.
induction Typ; intros Q' U1 U2 EQE EQT; subst;
try solve [ inversion Val | inversion EQT | eauto ].
Case "typing_sub".
inversion H; subst; eauto.
inversion select (sub _ _ _); subst...
inversion H0.
eapply IHTyp; auto.
Qed.
Lemma canonical_form_pair : forall e Q T1 T2,
value e ->
typing empty e (qtyp_qtyp Q (typ_pair T1 T2)) ->
exists P e1 e2, e = exp_pair P e1 e2.
Proof.
intros e Q T1 T2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Q (typ_pair T1 T2)) as T.
revert Q T1 T2 HeqE HeqT.
induction Typ; intros Q' U1 U2 EQE EQT; subst;
try solve [ inversion Val | inversion EQT | eauto ].
Case "typing_sub".
inversion H; subst; eauto.
inversion select (sub _ _ _); subst...
inversion H0.
eapply IHTyp; auto.
Qed.
Lemma canonical_form_qual : forall Q,
wf_qua empty Q ->
exists s, concretize Q = Some s.
Proof with eauto.
intros.
dependent induction H; simpl...
- analyze_binds H.
- analyze_binds H.
- destruct IHwf_qua1 as [s1 Eq1]...
destruct IHwf_qua2 as [s2 Eq2]...
rewrite Eq1; rewrite Eq2; destruct s1; destruct s2...
- destruct IHwf_qua1 as [s1 Eq1]...
destruct IHwf_qua2 as [s2 Eq2]...
rewrite Eq1; rewrite Eq2; destruct s1; destruct s2...
Qed.
(* ********************************************************************** *)
Lemma progress : forall e T,
typing empty e T ->
value e \/ exists e', red e e'.
Proof with unshelve eauto.
intros e T Typ.
remember empty as E. generalize dependent HeqE.
assert (Typ' : typing E e T)...
induction Typ; intros EQ; subst...
Case "typing_var".
inversion H0.
Case "typing_app".
assert (qual R).
eapply qual_from_typing_qtyp...
destruct IHTyp1 as [Val1 | [e1' Rede1']]...
SCase "Val1".
destruct IHTyp2 as [Val2 | [e2' Rede2']]...
SSCase "Val2".
destruct (canonical_form_abs _ _ _ _ Val1 Typ1) as [P [S [e3 EQ]]].
subst...
Case "typing_tapp".
right.
destruct IHTyp as [Val1 | [e1' Rede1']]...
SCase "Val1".
destruct (canonical_form_tabs _ _ _ _ Val1 Typ) as [P [S [e3 EQ]]].
subst.
exists (open_te e3 T)...
Case "typing_tapp".
right.
destruct IHTyp as [Val1 | [e1' Rede1']]...
SCase "Val1".
destruct (canonical_form_qabs _ _ _ _ Val1 Typ) as [P [S [e3 EQ]]].
subst.
exists (open_qe e3 Q)...
Case "typing_let".
assert (qual Q).
eapply qual_from_typing_qtyp...
right.
destruct IHTyp as [Val1 | [e1' Rede1']]...
Case "typing_inl".
destruct (typing_inv_inl _ _ _ _ Typ' P (qtyp_qtyp Q1 S1) T2) as [S1' [J2 J3]].
apply subqtype_reflexivity...
destruct IHTyp as [J1 | [e' J1]]...
Case "typing_inr".
destruct (typing_inv_inr _ _ _ _ Typ' P T1 (qtyp_qtyp Q2 S2)) as [S1 [J2 J3]].
apply subqtype_reflexivity...
destruct IHTyp as [J1 | [e' J1]]...
Case "typing_case".
assert (wf_qtyp empty (qtyp_qtyp R (typ_sum (qtyp_qtyp Q1 S1) (qtyp_qtyp Q2 S2))))...
assert (wf_typ empty (typ_sum (qtyp_qtyp Q1 S1) (qtyp_qtyp Q2 S2)))...
inversion H5; subst... inversion H9; subst... inversion H10; subst...
assert (qual Q1). eapply qual_from_wf_qua...
assert (qual Q2). eapply qual_from_wf_qua...
right.
destruct IHTyp as [Val1 | [e' Rede']]...
SCase "Val1".
destruct (canonical_form_sum _ _ _ _ Val1 Typ) as [P [e4 [J1 | J1]]]; subst...
SSCase "Left J1".
exists (open_ee e2 e4 Q1)... econstructor...
pick fresh x. exact x.
pick fresh x. exact x.
inversion Val1; subst...
inversion Val1; subst...
SSCase "Right J1".
exists (open_ee e3 e4 Q2)... econstructor...
pick fresh x. exact x.
pick fresh x. exact x.
inversion Val1; subst...
inversion Val1; subst...
Case "typing_pair".
destruct IHTyp1 as [Val1 | [e1' Rede1']]...
SCase "Val1".
destruct IHTyp2 as [Val2 | [e2' Rede2']]...
Case "typing_first".
right.
destruct IHTyp as [Val1 | [e' Rede']]...
SCase "Val1".
destruct (canonical_form_pair _ _ _ _ Val1 Typ) as [P [e3 [e4 EQ]]]; subst.
inversion Val1...
Case "typing_second".
right.
destruct IHTyp as [Val1 | [e' Rede']]...
SCase "Val1".
destruct (canonical_form_pair _ _ _ _ Val1 Typ) as [P [e3 [e4 EQ]]]; subst.
inversion Val1...
Case "typing_upqual".
right...
destruct IHTyp as [Val1 | [e' Rede']]...
unshelve epose proof (canonical_form_qual Q _) as [c EqC]...
unshelve epose proof (canonical_form_qual P _) as [d EqD]...
SCase "Val1".
unshelve epose proof (subqual_regular _ _ _ H)
as [? [? ?]]...
inversion Val1; subst...
SSCase "red_exp_abs".
inversion select (expr (exp_abs _ _ _)); subst...
exists (exp_abs P T0 e1)...
unshelve epose proof (typing_canonical_abs _ _ _ _ Q T _)
as [U1 [U2 [TypU1U2' [SubQ' SubC']]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_tabs".
inversion select (expr (exp_tabs _ _ _)); subst...
exists (exp_tabs P T0 e1)...
unshelve epose proof (typing_canonical_tabs _ _ _ _ Q T _)
as [U1 [U2 [TypU1U2' [SubQ' SubC']]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_qabs".
inversion select (expr (exp_qabs _ _ _)); subst...
exists (exp_qabs P Q0 e1)...
unshelve epose proof (typing_canonical_qabs _ _ _ _ Q T Typ)
as [U1 [U2 [TypU1U2' [SubQ' SubC']]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_inl".
exists (exp_inl P e1)...
unshelve epose proof (typing_canonical_inl _ _ _ Q T _)
as [U1 [U2 [U3 [TypU1U2' [SubQ' SubC']]]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_inr".
exists (exp_inr P e1)...
unshelve epose proof (typing_canonical_inr _ _ _ Q T _)
as [U1 [U2 [U3 [TypU1U2' [SubQ' SubC']]]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_pair".
exists (exp_pair P e1 e2)...
unshelve epose proof (typing_canonical_pair _ _ _ _ Q T Typ)
as [U1 [U2 [U3 [U4 [TypU1U2' [SubQ' SubC']]]]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
Case "typing_check".
right...
destruct IHTyp as [Val1 | [e' Rede']]...
unshelve epose proof (canonical_form_qual Q _) as [c EqC]...
unshelve epose proof (canonical_form_qual P _) as [d EqD]...
SCase "Val1".
unshelve epose proof (subqual_regular _ _ _ H)
as [? [? ?]]...
inversion Val1; subst...
SSCase "red_exp_abs".
inversion select (expr (exp_abs _ _ _)); subst...
exists (exp_abs P0 T0 e1)...
unshelve epose proof (typing_canonical_abs _ _ _ _ Q T _)
as [U1 [U2 [TypU1U2' [SubQ' SubC']]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_tabs".
inversion select (expr (exp_tabs _ _ _)); subst...
exists (exp_tabs P0 T0 e1)...
unshelve epose proof (typing_canonical_tabs _ _ _ _ Q T _)
as [U1 [U2 [TypU1U2' [SubQ' SubC']]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_qabs".
inversion select (expr (exp_qabs _ _ _)); subst...
exists (exp_qabs P0 Q0 e1)...
unshelve epose proof (typing_canonical_qabs _ _ _ _ Q T Typ)
as [U1 [U2 [TypU1U2' [SubQ' SubC']]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_inl".
exists (exp_inl P0 e1)...
unshelve epose proof (typing_canonical_inl _ _ _ Q T _)
as [U1 [U2 [U3 [TypU1U2' [SubQ' SubC']]]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_inr".
exists (exp_inr P0 e1)...
unshelve epose proof (typing_canonical_inr _ _ _ Q T _)
as [U1 [U2 [U3 [TypU1U2' [SubQ' SubC']]]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
SSCase "red_exp_pair".
exists (exp_pair P0 e1 e2)...
unshelve epose proof (typing_canonical_pair _ _ _ _ Q T Typ)
as [U1 [U2 [U3 [U4 [TypU1U2' [SubQ' SubC']]]]]]...
inversion SubQ'.
unshelve epose proof (subqual_transitivity Q empty P0 P _ _) as SubT...
unshelve epose proof (subqual_regular _ _ _ SubT) as [? [? ?]]...
unshelve epose proof (canonical_form_qual P0 _) as [b EqB]...
econstructor...
eapply subqual_implies_compatible...
Qed.