```(*************************************************************************** * Preservation and Progress for System-F with Subtyping - Infrastructure * * Brian Aydemir & Arthur Charguéraud, March 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory Fsub_Definitions. (* ********************************************************************** *) (** * Additional Definitions Used in the Proofs *) (** Computing free type variables in a type *) Fixpoint fv_tt (T : typ) {struct T} : vars := match T with | typ_top => {} | typ_bvar J => {} | typ_fvar X => {{X}} | typ_arrow T1 T2 => (fv_tt T1) \u (fv_tt T2) | typ_all T1 T2 => (fv_tt T1) \u (fv_tt T2) end. (** Computing free type variables in a term *) Fixpoint fv_te (e : trm) {struct e} : vars := match e with | trm_bvar i => {} | trm_fvar x => {} | trm_abs V e1 => (fv_tt V) \u (fv_te e1) | trm_app e1 e2 => (fv_te e1) \u (fv_te e2) | trm_tabs V e1 => (fv_tt V) \u (fv_te e1) | trm_tapp e1 V => (fv_tt V) \u (fv_te e1) end. (** Computing free term variables in a type *) Fixpoint fv_ee (e : trm) {struct e} : vars := match e with | trm_bvar i => {} | trm_fvar x => {{x}} | trm_abs V e1 => (fv_ee e1) | trm_app e1 e2 => (fv_ee e1) \u (fv_ee e2) | trm_tabs V e1 => (fv_ee e1) | trm_tapp e1 V => (fv_ee e1) end. (** Substitution for free type variables in types. *) Fixpoint subst_tt (Z : var) (U : typ) (T : typ) {struct T} : typ := match T with | typ_top => typ_top | typ_bvar J => typ_bvar J | typ_fvar X => if X == Z then U else (typ_fvar X) | typ_arrow T1 T2 => typ_arrow (subst_tt Z U T1) (subst_tt Z U T2) | typ_all T1 T2 => typ_all (subst_tt Z U T1) (subst_tt Z U T2) end. (** Substitution for free type variables in terms. *) Fixpoint subst_te (Z : var) (U : typ) (e : trm) {struct e} : trm := match e with | trm_bvar i => trm_bvar i | trm_fvar x => trm_fvar x | trm_abs V e1 => trm_abs (subst_tt Z U V) (subst_te Z U e1) | trm_app e1 e2 => trm_app (subst_te Z U e1) (subst_te Z U e2) | trm_tabs V e1 => trm_tabs (subst_tt Z U V) (subst_te Z U e1) | trm_tapp e1 V => trm_tapp (subst_te Z U e1) (subst_tt Z U V) end. (** Substitution for free term variables in terms. *) Fixpoint subst_ee (z : var) (u : trm) (e : trm) {struct e} : trm := match e with | trm_bvar i => trm_bvar i | trm_fvar x => if x == z then u else (trm_fvar x) | trm_abs V e1 => trm_abs V (subst_ee z u e1) | trm_app e1 e2 => trm_app (subst_ee z u e1) (subst_ee z u e2) | trm_tabs V e1 => trm_tabs V (subst_ee z u e1) | trm_tapp e1 V => trm_tapp (subst_ee z u e1) V end. (** Substitution for free type variables in environment. *) Definition subst_tb (Z : var) (P : typ) (b : bind) : bind := match b with | bind_sub T => bind_sub (subst_tt Z P T) | bind_typ T => bind_typ (subst_tt Z P T) end. (* ********************************************************************** *) (** * Tactics *) (** Constructors as hints. *) Hint Constructors type term wft ok okt value red. Hint Resolve sub_top sub_refl_tvar sub_arrow typing_var typing_app typing_tapp typing_sub. (** Gathering free names already used in the proofs *) Ltac gather_vars := let A := gather_vars_with (fun x : vars => x) in let B := gather_vars_with (fun x : var => {{ x }}) in let C := gather_vars_with (fun x : trm => fv_te x) in let D := gather_vars_with (fun x : trm => fv_ee x) in let E := gather_vars_with (fun x : typ => fv_tt x) in let F := gather_vars_with (fun x : env => dom x) in constr:(A \u B \u C \u D \u E \u F). (** "pick_fresh x" tactic create a fresh variable with name x *) Ltac pick_fresh x := let L := gather_vars in (pick_fresh_gen L x). (** "apply_fresh T as x" is used to apply inductive rule which use an universal quantification over a cofinite set *) Tactic Notation "apply_fresh" constr(T) "as" ident(x) := apply_fresh_base T gather_vars x. Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) := apply_fresh T as x; auto*. (** These tactics help applying a lemma which conclusion mentions an environment (E & F) in the particular case when F is empty *) Ltac get_env := match goal with | |- wft ?E _ => E | |- sub ?E _ _ => E | |- typing ?E _ _ => E end. Tactic Notation "apply_empty_bis" tactic(get_env) constr(lemma) := let E := get_env in rewrite <- (concat_empty E); eapply lemma; try rewrite concat_empty. Tactic Notation "apply_empty" constr(F) := apply_empty_bis (get_env) F. Tactic Notation "apply_empty" "*" constr(F) := apply_empty F; auto*. (** Tactic to undo when Coq does too much simplification *) Ltac unsimpl_map_bind := match goal with |- context [ ?B (subst_tt ?Z ?P ?U) ] => unsimpl ((subst_tb Z P) (B U)) end. Tactic Notation "unsimpl_map_bind" "*" := unsimpl_map_bind; auto*. (* ********************************************************************** *) (** * Properties of Substitutions *) (* ********************************************************************** *) (** ** Properties of type substitution in type *) (** Substitution for a fresh name is identity. *) Lemma subst_tt_fresh : forall Z U T, Z \notin fv_tt T -> subst_tt Z U T = T. Proof. induction T; simpl; intros; f_equal*. case_var*. notin_contradiction. Qed. (** Substitution distributes on the open operation. *) Lemma subst_tt_open_tt : forall T1 T2 X P, type P -> subst_tt X P (open_tt T1 T2) = open_tt (subst_tt X P T1) (subst_tt X P T2). Proof. unfold open_tt. use subst_tt_open_tt_rec. Qed. (** Substitution and open_var for distinct names commute. *) Lemma subst_tt_open_tt_var : forall X Y U T, Y <> X -> type U -> (subst_tt X U T) open_tt_var Y = subst_tt X U (T open_tt_var Y). Proof. introv Neq Wu. rewrite* subst_tt_open_tt. simpl. case_var*. Qed. (** Opening up a body t with a type u is the same as opening up the abstraction with a fresh name x and then substituting u for x. *) Lemma subst_tt_intro : forall X T2 U, X \notin fv_tt T2 -> type U -> open_tt T2 U = subst_tt X U (T2 open_tt_var X). Proof. introv Fr Wu. rewrite* subst_tt_open_tt. rewrite* subst_tt_fresh. simpl. case_var*. Qed. (* ********************************************************************** *) (** ** Properties of type substitution in terms *) (** Substitution for a fresh name is identity. *) Lemma subst_te_fresh : forall X U e, X \notin fv_te e -> subst_te X U e = e. Proof. induction e; simpl; intros; f_equal*; use subst_tt_fresh. Qed. (** Substitution distributes on the open operation. *) Lemma subst_te_open_te : forall e T X U, type U -> subst_te X U (open_te e T) = open_te (subst_te X U e) (subst_tt X U T). Proof. intros. unfold open_te. generalize 0. induction e; intros; simpls; f_equal*; use subst_tt_open_tt_rec. Qed. (** Substitution and open_var for distinct names commute. *) Lemma subst_te_open_te_var : forall X Y U e, Y <> X -> type U -> (subst_te X U e) open_te_var Y = subst_te X U (e open_te_var Y). Proof. introv Neq Wu. rewrite* subst_te_open_te. simpl. case_var*. Qed. (** Opening up a body t with a type u is the same as opening up the abstraction with a fresh name x and then substituting u for x. *) Lemma subst_te_intro : forall X U e, X \notin fv_te e -> type U -> open_te e U = subst_te X U (e open_te_var X). Proof. introv Fr Wu. rewrite* subst_te_open_te. rewrite* subst_te_fresh. simpl. case_var*. Qed. (* ********************************************************************** *) (** ** Properties of term substitution in terms *) (** Substitution for a fresh name is identity. *) Lemma subst_ee_fresh : forall x u e, x \notin fv_ee e -> subst_ee x u e = e. Proof. induction e; simpl; intros; f_equal*. case_var*. notin_contradiction. Qed. (** Substitution distributes on the open operation. *) Lemma subst_ee_open_ee : forall t1 t2 u x, term u -> subst_ee x u (open_ee t1 t2) = open_ee (subst_ee x u t1) (subst_ee x u t2). Proof. intros. unfold open_ee. generalize 0. induction t1; intros; simpls; f_equal*. case_nat*. case_var*. rewrite* <- open_ee_rec_term. Qed. (** Substitution and open_var for distinct names commute. *) Lemma subst_ee_open_ee_var : forall x y u e, y <> x -> term u -> (subst_ee x u e) open_ee_var y = subst_ee x u (e open_ee_var y). Proof. introv Neq Wu. rewrite* subst_ee_open_ee. simpl. case_var*. Qed. (** Opening up a body t with a type u is the same as opening up the abstraction with a fresh name x and then substituting u for x. *) Lemma subst_ee_intro : forall x u e, x \notin fv_ee e -> term u -> open_ee e u = subst_ee x u (e open_ee_var x). Proof. introv Fr Wu. rewrite* subst_ee_open_ee. rewrite* subst_ee_fresh. simpl. case_var*. Qed. (** Interactions between type substitutions in terms and opening with term variables in terms. *) Lemma subst_te_open_ee_var : forall Z P x e, (subst_te Z P e) open_ee_var x = subst_te Z P (e open_ee_var x). Proof. introv. unfold open_ee. generalize 0. induction e; intros; simpl; f_equal*. case_nat*. Qed. (** Interactions between term substitutions in terms and opening with type variables in terms. *) Lemma subst_ee_open_te_var : forall z u e X, term u -> (subst_ee z u e) open_te_var X = subst_ee z u (e open_te_var X). Proof. introv. unfold open_te. generalize 0. induction e; intros; simpl; f_equal*. case_var*. symmetry. use open_te_rec_term. Qed. (** Substitutions preserve local closure. *) Lemma subst_tt_type : forall T Z P, type T -> type P -> type (subst_tt Z P T). Proof. induction 1; intros; simpl; auto. case_var*. apply_fresh* type_all as X. rewrite* subst_tt_open_tt_var. Qed. Lemma subst_te_term : forall e Z P, term e -> type P -> term (subst_te Z P e). Proof. puts subst_tt_type. induction 1; intros; simpl; auto. apply_fresh* term_abs as x. rewrite* subst_te_open_ee_var. apply_fresh* term_tabs as x. rewrite* subst_te_open_te_var. Qed. Lemma subst_ee_term : forall e1 Z e2, term e1 -> term e2 -> term (subst_ee Z e2 e1). Proof. induction 1; intros; simpl; auto. case_var*. apply_fresh* term_abs as y. rewrite* subst_ee_open_ee_var. apply_fresh* term_tabs as Y. rewrite* subst_ee_open_te_var. Qed. Hint Resolve subst_tt_type subst_te_term subst_ee_term. (* ********************************************************************** *) (** * Properties of well-formedness of a type in an environment *) (** If a type is well-formed in an environment then it is locally closed. *) Lemma type_from_wft : forall E T, wft E T -> type T. Proof. induction 1; eauto. Qed. (** Through weakening *) Lemma wft_weaken : forall G T E F, wft (E & G) T -> ok (E & F & G) -> wft (E & F & G) T. Proof. intros. gen_eq (E & G) as K. gen E F G. induction H; intros; subst; eauto. (* case: var *) apply (@wft_var U). apply* binds_weaken. (* case: all *) apply_fresh* wft_all as Y. apply_ih_bind* H1. Qed. (** Through narrowing *) Lemma wft_narrow : forall V F U T E X, wft (E & X ~<: V & F) T -> ok (E & X ~<: U & F) -> wft (E & X ~<: U & F) T. Proof. intros. gen_eq (E & X ~<: V & F) as K. gen E F. induction H; intros; subst; eauto. binds_cases H. eapply wft_var. apply* binds_concat_ok. destruct (binds_single_inv B1). subst. apply (@wft_var U). apply* binds_mid. eapply wft_var. apply* binds_prepend. apply_fresh* wft_all as Y. apply_ih_bind* H1. Qed. (** Through strengthening *) Lemma wft_strengthen : forall E F x U T, wft (E & x ~: U & F) T -> wft (E & F) T. Proof. intros. gen_eq (E & x ~: U & F) as G. gen F. induction H; intros F EQ; subst; auto. apply* (@wft_var U0). binds_cases H; try discriminate; auto*. apply_fresh* wft_all as Y. apply_ih_bind* H1. Qed. (** Through type substitution *) Lemma wft_subst_tb : forall F Q E Z P T, wft (E & Z ~<: Q & F) T -> wft E P -> ok (E & map (subst_tb Z P) F) -> wft (E & map (subst_tb Z P) F) (subst_tt Z P T). Proof. introv WT WP. gen_eq (E & Z ~<: Q & F) as G. gen F. induction WT; intros F EQ Ok; subst; simpl subst_tt; auto. case_var*. apply_empty* wft_weaken. binds_cases H. apply* wft_var. apply (@wft_var (subst_tt Z P U)). unsimpl_map_bind*. apply_fresh* wft_all as Y. unsimpl ((subst_tb Z P) (bind_sub T1)). puts type_from_wft. rewrite* subst_tt_open_tt_var. apply_ih_map_bind* H0. Qed. (** Through type reduction *) Lemma wft_open : forall E U T1 T2, ok E -> wft E (typ_all T1 T2) -> wft E U -> wft E (open_tt T2 U). Proof. introv Ok WA WU. inversions WA. pick_fresh X. puts type_from_wft. rewrite* (@subst_tt_intro X). poses K (@wft_subst_tb empty). simpls*. Qed. (* ********************************************************************** *) (** * Relations between well-formed environment and types well-formed in environments *) (** If an environment is well-formed, then it does not contain duplicated keys. *) Lemma ok_from_okt : forall E, okt E -> ok E. Proof. induction 1; auto. Qed. Hint Extern 1 (ok _) => apply ok_from_okt. (** Extraction from a subtyping assumption in a well-formed environments *) Lemma wft_from_env_has_sub : forall x U E, okt E -> binds x (bind_sub U) E -> wft E U. Proof. unfold binds. induction E as [|(y,a)]; simpl; intros Ok B; env_fix. contradictions. case_var. inversions B. inversions Ok. apply_empty* wft_weaken. apply_empty* wft_weaken. inversions* Ok. Qed. (** Extraction from a typing assumption in a well-formed environments *) Lemma wft_from_env_has_typ : forall x U E, okt E -> binds x (bind_typ U) E -> wft E U. Proof. unfold binds. induction E as [|(y,a)]; simpl; intros Ok B; env_fix. contradictions. case_var. inversions B. inversions Ok. apply_empty* wft_weaken. apply_empty* wft_weaken. inversions* Ok. Qed. (** Extraction from a well-formed environment *) Lemma wft_from_okt_typ : forall x T E, okt (E & x ~: T) -> wft E T. Proof. intros. inversions* H. Qed. Lemma wft_from_okt_sub : forall x T E, okt (E & x ~<: T) -> wft E T. Proof. intros. inversions* H. Qed. (** Automation *) Lemma wft_weaken_right : forall T E F, wft E T -> ok (E & F) -> wft (E & F) T. Proof. intros. apply_empty* wft_weaken. Qed. Hint Resolve wft_weaken_right. Hint Immediate wft_from_env_has_sub wft_from_env_has_typ. Hint Resolve wft_subst_tb. Hint Resolve wft_from_okt_typ wft_from_okt_sub. (* ********************************************************************** *) (** ** Properties of well-formedness of an environment *) (** Through narrowing *) Lemma okt_narrow : forall V E F U X, okt (E & X ~<: V & F) -> wft E U -> okt (E & X ~<: U & F). Proof. induction F as [|(Y,B)]; simpl; introv Ok Wf; env_fix; inversions Ok. auto. apply okt_sub; auto. use wft_narrow. apply okt_typ; auto. use wft_narrow. Qed. (** Through strengthening *) Lemma okt_strengthen : forall x T E F, okt (E & x ~: T & F) -> okt (E & F). Proof. induction F as [|(Y,B)]; simpl; intros Ok; env_fix; inversions Ok. auto. apply okt_sub; auto. use wft_strengthen. apply okt_typ; auto. use wft_strengthen. Qed. (** Through type substitution *) Lemma okt_subst_tb : forall Q Z P E F, okt (E & Z ~<: Q & F) -> wft E P -> okt (E & map (subst_tb Z P) F). Proof. induction F as [|(Y,B)]; simpl; intros Ok WP; env_fix; inversions Ok; simpl subst_tb; env_fix. auto. apply okt_sub; auto. use wft_subst_tb. apply okt_typ; auto. use wft_subst_tb. Qed. (** Automation *) Hint Resolve okt_narrow okt_subst_tb wft_weaken. Hint Immediate okt_strengthen. (* ********************************************************************** *) (** ** Environment is unchanged by substitution from a fresh name *) Lemma notin_fv_wf : forall E X T, wft E T -> X # E -> X \notin fv_tt T. Proof. induction 1; intros Fr; simpl. eauto. rewrite notin_singleton. intro. subst. apply* binds_fresh. notin_simpl; auto. notin_simpl; auto. pick_fresh Y. apply* (@notin_fv_tt_open Y). Qed. Lemma map_subst_tb_id : forall G Z P, okt G -> Z # G -> G = map (subst_tb Z P) G. Proof. induction 1; simpl; intros Fr; auto. rewrite* <- IHokt. rewrite* subst_tt_fresh. apply* notin_fv_wf. rewrite* <- IHokt. rewrite* subst_tt_fresh. apply* notin_fv_wf. Qed. (* ********************************************************************** *) (** ** Regularity of relations *) (** The subtyping relation is restricted to well-formed objects. *) Lemma sub_regular : forall E S T, sub E S T -> okt E /\ wft E S /\ wft E T. Proof. induction 1. auto*. auto*. auto*. auto*. (* Coq bug here? *) split. auto*. split; apply_fresh* wft_all as Y; destructi~ (H1 Y); apply_empty* (@wft_narrow T1). Qed. (** The typing relation is restricted to well-formed objects. *) Lemma typing_regular : forall E e T, typing E e T -> okt E /\ term e /\ wft E T. Proof. induction 1. splits*. splits. pick_fresh y. forward~ (H0 y) as K. destructs K. inversions* H1. apply_fresh* term_abs as y. pick_fresh y. forward~ (H0 y) as K. destructs K. inversions H1. apply* type_from_wft. forward~ (H0 y) as K. destructs K. auto. pick_fresh y. forward~ (H0 y) as K. destructs K. apply* wft_arrow. inversions* H1. apply_empty* wft_strengthen. splits*. destructs IHtyping1. inversion* H4. splits. pick_fresh y. forward~ (H0 y) as K. destructs K. inversions* H1. apply_fresh* term_tabs as y. pick_fresh y. forward~ (H0 y) as K. destructs K. inversions H1. apply* type_from_wft. forward~ (H0 y) as K. destructs K. auto. apply_fresh* wft_all as Y. pick_fresh y. forward~ (H0 y) as K. destructs K. inversions* H1. forward~ (H0 Y) as K. destructs K. inversions* H1. splits*; destructs (sub_regular H0). apply* term_tapp. use type_from_wft. apply* wft_open. splits*. destructs (sub_regular H0). auto. Qed. (** The value relation is restricted to well-formed objects. *) Lemma value_regular : forall t, value t -> term t. Proof. induction 1; auto*. Qed. (** The reduction relation is restricted to well-formed objects. *) Lemma red_regular : forall t t', red t t' -> term t /\ term t'. Proof. induction 1; split; use value_regular. inversions H. pick_fresh y. rewrite* (@subst_ee_intro y). inversions H. pick_fresh Y. rewrite* (@subst_te_intro Y). Qed. (** Automation *) Hint Extern 1 (okt ?E) => match goal with | H: sub _ _ _ |- _ => apply (proj31 (sub_regular H)) | H: typing _ _ _ |- _ => apply (proj31 (typing_regular H)) end. Hint Extern 1 (wft ?E ?T) => match goal with | H: typing E _ T |- _ => apply (proj33 (typing_regular H)) | H: sub E T _ |- _ => apply (proj32 (sub_regular H)) | H: sub E _ T |- _ => apply (proj33 (sub_regular H)) end. Hint Extern 1 (type ?T) => let go E := apply (@type_from_wft 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. Hint Extern 1 (term ?e) => match goal with | H: typing _ ?e _ |- _ => apply (proj32 (typing_regular H)) | H: red ?e _ |- _ => apply (proj1 (red_regular H)) | H: red _ ?e |- _ => apply (proj2 (red_regular H)) end. ```