(*************************************************************************** * Calculus of Constructions - Properties of Beta Star * * Arthur Charguéraud, April 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory CoC_Definitions CoC_Infrastructure. (* ********************************************************************** *) (** ** Generalities on relations *) Lemma red_all_to_out : forall (R : relation), red_all R -> red_refl R -> red_out R. Proof. introz. auto*. Qed. Lemma red_out_to_rename : forall (R : relation), red_out R -> red_rename R. Proof. introz. rewrite* (@subst_intro x t). rewrite* (@subst_intro x t'). Qed. Lemma red_all_to_through : forall (R : relation), red_regular R -> red_all R -> red_through R. Proof. introz. puts (H _ _ H4). rewrite* (@subst_intro x t1). rewrite* (@subst_intro x u1). Qed. (* ********************************************************************** *) (** ** Properties of beta relation *) Lemma beta_red_out : red_out beta. Proof. introz. induction H0; simpl. rewrite* subst_open. apply* beta_app1. apply* beta_app2. apply* beta_abs1. apply_fresh* beta_abs2 as y. cross*. apply* beta_prod1. apply_fresh* beta_prod2 as y. cross*. Qed. Lemma beta_red_rename : red_rename beta. Proof. apply* (red_out_to_rename beta_red_out). Qed. (* ********************************************************************** *) (** ** Properties of beta star relation *) Lemma beta_star_app1 : forall t1 t1' t2, (beta star) t1 t1' -> term t2 -> (beta star) (trm_app t1 t2) (trm_app t1' t2). Proof. intros. induction H. apply* star_refl. apply* (@star_trans beta (trm_app t0 t2)). apply* star_step. Qed. Lemma beta_star_app2 : forall t1 t2 t2', (beta star) t2 t2' -> term t1 -> (beta star) (trm_app t1 t2) (trm_app t1 t2'). Proof. intros. induction H. apply* star_refl. apply* (@star_trans beta (trm_app t1 t2)). apply* star_step. Qed. Lemma beta_star_abs1 : forall t1 t1' t2, (beta star) t1 t1' -> body t2 -> (beta star) (trm_abs t1 t2) (trm_abs t1' t2). Proof. intros. induction H. apply* star_refl. apply* (@star_trans beta (trm_abs t0 t2)). apply* star_step. Qed. Lemma beta_star_prod1 : forall t1 t1' t2, (beta star) t1 t1' -> body t2 -> (beta star) (trm_prod t1 t2) (trm_prod t1' t2). Proof. intros. induction H. apply* star_refl. apply* (@star_trans beta (trm_prod t0 t2)). apply* star_step. Qed. Lemma beta_star_abs2 : forall L t1 t2 t2', term t1 -> (forall x, x \notin L -> (beta star) (t2 ^ x) (t2' ^ x)) -> (beta star) (trm_abs t1 t2) (trm_abs t1 t2'). Proof. introv R1 R2. pick_fresh x. forward~ (R2 x) as Red. assert (body t2). exists L. intros y Fry. forward* (R2 y). assert (body t2'). exists L. intros y Fry. forward* (R2 y). gen_eq (t2 ^ x) as u. gen_eq (t2' ^ x) as u'. clear R2. gen t2 t2'. induction Red; intros; subst. rewrite* (@open_var_inj x t2 t2'). destruct~ (@close_var_spec t2 x) as [u [P [Q R]]]. apply* (@star_trans beta (trm_abs t1 u)). apply star_step. apply_fresh* beta_abs2 as y. apply* (@beta_red_rename x). Qed. Lemma beta_star_prod2 : forall L t1 t2 t2', term t1 -> (forall x, x \notin L -> (beta star) (t2 ^ x) (t2' ^ x)) -> (beta star) (trm_prod t1 t2) (trm_prod t1 t2'). Proof. introv R1 R2. pick_fresh x. forward~ (R2 x) as Red. assert (body t2). exists L. intros y Fry. forward* (R2 y). assert (body t2'). exists L. intros y Fry. forward* (R2 y). gen_eq (t2 ^ x) as u. gen_eq (t2' ^ x) as u'. clear R2. gen t2 t2'. induction Red; intros; subst. rewrite* (@open_var_inj x t2 t2'). destruct~ (@close_var_spec t2 x) as [u [P [Q R]]]. apply* (@star_trans beta (trm_prod t1 u)). apply star_step. apply_fresh* beta_prod2 as y. apply* (@beta_red_rename x). Qed. Lemma beta_star_red_in : red_in (beta star). Proof. introv Wf Red. puts term. induction Wf; simpl. case_var*. apply~ (@star_trans beta (trm_app ([x ~> u']t1) ([x ~> u]t2))). apply* beta_star_app1. apply* beta_star_app2. auto*. apply~ (@star_trans beta (trm_abs ([x ~> u']t1) ([x ~> u]t2))). apply* beta_star_abs1. apply* (@beta_star_abs2 (L \u {{x}})). intros y Fr. cross*. apply~ (@star_trans beta (trm_prod ([x ~> u']t1) ([x ~> u]t2))). apply* beta_star_prod1. apply* (@beta_star_prod2 (L \u {{x}})). intros y Fr. cross*. Qed. Lemma beta_star_red_all : red_all (beta star). Proof. introv Redt. induction Redt; simpl; intros u u' Redu. apply* beta_star_red_in. apply* (@star_trans beta ([x ~> u]t2)). apply* (@star_trans beta ([x ~> u]t')). apply* star_step. apply* beta_red_out. apply* beta_star_red_in. Qed. Lemma beta_star_red_through : red_through (beta star). Proof. apply* (red_all_to_through red_regular_beta_star beta_star_red_all). Qed.