Commit 0f2eb41b by Ifaz Kabir

kDOT 8.8.1 port and literal bindings

parent f90a2d5a
......@@ -18,3 +18,4 @@ _CoqProject
Makefile.coq
Makefile.coq.conf
html/
.coqdeps.d
......@@ -9,10 +9,10 @@ If you want to understand the DOT safety proof, or are interested in creating yo
## Compiling the Proof
To compile the proof, we require `coq 8.7.2` and related tooling to be run in a unix-like environment. We also require `coq-tlc` library. We recommend installing both using `opam`.
To compile the proof, we require `coq 8.8.1` and related tooling to be run in a unix-like environment. We also require `coq-tlc` library. We recommend installing both using `opam`.
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq 8.7.2
opam pin add coq 8.8.1
opam install coq
opam install coq-tlc
......
......@@ -30,8 +30,6 @@ Proof.
intros. destruct d; reflexivity.
Qed.
Opaque label_of.
(** [l \notin labels(ds)] #<br>#
[――――――――――――――――――――――] #<br>#
[l \notin labels(ds[y/x]] *)
......@@ -51,27 +49,144 @@ Notation ctx := (env typ).
(** A heap, maps locations to heap items. *)
Notation heap := (env item).
Inductive trm_item_fun : item -> trm -> Prop :=
| trm_item_fun_c : forall T t,
trm_item_fun (item_fun T t) (trm_lambda T t).
Inductive lit_item_fun : item -> lit -> Prop :=
| lit_item_fun_c : forall T t,
lit_item_fun (item_fun T t) (lit_fun T t).
Inductive trm_item_con : item -> trm -> Prop :=
| trm_item_con_c : forall Ts T ds t,
trm_item_con (item_con Ts T ds t) (trm_con Ts T ds t).
Inductive lit_item_con : item -> lit -> Prop :=
| lit_item_con_c : forall Ts T ds t,
lit_item_con (item_con Ts T ds t) (lit_con Ts T ds t).
Hint Constructors trm_item_con trm_item_fun.
Hint Constructors lit_item_con lit_item_fun.
(** ** Tactics *)
(** Tactics for avars *)
Ltac fold_var_abs :=
repeat match goal with
| |- context [(AvarOpenable ?x)] =>
change (AvarOpenable x) with (@open_rec avar AvarOpenable x)
| |- context [(AvarFreeVar ?x)] =>
change (AvarFreeVar x) with (@fv avar AvarFreeVar x)
| |- context [(AvarSubstVar ?x)] =>
change (AvarSubstVar x) with (@subst_var avar AvarSubstVar x)
end.
Tactic Notation "fold_var_abs" "in" hyp(H) :=
repeat match type of H with
| context [(AvarOpenable ?x)] =>
change (AvarOpenable x) with (@open_rec avar AvarOpenable x) in H
| context [(AvarFreeVar ?x)] =>
change (AvarFreeVar x) with (@fv avar AvarFreeVar x) in H
| context [(AvarSubstVar ?x)] =>
change (AvarSubstVar x) with (@subst_var avar AvarSubstVar x) in H
end.
Tactic Notation "fold_var_abs" "in" "*" :=
repeat match goal with
| [H : context [(AvarOpenable ?x)] |- _] =>
change (AvarOpenable x) with (@open_rec avar AvarOpenable x) in *
| |- context [(AvarOpenable ?x)] =>
change (AvarOpenable x) with (@open_rec avar AvarOpenable x) in *
| [H : context [(AvarFreeVar ?x)] |- _] =>
change (AvarFreeVar x) with (@fv avar AvarFreeVar x) in *
| |- context [(AvarFreeVar ?x)] =>
change (AvarFreeVar x) with (@fv avar AvarFreeVar x) in *
| [H : context [(AvarSubstVar ?x)] |- _] =>
change (AvarSubstVar x) with (@subst_var avar AvarSubstVar x) in *
| |- context [(AvarSubstVar ?x)] =>
change (AvarSubstVar x) with (@subst_var avar AvarSubstVar x) in *
| [H : context [(@ListOpenable avar AvarOpenable ?x)] |- _] =>
change (@ListOpenable avar AvarOpenable ?x) with
(@open_rec (list avar) (@ListOpenable avar AvarOpenable) x) in *
| |- context [(@ListOpenable avar AvarOpenable ?x)] =>
change (@ListOpenable avar AvarOpenable ?x) with
(@open_rec (list avar) (@ListOpenable avar AvarOpenable) x) in *
| [H : context [(@ListFreeVar avar AvarFreeVar ?x)] |- _] =>
change (@ListFreeVar avar AvarFreeVar ?x) with
(@fv (list avar) (@ListFreeVar avar AvarFreeVar) x) in *
| |- context [(@ListFreeVar avar AvarFreeVar ?x)] =>
change (@ListFreeVar avar AvarFreeVar ?x) with
(@fv (list avar) (@ListFreeVar avar AvarFreeVar) x) in *
| [H : context [(@ListSubstVar avar AvarSubstVar ?x)] |- _] =>
change (@ListSubstVar avar AvarSubstVar ?x) with
(@subst_var (list avar) (@ListSubstVar avar AvarSubstVar) x) in *
| |- context [(@ListSubstVar avar AvarSubstVar ?x)] =>
change (@ListSubstVar avar AvarSubstVar ?x) with
(@subst_var (list avar) (@ListSubstVar avar AvarSubstVar) x) in *
end.
(** Tactics for Types *)
Tactic Notation "fold_typ_abs" "in" hyp(H) :=
change (open_rec_dec) with (@open_rec dec DecOpenable) in H;
change (open_rec_typs) with (@open_rec typs TypsOpenable) in H;
change (open_rec_typ) with (@open_rec typ TypOpenable) in H;
change (fv_dec) with (@fv dec DecFreeVar) in H;
change (fv_typs) with (@fv typs TypsFreeVar) in H;
change (fv_typ) with (@fv typ TypFreeVar) in H;
change (subst_dec) with (@subst_var dec DecSubstVar) in H;
change (subst_typs) with (@subst_var typs TypsSubstVar) in H;
change (subst_typ) with (@subst_var typ TypSubstVar) in H.
Tactic Notation "fold_typ_abs" "in" "*" :=
change (open_rec_dec) with (@open_rec dec DecOpenable) in *;
change (open_rec_typs) with (@open_rec typs TypsOpenable) in *;
change (open_rec_typ) with (@open_rec typ TypOpenable) in *;
change (fv_dec) with (@fv dec DecFreeVar) in *;
change (fv_typs) with (@fv typs TypsFreeVar) in *;
change (fv_typ) with (@fv typ TypFreeVar) in *;
change (subst_dec) with (@subst_var dec DecSubstVar) in *;
change (subst_typs) with (@subst_var typs TypsSubstVar) in *;
change (subst_typ) with (@subst_var typ TypSubstVar) in *.
(** Tactics for Terms *)
Tactic Notation "fold_trm_abs" "in" hyp(H) :=
change (open_rec_trm) with (@open_rec trm TrmOpenable) in H;
change (open_rec_lit) with (@open_rec lit LitOpenable) in H;
change (open_rec_def) with (@open_rec def DefOpenable) in H;
change (open_rec_defs) with (@open_rec defs DefsOpenable) in H;
change (fv_trm) with (@fv trm TrmFreeVar) in H;
change (fv_lit) with (@fv lit LitFreeVar) in H;
change (fv_def) with (@fv def DefFreeVar) in H;
change (fv_defs) with (@fv defs DefsFreeVar) in H;
change (subst_trm) with (@subst_var trm TrmSubstVar) in H;
change (subst_lit) with (@subst_var lit LitSubstVar) in H;
change (subst_def) with (@subst_var def DefSubstVar) in H;
change (subst_defs) with (@subst_var defs DefsSubstVar) in H.
Tactic Notation "fold_trm_abs" "in" "*" :=
change (open_rec_trm) with (@open_rec trm TrmOpenable) in *;
change (open_rec_lit) with (@open_rec lit LitOpenable) in *;
change (open_rec_def) with (@open_rec def DefOpenable) in *;
change (open_rec_defs) with (@open_rec defs DefsOpenable) in *;
change (fv_trm) with (@fv trm TrmFreeVar) in *;
change (fv_lit) with (@fv lit LitFreeVar) in *;
change (fv_def) with (@fv def DefFreeVar) in *;
change (fv_defs) with (@fv defs DefsFreeVar) in *;
change (subst_trm) with (@subst_var trm TrmSubstVar) in *;
change (subst_lit) with (@subst_var lit LitSubstVar) in *;
change (subst_def) with (@subst_var def DefSubstVar) in *;
change (subst_defs) with (@subst_var defs DefsSubstVar) in *.
(** Tactics for simplifying SyntaxClasses *)
Tactic Notation "sympl" :=
simpl; autorewrite with avar_db typ_db trm_db.
rewrite ? to_list_of_list, ? of_list_to_list;
simpl; repeat (fold_var_abs; fold_typ_abs; fold_trm_abs);
rewrite ? to_list_of_list, ? of_list_to_list.
Tactic Notation "sympl" "in" hyp(H) :=
simpl in H; autorewrite with avar_db typ_db trm_db in H.
rewrite ? to_list_of_list, ? of_list_to_list in H;
simpl in H;
repeat (fold_var_abs in H; fold_typ_abs in H; fold_trm_abs in H);
rewrite ? to_list_of_list, ? of_list_to_list in H.
Tactic Notation "sympl" "in" "*" :=
simpl in *; autorewrite with avar_db typ_db trm_db in *.
rewrite ? to_list_of_list, ? of_list_to_list in *; simpl in *;
repeat (fold_var_abs in *; fold_typ_abs in *; fold_trm_abs in *);
rewrite ? to_list_of_list, ? of_list_to_list in *.
Ltac sympls := sympl in *.
(** Tactics for generating fresh variables. *)
......@@ -87,12 +202,12 @@ Ltac gather_vars :=
let I := gather_vars_with (fun x : defs => fv x ) in
let J := gather_vars_with (fun x : typ => fv x ) in
let K := gather_vars_with (fun x : typs => fv x ) in
constr:(A \u B \u C \u D \u E \u F \u G \u H \u I \u J \u K).
let L := gather_vars_with (fun x : lit => fv x ) in
constr:(A \u B \u C \u D \u E \u F \u G \u H \u I \u J \u K \u L).
Ltac pick_fresh x :=
let L := gather_vars in
(pick_fresh_gen L x);
autorewrite with avar_db typ_db trm_db in *.
(pick_fresh_gen L x); sympl in *.
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
......@@ -78,7 +78,7 @@ Lemma strong_mu_to_new: forall G s x T,
ty_item_s G s x ->
binds x (typ_bnd T) G ->
exists ds, binds x (item_obj T (open x ds)) s /\
G /- open x ds :: open x T.
G open x ds open x T.
Proof.
introv Hi Hts Bi.
inversions Hts; binds_eq.
......@@ -173,8 +173,8 @@ Lemma canonical_forms_con: forall G s x Ts T,
fresh L (S (length_s Ts)) (cons x ys) ->
G & (ys ~** (to_list Ts))
& (x ~ open_vars (cons x ys) T)
/- (open_vars (cons x ys) ds)
:: (open_vars (cons x ys) T)) /\
(open_vars (cons x ys) ds)
(open_vars (cons x ys) T)) /\
(forall x ys,
length ys = length_s Ts ->
fresh L (S (length_s Ts)) (cons x ys) ->
......
......@@ -78,12 +78,13 @@ Lemma general_to_tight: forall G0,
G = G0 ->
G # S <: U) /\
(forall G avs Ts,
G avs :l Ts ->
G avs :: Ts ->
G = G0 ->
G # avs :l Ts).
G # avs :: Ts).
Proof.
intros G0 HG.
apply ts_mutind; intros; subst; try solve [eapply sel_replacement; auto]; eauto.
apply ts_mutind; intros; subst;
try solve [eapply sel_replacement; auto]; eauto.
Qed.
(** The general-to-tight lemma, formulated for term typing. *)
......
......@@ -47,8 +47,8 @@ Inductive ty_item_s : ctx -> heap -> var -> Prop :=
fresh L (S (length ys)) (cons x ys) ->
G & (ys ~** (to_list Ts))
& (x ~ open_vars (cons x ys) T)
/- (open_vars (cons x ys) ds)
:: (open_vars (cons x ys) T)) ->
(open_vars (cons x ys) ds)
(open_vars (cons x ys) T)) ->
(forall x ys,
length ys = length_s Ts ->
fresh L (S (length ys)) (cons x ys) ->
......@@ -60,7 +60,7 @@ Inductive ty_item_s : ctx -> heap -> var -> Prop :=
binds x T G ->
binds x (item_obj U (open x ds)) s ->
T = typ_bnd U ->
G /- open x ds :: open x U ->
G open x ds open x U ->
ty_item_s G s x.
Hint Constructors ty_item_s.
......@@ -171,7 +171,7 @@ Qed.
Lemma heap_correspond_push_obj: forall L G s x T ds,
heap_correspond G s ->
x # G ->
(forall x : var, x \notin L -> G & x ~ open x T /- open x ds :: open x T) ->
(forall x : var, x \notin L -> G & x ~ open x T open x ds open x T) ->
x \notin fv ds ->
heap_correspond (G & x ~ typ_bnd T) (s & x ~ item_obj T (open x ds)).
Proof.
......@@ -187,7 +187,7 @@ Proof.
pick_fresh z.
apply (@renaming_def _ _ z); auto.
-- rewrite fv_env_push; sympl; auto.
-- eapply (proj43 weaken_rules); auto.
-- eapply (proj54 weaken_rules); auto.
* apply ty_item_s_push; eauto using binds_to_dom.
Qed.
......
......@@ -52,7 +52,6 @@ Proof.
- unfold defs_hasnt; simpl.
assert (label_of d <> l).
{ inversion H0. cases_if. auto. }
unfold label_of in H1; simpl in H1.
cases_if.
assert (defs_hasnt ds l).
{ inversion H0. cases_if. auto. }
......@@ -72,13 +71,13 @@ Qed.
Require Import RecordAndInertTypes PreciseTyping HeapCorrespondence CanonicalForms.
Lemma defs_update_typing: forall G ds U ds' a x T,
Lemma defs_update_typing: forall G (ds : defs) U (ds' : defs) a x T,
defs_update ds a x ds' ->
record_type U ->
G /- ds :: U ->
G ds U ->
record_has U (dec_trm a T T) ->
G trm_var (avar_f x) T ->
G /- ds' :: U.
G ds' U.
Proof.
introv H; gen U T. induction H; intros.
- inversions H0. inversions H7.
......@@ -106,41 +105,37 @@ Lemma heap_update_inert: forall G s s' x y a T,
Proof.
introv Hin Hst Hty Hsto.
remember (trm_asn (avar_f x) a (avar_f y)) as t.
induction Hty; inversions Heqt; eauto.
pose proof (canonical_forms_obj Hin Hst Hty1) as [?S [?ds [?t [?H [?H ?H]]]]].
induction Hty; inversions Heqt; eauto. clear IHHty IHHty0.
pose proof (canonical_forms_obj Hin Hst H) as [?S [?ds [?t [?H [?H ?H]]]]].
unfold heap_update in Hsto.
destruct Hsto as [?Hoks [?Hoks' [?Hdom [?Hbi [?T [?ds [?ds' [?H [?Hdefup ?Hbis']]]]]]]]].
pose proof (binds_functional H2 H) as Hveq; inversions Hveq; clear H.
destruct Hsto as
[?Hoks [?Hoks' [?Hdom [?Hbi [?T [?ds [?ds' [?H [?Hdefup ?Hbis']]]]]]]]].
pose proof (binds_functional H4 H1) as Hveq; inversions Hveq; clear H1.
destruct Hst as [?H [?H [?H ?H]]].
unfold heap_correspond; repeat_split_right; auto; try congruence.
intros. clear IHHty1 IHHty2 H3.
pose proof (dom_to_binds H6) as [?T ?H].
pose proof (H5 _ H6) as Htyv.
rewrite H4 in H6.
pose proof (dom_to_binds H6) as [?v ?H].
unfold heap_correspond; repeat_split_right; try congruence; auto.
intros. clear H5 H1.
pose proof (dom_to_binds H8) as [?T ?H].
pose proof (H7 _ H8) as Htyv.
rewrite H6 in H8.
pose proof (dom_to_binds H8) as [?v ?H].
pose proof (defs_update_open x Hdefup ds eq_refl) as [?ds' ?Hds'].
destruct (var_decide x0 x).
- subst. clear H7 v.
- subst.
eapply ty_item_obj_s; eauto.
+ pose proof (var_typ_rcd_to_binds Hin Hty1) as [?S [?T [?Hbi ?H]]].
pose proof (binds_functional Hbi0 H3); subst T0; clear Hbi0.
+ pose proof (var_typ_rcd_to_binds Hin H) as [?S [?T [?Hbi ?H]]].
pose proof (binds_functional Hbi0 H1); subst T0; clear Hbi0.
inversions Htyv;
match goal with
| [ H : binds ?x ?T ?G, H' : binds ?x ?T' ?G |- _] =>
pose proof (binds_functional H H'); congruence
end.
+ inversions Htyv;
pose proof (binds_functional H8 H2); try congruence.
inversions H9.
pose proof (binds_functional H3 H7); subst; clear H7.
autorewrite with trm_db in *. rewrite H13 in *. clear H13.
pose proof (var_typ_rcd_to_binds Hin Hty1) as [?S [?T [?Hbi [?Hrh [?H ?H]]]]].
pose proof (binds_functional H3 Hbi0). inversions H11.
+ inversions Htyv; repeat binds_eq. rewrite H14 in *. clear H10 H11.
pose proof (var_typ_rcd_to_binds Hin H)
as [?S [?T [?Hbi [?Hrh [?H ?H]]]]]. binds_eq.
eapply defs_update_typing; eauto.
pose proof (binds_inert H3 Hin). inversions H11.
pose proof (binds_inert H1 Hin). inversions H10.
apply open_record_type; auto.
- apply (Hbi _ _ n) in H7. rename n into Hneq.
clear Hbis' H2 Hdefup.
- apply (Hbi _ _ n) in H5. rename n into Hneq.
inversions Htyv; eauto.
Qed.
......@@ -177,7 +172,6 @@ Proof.
pose proof (binds_push_inv H0) as [[?H ?H] | [?H ?H]]; subst.
+ exists (s & x ~ item_obj U (ds')) ds'.
repeat_split_right; auto.
* destruct (ok_push_inv H); auto.
* simpl_dom; auto.
* intros.
pose proof (binds_push_inv H4) as [[?H ?H] | [?H ?H]]; try congruence.
......@@ -186,7 +180,7 @@ Proof.
pose proof (IHs x0 _ _ _ _ y Hoks H4 H1) as
[?s' [?ds' [?Hoks' [?Hdeq [?H [?H ?H]]]]]].
exists (s' & x ~ v) (ds'0). repeat_split_right; auto.
* apply ok_push; auto.
* apply ok_push; auto 1.
pose proof (ok_push_inv H) as [_ ?H].
rewrite <- Hdeq; auto.
* simpl_dom. rewrite Hdeq; auto.
......
......@@ -11,17 +11,9 @@ Require Import AbstractSyntax
Hint Resolve general_to_tight_typing.
Lemma inert_con_typing : forall G Ts T ds t U,
inert G ->
G trm_con Ts T ds t U ->
con_sup G (typ_con Ts T) U.
Proof.
eauto using inert_tight_con_typing.
Qed.
Lemma inert_trm_con_typing : forall G Ts T Ts' T' ds t,
inert G ->
G trm_con Ts' T' ds t typ_con Ts T ->
G lit_con Ts' T' ds t typ_con Ts T ->
Ts' = Ts /\ T' = T.
Proof.
introv Hi HT.
......@@ -30,42 +22,36 @@ Qed.
Lemma inert_trm_con_defs : forall G Ts T ds t,
inert G ->
G trm_con Ts T ds t typ_con Ts T ->
G lit_con Ts T ds t typ_con Ts T ->
exists L, forall (x : var) (ys : list var),
length ys = length_s Ts ->
fresh L (S (length ys)) (x :: ys) ->
G & ys ~** to_list Ts & x ~ open_vars (x :: ys) T /-
open_vars (x :: ys) ds :: open_vars (x :: ys) T.
G & ys ~** to_list Ts & x ~ open_vars (x :: ys) T
open_vars (x :: ys) ds open_vars (x :: ys) T.
Proof.
introv Hi Ht.
pose proof (general_to_tight_typing Hi Ht) as Htt. clear Ht.
remember (trm_con Ts T ds t) as T' eqn:Heq.
induction Htt; inversions Heq; eauto.
introv Hi Ht. inversions Ht; eauto.
Qed.
Lemma inert_trm_con_trm : forall G Ts T ds t,
inert G ->
G trm_con Ts T ds t typ_con Ts T ->
G lit_con Ts T ds t typ_con Ts T ->
exists L T', forall (x : var) (ys : list var),
length ys = length_s Ts ->
fresh L (S (length ys)) (x :: ys) ->
(G & ys ~** to_list Ts & x ~ open_vars (x :: ys) T)
open_vars (x :: ys) t open_vars (x :: ys) T'.
Proof.
introv Hi Ht.
pose proof (general_to_tight_typing Hi Ht) as Htt. clear Ht.
remember (trm_con Ts T ds t) as T' eqn:Heq.
induction Htt; inversions Heq; eauto.
introv Hi Ht. inversions Ht; eauto.
Qed.
Lemma inert_trm_con_apply_trm : forall G Ts T ds t x xs avs,
inert G ->
G trm_con Ts T ds t typ_con Ts T ->
G lit_con Ts T ds t typ_con Ts T ->
x # G ->
x \notin fv (open_rec_vars 1 xs ds) ->
length xs = length_s Ts ->
vars_of_avars xs avs ->
G avs :l Ts ->
G avs :: Ts ->
exists T', G & x ~ open_rec_vars 1 xs (open x T)
open_rec_vars 1 xs (open x t) T'.
Proof.
......@@ -127,15 +113,15 @@ Qed.
Lemma inert_trm_con_apply_defs : forall G Ts T ds t x xs avs,
inert G ->
G trm_con Ts T ds t typ_con Ts T ->
G lit_con Ts T ds t typ_con Ts T ->
x # G ->
x \notin fv (open_rec_vars 1 xs ds) ->
length xs = length_s Ts ->
vars_of_avars xs avs ->
G avs :l Ts ->
G avs :: Ts ->
G & x ~ open_rec_vars 1 xs (open x T)
/- open_rec_vars 1 xs (open x ds)
:: open_rec_vars 1 xs (open x T).
open_rec_vars 1 xs (open x ds)
open_rec_vars 1 xs (open x T).
Proof.
intros.
apply (inert_trm_con_defs H) in H0. destruct H0 as [L Hdefs].
......@@ -151,8 +137,8 @@ Proof.
destruct H0 as [x' [ys' [?H ?H]]].
assert (fresh L (S (length ys')) (x' :: ys')) by (subst L'; auto).
specialize (Hdefs _ _ H6 H7). clear H7.
assert (G & x' ~ open_vars (x' :: xs) T /-
open_vars (x' :: xs) ds :: open_vars (x' :: xs) T).
assert (G & x' ~ open_vars (x' :: xs) T
open_vars (x' :: xs) ds open_vars (x' :: xs) T).
{ sympl. destruct H0.
eapply (weaken_middle_singles_defs) with (L:=L); subst; eauto 3.
pose proof (fv_open_cases x' T 0) as Hfv1.
......@@ -185,7 +171,7 @@ Qed.
Lemma inert_trm_con_record_type : forall G Ts T ds t,
inert G ->
G trm_con Ts T ds t typ_con Ts T ->
G lit_con Ts T ds t typ_con Ts T ->
record_type T.
Proof.
introv Hi Ht. pose proof (inert_trm_con_defs Hi Ht) as [L H].
......
......@@ -2,14 +2,10 @@
Set Implicit Arguments.
Require Import Coq.Program.Equality.
Require Import LibExtra DotTactics.
Require Import AbstractSyntax GeneralTyping
RecordAndInertTypes PreciseTyping TightTyping Narrowing.
Local Hint Resolve x_bound_unique.
Local Hint Resolve pf_inert_unique_tight_bounds.
(** * Super Types of Objects *)
Inductive bnd_sup : ctx -> typ -> typ -> Prop :=
| bnd_sup_top : forall G T,
......@@ -32,10 +28,12 @@ Ltac unique_bind_bounds :=
| [ Hin : inert ?G,
H : ?G ! ?x ?U typ_rcd (dec_typ ?A ?S ?S),
H' : ?G ! ?x ?U' typ_rcd (dec_typ ?A ?S' ?S') |- _ ] =>
replace U' with U in * by eauto 3;
replace S' with S in * by eauto 3
pose proof (x_bound_unique H H'); subst;
pose proof (pf_inert_unique_tight_bounds Hin H H'); subst
end.
Local Hint Extern 1 => unique_bind_bounds.
Lemma tight_bnd_sup: forall G S T U,
inert G ->
G # T <: U ->
......@@ -43,13 +41,11 @@ Lemma tight_bnd_sup: forall G S T U,
bnd_sup G (typ_bnd S) U.
Proof.
introv Hi H.
dependent induction H; intros;
induction H; intros;
match goal with
| [ H : bnd_sup _ _ _ |- _ ] =>
try solve [inversions H; auto]
end; eauto.
inversions H0; auto.
unique_bind_bounds; auto.
Qed.
Local Hint Resolve tight_bnd_sup.
......@@ -86,43 +82,38 @@ Lemma tight_all_sup: forall G S T U1 U2,
all_sup G (typ_all S T) U2.
Proof.
introv Hi H.
dependent induction H; intros; auto;
induction H; intros; auto;
match goal with
| |- all_sup _ _ (typ_sel (avar_f _) _) =>
eauto
| [ H : all_sup _ _ _ |- _ ] =>
try solve [inversions H; auto]
end.
- inversions H0; auto.
unique_bind_bounds; auto.
- pose proof ((proj32 tight_to_general) _ _ _ H);
pose proof ((proj32 tight_to_general) _ _ _ H);
inversions H1; apply_fresh all_sup_all as z.
+ eauto.
+ assert (G & z ~ S2 open z T <: open z T1)
by apply* narrow_subtyping; eauto.
- eauto.
- assert (G & z ~ S2 open z T <: open z T1)
by apply* narrow_subtyping; eauto.
Qed.
Local Hint Resolve tight_all_sup.
Lemma inert_tight_lambda_typing : forall G S t U,
inert G ->
G # trm_lambda S t U ->
G lit_fun S t U ->
exists T, all_sup G (typ_all S T) U.
Proof.
introv Hi Hty. dependent induction Hty; eauto.
pose proof (IHHty _ _ Hi eq_refl) as [?T ?H].
exists T0. eapply tight_all_sup; eauto.
introv Hi Hty.
inversions Hty; eauto.
Qed.
Lemma inert_tight_lambda_typing_precise : forall G S t U,
inert G ->
G # trm_lambda S t U ->
G lit_fun S t U ->
exists T L,
(forall x, x \notin L -> G & x ~ S open x t open x T) /\
all_sup G (typ_all S T) U.
Proof.
introv Hi Hty. dependent induction Hty; eauto.
pose proof (IHHty _ _ Hi eq_refl) as [?T [?L ?H]].
exists T0 L. destruct_all; split; eauto using tight_all_sup.
introv Hi Hty. inversion Hty; eauto.
Qed.
(** * Super Types of Constructors *)
......@@ -148,23 +139,21 @@ Lemma tight_con_sup: forall G Ts T U1 U2,
con_sup G (typ_con Ts T) U2.
Proof.
introv Hi H.
dependent induction H; intros;
induction H; intros;
match goal with
| [ H : con_sup _ _ _ |- _ ] =>
try solve [inversions H; auto]
end; eauto.
inversions H0; auto.
unique_bind_bounds; auto.
Qed.
Local Hint Resolve tight_con_sup.
Lemma inert_tight_con_typing : forall G Ts T ds t U,
Lemma inert_con_typing : forall G Ts T ds t U,
inert G ->
G # trm_con Ts T ds t U ->
G lit_con Ts T ds t U ->
con_sup G (typ_con Ts T) U.
Proof.
introv Hi Hty.
dependent induction Hty; eauto.
inversion Hty; eauto.
Qed.
(** * Tight SubTyping Contradictions *)
......
......@@ -198,13 +198,9 @@ Lemma tight_to_invertible :
G ## x U.
Proof.
intros G U x Hgd Hty.
dependent induction Hty.
- eapply ty_precise_inv; econstructor; eauto.
- specialize (IHHty _ Hgd eq_refl).
eapply ty_bnd_inv.
apply IHHty.
- specialize (IHHty _ Hgd eq_refl).
inversion IHHty; subst. apply* ty_precise_inv. assumption.
- apply ty_and_inv; auto.
remember (trm_var (avar_f x)) as t eqn:Heq.
induction Hty; try congruence; inversions Heq; eauto.
- specialize (IHHty Hgd eq_refl).
inversion IHHty; subst; eauto using ty_precise_inv.
- eapply invertible_typing_closure_tight; auto.
Qed.
......@@ -73,7 +73,7 @@ Lemma rev_length_eq_implies_length_eq : forall A B (l1 : list A) (l2 : list B),
Proof.
intros. rewrite ? List.rev_length in *. auto.
Qed.
Hint Resolve length_eq_implies_rev_length_eq rev_length_eq_implies_length_eq.
Hint Resolve length_eq_implies_rev_length_eq.
Lemma var_decide : forall (x y : var), {x = y} + {x <> y}.
......@@ -136,6 +136,18 @@ match goal with
| [H : dom ?G2 = dom ?G1, _ : ?x # ?G1 |- ?x # ?G2 ] => rewrite H; assumption
end.
Lemma ok_val : forall A (E : env A) x v1 v2,
ok (E & x ~ v1) ->
ok (E & x ~ v2).
Proof.
introv H; apply ok_push_inv in H as [? ?]; auto 2.
Qed.
Hint Extern 1 (ok _) =>
match goal with
| [H : ok (?E & ?x ~ ?v1) |- ok (?E & ?x ~ ?v2)] =>
apply (ok_val (v1:=v1)); assumption
end.
Lemma binds_weaken :
forall (A : Type) (x : var) (a : A) (E F G : env A),
binds x a (E & G) -> ok (E & F) -> binds x a (E & F & G).
......@@ -380,7 +392,6 @@ Lemma fresh_ok : forall A (E : env A) v vs x ys,
Proof.
intros. apply ok_push; eauto 2 using fresh_ok_ys, fresh_cons_notin.
Qed.
Hint Resolve fresh_ok.
Lemma fresh_ok_rev : forall A (E : env A) v vs x ys,
fresh (dom E) (S (length ys)) (x :: ys) ->
......@@ -390,6 +401,7 @@ Lemma fresh_ok_rev : forall A (E : env A) v vs x ys,
Proof.
auto using fresh_ok.
Qed.