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.

  Lemma star_trans R:
    transitive (star R).

  Lemma star_pow R x y :
    star R x y ↔ ∃ n, pow R n x y.

  Lemma pow_star R x y n:
    pow R n x y → star R x y.

  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).

  Lemma ecl_sym R :
    symmetric (ecl R).

  Lemma star_ecl R :
    star R <=2 ecl R.

  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.

  Lemma diamond_to_semi_confluent R :
    diamond R → semi_confluent R.

  Lemma semi_confluent_confluent R :
    semi_confluent R ↔ confluent R.

  Lemma diamond_to_confluent R :
    diamond R → confluent R.

  Lemma confluent_CR R :
    church_rosser R ↔ confluent R.


  Lemma pow_add R n m (x y : X) : pow R (n + m) x y ↔ rcomp (pow R n) (pow R m) x y.

  Lemma rcomp_1 (R : X → X → Prop): R =2 pow R 1.

End FixX.

  Instance star_PreOrder X (R:X → X → Prop): PreOrder (star R).

  Instance ecl_equivalence X (R:X → X → Prop): Equivalence (ecl R).

  Instance R_star_subrelation X (R:X → X → Prop): subrelation R (star R).

  Instance pow_star_subrelation X (R:X → X → Prop) n: subrelation (pow R n) (star R).

  Instance star_ecl_subrelation X (R:X → X → Prop) : subrelation (star R) (ecl R).

  Instance R_ecl_subrelation X (R:X → X → Prop): subrelation R (ecl R).