Require Export ARS.

Section FixX.
  Variable X : Type.
  Variable R : X → X → Prop.
  Implicit Types x y z : X.
  Local Notation "x '>>' y":=(R x y) (at level 8).
  Local Notation "x '>^' n" := (pow R n x) (at level 8,format "x '>^' n").

  Definition uniformly_confluent :=
    ∀ x y1 y2 k1 k2,
      x >^k1 y1 → x >^k2 y2 →
      ∃ z l1 l2 , y1 >^l1 z ∧ y2 >^l2 z ∧ (k1 + l1 = k2 + l2 ∧ l1≤k2 ∧ l2 ≤ k1).

  Definition uniform_diamond:= ∀ x y1 y2, x >> y1 → x >> y2 → y1 = y2 ∨ ∃ z, y1 >> z ∧ y2 >> z.

  Lemma uniformly_semi_confluent x y1 y2 k:
    uniform_diamond →
    x >> y1 →
    x >^ k y2 →
    ∃ z l1 l2, y1 >^l1 z ∧ y2 >^ l2 z ∧ (l2 ≤ 1 ∧ l1 ≤ k ∧ 1+l1=k+l2).
  Proof.
    intros UC. revert x y1 y2. induction k; intros ? ? ? x_y1 x_y2.
    -inv x_y2. ∃ y1,0,1. firstorder.
    -destruct x_y2 as [x' [x_x' x'_y2]]. change (it (rcomp R) k eq x' y2) with (x' >^k y2) in x'_y2.
     destruct (UC _ _ _ x_y1 x_x') as [eq | [z [y1_z x'_z]]].
     +subst x'. eexists y2,k,0. firstorder.
     +destruct (IHk _ _ _ x'_z x'_y2) as [z' [l1 [l2 [z_z' [y2_z' H]]]]].
      ∃ z',(1+l1),l2. rewrite !pow_add. firstorder.
  Qed.

  Lemma UD_UC : uniform_diamond → uniformly_confluent.
  Proof.
    intros UC x y1 y2 k1 k2. revert x y1 y2 k1. induction k2 as [?|k2 IH]; intros ? ? ? ? x_y1 x_y2.
    -inv x_y2. ∃ y1,0,k1. firstorder.
    -replace (S k2) with (k2+1) in x_y2 by omega. rewrite pow_add in x_y2. destruct x_y2 as [x' [x_x' x'_y2]]. apply rcomp_1 in x'_y2.
     destruct (IH _ _ _ _ x_y1 x_x') as [z [l1 [l2 [y1_z [x'_z H]]]]].
     destruct (uniformly_semi_confluent UC x'_y2 x'_z) as [z' [m2[m1[y2_z' [z_z' H']]]]].
     ∃ z',(l1+m1),m2. rewrite pow_add. firstorder.
  Qed.

  Lemma UC_DC : uniformly_confluent → uniform_diamond.
  Proof.
    intros PC x y1 y2 x_y1 x_y2. apply rcomp_1 in x_y1. apply rcomp_1 in x_y2.
    destruct (PC _ _ _ _ _ x_y1 x_y2) as [z [l1 [l2 [y1_z [y2_z H]]]]].
    destruct l1,l2;try omega.
    -inv y1_z. inv y2_z. now left.
    -destruct l1,l2;try omega. right. ∃ z. cbv in y1_z,y2_z. now firstorder subst.
  Qed.

  Lemma UC_confluent: uniformly_confluent → confluent R.
  Proof.
    intros PC. intros x y1 y2 R1 R2. rewrite star_pow in R1,R2. destruct R1 as [l1 R1]. destruct R2 as [l2 R2]. destruct (PC _ _ _ _ _ R1 R2) as [z [? [? [? [? _]]]]]. ∃ z. rewrite !star_pow. firstorder.
  Qed.

  Definition UC_niehren :=
    ∀ x y1 y2 k1 k2 , x>^k1 y1 → x>^k2 y2 →
                           ∃ z m, m ≤ min k1 k2 ∧ y1 >^(k2-m) z ∧ y2 >^(k1-m) z.

  Lemma UC_niehren_iff:
    UC_niehren ↔ uniformly_confluent.
  Proof.
    split.
    -intros UCN x y1 y2 k1 k2 R1 R2.
     destruct (UCN x y1 y2 k1 k2 R1 R2) as (z&m&le&?R1'&R2').
     ∃ z, (k2-m), (k1-m).
     repeat split;try assumption;try omega.
     rewrite !Nat.add_sub_assoc;try omega. eapply Min.min_glb_l; eauto. eapply Min.min_glb_r; eauto.
    -intros UC x y1 y2 k1 k2 R1 R2.
     destruct (UC x y1 y2 k1 k2 R1 R2) as (z&l1&l2&R1'&R2'&eq&le1&le2).
     ∃ z,((k1+k2)-(k1+l1)).
     repeat split.
     +apply Min.min_case_strong; omega.
     +replace ((k2 - (k1 + k2 - (k1 + l1)))) with l1 by omega. assumption.
     +replace ((k1 - (k1 + k2 - (k1 + l1)))) with l2 by omega. assumption.
  Qed.

  Definition irred x := ∀ y, ¬ x >> y.

  Lemma irred_pow x y k : irred x → x >^k y → k=0.
  Proof.
    intros n R1. destruct k. auto. destruct R1 as [z ?]. specialize (n z). tauto.
  Qed.

  Section UC.
  Variable UC:uniformly_confluent.

  Lemma unif_pow_normal_part x y z k1 k2:
    irred y → x >^k1 y → x >^k2 z → k2 ≤ k1 ∧ z >^(k1-k2) y.
  Proof.
    intros n R1 R2. destruct (UC R1 R2) as [v [l1 [l2 [R1' [R2' [H _]]]]]].
    specialize (irred_pow n R1');intros;subst l1. inv R1'. assert (k1-k2=l2) by omega. split. omega. now subst l2.
  Qed.

  Lemma unif_pow_normal x y k1 k2: irred y → x >^k1 y → x >^k2 y → k1=k2.
  Proof.
    intros n R1 R2. specialize (unif_pow_normal_part n R1 R2). specialize (unif_pow_normal_part n R2 R1). omega.
  Qed.

  Lemma unif_unique x y1 y2 k1 k2: irred y1 → irred y2 → x >^k1 y1 → x >^k2 y2 → k1=k2 ∧ y1 = y2.
  Proof.
    intros n1 n2 R1 R2. destruct (UC R1 R2) as (z&l1&l2&R1'&R2'&eq&le1&le2).
    specialize (irred_pow n1 R1'). intros →.
    specialize (irred_pow n2 R2'). intros →.
    inv R1'. inv R2'. split. omega. auto.
  Qed.
  End UC.
End FixX.