Require Export Base.

Notation "p '<=1' q" := (∀ x, p x → q x) (at level 70).
Notation "p '=1' q" := (p <=1 q ∧ q <=1 p) (at level 70).
Notation "R '<=2' S" := (∀ x y, R x y → S x y) (at level 70).
Notation "R '=2' S" := (R <=2 S ∧ S <=2 R) (at level 70).

Definition rcomp X Y Z (R : X → Y → Prop) (S : Y → Z → Prop)
: X → Z → Prop :=
  fun x z ⇒ ∃ y, R x y ∧ S y z.

Require Import Arith.
Definition pow X R n : X → X → Prop := it (rcomp R) n eq.

Section FixX.
  Variable X : Type.
  Implicit Types R S : X → X → Prop.
  Implicit Types x y z : X.

  Definition reflexive R := ∀ x, R x x.
  Definition symmetric R := ∀ x y, R x y → R y x.
  Definition transitive R := ∀ x y z, R x y → R y z → R x z.
  Definition functional R := ∀ x y z, R x y → R x z → y = z.

  Inductive star R : X → X → Prop :=
  | starR x : star R x x
  | starC x y z : R x y → star R y z → star R x z.


  Lemma star_simpl_ind R (p : X → Prop) y :
    p y →
    (∀ x x', R x x' → star R x' y → p x' → p x) →
    ∀ x, star R x y → p x.
  Proof.
    intros A B. induction 1; eauto.
  Qed.

  Lemma star_trans R:
    transitive (star R).
  Proof.
    induction 1; eauto using star.
  Qed.

  Lemma star_pow R x y :
    star R x y ↔ ∃ n, pow R n x y.
  Proof.
    split; intros A.
    - induction A as [|x x' y B _ [n IH]].
      + ∃ 0. reflexivity.
               + ∃ (S n), x'. auto.
               - destruct A as [n A].
                 revert x A. induction n; intros x A.
                 + destruct A. constructor.
                 + destruct A as [x' [A B]]. econstructor; eauto.
  Qed.

  Lemma pow_star R x y n:
    pow R n x y → star R x y.
  Proof.
    intros A. erewrite star_pow. eauto.
  Qed.

  Inductive ecl R : X → X → Prop :=
  | eclR x : ecl R x x
  | eclC x y z : R x y → ecl R y z → ecl R x z
  | eclS x y z : R y x → ecl R y z → ecl R x z.

  Lemma ecl_trans R :
    transitive (ecl R).
  Proof.
    induction 1; eauto using ecl.
  Qed.

  Lemma ecl_sym R :
    symmetric (ecl R).
  Proof.
    induction 1; eauto using ecl, (@ecl_trans R).
  Qed.

  Lemma star_ecl R :
    star R <=2 ecl R.
  Proof.
    induction 1; eauto using ecl.
  Qed.

  Definition joinable R x y :=
    ∃ z, R x z ∧ R y z.

  Definition diamond R :=
    ∀ x y z, R x y → R x z → joinable R y z.

  Definition confluent R := diamond (star R).

  Definition semi_confluent R :=
    ∀ x y z, R x y → star R x z → joinable (star R) y z.

  Definition church_rosser R :=
    ecl R <=2 joinable (star R).

  Goal ∀ R, diamond R → semi_confluent R.
  Proof.
    intros R A x y z B C.
    revert x C y B.
    refine (star_simpl_ind _ _).
    - intros y C. ∃ y. eauto using star.
    - intros x x' C D IH y E.
      destruct (A _ _ _ C E) as [v [F G]].
      destruct (IH _ F) as [u [H I]].
      assert (J:= starC G H).
      ∃ u. eauto using star.
  Qed.

  Lemma diamond_to_semi_confluent R :
    diamond R → semi_confluent R.
  Proof.
    intros A x y z B C. revert y B.
    induction C as [|x x' z D _ IH]; intros y B.
    - ∃ y. eauto using star.
             - destruct (A _ _ _ B D) as [v [E F]].
               destruct (IH _ F) as [u [G H]].
               ∃ u. eauto using star.
  Qed.

  Lemma semi_confluent_confluent R :
    semi_confluent R ↔ confluent R.
  Proof.
    split; intros A x y z B C.
    - revert y B.
      induction C as [|x x' z D _ IH]; intros y B.
      + ∃ y. eauto using star.
               + destruct (A _ _ _ D B) as [v [E F]].
                 destruct (IH _ E) as [u [G H]].
                 ∃ u. eauto using (@star_trans R).
               - apply (A x y z); eauto using star.
  Qed.

  Lemma diamond_to_confluent R :
    diamond R → confluent R.
  Proof.
    intros A. apply semi_confluent_confluent, diamond_to_semi_confluent, A.
  Qed.

  Lemma confluent_CR R :
    church_rosser R ↔ confluent R.
  Proof.
    split; intros A.
    - intros x y z B C. apply A.
      eauto using (@ecl_trans R), star_ecl, (@ecl_sym R).
    - intros x y B. apply semi_confluent_confluent in A.
      induction B as [x|x x' y C B IH|x x' y C B IH].
      + ∃ x. eauto using star.
      + destruct IH as [z [D E]]. ∃ z. eauto using star.
      + destruct IH as [u [D E]].
        destruct (A _ _ _ C D) as [z [F G]].
        ∃ z. eauto using (@star_trans R).
  Qed.


  Lemma pow_add R n m (x y : X) : pow R (n + m) x y ↔ rcomp (pow R n) (pow R m) x y.
  Proof.
    revert m x y; induction n; intros m x y.
    - simpl. split; intros. econstructor. split. unfold pow. simpl. reflexivity. eassumption.
      destruct H as [u [H1 H2]]. unfold pow in H1. simpl in ×. subst x. eassumption.
    - simpl in *; split; intros.
      + destruct H as [u [H1 H2]].
        change (it (rcomp R) (n + m) eq) with (pow R (n+m)) in H2.
        rewrite IHn in H2.
        destruct H2 as [u' [A B]]. unfold pow in A.
        econstructor.
        split. econstructor. repeat split; repeat eassumption. eassumption.
      + destruct H as [u [H1 H2]].
        destruct H1 as [u' [A B]].
        econstructor. split. eassumption. change (it (rcomp R) (n + m) eq) with (pow R (n + m)).
        rewrite IHn. econstructor. split; eassumption.
  Qed.

  Lemma rcomp_1 (R : X → X → Prop): R =2 pow R 1.
  Proof.
    split; intros x t; unfold pow in *; simpl in *; intros H.
    - ∃ t. tauto.
    - destruct H as [u [H1 H2]]; subst u; eassumption.
  Qed.

End FixX.

  Instance star_PreOrder X (R:X → X → Prop): PreOrder (star R).
  Proof.
    constructor; hnf.
    - eapply starR.
    - eapply star_trans.
  Qed.

  Instance ecl_equivalence X (R:X → X → Prop): Equivalence (ecl R).
  Proof.
    constructor; hnf.
    - apply eclR.
    - apply ecl_sym.
      -apply ecl_trans.
  Qed.

  Instance R_star_subrelation X (R:X → X → Prop): subrelation R (star R).
  Proof.
    intros s t st. eauto using star.
  Qed.

  Instance pow_star_subrelation X (R:X → X → Prop) n: subrelation (pow R n) (star R).
  Proof.
    intros ? ?. apply pow_star.
  Qed.

  Instance star_ecl_subrelation X (R:X → X → Prop) : subrelation (star R) (ecl R).
  Proof.
    intros ? ?. apply star_ecl.
  Qed.

  Instance R_ecl_subrelation X (R:X → X → Prop): subrelation R (ecl R).
  Proof.
    intros ? ? ?. apply star_ecl_subrelation. now apply R_star_subrelation.
  Qed.