(** * Confluence *) Set Implicit Arguments. Unset Strict Implicit. Notation "R <<= S" := (forall x y, R x y -> S x y) (at level 70). Notation "R === S" := (R <<= S /\ S <<= R) (at level 70). Section Sec1. Variables (X: Type) (R: X -> X -> Prop). Implicit Types x y z : X. Definition functional := forall x y z, R x y -> R x z -> y = z. Inductive star : X -> X -> Prop := | starRefl x : star x x | starStep x x' y : R x x' -> star x' y -> star x y. Fact star_trans x y z : star x y -> star y z -> star x z. Proof. intros H1 H2. induction H1 as [x|x x' y H _ IH]. + exact H2. + econstructor 2. exact H. auto. Qed. Fact star_exp : R <<= star. Proof. intros x y H. econstructor 2. exact H. constructor. Qed. End Sec1. Hint Constructors star : core. Hint Resolve star_exp star_trans : core. Section Sec2. Variable X: Type. Implicit Types (x y z : X) (R : X -> X -> Prop). Definition joinable R x y := exists z, R x z /\ R y z. Definition diamond R := forall x y z, R x y -> R x z -> joinable R y z. Definition confluent R := diamond (star R). Definition semi_confluent R := forall x y z, R x y -> star R x z -> joinable (star R) y z. Fact diamond_semi_confluent R : diamond R -> semi_confluent R. Proof. intros H x y1 y2 H1 H2. induction H2 as [x|x x' y2 H2 _ IH] in y1, H1 |-*. - exists y1. auto. - assert (joinable R y1 x') as (z&H3&H4). { eapply H; eauto. } assert (joinable (star R) z y2) as (u&H5&H6). { apply IH; auto. } exists u. eauto. Qed. Fact confluent_semi R : confluent R <-> semi_confluent R. Proof. split. - intros H x y1 y2 H1 H2. eapply H. 2:exact H2. auto. - intros H x y1 y2 H1 H2. induction H1 as [x|x x' y1 H1 _ IH] in y2, H2. + exists y2. auto. + assert (joinable (star R) x' y2) as (z&H3&H4). { eapply H; eauto. } assert (joinable (star R) y1 z) as (u&H5&H6). { apply IH; auto. } exists u. eauto. Qed. Fact diamond_confluent R : diamond R -> confluent R. Proof. intros H. apply confluent_semi, diamond_semi_confluent, H. Qed. Definition prediamond R := forall x y z, R x y -> R x z -> y=z \/ R y z \/ R z y \/ joinable R y z. Fact prediamond_confluent R: prediamond R -> confluent R. Proof. intros H. apply confluent_semi. intros x y1 y2 H1 H2. induction H2 as [x|x x' y2 H2 H3 IH] in y1, H1 |-*. - exists y1. auto. - destruct (H _ _ _ H1 H2) as [->|[H4|[H4|H4]]]. + exists y2. auto. + exists y2. eauto. + apply IH, H4. + destruct H4 as (z&H5&H6). specialize (IH _ H6). destruct IH as (u&H7&H8). exists u. eauto. Qed. End Sec2. (** Evaluation *) Section Iter. Variables (X: Type) (f: X -> X). Fixpoint it n x : X := match n with | 0 => x | S n'=> f (it n' x) end. Fact it_shift n x : f (it n x) = it n (f x). Proof. induction n; cbn; congruence. Qed. End Iter. Section Eval. Variables (X: Type) (R: X -> X -> Prop). Implicit Types x y z : X. Notation "x ≻ y" := (R x y) (at level 70). Notation "x ≻* y" := (star R x y) (at level 70). Definition normal x := ~ exists y, x ≻ y. Definition eval x y := x ≻* y /\ normal y. Notation "x ⊳ y" := (eval x y) (at level 70). Fact star_normal x y: x ≻* y -> normal x -> x = y. Proof. intros H1 H2. destruct H1 as [x|x y z H1 _]. - reflexivity. - exfalso. apply H2. eauto. Qed. Fact eval_functional: confluent R -> functional eval. Proof. intros H x y z [H1 H2] [H3 H4]. assert (joinable (star R) y z) as (u&H5&H6). { eapply H; eauto. } apply star_normal in H5. 2:exact H2. apply star_normal in H6. 2:exact H4. congruence. Qed. Definition red_fun rho := (forall x, x ≻* rho x) /\ (forall x y, x ⊳ y -> exists n, it rho n x = y). Section Evaluator. Variables (rho: X -> X) (red: red_fun rho). Fact red_fun_fp x : normal x -> rho x = x. Proof. intros H. symmetry. apply star_normal. - apply red. - exact H. Qed. Fact red_fun_fp_it x n : normal x -> it rho n x = x. Proof. intros H. induction n as [|n IH]; cbn. - reflexivity. - rewrite IH. apply red_fun_fp, H. Qed. Fact red_fun_normal x y : x ⊳ y <-> normal y /\ exists n, it rho n x = y. Proof. destruct red as [H1 H2]. split. - intros [H3 H4]. split. exact H4. apply H2. hnf. auto. - intros [H3 [n <-]]. split. 2:exact H3. clear H2 H3. induction n as [|n IH]; cbn; eauto. Qed. Variable (delta: forall x, normal x + ~ normal x). Fixpoint E n x : option X := match n with | 0 => None | S n' => if delta x then Some x else E n' (rho x) end. Fact E_S n x : E (S n) x = if delta x then Some x else E n (rho x). Proof. reflexivity. Qed. Fact E_it x n : normal (it rho n x) -> E (S n) x = Some (it rho n x). Proof. induction n as [|n IH] in x |-*. - cbn. destruct (delta x) as [H|H]; tauto. - cbn [it]. rewrite it_shift. intros H1 % IH. rewrite E_S. destruct (delta x) as [H|H]. 2:exact H1. rewrite red_fun_fp by exact H. rewrite red_fun_fp_it by exact H. reflexivity. Qed. Fact E_correct x y : x ⊳ y <-> exists n, E n x = Some y. Proof. split. - intros H. generalize H. intros [n <-] % red. exists (S n). apply E_it, H. - intros [n H]. induction n as [|n IH] in x, H |-*; cbn in *. + discriminate. + destruct (delta x). * assert (x=y) as <- by congruence. split; auto. * apply IH in H as [H1 H2]. split. 2:exact H2. eapply star_trans. 2: exact H1. apply red. Qed. End Evaluator. End Eval. (** Strong normalisation *) Section SN1. Variables (X: Type) (R: X -> X -> Prop). Inductive SN x : Prop := | SNC: (forall y, R x y -> SN y) -> SN x. Fact SN_unfold x : SN x <-> forall y, R x y -> SN y. Proof. split. - destruct 1 as [H]. exact H. - intros H. constructor. exact H. Qed. End SN1. Section Newman. Variable (X: Type). Implicit Types (x y z : X) (R: X -> X -> Prop). Definition terminating R := forall x, SN R x. Definition locally_confluent R := forall x y z, R x y -> R x z -> joinable (star R) y z. Fact Newman R : terminating R -> locally_confluent R -> confluent R. Proof. intros H1 H2 x. generalize (H1 x). induction 1 as [x _ IH]. intros y z H3 H4. destruct H3 as [x|x x1 y H5 H6]. { exists z. auto. } destruct H4 as [x|x x2 z H7 H8]. { exists y. eauto. } assert (joinable (star R) x1 x2) as (u&H9&H10). { eapply H2; eassumption. } assert (joinable (star R) u z) as (v&H11&H12). { eapply (IH x2); eauto. } assert (joinable (star R) y v) as (w&H13&H14). { eapply (IH x1); eauto. } exists w. eauto. Qed. End Newman. Section SN2. Variables (X: Type). Implicit Types (x y z : X) (R: X -> X -> Prop). Fact normal_SN x R : normal R x -> SN R x. Proof. intros H. constructor. intros y H1. exfalso. eapply H; eauto. Qed. Definition tc R x y := exists x', R x x' /\ star R x' y. Fact tc_star R : tc R <<= star R. Proof. intros x y (x'&H1&H2). eauto. Qed. Fact tc_case R x y : tc R x y <-> R x y \/ exists x', R x x' /\ tc R x' y. Proof. split. - intros (x'&H1&H2). destruct H2 as [x'|x' x'' y]. + auto. + right. unfold tc. eauto. - intros [H|(x'&H1&H2)]. + exists y. auto. + exists x'. auto using tc_star. Qed. Fact SN_tc R x : SN R x <-> SN (tc R) x. Proof. split. - induction 1 as [x _ IH]. constructor. intros y [H1|(x'&H1&H2)]%tc_case. + auto. + apply IH in H1 as [H1]. eauto. - induction 1 as [x _ IH]. constructor. intros y H1. apply IH. exists y. auto. Qed. End SN2.