```(*************************************************************************** * Calculus of Constructions - Church-Rosser Property * * Arthur Charguéraud, April 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_BetaStar. (* ********************************************************************** *) (** ** Additional Definitions Used in this Proof *) (* ********************************************************************** *) (** Definition of parallel reduction *) Inductive para : relation := | para_red : forall L t1 t2 t2' u u', term t1 -> (forall x, x \notin L -> para (t2 ^ x) (t2' ^ x) ) -> para u u' -> para (trm_app (trm_abs t1 t2) u) (t2' ^^ u') | para_var : forall x, para (trm_fvar x) (trm_fvar x) | para_srt : forall n, para (trm_type n) (trm_type n) | para_app : forall t1 t1' t2 t2', para t1 t1' -> para t2 t2' -> para (trm_app t1 t2) (trm_app t1' t2') | para_abs : forall L t1 t1' t2 t2', para t1 t1' -> (forall x, x \notin L -> para (t2 ^ x) (t2' ^ x) ) -> para (trm_abs t1 t2) (trm_abs t1' t2') | para_prod : forall L t1 t1' t2 t2', para t1 t1' -> (forall x, x \notin L -> para (t2 ^ x) (t2' ^ x) ) -> para (trm_prod t1 t2) (trm_prod t1' t2'). (* ********************************************************************** *) (** Definition of the transitive closure of a relation *) Inductive iter_ (R : relation) : relation := | iter_trans : forall t2 t1 t3, iter_ R t1 t2 -> iter_ R t2 t3 -> iter_ R t1 t3 | iter_step : forall t t', R t t' -> iter_ R t t'. Notation "R 'iter'" := (iter_ R) (at level 69). (* ********************************************************************** *) (** ** Lemmas Associated to Additional Definitions *) Hint Constructors para iter_. (* ********************************************************************** *) (** Regularity *) Lemma red_regular_para : red_regular para. Proof. introz. induction* H. Qed. Lemma red_regular_para_iter : red_regular (para iter). Proof. introz. induction* H. apply* red_regular_para. Qed. Hint Extern 1 (term ?t) => match goal with | H: para t _ |- _ => apply (proj1 (red_regular_para H)) | H: para _ t |- _ => apply (proj2 (red_regular_para H)) | H: (para iter) t _ |- _ => apply (proj1 (red_regular_para_iter)) | H: (para iter) _ t |- _ => apply (proj2 (red_regular_para_iter)) end. (* ********************************************************************** *) (** Automation *) Hint Resolve para_var para_srt 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_prod _ _) (trm_prod _ _)) => let y := fresh "y" in apply_fresh para_prod as y. Hint Extern 1 (para (trm_app (trm_abs _ _) _) (_ ^^ _)) => let y := fresh "y" in apply_fresh para_red as y. (* ********************************************************************** *) (** Properties of parallel reduction 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*. apply_fresh* para_prod 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. (* ********************************************************************** *) (** Equality of beta star and iterated parallel reductions *) 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 (t2 ^^ u)). pick_fresh x. apply* (@beta_star_red_through x). apply* star_refl. apply* star_refl. apply~ (@star_trans beta (trm_app t1' t2)). apply* beta_star_app1. apply* beta_star_app2. apply~ (@star_trans beta (trm_abs t1' t2)). apply* beta_star_abs1. apply* beta_star_abs2. apply~ (@star_trans beta (trm_prod t1' t2)). apply* beta_star_prod1. apply* beta_star_prod2. Qed. (* ********************************************************************** *) (** ** Proof of Church-Rosser Property for Beta Reduction *) (* ********************************************************************** *) (** Confluence of parallel reduction *) Lemma para_abs_inv : forall t1 t2 u, para (trm_abs t1 t2) u -> exists L, exists t1' : trm, exists t2' : trm, u = (trm_abs t1' t2') /\ para t1 t1' /\ forall x : var, x \notin L -> para (t2 ^ x) (t2' ^ x). intros. inversion H. exists* L. Qed. Lemma para_prod_inv : forall t1 t2 u, para (trm_prod t1 t2) u -> exists L, exists t1' : trm, exists t2' : trm, u = (trm_prod t1' t2') /\ para t1 t1' /\ forall x : var, x \notin L -> para (t2 ^ x) (t2' ^ x). Proof. intros. inversion H. exists* L. Qed. Lemma para_confluence : confluence para. Proof. introv HS. gen T. induction HS; intros T HT; inversions HT. (* case: red / red *) destructi~ (IHHS u'0) as [u2 [U2a U2b]]. pick_fresh x. forward~ (H1 x) as K. destruct~ (K (t2'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 H4) as [L2 [t1'0x [t2'0x [EQ [Ht1'0 Ht2'0]]]]]. rewrite EQ in H4 |- *. pick_fresh x. forward~ (H1 x) as K. destruct~ (K (t2'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: srt / srt *) auto*. (* case: trm_app / red *) destruct~ (IHHS2 u') as [u2 [U2a U2b]]. destruct (para_abs_inv HS1) as [L2 [t1'x [t2'x [EQ [Ht1'x Ht2'x]]]]]. destruct (IHHS1 (trm_abs t1'x t2'0)) as [u1x [U1a U1b]]. auto. rewrite EQ in HS1, U1a |- *. destruct (para_abs_inv U1b) as [L1 [v1 [v2 [EQ' [Hv1 Hv2]]]]]. rewrite EQ' in U1a, U1b. exists (v2 ^^ u2). split. inversion U1a. clear IHHS1 IHHS2 Hv2 U1a U1b. 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 (t2'0 ^ x)) as [px [P0 P1]]. destructi~ (IHHS t1'0) as [u1 [HP1 HP2]]. destruct~ (@close_var_spec px x) as [p [EQP termp]]. rewrite EQP in P0, P1. exists (trm_abs u1 p). split; apply_fresh* para_abs as y; apply* (@para_red_rename x). (* case: trm_prod / trm_prod *) pick_fresh x. forward~ (H0 x) as K. destruct~ (K (t2'0 ^ x)) as [px [P0 P1]]. destructi~ (IHHS t1'0) as [u1 [HP1 HP2]]. destruct~ (@close_var_spec px x) as [p [EQP termp]]. rewrite EQP in P0, P1. exists (trm_prod u1 p). split; apply_fresh* para_prod as y; apply* (@para_red_rename x). Qed. (* ********************************************************************** *) (** Confluence of iterated parallel reduction *) 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; intros T 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; intros T MtoT. destructi~ (IHMtoS1 T) as [P [HP1 HP2]]. destructi~ (IHMtoS2 P) as [Q [HQ1 HQ2]]. exists* Q. destruct* (para_iter_parallelogram MtoT H). Qed. (* ********************************************************************** *) (** Church-Rosser property of beta reduction *) Lemma confluence_beta_star : 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 church_rosser_beta : 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 (confluence_beta_star Qu Pv) as [w [Pw Qw]]. exists w. split. apply* (@star_trans beta u). apply* (@star_trans beta v). exists* t'. Qed. ```