```(*************************************************************************** * Calculus of Constructions - Infrastructure * * Arthur Charguéraud, April 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory CoC_Definitions. (* ********************************************************************** *) (** ** Additional Definitions Used in the Proofs *) (* ********************************************************************** *) (** Computing free variables of a term *) Fixpoint fv (t : trm) {struct t} : vars := match t with | trm_bvar i => {} | trm_fvar x => {{x}} | trm_type n => {} | trm_app t1 t2 => (fv t1) \u (fv t2) | trm_abs t1 t2 => (fv t1) \u (fv t2) | trm_prod t1 t2 => (fv t1) \u (fv t2) end. (* ********************************************************************** *) (** Substitution for a name *) Fixpoint subst (z : var) (u : trm) (t : trm) {struct t} : trm := match t with | trm_bvar i => trm_bvar i | trm_fvar x => if x == z then u else (trm_fvar x) | trm_type n => trm_type n | trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2) | trm_abs t1 t2 => trm_abs (subst z u t1) (subst z u t2) | trm_prod t1 t2 => trm_prod (subst z u t1) (subst z u t2) end. Notation "[ z ~> u ] t" := (subst z u t) (at level 68). (* ********************************************************************** *) (** Abstracting a name out of a term *) Fixpoint close_var_rec (k : nat) (z : var) (t : trm) {struct t} : trm := match t with | trm_bvar i => trm_bvar i | trm_fvar x => if x == z then (trm_bvar k) else (trm_fvar x) | trm_type n => trm_type n | trm_app t1 t2 => trm_app (close_var_rec k z t1) (close_var_rec k z t2) | trm_abs t1 t2 => trm_abs (close_var_rec k z t1) (close_var_rec (S k) z t2) | trm_prod t1 t2 => trm_prod (close_var_rec k z t1) (close_var_rec (S k) z t2) end. Definition close_var z t := close_var_rec 0 z t. (* ********************************************************************** *) (** An environment contains only terms *) Definition contains_terms E := forall x U, binds x U E -> term U. (* ********************************************************************** *) (** Inclusion between relations (simulation or a relation by another) *) Definition simulated (R1 R2 : relation) := forall (t t' : trm), R1 t t' -> R2 t t'. Infix "simulated_by" := simulated (at level 69). (* ********************************************************************** *) (** Properties of relations *) Definition red_regular (R : relation) := forall t t', R t t' -> term t /\ term t'. Definition red_refl (R : relation) := forall t, term t -> R t t. Definition red_in (R : relation) := forall t x u u', term t -> R u u' -> R ([x ~> u]t) ([x ~> u']t). Definition red_all (R : relation) := forall x t t', R t t' -> forall u u', R u u' -> R ([x~>u]t) ([x~>u']t'). Definition red_out (R : relation) := forall x u t t', term u -> R t t' -> R ([x~>u]t) ([x~>u]t'). Definition red_rename (R : relation) := forall x t t' y, R (t ^ x) (t' ^ x) -> x \notin (fv t) -> x \notin (fv t') -> R (t ^ y) (t' ^ y). Definition red_through (R : relation) := forall x t1 t2 u1 u2, x \notin (fv t1) -> x \notin (fv u1) -> R (t1 ^ x) (u1 ^ x) -> R t2 u2 -> R (t1 ^^ t2) (u1 ^^ u2). (* ********************************************************************** *) (** ** Instanciation of Tactics *) 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 x) in let D := gather_vars_with (fun x : env => dom x) in constr:(A \u B \u C \u D). Ltac pick_fresh X := let L := gather_vars in (pick_fresh_gen L X). 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*. Ltac exists_fresh := let L := gather_vars_with (fun x : vars => x) in exists L. Scheme typing_induct := Induction for typing Sort Prop with wf_induct := Induction for wf Sort Prop. Hint Constructors beta star_ equiv_ less typing wf. Hint Unfold conv. (* ********************************************************************** *) (** ** Lemmas *) (* ********************************************************************** *) (** Properties of substitutions *) Section SubstProperties. Hint Constructors term. (** Substitution for a fresh name is identity. *) Lemma subst_fresh : forall x t u, x \notin fv t -> [x ~> u] t = t. Proof. intros. induction t; simpls; f_equal*. case_var*. notin_contradiction. Qed. (** Substitution distributes on the open operation. *) Lemma subst_open : forall x u t1 t2, term u -> [x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2). Proof. intros. unfold open. generalize 0. induction t1; intros; simpl; f_equal*. case_nat*. case_var*. apply* open_rec_term. Qed. (** Substitution and open_var for distinct names commute. *) Lemma subst_open_var : forall x y u e, y <> x -> term u -> ([x ~> u]e) ^ y = [x ~> u] (e ^ y). Proof. introv Neq Wu. rewrite* subst_open. simpl. case_var*. Qed. (** Opening up an abstraction of body t with a term u is the same as opening up the abstraction with a fresh name x and then substituting u for x. *) Lemma subst_intro : forall x t u, x \notin (fv t) -> term u -> t ^^ u = [x ~> u](t ^ x). Proof. introv Fr Wu. rewrite* subst_open. rewrite* subst_fresh. simpl. case_var*. Qed. End SubstProperties. (** Tactic to permute subst and open var *) Ltac cross := rewrite subst_open_var; try cross. Tactic Notation "cross" "*" := cross; auto*. (* ********************************************************************** *) (** Lifting operations to terms *) Hint Constructors term. (** Terms are stable by substitution *) Lemma subst_term : forall t z u, term u -> term t -> term ([z ~> u]t). Proof. induction 2; simpl*. case_var*. apply_fresh* term_abs as y. rewrite* subst_open_var. apply_fresh* term_prod as y. rewrite* subst_open_var. Qed. (** Terms are stable by open *) Lemma open_term : forall t u, body t -> term u -> term (t ^^ u). Proof. intros. destruct H. pick_fresh y. rewrite* (@subst_intro y). apply* subst_term. Qed. Hint Resolve subst_term open_term. (* ********************************************************************** *) (** Properties of Body *) Lemma term_abs1 : forall t2 t1, term (trm_abs t1 t2) -> term t1. Proof. intros. inversion* H. Qed. Lemma body_abs2 : forall t1 t2, term (trm_abs t1 t2) -> body t2. Proof. intros. unfold body. inversion* H. Qed. Lemma body_prod2 : forall t1 t2, term (trm_prod t1 t2) -> body t2. Proof. intros. unfold body. inversion* H. Qed. Hint Extern 1 (term ?t) => match goal with H: term (trm_abs t ?t2) |- _ => apply (@term_abs1 t2) end. Hint Extern 1 (body ?t) => match goal with | H: context [trm_abs ?t1 t] |- _ => apply (@body_abs2 t1) | H: context [trm_prod ?t1 t] |- _ => apply (@body_prod2 t1) | H: context [t ^ _] |- _ => let x := fresh in let L := gather_vars in exists L; intros x Fr; destructi (H x); auto end. Lemma term_abs_prove : forall t1 t2, term t1 -> body t2 -> term (trm_abs t1 t2). Proof. intros. apply_fresh* term_abs as x. Qed. Lemma term_prod_prove : forall t1 t2, term t1 -> body t2 -> term (trm_prod t1 t2). Proof. intros. apply_fresh* term_prod as x. Qed. Hint Resolve term_abs_prove term_prod_prove. Lemma body_prove : forall L t, (forall x, x \notin L -> term (t ^ x)) -> body t. Proof. intros. exists* L. Qed. Hint Extern 1 (body ?t) => match goal with | H: forall _, _ \notin ?L -> term (t ^ _) |- _ => apply (@body_prove L) end. Lemma body_subst : forall x t u, term u -> body t -> body ([x ~> u]t). Proof. introv. intros Wu [L Bt]. exists ({{x}} \u L). intros y Fr. cross*. Qed. Hint Resolve body_subst. (* ********************************************************************** *) (** ** Additional results on primitive operations *) Section PrimProperties. Hint Constructors term. (** Open_var with fresh names is an injective operation *) Lemma open_var_inj : forall x t1 t2, x \notin (fv t1) -> x \notin (fv t2) -> (t1 ^ x = t2 ^ x) -> (t1 = t2). Proof. intros x t1. unfold open. generalize 0. induction t1; intro k; destruct t2; simpl; intros; inversion H1; try solve [ f_equal* | do 2 try case_nat; inversions* H1; try notin_contradiction ]. Qed. (** Close var is an operation returning a body of an abstraction *) Lemma close_var_fresh : forall x t, x \notin fv (close_var x t). Proof. introv. unfold close_var. generalize 0. induction t; intros k; simpls; notin_simpl; auto. case_var; simpl*. Qed. (** Close var is an operation returning a body of an abstraction *) Lemma close_var_body : forall x t, term t -> body (close_var x t). Proof. introv W. exists {{x}}. intros y Fr. unfold open, close_var. generalize 0. gen y. induction W; intros y Fr k; simpls. case_var; simpl*. case_nat*. auto*. auto*. apply_fresh* term_abs as z. unfolds open. rewrite* close_var_rec_open. apply_fresh* term_prod as z. unfolds open. rewrite* close_var_rec_open. Qed. (** Close var is the right inverse of open_var *) Lemma close_var_open : forall x t, term t -> t = (close_var x t) ^ x. Proof. introv W. unfold close_var, open. generalize 0. induction W; intros k; simpls; f_equal*. case_var*. simpl. case_nat*. let L := gather_vars in match goal with |- _ = ?t => destruct (var_fresh (L \u fv t)) as [y Fr] end. apply* (@open_var_inj y). unfolds open. rewrite* close_var_rec_open. let L := gather_vars in match goal with |- _ = ?t => destruct (var_fresh (L \u fv t)) as [y Fr] end. apply* (@open_var_inj y). unfolds open. rewrite* close_var_rec_open. Qed. (** An abstract specification of close_var, which packages the result of the operation and all the properties about it. *) Lemma close_var_spec : forall t x, term t -> exists u, t = u ^ x /\ body u /\ x \notin (fv u). Proof. intros. exists (close_var x t). split3. apply* close_var_open. apply* close_var_body. apply* close_var_fresh. Qed. End PrimProperties. (* ********************************************************************** *) (** ** Regularity: relations are restricted to terms *) Lemma red_regular_beta : red_regular beta. Proof. introz. induction* H. Qed. Lemma red_regular_beta_star : red_regular (beta star). introz. induction* H. apply* red_regular_beta. Qed. Lemma red_regular_conv : red_regular conv. Proof. introz. induction* H. apply* red_regular_beta. Qed. Hint Extern 1 (term ?t) => match goal with | H: beta t _ |- _ => apply (proj1 (red_regular_beta H)) | H: beta _ t |- _ => apply (proj2 (red_regular_beta H)) | H: (beta star) t _ |- _ => apply (proj1 (red_regular_beta_star H)) | H: (beta star) _ t |- _ => apply (proj2 (red_regular_beta_star H)) | H: conv t _ |- _ => apply (proj1 (red_regular_conv H)) | H: conv _ t |- _ => apply (proj2 (red_regular_conv H)) end. Hint Extern 1 (term (trm_abs ([?x ~> ?u]?t1) ([?x ~> ?u]?t2))) => match goal with H: term (trm_abs t1 t2) |- _ => unsimpl ([x ~> u](trm_abs t1 t2)) end. Lemma red_regular_less : red_regular less. Proof. introz. induction* H. Qed. Hint Extern 1 (term ?t) => match goal with | H: less t _ |- _ => apply (proj1 (red_regular_less H)) | H: less _ t |- _ => apply (proj2 (red_regular_less H)) end. Lemma regular_typing : forall E t T, typing E t T -> (wf E /\ ok E /\ contains_terms E /\ term t /\ term T). Proof. apply typing_induct with (P0 := fun E (_ : wf E) => ok E /\ contains_terms E); unfolds contains_terms; intros; splits*. apply_fresh* term_prod as y. forward* (H0 y). apply_fresh* term_abs as y. pick_fresh y. forward~ (H0 y) as K. destructs K; auto*. forward* (H0 y). intros. inversion H. intros. unfolds binds. destructs H. simpls. case_var*. inversions* H0. Qed. Hint Extern 1 (term ?t) => match goal with | H: typing _ t _ |- _ => apply (proj32 (proj33 (regular_typing H))) | H: typing _ _ t |- _ => apply (proj33 (proj33 (regular_typing H))) end. Lemma ok_from_wf : forall E, wf E -> ok E. Proof. induction 1. auto. use (regular_typing H0). Qed. Hint Extern 1 (ok ?E) => match goal with | H: wf E |- _ => apply (ok_from_wf H) end. Hint Extern 1 (wf ?E) => match goal with | H: typing E _ _ |- _ => apply (proj1 (regular_typing H)) end. Lemma term_from_binds_in_wf : forall x E U, wf E -> binds x U E -> term U. Proof. unfold binds. introv W Has. induction E as [|(y,a)]; simpls. contradictions. inversions W. case_var*. inversions* Has. Qed. Hint Extern 1 (term ?t) => match goal with H: binds ?x t ?E |- _ => apply (@term_from_binds_in_wf x E) end. Lemma wf_left : forall E F, wf (E & F) -> wf E. Proof. intros. induction F as [|(y,a)]; env_fix. auto. rewrite <- concat_assoc in H. inversions H. env_fix. use (proj1 (regular_typing H4)). Qed. Implicit Arguments wf_left [E F]. (* ********************************************************************** *) (** ** Some freshness results *) Lemma fv_open_var : forall y x t, x <> y -> x \notin fv (t ^ y) -> x \notin fv t. Proof. introv Neq. unfold open. generalize 0. induction t; simpl; intros; try notin_solve. puts (IHt1 n). puts (IHt2 n). notin_simpl; auto. puts (IHt1 n). puts (IHt2 (S n)). notin_simpl; auto. puts (IHt1 n). puts (IHt2 (S n)). notin_simpl; auto. Qed. Lemma typing_fresh : forall E T i x, typing E T (trm_type i) -> x # E -> x \notin fv T. Proof. introv Typ. induction Typ; simpls; intros. auto. rewrite notin_singleton. intro. subst. apply* binds_fresh. pick_fresh y. notin_simpl. auto. apply* (@fv_open_var y). pick_fresh y. puts (IHTyp H1). notin_simpl. auto. apply* (@fv_open_var y). puts (IHTyp1 H). puts (IHTyp2 H). auto. auto. Qed. Lemma notin_fv_from_wf : forall E F x V, wf (E & x ~ V & F) -> x \notin fv V. Proof. intros. poses W (wf_left H). inversions W. apply* typing_fresh. Qed. Lemma notin_fv_from_binds : forall x y U E, wf E -> binds y U E -> x # E -> x \notin fv U. Proof. induction E as [|(z,a)]; simpl; intros; env_fix. inversions H0. inversions H0. case_var. inversions H3. inversions H. apply* typing_fresh. inversions H. apply* IHE. Qed. Lemma notin_fv_from_binds' : forall E F x V y U, wf (E & x ~ V & F) -> binds y U E -> x \notin fv U. Proof. intros. poses W (wf_left H). inversions W. poses W' (wf_left W). apply* notin_fv_from_binds. Qed. Hint Extern 1 (?x \notin fv ?V) => match goal with H: wf (?E & x ~ V & ?F) |- _ => apply (@notin_fv_from_wf E F) end. Hint Extern 1 (?x \notin fv ?U) => match goal with H: wf (?E & x ~ ?V & ?F), B: binds ?y U ?E |- _ => apply (@notin_fv_from_binds' E F x V y) end. ```