LN.Fsub_Lemmas
Administrative lemmas for Fsub.
Authors: Brian Aydemir and Arthur Chargu\'eraud, with help from
Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
This file contains a number of administrative lemmas that we
require for proving type-safety. The lemmas mainly concern the
relations wf_typ and wf_env.
This file also contains regularity lemmas, which show that various
relations hold only for locally closed terms. In addition to
being necessary to complete the proof of type-safety, these lemmas
help demonstrate that our definitions are correct; they would be
worth proving even if they are unneeded for any "real" proofs.
Table of contents:
Require Export Fsub_Infrastructure.
(* ********************************************************************** *)
Lemma type_from_wf_typ : forall E T,
wf_typ E T -> type T.
Proof.
intros E T H; induction H; eauto.
Qed.
The remaining properties are analogous to the properties that we
need to show for the subtyping and typing relations.
Lemma wf_typ_weakening : forall T E F G,
wf_typ (G ++ E) T ->
uniq (G ++ F ++ E) ->
wf_typ (G ++ F ++ E) T.
Proof with simpl_env; eauto.
intros T E F G Hwf_typ Hk.
remember (G ++ E) as F'.
generalize dependent G.
induction Hwf_typ; intros G Hok Heq; subst...
Case "type_all".
pick fresh Y and apply wf_typ_all...
rewrite <- app_assoc.
apply H0...
Qed.
Lemma wf_typ_weaken_head : forall T E F,
wf_typ E T ->
uniq (F ++ E) ->
wf_typ (F ++ E) T.
Proof.
intros.
rewrite_env (empty ++ F++ E).
auto using wf_typ_weakening.
Qed.
Lemma wf_typ_narrowing : forall V U T E F X,
wf_typ (F ++ X ~ bind_sub V ++ E) T ->
wf_typ (F ++ X ~ bind_sub U ++ E) T.
Proof with simpl_env; eauto.
intros V U T E F X Hwf_typ.
remember (F ++ X ~ bind_sub V ++ E) as G.
generalize dependent F.
induction Hwf_typ; intros F Heq; subst...
Case "wf_typ_var".
analyze_binds H...
Case "typ_all".
pick fresh Y and apply wf_typ_all...
rewrite <- app_assoc.
apply H0...
Qed.
Lemma wf_typ_strengthening : forall E F x U T,
wf_typ (F ++ x ~ bind_typ U ++ E) T ->
wf_typ (F ++ E) T.
Proof with simpl_env; eauto.
intros E F x U T H.
remember (F ++ x ~ bind_typ U ++ E) as G.
generalize dependent F.
induction H; intros F Heq; subst...
Case "wf_typ_var".
analyze_binds H...
Case "wf_typ_all".
pick fresh Y and apply wf_typ_all...
rewrite <- app_assoc.
apply H1...
Qed.
Lemma wf_typ_subst_tb : forall F Q E Z P T,
wf_typ (F ++ Z ~ bind_sub Q ++ E) T ->
wf_typ E P ->
uniq (map (subst_tb Z P) F ++ E) ->
wf_typ (map (subst_tb Z P) F ++ E) (subst_tt Z P T).
Proof with simpl_env; eauto using wf_typ_weaken_head, type_from_wf_typ.
intros F Q E Z P T WT WP.
remember (F ++ Z ~ bind_sub Q ++ E) as G.
generalize dependent F.
induction WT; intros F EQ Ok; subst; simpl subst_tt...
Case "wf_typ_var".
destruct (X == Z); subst...
SCase "X <> Z".
analyze_binds H...
apply (wf_typ_var (subst_tt Z P U))...
Case "wf_typ_all".
pick fresh Y and apply wf_typ_all...
rewrite subst_tt_open_tt_var...
rewrite_env (map (subst_tb Z P) (Y ~ bind_sub T1 ++ F) ++ E).
apply H0...
Qed.
Lemma wf_typ_open : forall E U T1 T2,
uniq E ->
wf_typ E (typ_all T1 T2) ->
wf_typ E U ->
wf_typ E (open_tt T2 U).
Proof with simpl_env; eauto.
intros E U T1 T2 Ok WA WU.
inversion WA; subst.
pick fresh X.
rewrite (subst_tt_intro X)...
rewrite_env (map (subst_tb X U) empty ++ E).
eapply wf_typ_subst_tb...
Qed.
(* ********************************************************************** *)
We add uniq_from_wf_env as a hint here since it helps blur the
distinction between wf_env and uniq in proofs. The lemmas in
the MetatheoryEnv library use uniq, whereas here we naturally
have (or can easily show) the stronger wf_env. Thus,
uniq_from_wf_env serves as a bridge that allows us to use the
environments library.
Hint Resolve uniq_from_wf_env : core.
Lemma wf_typ_from_binds_typ : forall x U E,
wf_env E ->
binds x (bind_typ U) E ->
wf_typ E U.
Proof with auto using wf_typ_weaken_head.
induction 1; intros J; analyze_binds J...
injection BindsTacVal; intros; subst...
Qed.
Lemma wf_typ_from_wf_env_typ : forall x T E,
wf_env (x ~ bind_typ T ++ E) ->
wf_typ E T.
Proof.
intros x T E H. inversion H; auto.
Qed.
Lemma wf_typ_from_wf_env_sub : forall x T E,
wf_env (x ~ bind_sub T ++ E) ->
wf_typ E T.
Proof.
intros x T E H. inversion H; auto.
Qed.
(* ********************************************************************** *)
Properties of wf_env
Lemma wf_env_narrowing : forall V E F U X,
wf_env (F ++ X ~ bind_sub V ++ E) ->
wf_typ E U ->
wf_env (F ++ X ~ bind_sub U ++ E).
Proof with eauto using wf_typ_narrowing.
induction F; intros U X Wf_env Wf;
inversion Wf_env; subst; simpl_env in *...
Qed.
Lemma wf_env_strengthening : forall x T E F,
wf_env (F ++ x ~ bind_typ T ++ E) ->
wf_env (F ++ E).
Proof with eauto using wf_typ_strengthening.
induction F; intros Wf_env; inversion Wf_env; subst; simpl_env in *...
Qed.
Lemma wf_env_subst_tb : forall Q Z P E F,
wf_env (F ++ Z ~ bind_sub Q ++ E) ->
wf_typ E P ->
wf_env (map (subst_tb Z P) F ++ E).
Proof with eauto 6 using wf_typ_subst_tb.
induction F; intros Wf_env WP; simpl_env;
inversion Wf_env; simpl_env in *; simpl subst_tb...
Qed.
(* ********************************************************************** *)
Lemma notin_fv_tt_open : forall (Y X : atom) T,
X `notin` fv_tt (open_tt T Y) ->
X `notin` fv_tt T.
Proof.
intros Y X T. unfold open_tt.
generalize 0.
induction T; simpl; intros k Fr; eauto.
Qed.
Lemma notin_fv_wf : forall E (X : atom) T,
wf_typ E T ->
X `notin` dom E ->
X `notin` fv_tt T.
Proof with auto.
intros E X T Wf_typ.
induction Wf_typ; intros Fr; simpl...
Case "wf_typ_var".
assert (X0 `in` (dom E))...
eapply binds_In; eauto.
assert (X <> X0) by fsetdec. fsetdec.
Case "wf_typ_all".
apply notin_union...
pick fresh Y.
apply (notin_fv_tt_open Y)...
Qed.
Lemma map_subst_tb_id : forall G Z P,
wf_env G ->
Z `notin` dom G ->
G = map (subst_tb Z P) G.
Proof with auto.
intros G Z P H.
induction H; simpl; intros Fr; simpl_env...
rewrite <- IHwf_env...
rewrite <- subst_tt_fresh... eapply notin_fv_wf; eauto.
rewrite <- IHwf_env...
rewrite <- subst_tt_fresh... eapply notin_fv_wf; eauto.
Qed.
(* ********************************************************************** *)
Lemma sub_regular : forall E S T,
sub E S T ->
wf_env E /\ wf_typ E S /\ wf_typ E T.
Proof with simpl_env; try solve [auto | intuition auto].
intros E S T H.
induction H...
Case "sub_trans_tvar".
intuition eauto.
Case "sub_all".
repeat split...
SCase "Second of original three conjuncts".
pick fresh Y and apply wf_typ_all...
destruct (H1 Y)...
rewrite_env (empty ++ Y ~ bind_sub S1 ++ E).
apply (wf_typ_narrowing T1)...
SCase "Third of original three conjuncts".
pick fresh Y and apply wf_typ_all...
destruct (H1 Y)...
Qed.
Lemma typing_regular : forall E e T,
typing E e T ->
wf_env E /\ expr e /\ wf_typ E T.
Proof with simpl_env; try solve [auto | intuition auto].
intros E e T H; induction H...
Case "typing_var".
repeat split...
eauto using wf_typ_from_binds_typ.
Case "typing_abs".
pick fresh y.
destruct (H0 y) as [Hok [J K]]...
repeat split. inversion Hok...
SCase "Second of original three conjuncts".
pick fresh x and apply expr_abs.
eauto using type_from_wf_typ, wf_typ_from_wf_env_typ.
destruct (H0 x)...
SCase "Third of original three conjuncts".
apply wf_typ_arrow; eauto using wf_typ_from_wf_env_typ.
rewrite_env (empty ++ E).
eapply wf_typ_strengthening; simpl_env; eauto.
Case "typing_app".
repeat split...
destruct IHtyping1 as [_ [_ K]].
inversion K...
Case "typing_tabs".
pick fresh Y.
destruct (H0 Y) as [Hok [J K]]...
inversion Hok; subst.
repeat split...
SCase "Second of original three conjuncts".
pick fresh X and apply expr_tabs.
eauto using type_from_wf_typ, wf_typ_from_wf_env_sub...
destruct (H0 X)...
SCase "Third of original three conjuncts".
pick fresh Z and apply wf_typ_all...
destruct (H0 Z)...
Case "typing_tapp".
destruct (sub_regular _ _ _ H0) as [R1 [R2 R3]].
repeat split...
SCase "Second of original three conjuncts".
apply expr_tapp...
eauto using type_from_wf_typ.
SCase "Third of original three conjuncts".
destruct IHtyping as [R1' [R2' R3']].
eapply wf_typ_open; eauto.
Case "typing_sub".
repeat split...
destruct (sub_regular _ _ _ H0)...
Case "typing_let".
repeat split...
SCase "Second of original three conjuncts".
pick fresh y and apply expr_let...
destruct (H1 y) as [K1 [K2 K3]]...
SCase "Third of original three conjuncts".
pick fresh y.
destruct (H1 y) as [K1 [K2 K3]]...
rewrite_env (empty ++ E).
eapply wf_typ_strengthening; simpl_env; eauto.
Case "typing_case".
repeat split...
SCase "Second of original three conjuncts".
pick fresh x and apply expr_case...
destruct (H1 x) as [? [? ?]]...
destruct (H3 x) as [? [? ?]]...
SCase "Third of original three conjuncts".
pick fresh y.
destruct (H1 y) as [K1 [K2 K3]]...
rewrite_env (empty ++ E).
eapply wf_typ_strengthening; simpl_env; eauto.
Qed.
Lemma value_regular : forall e,
value e ->
expr e.
Proof.
intros e H. induction H; auto.
Qed.
Lemma red_regular : forall e e',
red e e' ->
expr e /\ expr e'.
Proof with try solve [auto | intuition auto].
intros e e' H.
induction H; assert(J := value_regular); split...
Case "red_abs".
inversion H. pick fresh y. rewrite (subst_ee_intro y)...
Case "red_tabs".
inversion H. pick fresh Y. rewrite (subst_te_intro Y)...
Qed.
(* *********************************************************************** *)
Automation
Hint Extern 1 (wf_env ?E) =>
match goal with
| H: sub _ _ _ |- _ => apply (proj1 (sub_regular _ _ _ H))
| H: typing _ _ _ |- _ => apply (proj1 (typing_regular _ _ _ H))
end : core.
Hint Extern 1 (wf_typ ?E ?T) =>
match goal with
| H: typing E _ T |- _ => apply (proj2 (proj2 (typing_regular _ _ _ H)))
| H: sub E T _ |- _ => apply (proj1 (proj2 (sub_regular _ _ _ H)))
| H: sub E _ T |- _ => apply (proj2 (proj2 (sub_regular _ _ _ H)))
end : core.
Hint Extern 1 (type ?T) =>
let go E := apply (type_from_wf_typ E); auto in
match goal with
| H: typing ?E _ T |- _ => go E
| H: sub ?E T _ |- _ => go E
| H: sub ?E _ T |- _ => go E
end : core.
Hint Extern 1 (expr ?e) =>
match goal with
| H: typing _ ?e _ |- _ => apply (proj1 (proj2 (typing_regular _ _ _ H)))
| H: red ?e _ |- _ => apply (proj1 (red_regular _ _ H))
| H: red _ ?e |- _ => apply (proj2 (red_regular _ _ H))
end : core.