Fsub.FuncColour.Fsub_LetSum_Soundness
Type-safety proofs for FuncColour.
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 FuncColour.Tactics.
Require Import Coq.Program.Equality.
Require Export FuncColour.Fsub_LetSum_Lemmas.
(* ********************************************************************** *)
Require Import Coq.Program.Equality.
Require Export FuncColour.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_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_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)...
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_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_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)...
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.
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_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_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 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_meet_split : forall E P Q R,
subqual E P (qua_meet Q R) ->
subqual E P Q /\ subqual E P R.
Proof with intuition eauto.
intros * Sub.
dependent induction Sub...
- eapply subqual_trans_qvar...
eapply IHSub with (Q := Q) (R := R)...
- eapply subqual_trans_qvar...
eapply IHSub with (Q := Q) (R := R)...
- destruct IHSub1 with (Q := Q) (R := R)...
destruct IHSub2 with (Q := Q) (R := R)...
- destruct IHSub1 with (Q := Q) (R := R)...
destruct IHSub2 with (Q := Q) (R := R)...
- destruct IHSub with (Q := Q) (R := R)...
- destruct IHSub with (Q := Q) (R := R)...
- destruct IHSub with (Q := Q) (R := R)...
- destruct IHSub with (Q := Q) (R := R)...
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 T QsubT...
* dependent induction QsubT...
* eapply subqual_trans_qvar with (R := R)...
* 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 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_arrow".
apply sub_arrow.
eapply subqtype_transitivity_rec with (Q := T1)...
eapply subqtype_transitivity_rec with (Q := T2)...
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 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))...
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_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_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_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_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 typing_weakening : forall E F G Q e T,
typing (G ++ E) Q e T ->
wf_env (G ++ F ++ E) ->
typing (G ++ F ++ E) Q 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 Q 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 (H x); [intros K | auto].
rewrite <- app_assoc.
apply (H0 x)...
Case "typing_tabs".
pick fresh X and apply typing_tabs...
lapply (H X); [intros K | auto].
rewrite <- app_assoc.
apply (H0 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 (H x); [intros K | auto].
rewrite <- app_assoc.
apply H0...
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 (H x); [intros K | auto].
rewrite <- app_assoc.
apply H0...
SCase "inr branch".
lapply (H1 x); [intros K | auto].
rewrite <- app_assoc.
apply H2...
Case "typing_pair".
apply typing_pair...
Qed.
(* ********************************************************************** *)
Lemma subqual_strengthening_typ : forall x U E F S T,
subqual (F ++ x ~ bind_typ U ++ E) S T ->
subqual (F ++ E) S T.
Proof with eauto using wf_typ_strengthening_typ, wf_env_strengthening,
wf_qtyp_strengthening_typ, wf_qua_strengthening_typ.
intros x U E F S T SsubT.
remember (F ++ x ~ bind_typ U ++ E) as E'.
generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "subqual_trans_qvar".
apply (subqual_trans_qvar R)...
analyze_binds H...
Qed.
Lemma subqual_strengthening_sub_head : forall X U E S T,
subqual (X ~ bind_sub U ++ E) S T ->
subqual E S T.
Proof with eauto using wf_qua_strengthening_sub.
intros X U E S T SsubT.
assert (wf_env E). {
assert (wf_env (X ~ bind_sub U ++ E))...
inversion H...
}
dependent induction SsubT; subst;
try select (wf_qua _ _)
(fun H => rewrite_env (empty ++ X ~ bind_sub U ++ E) in H; apply wf_qua_strengthening_sub in H);
simpl_env in *...
Case "subqual_trans_qvar".
apply (subqual_trans_qvar R)...
analyze_binds H...
Qed.
Lemma sub_strengthening_typ : forall x U E F S T,
sub (F ++ x ~ bind_typ U ++ E) S T ->
sub (F ++ E) S T
with subqtype_strengthening_typ : forall x U E F S T,
subqtype (F ++ x ~ bind_typ U ++ E) S T ->
subqtype (F ++ E) S T.
Proof with eauto using wf_typ_strengthening_typ, wf_env_strengthening,
wf_qtyp_strengthening_typ, wf_qua_strengthening_typ.
------
intros x U E F S T SsubT.
remember (F ++ x ~ bind_typ U ++ E) as E'.
generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_trans_tvar".
apply (sub_trans_tvar U0)...
analyze_binds H...
Case "sub_all".
pick fresh X and apply sub_all...
rewrite <- app_assoc.
apply (subqtype_strengthening_typ x U E (X ~ bind_sub T1 ++ F))...
apply H...
Case "sub_qall".
pick fresh X and apply sub_qall...
- eapply subqual_strengthening_typ...
- rewrite <- app_assoc.
apply (subqtype_strengthening_typ x U E (X ~ bind_qua T1 ++ F))...
apply H0...
------
clear subqtype_strengthening_typ.
intros x U E F S T SsubT.
remember (F ++ x ~ bind_typ U ++ E) as E'.
generalize dependent F.
induction SsubT; intros F EQ; subst...
Case "sub_qtyp_qtyp".
apply sub_qtyp_qtyp...
apply (subqual_strengthening_typ x U)...
Qed.
(************************************************************************ *)
Lemma typing_narrowing_sub : forall Q E F R X P e T,
sub E P Q ->
typing (F ++ X ~ bind_sub Q ++ E) R e T ->
typing (F ++ X ~ bind_sub P ++ E) R 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 R 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 H0...
Case "typing_tabs".
pick fresh y and apply typing_tabs...
rewrite <- app_assoc.
apply H0...
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 H0...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite <- app_assoc.
apply H0...
SCase "inr branch".
rewrite <- app_assoc.
apply H2...
Qed.
Lemma typing_narrowing_qua : forall Q E F R X P e T,
subqual E P Q ->
typing (F ++ X ~ bind_qua Q ++ E) R e T ->
typing (F ++ X ~ bind_qua P ++ E) R 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 R 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 H0...
Case "typing_tabs".
pick fresh Y and apply typing_tabs...
rewrite <- app_assoc.
apply H0...
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 H0...
Case "typing_case".
pick fresh y and apply typing_case...
SCase "inl branch".
rewrite <- app_assoc.
apply H0...
SCase "inr branch".
rewrite <- app_assoc.
apply H2...
Qed.
(************************************************************************ *)
NEW : we can only splice in expression that are typed
in an unsuspendable environment.
In practice we only substitute values and those do not
call anything.
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_typ_strengthening_typ,
wf_qtyp_strengthening_typ,
wf_qua_strengthening_typ,
wf_env_strengthening,
sub_strengthening_typ,
subqtype_strengthening_typ,
subqual_strengthening_typ.
The proof proceeds by induction on the given typing derivation
for e. We use the remember tactic, along with generalize
dependent, to ensure that the goal is properly strengthened
before we use induction.
intros U E F R x T e u TypT TypU.
remember (F ++ x ~ bind_typ U ++ E) as E'.
generalize dependent F.
induction TypT; intros F EQ; subst; simpl subst_ee...
The typing_var case involves a case analysis on whether the
variable is the same as the one being substituted for.
In the case where x0=x, we first observe that hypothesis
H0 implies that T=U, since x can only be bound once in
the environment. The conclusion then follows from hypothesis
TypU and weakening. We can use the analyze_binds_uniq
tactic, described in the MetatheoryEnv library, with H0 to
obtain the fact that T=U.
SCase "x0 = x".
analyze_binds_uniq H0.
injection BindsTacVal; intros; subst.
In order to apply typing_weakening, we need to rewrite
the environment so that it has the right shape. (We could
also prove a corollary of typing_weakening.) The
rewrite_env tactic, described in the Environment
library, is one way to perform this rewriting.
In the case where x0<>x, the result follows by an exhaustive
case analysis on exactly where x0 is bound in the
environment. We perform this case analysis by using the
analyze_binds tactic, described in the MetatheoryEnv
library.
SCase "x0 <> x".
analyze_binds H0.
eauto using wf_env_strengthening.
eauto using wf_env_strengthening.
Informally, the typing_abs case is a straightforward
application of the induction hypothesis, which is called H0
here.
Case "typing_abs".
We use the "pick fresh and apply" tactic to apply the rule
typing_abs without having to calculate the appropriate
finite set of atoms.
We cannot apply H0 directly here. The first problem is that
the induction hypothesis has (subst_ee open_ee), whereas in
the goal we have (open_ee subst_ee). The lemma
subst_ee_open_ee_var lets us swap the order of these two
operations.
The second problem is how the concatenations are associated in
the environments. In the goal, we currently have
(y ~ bind_typ V ++ F ++ E),
>>
where concatenation associates to the right. In order to
apply the induction hypothesis, we need
((y ~ bind_typ V ++ F) ++ E).
>>
We can use the rewrite_env tactic to perform this rewriting,
or we can rewrite directly with an appropriate lemma from the
MetatheoryEnv library.
Now we can apply the induction hypothesis.
apply H0...
The remaining cases in this proof are straightforward, given
everything that we have pointed out above.
Case "typing_tabs".
pick fresh Y and apply typing_tabs...
rewrite subst_ee_open_te_var...
rewrite <- app_assoc.
apply H0...
Case "typing_qabs".
pick fresh Y and apply typing_qabs...
rewrite subst_ee_open_qe_var...
rewrite <- app_assoc.
apply H1...
Case "typing_let".
pick fresh y and apply typing_let...
rewrite subst_ee_open_ee_var...
rewrite <- app_assoc.
apply H0...
Case "typing_inl".
apply typing_inl...
Case "typing_inr".
apply typing_inr...
Case "typing_case".
pick fresh y and apply typing_case...
rewrite subst_ee_open_ee_var...
rewrite <- app_assoc.
apply H0...
rewrite subst_ee_open_ee_var...
rewrite <- app_assoc.
apply H2...
Case "typing_pair".
apply typing_pair...
Qed.
(************************************************************************ *)
Lemma typing_through_subst_te : forall Q E F R Z e T P,
typing (F ++ Z ~ bind_sub Q ++ E) R e T ->
sub E P Q ->
typing (map (subst_tb Z P) F ++ E) R (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 R 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".
apply typing_var...
rewrite (map_subst_tb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H0...
Case "typing_abs".
pick fresh y and apply typing_abs...
rewrite subst_te_open_ee_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_typ V ++ F) ++ E).
apply H0...
unshelve epose proof (H y _)...
Case "typing_tabs".
pick fresh Y and apply typing_tabs...
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 H0...
unshelve epose proof (H Y _)...
Case "typing_tapp".
rewrite subst_tqt_open_tqt...
Case "typing_qabs".
pick fresh y and apply typing_qabs...
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 T1 ++ F) ++ E).
apply H0...
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 T1 ++ F) ++ E).
apply H0...
unshelve epose proof (H y _)...
SCase "inr branch".
rewrite subst_te_open_ee_var...
rewrite_env (map (subst_tb Z P) (y ~ bind_typ T2 ++ F) ++ E).
apply H2...
unshelve epose proof (H1 y _)...
Case "typing_pair".
eapply typing_pair...
Qed.
Lemma typing_through_subst_qe : forall Q E F R Z e T P,
typing (F ++ Z ~ bind_qua Q ++ E) R e T ->
subqual E P Q ->
typing (map (subst_qb Z P) F ++ E) (subst_qq Z P R) (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 R Z e T P Typ PsubQ.
remember (F ++ Z ~ bind_qua Q ++ E) as G.
generalize dependent F.
assert (wf_env G) as WfEnv...
induction Typ; intros F EQ; subst;
simpl subst_qe in *; simpl subst_qt in *;
simpl subst_qqt in *...
Case "typing_var".
apply typing_var...
rewrite (map_subst_qb_id E Z P);
[ | auto | eapply fresh_mid_tail; eauto ].
analyze_binds H0...
Case "typing_abs".
pick fresh y and apply typing_abs...
rewrite subst_qe_open_ee_var...
rewrite_env (map (subst_qb Z P) (y ~ bind_typ V ++ F) ++ E).
apply H0...
unshelve epose proof (H y _)...
Case "typing_tabs".
pick fresh Y and apply typing_tabs...
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 H0...
unshelve epose proof (H Y _)...
Case "typing_tapp".
rewrite subst_qqt_open_tqt...
Case "typing_qabs".
pick fresh y and apply typing_qabs...
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 T1 ++ F) ++ E).
apply H0...
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 T1 ++ F) ++ E).
apply H0...
unshelve epose proof (H y _)...
SCase "inr branch".
rewrite subst_qe_open_ee_var...
rewrite_env (map (subst_qb Z P) (y ~ bind_typ T2 ++ F) ++ E).
apply H2...
unshelve epose proof (H1 y _)...
Case "typing_pair".
eapply typing_pair...
Qed.
(* ********************************************************************** *)
(* ********************************************************************** *)
Lemma typing_inv_abs : forall E R P S1 e1 T,
typing E R (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) P (open_ee e1 x) S2 /\ subqtype E S2 U2 /\
subqual E P Q.
Proof with auto.
intros E R P S1 e1 T Typ.
remember (exp_abs P S1 e1) as e.
generalize dependent e1.
generalize dependent S1.
generalize dependent P.
induction Typ; intros P' 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...
Case "typing_sub".
eapply IHTyp...
auto using (subqtype_transitivity T).
Case "typing_subqual".
eapply IHTyp...
Qed.
Lemma typing_canonical_abs_rec : forall E R P V e1 Qt Q T,
typing E R (exp_abs P V e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_abs P V e1) (qtyp_qtyp P (typ_arrow U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_arrow U1 U2)) Qt.
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']]]...
eapply subqtype_transitivity...
exists U1. exists U2; split...
eapply subqtype_transitivity...
Case "typing_subqual".
destruct (IHTyp P V e1) as [U1 [U2 [Typ' Sub']]]...
Qed.
Lemma typing_canonical_abs : forall E R P V e1 Q T,
typing E R (exp_abs P V e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (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).
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_abs_rec...
Qed.
Lemma typing_inv_tabs : forall E R P S1 e1 T,
typing E R (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) P (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 R 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).
Case "typing_subqual".
destruct (IHTyp S1 e0 ltac:(auto) Q' U1 U2)
as [Sub1 [S2 [L TypBody]]]...
Qed.
Lemma typing_inv_tabs_wide : forall E R P S1 e1 T,
typing E R (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) P (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 R 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).
Case "typing_subqual".
destruct (IHTyp S1 e0 ltac:(auto) Q' U1 U2)
as [Sub1 [S2 [L TypBody]]]...
Qed.
Lemma typing_canonical_tabs_rec : forall E R P S1 e1 Qt Q T,
typing E R (exp_tabs P S1 e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_tabs P S1 e1) (qtyp_qtyp P (typ_all U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_all U1 U2)) Qt.
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']]]...
eapply subqtype_transitivity...
exists U1. exists U2; split...
eapply subqtype_transitivity...
Case "typing_subqual".
destruct (IHTyp P S1 e1) as [U1 [U2 [Typ' Sub']]]...
Qed.
Lemma typing_canonical_tabs : forall E R P S1 e1 Q T,
typing E R (exp_tabs P S1 e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (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).
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_tabs_rec...
Qed.
Lemma typing_inv_qabs : forall E R P S1 e1 T,
typing E R (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) P (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 R 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).
Case "typing_subqual".
destruct (IHTyp S1 e0 ltac:(auto) Q' U1 U2)
as [Sub1 [S2 [L TypBody]]]...
Qed.
Lemma typing_inv_qabs_wide : forall E R P S1 e1 T,
typing E R (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) P (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 R 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).
Case "typing_subqual".
destruct (IHTyp S1 e0 ltac:(auto) Q' U1 U2)
as [Sub1 [S2 [L TypBody]]]...
Qed.
Lemma typing_canonical_qabs_rec : forall E R P S1 e1 Qt Q T,
typing E R (exp_qabs P S1 e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_qabs P S1 e1) (qtyp_qtyp P (typ_qall U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_qall U1 U2)) Qt.
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']]]...
eapply subqtype_transitivity...
exists U1. exists U2; split...
eapply subqtype_transitivity...
Case "typing_subqual".
destruct (IHTyp P S1 e1) as [U1 [U2 [Typ' Sub']]]...
Qed.
Lemma typing_canonical_qabs : forall E R P S1 e1 Q T,
typing E R (exp_qabs P S1 e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (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).
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_qabs_rec...
Qed.
Lemma typing_inv_inl : forall E R P e1 T,
typing E R (exp_inl P e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_sum U1 U2)) ->
exists S1, typing E R e1 S1 /\ subqtype E S1 U1 /\ subqual E P Q.
Proof with eauto.
intros E R 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_subqual".
destruct (IHTyp e' ltac:(auto) Q' U1 U2)
as [S1 [Typ' Sub']]...
Case "typing_inl".
inversion Sub; subst...
inversion select (sub _ (typ_sum _ _) (typ_sum _ _))...
Qed.
Lemma typing_canonical_inl_rec : forall E R P e1 Qt Q T,
typing E R (exp_inl P e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_inl P e1) (qtyp_qtyp P (typ_sum U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_sum U1 U2)) Qt.
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 [Typ' Sub']]]...
eapply subqtype_transitivity...
exists U1. exists U2; split...
eapply subqtype_transitivity...
Case "typing_subqua".
destruct (IHTyp P e1) as [U1 [U2 [Typ' Sub']]]...
Case "typing_inl".
inversion Sub; subst...
exists T1. exists T2; split...
Qed.
Lemma typing_canonical_inl : forall E R P e1 Q T,
typing E R (exp_inl P e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_inl P e1) (qtyp_qtyp P (typ_sum U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_sum U1 U2)) (qtyp_qtyp Q T).
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_inl_rec...
Qed.
Lemma typing_inv_inr : forall E R P e1 T,
typing E R (exp_inr P e1) T ->
forall Q U1 U2, subqtype E T (qtyp_qtyp Q (typ_sum U1 U2)) ->
exists S1, typing E R e1 S1 /\ subqtype E S1 U2 /\ subqual E P Q.
Proof with eauto.
intros E R 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_subqual".
destruct (IHTyp e' ltac:(auto) Q' U1 U2)
as [S1 [Typ' Sub']]...
Case "typing_inr".
inversion Sub; subst...
inversion select (sub _ (typ_sum _ _) (typ_sum _ _))...
Qed.
Lemma typing_canonical_inr_rec : forall E R P e1 Qt Q T,
typing E R (exp_inr P e1) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_inr P e1) (qtyp_qtyp P (typ_sum U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_sum U1 U2)) Qt.
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 [Typ' Sub']]]...
eapply subqtype_transitivity...
exists U1. exists U2; split...
eapply subqtype_transitivity...
Case "typing_subqual".
destruct (IHTyp P e1) as [U1 [U2 [Typ' Sub']]]...
Case "typing_inr".
inversion Sub; subst...
exists T1. exists T2; split...
Qed.
Lemma typing_canonical_inr : forall E R P e1 Q T,
typing E R (exp_inr P e1) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_inr P e1) (qtyp_qtyp P (typ_sum U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_sum U1 U2)) (qtyp_qtyp Q T).
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_inr_rec...
Qed.
Lemma typing_inv_pair : forall E R P e1 e2 T,
typing E R (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 R e1 S1 /\ subqtype E S1 U1 /\
typing E R e2 S2 /\ subqtype E S2 U2 /\ subqual E P Q.
Proof with eauto.
intros E R 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_subqual".
destruct (IHTyp e2' e1' ltac:(auto) Q' U1 U2)
as [S1 [S2 [Typ1 [Sub1 [Typ2 [Sub2 SubQ']]]]]]...
exists S1. exists S2.
repeat split...
Case "typing_inr".
inversion Sub; subst...
inversion select (sub _ (typ_pair _ _) (typ_pair _ _)); subst...
exists T1. exists T2...
Qed.
Lemma typing_canonical_pair_rec : forall E R P e1 e2 Qt Q T,
typing E R (exp_pair P e1 e2) Qt ->
subqtype E Qt (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_pair P e1 e2) (qtyp_qtyp P (typ_pair U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_pair U1 U2)) Qt.
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 [Typ' Sub']]]...
eapply subqtype_transitivity...
exists U1. exists U2; split...
eapply subqtype_transitivity...
Case "typing_subqual".
destruct (IHTyp P e1 e2) as [U1 [U2 [Typ' Sub']]]...
Case "typing_inl".
inversion Sub; subst...
exists T1. exists T2; split...
Qed.
Lemma typing_canonical_pair : forall E R P e1 e2 Q T,
typing E R (exp_pair P e1 e2) (qtyp_qtyp Q T) ->
exists U1 U2,
typing E R (exp_pair P e1 e2) (qtyp_qtyp P (typ_pair U1 U2)) /\
subqtype E (qtyp_qtyp P (typ_pair U1 U2)) (qtyp_qtyp Q T).
Proof with eauto using subqtype_reflexivity.
intros.
eapply typing_canonical_pair_rec...
Qed.
Lemma typing_inv_upqual : forall E R P e1 T,
typing E R (exp_upqual P e1) T ->
forall Q U, subqtype E T (qtyp_qtyp Q U) ->
exists S1 S2,
typing E R e1 (qtyp_qtyp S1 S2)
/\ subqual E S1 P
/\ sub E S2 U
/\ subqual E P Q.
Proof with eauto using subqual_reflexivity, sub_reflexivity.
intros E R P e1 T Typ.
remember (exp_upqual P e1) as e. generalize dependent e1.
induction Typ; intros e' EQ Q' U' Sub; inversion EQ; subst.
Case "typing_sub".
eauto using (subqtype_transitivity T).
Case "typing_subqual".
destruct (IHTyp e' ltac:(auto) Q' U')
as [S1 [S2 [Typ' [Sub1' [Sub2' Sub3']]]]]...
exists S1... exists S2...
Case "typing_upqual".
inversion Sub; subst...
exists P. exists U'... repeat split...
Qed.
Lemma typing_inv_check : forall E R P e1 T,
typing E R (exp_check P e1) T ->
forall Q U, subqtype E T (qtyp_qtyp Q U) ->
exists S1 S2,
typing E R e1 (qtyp_qtyp S1 S2)
/\ subqual E S1 P
/\ sub E S2 U
/\ subqual E S1 Q.
Proof with eauto using subqual_reflexivity, sub_reflexivity.
intros E R P e1 T Typ.
remember (exp_check P e1) as e. generalize dependent e1.
induction Typ; intros e' EQ Q' U' Sub; inversion EQ; subst.
Case "typing_sub".
eauto using (subqtype_transitivity T).
Case "typing_subqual".
destruct (IHTyp e' ltac:(auto) Q' U')
as [S1 [S2 [Typ' [Sub1' [Sub2' Sub3]]]]]...
exists S1... exists S2...
Case "typing_check".
inversion Sub; subst... exists Q...
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.
- 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.
- 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 typing_value_inert : forall E Q e T,
typing E Q e T ->
value e ->
typing E `sync e T.
Proof with eauto.
intros * Typ Val.
dependent induction Typ;
inversion Val; subst; simpl...
- eapply typing_abs...
- eapply typing_tabs...
- eapply typing_qabs...
Qed.
Lemma typing_upqual_same : forall E R e P T,
typing E R (exp_upqual P e) T ->
typing E R e T.
Proof with eauto using sub_reflexivity.
intros.
dependent induction H...
Qed.
Lemma preservation : forall E s s',
typing_state E s ->
s --> s' ->
typing_state E s'.
Proof with simpl_env; eauto using
concrete_sub_qualifier, qualifier_sub_concrete, typing_upqual_same.
intros E s s' TypState Step.
inversion TypState; inversion Step; subst...
all: try rename select (typing _ _ _ T) into Typ.
all: try rename select (typing _ _ _ T0) into Typ.
all: try rename select (typing_ctx _ _ _ T) into TypCtx.
all: try rename select (typing_ctx _ _ _ T0) into TypCtx.
Case "step_barrier".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx...
SCase "typing_ctx_barrier".
econstructor...
inversion select (cqua_compatible _ _); subst; simpl...
Case "step_abs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_app".
econstructor...
econstructor...
Case "step_app".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
econstructor...
eapply typing_ctx_app...
Case "step_tabs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_abs".
assert (wf_typ E (typ_all T1 T2)) as WfTyp...
inversion WfTyp; subst...
econstructor; simpl in *...
eapply typing_ctx_tabs with (L := L)...
Case "step_qabs" .
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_qabs".
assert (wf_typ E (typ_qall Q1 T)) as WfTyp...
inversion WfTyp; subst...
econstructor...
eapply typing_ctx_qabs with (L := L)...
Case "step_let".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_let".
econstructor...
eapply typing_ctx_let with (L := L)...
Case "step_inl".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_inl".
econstructor...
eapply typing_ctx_inl...
Case "step_inr".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_inr".
econstructor...
eapply typing_ctx_inr...
Case "step_case".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_case".
econstructor...
eapply typing_ctx_case...
eapply typing_regular in Typ as [WfE [Expr [WfQT WfQ]]]...
Case "step_pair_1".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_ctx_1".
econstructor...
eapply typing_ctx_pair_1...
Case "step_pair_2".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
SCase "typing_ctx_2".
econstructor...
eapply typing_ctx_pair_2...
Case "step_first".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_first".
assert (wf_typ E (typ_pair T1 T2)) as WfPair...
inversion WfPair; subst...
econstructor...
eapply typing_ctx_first...
eapply typing_regular in Typ as [WfE [Expr [WfQT WfQ]]]...
Case "step_second".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction Typ; subst...
SCase "typing_second".
assert (wf_typ E (typ_pair T1 T2)) as WfPair...
inversion WfPair; subst...
econstructor...
eapply typing_ctx_second...
eapply typing_regular in Typ as [WfE [Expr [WfQT WfQ]]]...
Case "step_app".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_abs _ _ _ _ _ _ H0 Q T1 T2) as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
pick fresh x.
destruct (P2 x) as [? [? ?]]...
rewrite (subst_ee_intro x)...
eapply typing_step with (Q:= Q0) (T := T2).
SCase "typing_app".
rewrite_env (empty ++ E).
apply (typing_through_subst_ee V).
apply (typing_sub S2)...
rewrite_env (empty ++ x ~ bind_typ V ++ E).
eapply subqtype_weakening...
eapply (typing_sub T1)...
eapply typing_value_inert...
SCase "barrier_compatible".
eapply typing_ctx_subqual with (abstractize t)...
eapply typing_ctx_barrier with (Q := Q0)...
Case "step_tapp".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_tabs _ _ _ _ _ _ Typ Q T1 T2)
as [P1 [S2 [L' P2]]] ...
eapply subqtype_reflexivity...
pick fresh X.
destruct (P2 X) as [? [? ?]]...
eapply typing_step with (Q := P) (T := open_tqt T2 V)...
SCase "typing_tapp".
rewrite (subst_te_intro X)...
rewrite (subst_tqt_intro X)...
rewrite_env (map (subst_tb X V) empty ++ E).
apply (typing_through_subst_te T1)...
SCase "barrier_compatible".
eapply typing_ctx_subqual with (abstractize t)...
eapply typing_ctx_barrier with (Q := P)...
Case "step_qapp".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_qabs _ _ _ _ _ _ Typ Q R0 T2)
as [P1 [S2 [L' P2]]] ...
eapply subqtype_reflexivity...
pick fresh X.
destruct (P2 X) as [? [? ?]]...
eapply typing_step with (Q := P) (T := open_qqt T2 R)...
SCase "typing_tapp".
rewrite (subst_qe_intro X)...
rewrite (subst_qqt_intro X)...
rewrite_env (map (subst_qb X R) empty ++ E).
replace P with (subst_qq X R P).
apply (typing_through_subst_qe R0)...
symmetry; apply subst_qq_fresh...
SCase "barrier_compatible".
eapply typing_ctx_subqual with (abstractize t)...
eapply typing_ctx_barrier with (Q := P)...
Case "step_let".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
SCase "typing_let".
econstructor...
pick fresh x.
rewrite (subst_ee_intro x)...
rewrite_env (empty ++ E).
apply (typing_through_subst_ee T1)...
eapply typing_value_inert...
Case "step_case_inl".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_inl _ _ _ _ _ Typ P0 T1 T2) as
[S1 [P1 [P2 P3]]].
eapply subqtype_reflexivity...
SCase "typing_case".
econstructor...
pick fresh x.
rewrite (subst_ee_intro x)...
rewrite_env (empty ++ E).
apply (typing_through_subst_ee T1)...
eapply typing_value_inert...
Case "step_case_inr".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_inr _ _ _ _ _ Typ P0 T1 T2) as
[S1 [P1 [P2 P3]]].
eapply subqtype_reflexivity...
SCase "typing_case".
econstructor...
pick fresh x.
rewrite (subst_ee_intro x)...
rewrite_env (empty ++ E).
apply (typing_through_subst_ee T2)...
eapply typing_value_inert...
Case "step_first".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_pair _ _ _ _ _ _ Typ P0 T1 T2)
as [P1 [S2 [Typ1 [Sub1 [Typ2 [Sub2 SubQ]]]]]]...
eapply subqtype_reflexivity...
SCase "typing_first".
econstructor...
Case "step_second".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
destruct (typing_inv_pair _ _ _ _ _ _ Typ P0 T1 T2)
as [P1 [S2 [Typ1 [Sub1 [Typ2 [Sub2 SubQ]]]]]]...
eapply subqtype_reflexivity...
SCase "typing_second".
econstructor...
Case "step_make_inl".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
assert (wf_qtyp E (qtyp_qtyp P (typ_sum T1 T2))) as WfQTyp...
assert (wf_typ E (typ_sum T1 T2)) as WfTyp...
SCase "typing_inl".
eapply typing_step with (Q := Q) (T := qtyp_qtyp P (typ_sum T1 T2))...
eapply typing_inl... inversion WfTyp...
Case "step_make_inr".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
assert (wf_qtyp E (qtyp_qtyp P (typ_sum T1 T2))) as WfQTyp...
assert (wf_typ E (typ_sum T1 T2)) as WfTyp...
SCase "typing_inr".
eapply typing_step with (Q := Q) (T := qtyp_qtyp P (typ_sum T1 T2))...
eapply typing_inr... inversion WfTyp...
Case "step_make_pair".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
SCase "typing_pair".
eapply typing_step with (Q := Q) (T := qtyp_qtyp P (typ_pair T1 T2))...
Case "step_upqual".
inversion select (state_step _ _ = state_step _ _); subst...
destruct T as [Q' T'].
unshelve epose proof (typing_inv_upqual _ _ _ _ _ Typ Q' T' _)
as [S1 [S2 [TypU [Sub1 [Sub2 Sub3]]]]]...
eapply subqtype_reflexivity...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P T')...
eapply typing_ctx_upqual...
eapply typing_ctx_sub with (T := qtyp_qtyp Q' T');
eauto using sub_reflexivity.
SCase "step_upqual_abs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
eapply typing_step with (Q := Q)...
unshelve epose proof (typing_canonical_abs _ _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 SubU1U2]]].
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_subqual with (Q := `sync)...
pick fresh x and apply typing_abs...
eapply typing_subqual with (Q := Q0)...
unshelve eapply (P2 x _)...
rewrite_env (empty ++ x ~ bind_typ V ++ E).
eapply subqual_weakening...
econstructor; eauto using subqual_reflexivity...
pick fresh x. destruct (P2 x) as [Typ' [Sub1 Sub2]]...
econstructor; eauto using subqual_reflexivity...
SCase "step_upqual_tabs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
eapply typing_step with (Q := Q)...
unshelve epose proof (typing_canonical_tabs _ _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 SubU1U2]]].
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_subqual with (Q := `sync)...
eapply typing_sub with (S := qtyp_qtyp P (typ_all V S2))...
pick fresh X and apply typing_tabs...
eapply typing_subqual with (Q := Q0)...
eapply (P2 X)...
rewrite_env (empty ++ X ~ bind_sub V ++ E).
eapply subqual_weakening...
econstructor; eauto using subqual_reflexivity...
pick fresh X and apply sub_all...
destruct (P2 X) as [Typ' [Sub1 Sub2]]...
econstructor; eauto using subqual_reflexivity...
SCase "step_upqual_qabs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
eapply typing_step with (Q := Q)...
unshelve epose proof (typing_canonical_qabs _ _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 SubU1U2]]].
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_subqual with (Q := `sync)...
eapply typing_sub with (S := qtyp_qtyp P (typ_qall V S2))...
pick fresh X and apply typing_qabs...
eapply typing_subqual with (Q := Q0)...
eapply (P2 X)...
rewrite_env (empty ++ X ~ bind_qua V ++ E).
eapply subqual_weakening...
econstructor; eauto using subqual_reflexivity...
pick fresh X and apply sub_qall...
destruct (P2 X) as [Typ' [Sub1 Sub2]]...
econstructor; eauto using subqual_reflexivity...
SCase "step_upqual_inl".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
eapply typing_step with (Q := Q)...
unshelve epose proof (typing_canonical_inl _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_sum U1 U2))...
destruct (typing_inv_inl _ _ _ _ _ TypU1U2 Q0 U1 U2)
as [S1 [TypS1 [SubS1 SubQ]]]...
eapply subqtype_reflexivity...
eapply typing_inl...
apply typing_regular in TypU1U2 as [_ [_ [WfU1U2 _]]]...
inversion WfU1U2; subst...
inversion select (wf_typ _ (typ_sum _ _))...
econstructor... eapply subqual_reflexivity...
SCase "step_upqual_inr".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
eapply typing_step with (Q := Q)...
unshelve epose proof (typing_canonical_inr _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_sum U1 U2))...
destruct (typing_inv_inr _ _ _ _ _ TypU1U2 Q0 U1 U2)
as [S1 [TypS1 [SubS1 SubQ]]]...
eapply subqtype_reflexivity...
eapply typing_inr...
apply typing_regular in TypU1U2 as [_ [_ [WfU1U2 _]]]...
inversion WfU1U2; subst...
inversion select (wf_typ _ (typ_sum _ _))...
econstructor... eapply subqual_reflexivity...
SCase "step_upqual_pair".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
eapply typing_step with (Q := Q)...
unshelve epose proof (typing_canonical_pair _ _ _ _ _ _ _ Typ)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
eapply typing_sub with (S := qtyp_qtyp P (typ_pair U1 U2))...
destruct (typing_inv_pair _ _ _ _ _ _ TypU1U2 Q0 U1 U2)
as [S1 [S2 [TypS1 [SubS1 [TypS2 [SubS2 SubQ]]]]]]...
eapply subqtype_reflexivity...
econstructor... eapply subqual_reflexivity...
Case "step_check".
inversion select (state_step _ _ = state_step _ _); subst...
destruct T as [Q' T'].
unshelve epose proof (typing_inv_check _ _ _ _ _ Typ Q' T' _)
as [S1 [S2 [TypU [Sub1 [Sub2 Sub3]]]]]...
eapply subqtype_reflexivity...
eapply typing_step with (Q := Q)
(T := qtyp_qtyp (qua_meet Q' P) T')...
eapply typing_ctx_check...
SCase "step_check_abs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx) as [WfE [WfQT WfQua]]...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P0 T)...
eapply typing_sub with (S := qtyp_qtyp (qua_meet P0 P) T)...
econstructor; eauto using sub_reflexivity...
eapply subqual_meet_eliml...
eapply subqual_reflexivity...
SCase "step_check_tabs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx) as [WfE [WfQT WfQua]]...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P0 T)...
eapply typing_sub with (S := qtyp_qtyp (qua_meet P0 P) T)...
econstructor; eauto using sub_reflexivity...
eapply subqual_meet_eliml...
eapply subqual_reflexivity...
SCase "step_check_qabs".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx) as [WfE [WfQT WfQua]]...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P0 T)...
eapply typing_sub with (S := qtyp_qtyp (qua_meet P0 P) T)...
econstructor; eauto using sub_reflexivity...
eapply subqual_meet_eliml...
eapply subqual_reflexivity...
SCase "step_check_inl".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx) as [WfE [WfQT WfQua]]...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P0 T)...
eapply typing_sub with (S := qtyp_qtyp (qua_meet P0 P) T)...
econstructor; eauto using sub_reflexivity...
eapply subqual_meet_eliml...
eapply subqual_reflexivity...
SCase "step_check_inr".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx) as [WfE [WfQT WfQua]]...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P0 T)...
eapply typing_sub with (S := qtyp_qtyp (qua_meet P0 P) T)...
econstructor; eauto using sub_reflexivity...
eapply subqual_meet_eliml...
eapply subqual_reflexivity...
SCase "step_check_pair".
inversion select (state_step _ _ = state_step _ _); subst...
dependent induction TypCtx; subst...
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx) as [WfE [WfQT WfQua]]...
eapply typing_step with (Q := Q) (T := qtyp_qtyp P0 T)...
eapply typing_sub with (S := qtyp_qtyp (qua_meet P0 P) T)...
econstructor; eauto using sub_reflexivity...
eapply subqual_meet_eliml...
eapply subqual_reflexivity...
Qed.
(* ********************************************************************** *)
(* ********************************************************************** *)
Lemma canonical_form_abs : forall e Qt Qf U1 U2,
value e ->
typing empty Qt e (qtyp_qtyp Qf (typ_arrow U1 U2)) ->
exists P V e1, e = exp_abs P V e1.
Proof.
intros e Qt Qf U1 U2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Qf (typ_arrow U1 U2)) as T.
revert Qf U1 U2 HeqT HeqE.
induction Typ; intros Qf 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 (Qf := Q1) (U1 := S1) (U2 := S2); auto.
Qed.
Lemma canonical_form_abs_qua : forall Qt Q V e1 T,
typing empty Qt (exp_abs Q V e1) T ->
wf_qua empty Q.
Proof with eauto 4.
intros.
dependent induction H; subst...
pick fresh X. unshelve epose proof (H X ltac:(auto))...
assert (wf_qua (X ~ bind_typ V ++ empty) Q)...
rewrite_env (empty ++ empty).
eapply wf_qua_strengthening_typ...
Qed.
Lemma canonical_form_tabs : forall e Qt Qf U1 U2,
value e ->
typing empty Qt e (qtyp_qtyp Qf (typ_all U1 U2)) ->
exists P, exists V, exists e1, e = exp_tabs P V e1.
Proof.
intros e Qt Qf U1 U2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Qf (typ_all U1 U2)) as T.
revert Qf U1 U2 HeqT HeqT.
induction Typ; intros Qf 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 (Qf := Q1) (U1 := S1) (U2 := S2); auto.
Qed.
Lemma canonical_form_qabs : forall e Qt Qf U1 U2,
value e ->
typing empty Qt e (qtyp_qtyp Qf (typ_qall U1 U2)) ->
exists P, exists V, exists e1, e = exp_qabs P V e1.
Proof.
intros e Qt Qf U1 U2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Qf (typ_qall U1 U2)) as T.
revert Qf U1 U2 HeqT HeqT.
induction Typ; intros Qf 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 (Qf := Q1) (U1 := S1) (U2 := S2); auto.
Qed.
Lemma canonical_form_sum : forall e Qt Qs T1 T2,
value e ->
typing empty Qt e (qtyp_qtyp Qs (typ_sum T1 T2)) ->
exists P e1, e = exp_inl P e1 \/ e = exp_inr P e1.
Proof.
intros e Qt Qs T1 T2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Qs (typ_sum T1 T2)) as T.
revert Qs T1 T2 HeqE HeqT.
induction Typ; intros Qs 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 Qt Qp T1 T2,
value e ->
typing empty Qt e (qtyp_qtyp Qp (typ_pair T1 T2)) ->
exists P e1 e2, e = exp_pair P e1 e2.
Proof.
intros e Qt Qp T1 T2 Val Typ.
remember empty as E.
remember (qtyp_qtyp Qp (typ_pair T1 T2)) as T.
revert Qp T1 T2 HeqE HeqT.
induction Typ; intros Qt 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.
- 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 compatible_barriers : forall Q t Qk k T,
concretize Q = Some t ->
subqual empty Q Qk ->
typing_ctx empty Qk k T ->
barrier_compatible k t.
Proof with auto.
intros.
dependent induction H1;
try solve [apply barrier_compatible_other; auto; discriminate]...
Case "typing_ctx_barrier".
eapply barrier_compatible_frame...
SCase "barrier_compatible_tail".
unshelve epose proof (concrete_sub_qualifier empty _ _ H _ _)...
unshelve epose proof (concrete_sub_qualifier empty _ _ H2 _ _)...
unshelve epose proof (qualifier_sub_concrete empty _ _ H _ _)...
unshelve epose proof (qualifier_sub_concrete empty _ _ H2 _ _)...
eapply IHtyping_ctx...
eapply subqual_transitivity with (Q := abstractize t0)...
inversion H3; subst...
SCase "barrier_compatible_current".
eapply subqual_compatible...
unshelve epose proof (concrete_sub_qualifier empty _ _ H _ _)...
unshelve epose proof (concrete_sub_qualifier empty _ _ H2 _ _)...
unshelve epose proof (qualifier_sub_concrete empty _ _ H _ _)...
unshelve epose proof (qualifier_sub_concrete empty _ _ H2 _ _)...
inversion H3; subst; simpl...
eapply subqual_transitivity with (Q := Q)...
eapply subqual_transitivity with (Q := Q)...
Case "typing_ctx_subqual".
eapply IHtyping_ctx...
eapply subqual_transitivity with (Q := R)...
Qed.
Lemma progress_value_step : forall v k,
value v ->
typing_state empty (state_step v k) ->
done_state (state_step v k) \/ exists s', (state_step v k) --> s'.
Proof with eauto.
intros * Val Typ.
inversion Typ; subst.
rename select (typing_ctx _ _ _ _) into TypCtx.
dependent induction TypCtx...
Case "step_app".
unshelve epose proof (canonical_form_abs _ _ _ _ _ _ H0)
as [Qf [V [e2 Eq]]]; subst...
unshelve epose proof (typing_inv_abs _ _ _ _ _ _ H0 Q T1 T2)
as [P1 [S2 [L P2]]]...
eapply subqtype_reflexivity...
pick fresh x. unshelve epose proof (P2 x _)
as [Typ' [SubQ SubQual]]...
destruct (canonical_form_qual Qf) as [t ComputeQf]...
unshelve epose proof (compatible_barriers _ _ _ _ _ ComputeQf _ TypCtx)...
Case "step_tapp".
unshelve epose proof (canonical_form_tabs _ _ _ _ _ _ H2)
as [Qf [V [e2 Eq]]]; subst...
unshelve epose proof (typing_inv_tabs _ _ _ _ _ _ H2 Q T1 T2)
as [P1 [S2 [L' P2]]]...
eapply subqtype_reflexivity...
pick fresh x. unshelve epose proof (P2 x _)
as [Typ' [SubQ SubQual]]...
destruct (canonical_form_qual Qf) as [t ComputeQf]...
unshelve epose proof (compatible_barriers _ _ _ _ _ ComputeQf _ TypCtx)...
Case "step_qapp".
unshelve epose proof (canonical_form_qabs _ _ _ _ _ _ H2)
as [Qf [V [e2 Eq]]]; subst...
unshelve epose proof (typing_inv_qabs _ _ _ _ _ _ H2 Q R T2)
as [P1 [S2 [L' P2]]]...
eapply subqtype_reflexivity...
pick fresh x. unshelve epose proof (P2 x _)
as [Typ' [SubQ SubQual]]...
destruct (canonical_form_qual Qf) as [t ComputeQf]...
unshelve epose proof (compatible_barriers _ _ _ _ _ ComputeQf _ TypCtx)...
Case "step_case".
unshelve epose proof (canonical_form_sum _ _ _ _ _ _ H2)
as [? [? [Eq | Eq]]]; subst...
Case "step_first".
unshelve epose proof (canonical_form_pair _ _ _ _ _ _ H2)
as [? [? [? Eq]]]; subst...
Case "step_second".
unshelve epose proof (canonical_form_pair _ _ _ _ _ _ H2)
as [? [? [? Eq]]]; subst...
Case "step_upqual".
inversion Val; subst...
SCase "val_abs".
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx)
as [_ [WfTyp2 WfQua2]]...
unshelve epose proof (typing_canonical_abs _ _ _ _ _ _ _ H2)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
unshelve epose proof (canonical_form_qual P0 _)
as [cP0 EqP0]...
unshelve epose proof (canonical_form_qual P _)
as [cP EqP]...
right. eexists. eapply step_upqual_abs...
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P0)...
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := P)...
eapply qualifier_sub_concrete...
SCase "val_tabs".
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx)
as [_ [WfTyp2 WfQua2]]...
unshelve epose proof (typing_canonical_tabs _ _ _ _ _ _ _ H2)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
unshelve epose proof (canonical_form_qual P0 _)
as [cP0 EqP0]...
unshelve epose proof (canonical_form_qual P _)
as [cP EqP]...
right. eexists. eapply step_upqual_tabs...
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P0)...
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := P)...
eapply qualifier_sub_concrete...
SCase "val_qabs".
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx)
as [_ [WfTyp2 WfQua2]]...
unshelve epose proof (typing_canonical_qabs _ _ _ _ _ _ _ H2)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
unshelve epose proof (canonical_form_qual P0 _)
as [cP0 EqP0]...
unshelve epose proof (canonical_form_qual P _)
as [cP EqP]...
right. eexists. eapply step_upqual_qabs...
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P0)...
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := P)...
eapply qualifier_sub_concrete...
Case "step_check".
inversion Val; subst...
SCase "val_abs".
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx)
as [_ [WfTyp2 WfQua2]]...
unshelve epose proof (typing_canonical_abs _ _ _ _ _ _ _ H2)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
unshelve epose proof (canonical_form_qual P0 _)
as [cP0 EqP0]...
unshelve epose proof (canonical_form_qual P _)
as [cP EqP]...
unshelve epose proof (canonical_form_qual R _)
as [cR EqR]...
right. eexists. eapply step_check_abs...
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P0)...
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := R)...
eapply subqual_meet_split with (Q := R).
eapply subqual_transitivity with (Q := qua_meet P R)...
eapply subqual_meet_intro; eauto using subqual_reflexivity.
eapply qualifier_sub_concrete...
SCase "val_tabs".
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx)
as [_ [WfTyp2 WfQua2]]...
unshelve epose proof (typing_canonical_tabs _ _ _ _ _ _ _ H2)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
unshelve epose proof (canonical_form_qual R _)
as [cR EqR]...
unshelve epose proof (canonical_form_qual P _)
as [cP EqP]...
unshelve epose proof (canonical_form_qual P0 _)
as [cP0 EqP0]...
right. eexists. eapply step_check_tabs...
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P0)...
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := R)...
eapply subqual_meet_split with (Q := R).
eapply subqual_transitivity with (Q := qua_meet P R)...
eapply subqual_meet_intro; eauto using subqual_reflexivity.
eapply qualifier_sub_concrete...
SCase "val_qabs".
unshelve epose proof (typing_ctx_regular _ _ _ _ TypCtx)
as [_ [WfTyp2 WfQua2]]...
unshelve epose proof (typing_canonical_qabs _ _ _ _ _ _ _ H2)
as [U1 [U2 [TypU1U2 SubU1U2]]].
inversion SubU1U2; subst...
unshelve epose proof (canonical_form_qual P0 _)
as [cP0 EqP0]...
unshelve epose proof (canonical_form_qual P _)
as [cP EqP]...
unshelve epose proof (canonical_form_qual R _)
as [cR EqR]...
right. eexists. eapply step_check_qabs...
eapply subqual_compatible...
eapply subqual_transitivity with (Q := P0)...
eapply concrete_sub_qualifier...
eapply subqual_transitivity with (Q := R)...
eapply subqual_meet_split with (Q := R).
eapply subqual_transitivity with (Q := qua_meet P R)...
eapply subqual_meet_intro; eauto using subqual_reflexivity.
eapply qualifier_sub_concrete...
Qed.
Lemma progress : forall s,
typing_state empty s ->
done_state s \/ exists s', s --> s'.
Proof with eauto.
intros s TypS.
inversion TypS; subst...
assert (typing empty Q e T) as Typ...
dependent induction H; subst...
all: try rename select (typing _ _ _ _) into Typ.
all: try rename select (typing _ _ _ _) into Typ.
all: try rename select (typing_ctx _ _ _ _) into TypCtx.
all: try rename select (typing_ctx _ _ _ _) into TypCtx.
Case "typing_var".
select (binds _ _ _) (fun H => analyze_binds H).
Case "typing_app".
eapply progress_value_step...
Case "typing_tapp".
eapply progress_value_step...
Case "typing_qapp".
eapply progress_value_step...
Qed.