(** * Church Rosser Property and Cofinality of Parallel Reduction Operator *) Require Import ARS LC_Basis. (** * Setoid instances for reduction. *) Instance red_PreOrder : PreOrder (star step). Proof. constructor; hnf. - apply starR. - apply star_trans. Qed. Instance red_app_proper : Proper (star step ==> star step ==> star step) App. Proof. cbv. intros s s' A t t' B. transitivity (s' t). - induction A; eauto using star, step. - induction B; eauto using star, step. Qed. Instance red_lam_proper : Proper (star step ==> star step) Lam. Proof. cbv. intros s s' A. induction A; eauto using star, step. Qed. (** * Parallel Reduction and Cofinality *) Fixpoint rho (s : term) : term := match s with | Var n => Var n | App (Lam s) t => beta (rho t) ! rho s | App s t => App (rho s) (rho t) | Lam s => Lam (rho s) end. Inductive pstep : term -> term -> Prop := | pstepV n : pstep (Var n) (Var n) | pstepA s s' t t' : pstep s s' -> pstep t t' -> pstep (App s t) (App s' t') | pstepL s s' : pstep s s' -> pstep (Lam s) (Lam s') | pstepB s s' t t' : pstep s s' -> pstep t t' -> pstep (App (Lam s) t) (beta t' ! s'). Lemma pstep_refl : reflexive pstep. Proof. intros s. induction s ; auto using pstep. Qed. Lemma step_pstep : step <=2 pstep. Proof. induction 1; auto using pstep, pstep_refl. Qed. Lemma pstep_step : pstep <=2 star step. Proof. intros s t A. induction A. - reflexivity. - rewrite IHA1, IHA2. constructor. - rewrite IHA. constructor. - rewrite IHA1, IHA2. eauto using star, step. Qed. Lemma red_agrees : star step =2 star pstep. Proof. apply interpolation. - apply step_pstep. - apply pstep_step. Qed. Lemma pstep_substitutive sigma s t : pstep s t -> pstep (sigma ! s) (sigma ! t). Proof. intros A. revert sigma. induction A as [n | s s' t t' _ IHs _ IHt | s s' _ IHs | s s' t t' _ IHs _ IHt ]; simpl ; intros sigma. - apply pstep_refl. - constructor; auto. - constructor; auto. - rewrite subst_beta_com. constructor; auto. Qed. Definition psstep (sigma tau : substitution) : Prop := forall n, pstep (sigma n) (tau n). Lemma pstep_up sigma tau : psstep sigma tau -> psstep (up sigma) (up tau). Proof. intros A [|n] ; simpl. - constructor. - do 2 rewrite subst_ren. apply pstep_substitutive, A. Qed. Lemma pstep_compatible sigma tau s s' : psstep sigma tau -> pstep s s' -> pstep (sigma ! s) (tau ! s'). Proof. intros A B. revert sigma tau A. induction B as [n | s s' t t' _ IHs _ IHt | s s' _ IHs | s s' t t' _ IHs _ IHt ]; simpl ; intros sigma tau A. - apply A. - constructor; auto. - constructor. apply IHs. apply pstep_up, A. - rewrite subst_beta_com. constructor. + apply IHs. apply pstep_up, A. + auto. Qed. Lemma triangle_pstep_rho : triangle pstep rho. Proof. intros s s' A. induction A as [n | s s' t t' As IHs _ IHt | s s' _ IHs | s s' t t' _ IHs _ IHt ]. - constructor. - destruct s as [n |u v|u]. + constructor; assumption. + constructor; assumption. + inv As. simpl. inv IHs. constructor; assumption. - constructor; assumption. - simpl. apply pstep_compatible. + intros [|n] ; simpl. exact IHt. constructor. + exact IHs. Qed. Lemma rho_sound : sound step rho. Proof. apply sound_stable with (S := pstep). exact red_agrees. apply triangle_to_sound. exact triangle_pstep_rho. exact pstep_refl. Qed. Lemma rho_cofinal : cofinal step rho. Proof. apply cofinal_stable with (S := pstep). exact red_agrees. apply triangle_to_cofinal. exact triangle_pstep_rho. Qed. (** * Church Rosser Property *) Theorem CR : church_rosser step. Proof. apply confluent_CR. eapply rho_to_confluent. exact rho_sound. exact rho_cofinal. Qed. (** Alternatively, CR follows directly from the triangle property, but cofinality of rho is a useful property in its own right. *)