```(*************************************************************************** * Church-Rosser Property in Pure Lambda-Calculus - Proofs * * Arthur Charguéraud, March 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory Lambda_Definitions Lambda_Infrastructure. (* ********************************************************************** *) (** ** Main Development *) (* ********************************************************************** *) (** Putting constructors as hints for auto *) Hint Constructors beta star_ equiv_ iter_. Hint Resolve para_var para_app. Hint Extern 1 (para (trm_abs _) (trm_abs _)) => let y := fresh "y" in apply_fresh para_abs as y. Hint Extern 1 (para (trm_app (trm_abs _) _) (_ ^^ _)) => let y := fresh "y" in apply_fresh para_red as y. (* ********************************************************************** *) (** Some relations between the properties of 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_fresh* beta_abs 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_abs : forall L t1 t1', (forall x, x \notin L -> (beta star) (t1 ^ x) (t1' ^ x)) -> (beta star) (trm_abs t1) (trm_abs t1'). Proof. introv R. pick_fresh x. forward~ (R x) as Red. asserts B1 (term (trm_abs t1')). apply_fresh term_abs as y. forward* (R y). asserts B2 (term (trm_abs t1')). apply_fresh term_abs as y. forward* (R y). gen_eq (t1 ^ x) as u. gen_eq (t1' ^ x) as u'. clear R. gen t1 t1'. induction Red; intros; subst. rewrite* (@open_var_inj x t1 t1'). destruct~ (@close_var_spec t2 x) as [u [P [Q R]]]. apply* (@star_trans beta (trm_abs u)). apply star_step. apply_fresh* beta_abs 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. apply_fresh* beta_star_abs as y. 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. (* ********************************************************************** *) (** Properties of parallel relation and its iterated version *) Section ParaProperties. Hint Extern 1 (para (if _ == _ then _ else _) _) => case_var. Lemma para_red_all : red_all para. Proof. intros x t t' H. induction H; intros; simpl*. rewrite* subst_open. apply_fresh* para_red as y. cross*. apply_fresh* para_abs as y. cross*. Qed. Lemma para_red_refl : red_refl para. Proof. introz. induction* H. Qed. Lemma para_red_out : red_out para. Proof. apply* (red_all_to_out para_red_all para_red_refl). Qed. Lemma para_red_rename : red_rename para. Proof. apply* (red_out_to_rename para_red_out). Qed. Lemma para_red_through : red_through para. Proof. apply* (red_all_to_through red_regular_para para_red_all). Qed. Lemma para_iter_red_refl : red_refl (para iter). Proof. introz. use para_red_refl. Qed. End ParaProperties. (* ********************************************************************** *) (** Confluence of parallel relation *) Lemma para_abs_inv : forall t1 u, para (trm_abs t1) u -> exists L, exists t2, u = (trm_abs t2) /\ forall x : var, x \notin L -> para (t1 ^ x) (t2 ^ x). Proof. intros. inversion* H. Qed. Lemma para_confluence : confluence para. Proof. introv HS. gen T. induction HS; intros T HT; inversions HT. (* case: red / red *) destructi~ (IHHS t2'0) as [u2 [U2a U2b]]. pick_fresh x. forward~ (H0 x) as K. destruct~ (K (t1'0 ^ x)) as [u1x [U1a U1b]]. destruct~ (@close_var_spec u1x x) as [u1 [EQu1 termu1]]. rewrite EQu1 in U1a, U1b. exists (u1 ^^ u2). split; apply* (@para_red_through x). (* case: red / trm_app *) destructi~ (IHHS t2'0) as [u2 [U2a U2b]]. destruct (para_abs_inv H3) as [L2 [t1'0x [EQ Ht1'0]]]. rewrite EQ in H3 |- *. pick_fresh x. forward~ (H0 x) as K. destruct ~ (K (t1'0x ^ x)) as [u1x [U1a U1b]]. destruct~ (@close_var_spec u1x x) as [u1 [EQu1 termu1]]. rewrite EQu1 in U1a, U1b. exists (u1 ^^ u2). split. apply* (@para_red_through x). apply_fresh para_red as y; auto. apply* (@para_red_rename x). (* case: var / var *) auto*. (* case: trm_app / red *) destruct~ (IHHS2 t2'0) as [u2 [U2a U2b]]. destruct (para_abs_inv HS1) as [L2 [t1'x [EQ Ht1'x]]]. destruct (IHHS1 (trm_abs t1'0)) as [u1x [U1a U1b]]. apply_fresh* para_abs as y. rewrite EQ in HS1, U1a |- *. destruct (para_abs_inv U1b) as [L1 [u1 [EQ' Hu1]]]. rewrite EQ' in U1a, U1b. exists (u1 ^^ u2). split. inversion U1a. apply* (@para_red L0). pick_fresh x. apply* (@para_red_through x). (* case: trm_app / trm_app *) destructi~ (IHHS1 t1'0) as [P1 [HP11 HP12]]. destructi~ (IHHS2 t2'0) as [P2 [HP21 HP22]]. exists* (trm_app P1 P2). (* case: trm_abs / trm_abs *) pick_fresh x. forward~ (H0 x) as K. destruct~ (K (t1'0 ^ x)) as [px [P0 P1]]. destruct~ (@close_var_spec px x) as [p [EQP termp]]. rewrite EQP in P0, P1. exists (trm_abs p). split; apply_fresh* para_abs as y; apply* (@para_red_rename x). Qed. (* ********************************************************************** *) (** Confluence of iterated parallel relation *) Lemma para_iter_parallelogram : forall M S, (para iter) M S -> forall T, para M T -> exists P : trm, para S P /\ (para iter) T P. Proof. introv H. induction H; introv MtoT. destructi~ (IHiter_1 T) as [P [HP1 HP2]]. destructi~ (IHiter_2 P) as [Q [HQ1 HQ2]]. exists Q. use (@iter_trans para P). destruct* (para_confluence H MtoT). Qed. Lemma para_iter_confluence : confluence (para iter). Proof. introv MtoS MtoT. gen T. induction MtoS; introv MtoT. destructi~ (IHMtoS1 T) as [P [HP1 HP2]]. destructi~ (IHMtoS2 P) as [Q [HQ1 HQ2]]. exists* Q. destruct* (para_iter_parallelogram MtoT H). Qed. (* ********************************************************************** *) (** Equality of beta star and iterated parallel relations *) Lemma beta_star_to_para_iter : (beta star) simulated_by (para iter). Proof. introz. induction* H. apply* para_iter_red_refl. apply iter_step. induction H; use para_red_refl. Qed. Lemma para_iter_to_beta_star : (para iter) simulated_by (beta star). Proof. introz. induction H; eauto. induction H. apply~ (@star_trans beta (t1 ^^ t2)). pick_fresh x. apply* (@beta_star_red_through x). apply* star_refl. apply~ (@star_trans beta (trm_app t1' t2)). apply* beta_star_app1. apply* beta_star_app2. apply* beta_star_abs. Qed. (* ********************************************************************** *) (** Church-Rosser property of beta relation *) Lemma beta_star_confluence : confluence (beta star). Proof. introz. destruct (@para_iter_confluence M S T). use beta_star_to_para_iter. use beta_star_to_para_iter. use para_iter_to_beta_star. Qed. Lemma beta_church_rosser : church_rosser beta. Proof. introz. induction H. exists* t. destruct* IHequiv_. destruct IHequiv_1 as [u [Pu Qu]]. destruct IHequiv_2 as [v [Pv Qv]]. destruct (beta_star_confluence Qu Pv) as [w [Pw Qw]]. exists w. split. apply* (@star_trans beta u). apply* (@star_trans beta v). exists* t'. Qed. ```