```(*************************************************************************** * Correctness of the CPS-transformation - Infrastructure * * Arthur Charguéraud, January 2009, Coq v8.1pl4 * ***************************************************************************) Set Implicit Arguments. Require Import CPS_Definitions Omega. Implicit Types x y z : var. (* ********************************************************************** *) (* ********************************************************************** *) (** * 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 constr:(A \u B \u C). Tactic Notation "pick_fresh" ident(x) := let L := gather_vars in pick_fresh_gen L x. Tactic Notation "pick_fresh" ident(x) "from" constr(E) := let L := gather_vars in pick_fresh_gen (L \u E) 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_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. Tactic Notation "exists_fresh" := let y := fresh "y" in let Fry := fresh "Fr" y in exists_fresh_gen gather_vars y Fry. Hint Constructors term. (* ********************************************************************** *) (* ********************************************************************** *) (** * Properties of the syntax *) (* ********************************************************************** *) (** ** Extra definitions *) Notation "'[[' x '~>' y ']]' t" := (subst x (trm_fvar y) t) (at level 69). (* ********************************************************************** *) (** ** Properties of local closure *) (** 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. (* ********************************************************************** *) (** ** Properties of open and subst *) (** Substitution for a fresh name is the 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. (** Opening of a locally-closed term is the identity *) Lemma open_rec_term_ind :forall t j v i u, i <> j -> {i ~> u}({j ~> v}t) = {j ~> v}t -> {i ~> u}t = t. Proof. induction t; introv Neq Equ; simpls; inversions~ Equ; fequals*. case_nat~. case_nat~. Qed. Lemma open_rec_term : forall t u k, term t -> {k ~> u}t = t. Proof. introv H. gen k. induction H; intros; simpl; fequals~. unfolds open. pick_fresh x. apply~ (@open_rec_term_ind t1 0 (trm_fvar x)). Qed. (** Open_var with fresh names *) Lemma open_fresh : forall x y t, x \notin fv t -> x <> y -> x \notin fv (t^y). Proof. introv. unfold open. generalize 0. induction t; simpl; intros i Fr Neq; auto. case_nat; simple~. Qed. Hint Resolve open_fresh. (** Open_var with fresh names is injective *) 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 [ fequals* | do 2 try case_nat; inversions~ H1; try notin_false ]. Qed. (** Substitution distributes on open *) 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~. rewrite~ open_rec_term. Qed. (** Substitution commutes with open_var for distinct names *) 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. (** Open can be decomposed as open_var followed with substitution *) 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. (** Substitution perserves local closure *) Lemma subst_term : forall t z u, term u -> term t -> term ([z ~> u]t). Proof. induction 2; simple~. case_var~. apply_fresh term_abs. rewrite~ subst_open_var. Qed. Hint Resolve subst_term. (** Open preserves local closure *) 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. (** Substitution preserves bodies -- todo: remove ? *) Lemma body_subst : forall t u x, body t -> term u -> body ([x~>u]t). Proof. introv T U. invert T. intros L B. exists_fresh. rewrite~ subst_open_var. Qed. (* ********************************************************************** *) (** ** Properties of close_var *) (* Closing on a fresh name is the identity *) Lemma close_var_fresh : forall x t i, x \notin fv t -> close_var_rec i x t = t. Proof. induction t; simpl; intros i Fr; fequals~. case_var~. Qed. (** Close_var on x returns a term with no occurence of x *) Lemma close_var_notin : 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; simple~. Qed. Hint Resolve close_var_notin. Lemma close_var_notin_keep : forall x y t, x \notin fv t -> x \notin fv (close_var y t). Proof. introv. unfold close_var. generalize 0. induction t; simpl; intros i Fr; auto. case_var; simple~. Qed. (** Close_var is the reciprocal of open_var *) Lemma close_var_open_ind : forall x y z t1 i j, i <> j -> y <> x -> y \notin (fv t1) -> {i ~> trm_fvar y} ({j ~> trm_fvar z} (close_var_rec j x t1) ) = {j ~> trm_fvar z} (close_var_rec j x ({i ~> trm_fvar y}t1) ). Proof. induction t1; simpl; intros; try solve [ fequals~ ]. do 2 (case_nat; simpl); try solve [ case_var~ | case_nat~ ]. case_var~. simpl. case_nat~. Qed. 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 j; simpls; fequals~. case_var~. simpl. case_nat~. match goal with |- _ = ?t => pick_fresh y from (fv t) end. apply~ (@open_var_inj y). unfolds open. rewrite~ close_var_open_ind. Qed. (** Close_var returns a body *) 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 j; simpls. case_var; simple~. case_nat~. auto. auto. apply_fresh term_abs as z. unfolds open. rewrite~ close_var_open_ind. Qed. Hint Resolve close_var_body. (** Abstract specification of close_var *) 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). splits 3. apply* close_var_open. apply* close_var_body. apply* close_var_notin. Qed. (* Close_var commutes with substitution for fresh names *) Lemma close_var_subst : forall x t z u, x \notin fv u -> x <> z -> close_var x ([z~>u]t) = [z~>u](close_var x t). Proof. introv Fr Neq. unfold close_var. generalize 0. induction t; intros i; simpl; fequals~. case_var; case_var; simpl. case_var. rewrite~ close_var_fresh. case_var~. do 2 case_var~. Qed. (* Close_var and renaming *) Lemma close_var_rename : forall y x t, y \notin fv t -> close_var y ([[x ~> y]]t) = close_var x t. Proof. introv Fr. unfold close_var. generalize 0. gen Fr. induction t; simpl; intros Fr i; fequals~. case_var; simpl; case_var~. Qed. (* ********************************************************************** *) (** ** Properties of size *) Lemma trm_size_rename : forall x y t, trm_size ([x ~> trm_fvar y]t) = trm_size t. Proof. induction t; simpl; fequals. case_var~. Qed. Lemma trm_size_open : forall x t, trm_size (t^x) = trm_size t. Proof. intros. unfold open. generalize 0. induction t; intros; simpl; fequals. case_nat~. rewrite IHt1. rewrite~ IHt2. rewrite~ IHt. Qed. Lemma term_size : forall P : trm -> Prop, (forall x, P (trm_fvar x)) -> (forall k, P (trm_cst k)) -> (forall t1 t2, term t1 -> P t1 -> term t2 -> P t2 -> P (trm_app t1 t2)) -> (forall t1, body t1 -> (forall t2 x, x \notin fv t2 -> trm_size t2 = trm_size t1 -> term (t2 ^ x) -> P (t2 ^ x)) -> P (trm_abs t1)) -> (forall t, term t -> P t). Proof. intros P Ha Hb Hc Hd t. gen_eq n: (trm_size t). gen t. induction n using peano_induction. introv Eq T. subst. inverts T. apply Ha. apply Hb. apply~ Hc. apply~ H. simpl; omega. apply~ H. simpl; omega. apply~ Hd. exists_fresh; auto. introv Fr Eq T. apply~ H. rewrite trm_size_open. simpl. omega. Qed. (* ********************************************************************** *) (* ********************************************************************** *) (** * Tactics *) (* ********************************************************************** *) (** Computation of beta-reductions *) Tactic Notation "calc_open" := unfold open; simpl; rewrite_all open_rec_term. Tactic Notation "calc_open" "~" := calc_open; auto_tilde. Tactic Notation "calc_open" "*" := calc_open; auto_star. (* ********************************************************************** *) (** Proving local closure *) Hint Extern 1 (body _) => exists_fresh; calc_open. Hint Extern 1 (term (trm_abs _)) => apply_fresh term_abs; calc_open; auto. Hint Extern 1 (term ?x) => match goal with H: x = _ |- _ => subst x end. (* ********************************************************************** *) (** Shortand for naming [var_gen] variables *) Tactic Notation "name_var_gen" ident(x) := match goal with | |- context [var_gen ?L] => sets x: (var_gen L) | H: context [var_gen ?L] |- _ => sets x: (var_gen L) end. (* ********************************************************************** *) (** Proving freshness of [var_gen] variables *) Hint Extern 5 (?x \notin _) => progress (unfold x); apply notin_var_gen; intros. Hint Resolve open_fresh. (* ********************************************************************** *) (* ********************************************************************** *) (** * Properties of definitions *) (* ********************************************************************** *) (** Fixpoint equation for the CPS transformation *) Lemma cps_fix : forall t, cps t = cps_body cps t. Proof. prove_fixf. destruct x; fequals. rewrite IH. rewrite IH. auto. simpl; omega. simpl; omega. rewrite IH. auto. simpl. rewrite trm_size_open. omega. Qed. Hint Resolve cps_fix. (* ********************************************************************** *) (** Regularity lemmas *) Lemma cps_term : forall t, term t -> term (cps t). Proof. introv T. induction T using term_size; simplfix cps. auto. auto. auto. name_var_gen x. protects (trm_abs (close_var x (cps (t1^x)))) do auto 8. Qed. Lemma cps_term_abs : forall t1, term (trm_abs t1) -> term (trm_abs (cps_abs_body t1)). Proof. intros. unfold cps_abs_body. name_var_gen x. lets: cps_term. auto 8. Qed. Hint Resolve cps_term cps_term_abs. Lemma cpsval_term : forall v, value v -> term (cpsval v). Proof. introv V. inverts V; simple~. Qed. Hint Resolve cpsval_term. Lemma value_regular : forall t, value t -> term t. Proof. induction 1; auto. Qed. Lemma eval_regular : forall t v, eval t v -> term t /\ term v. Proof. induction 1; auto* value_regular. Qed. (* ********************************************************************** *) (* ********************************************************************** *) (** * Automation *) Hint Extern 1 (term ?t) => match goal with | H: value t |- _ => apply (value_regular H) | H: eval t _ |- _ => apply (proj1 (eval_regular H)) | H: eval _ t |- _ => apply (proj2 (eval_regular H)) end. ```