``` Set Implicit Arguments. Require Import LibLN BigStep_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_abs t1 => (fv t1) | trm_app t1 t2 => (fv t1) \u (fv t2) end. (** Substitution for names *) 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_abs t1 => trm_abs (subst z u t1) | trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2) end. Notation "[ z ~> u ] t" := (subst z u t) (at level 68). Notation "{ k ~> u } t" := (open_rec k u t) (at level 67) : infrastructure_scope. Open Local Scope infrastructure_scope. (* ********************************************************************** *) (** ** Instanciation of tactics *) (** Tactic [gather_vars] returns a set of variables occurring in the context of proofs, including domain of environments and free variables in terms mentionned in the context. *) 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 constr:(A \u B \u C). (** Tactic [pick_fresh x] adds to the context a new variable x and a proof that it is fresh from all of the other variables gathered by tactic [gather_vars]. *) Ltac pick_fresh Y := let L := gather_vars in (pick_fresh_gen L Y). (** Tactic [apply_fresh T as y] takes a lemma T of the form [forall L ..., (forall x, x \notin L, P x) -> ... -> Q.] instantiate L to be the set of variables occuring in the context (by [gather_vars]), then introduces for the premise with the cofinite quantification the name x as "y" (the second parameter of the tactic), and the proof that x is not in L. *) 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_star. Tactic Notation "apply_fresh" constr(T) := apply_fresh_base T gather_vars ltac_no_arg. Tactic Notation "apply_fresh" "*" constr(T) := apply_fresh T; auto_star. Hint Constructors term value beta reds. (* ********************************************************************** *) (** ** Properties of substitution *) (** Substitution on indices is identity on well-formed terms. *) Lemma open_rec_term_core :forall t j v i u, i <> j -> {j ~> v}t = {i ~> u}({j ~> v}t) -> t = {i ~> u}t. Proof. induction t; introv Neq Equ; simpls; inversion* Equ; fequals*. case_nat*. case_nat*. Qed. Lemma open_rec_term : forall t u, term t -> forall k, t = {k ~> u}t. Proof. induction 1; intros; simpl; fequals*. unfolds open. pick_fresh x. apply* (@open_rec_term_core t1 0 (trm_fvar x)). Qed. (** 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; fequals*. case_var*. 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; fequals*. 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 t, y <> x -> term u -> ([x ~> u]t) ^ y = [x ~> u] (t ^ 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. Lemma subst_intro' : forall x t u, x \notin (fv t) -> t ^^ u = [x ~> u](t ^ x). Proof. introv H. unfold open. generalize 0. gen H. induction t; simpl; intros; fequals*. case_nat*. simpl. case_var*. case_var*. Qed. (* ********************************************************************** *) (** ** Terms are stable through substitutions *) (** Terms are stable by substitution *) Lemma subst_term : forall t z u, term u -> term t -> term ([z ~> u]t). Proof. induction 2; simpls*. case_var*. apply_fresh term_abs. rewrite* subst_open_var. Qed. Hint Resolve subst_term. (* ********************************************************************** *) (** ** Terms are stable through open *) (** Conversion from locally closed abstractions and bodies *) Lemma term_abs_to_body : forall t1, term (trm_abs t1) -> body t1. Proof. intros. unfold body. inversion* H. Qed. Lemma body_to_term_abs : forall t1, body t1 -> term (trm_abs t1). Proof. intros. inversion* H. Qed. Hint Resolve term_abs_to_body body_to_term_abs. (** ** Opening a body with a term gives a term *) Lemma open_term : forall t u, body t -> term u -> term (t ^^ u). Proof. intros. destruct H. pick_fresh y. rewrite* (@subst_intro y). Qed. Hint Resolve open_term. (* ********************************************************************** *) (** ** Regularity of relations *) (** The value predicate only holds on locally-closed terms. *) Lemma value_regular : forall e, value e -> term e. Proof. induction 1; auto*. Qed. (** A reduction relation only holds on pairs of locally-closed terms. *) Lemma beta_regular : forall e e', beta e e' -> term e /\ term e'. Proof. induction 1; auto* value_regular. Qed. Lemma beta_star_regular : forall e e', beta_star e e' -> term e /\ term e'. Proof. induction 1. auto*. destruct* (beta_regular H). Qed. Lemma reds_regular : forall e e', reds e e' -> term e /\ term e'. Proof. induction 1; auto* value_regular. Qed. (** Automation for reasoning on well-formedness. *) Hint Extern 1 (term ?t) => match goal with | H: value t |- _ => apply (value_regular H) | H: beta t _ |- _ => apply (proj1 (beta_regular H)) | H: beta _ t |- _ => apply (proj2 (beta_regular H)) | H: beta_star t _ |- _ => apply (proj1 (beta_star_regular H)) | H: beta_star _ t |- _ => apply (proj2 (beta_star_regular H)) | H: reds t _ |- _ => apply (proj1 (reds_regular H)) | H: reds _ t |- _ => apply (proj2 (reds_regular H)) end. ```