Library UnifConfl

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

Uniform Confluence

  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 l1k2 l2 k1).

Uniform Diamond

  Definition uniform_diamond:= x y1 y2, x >> y1 x >> y2 y1 = y2 z, y1 >> z y2 >> z.

Proof of Equivalence

  Lemma uniformly_semi_confluent x y1 y2 k:
    x >> y1
    x >^ k y2
     z l1 l2, y1 >^l1 z y2 >^ l2 z (l2 1 l1 k 1+l1=k+l2).
    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.

  Lemma UD_UC : uniform_diamond uniformly_confluent.
    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.

  Lemma UC_DC : uniformly_confluent uniform_diamond.
    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.

  Lemma UC_confluent: uniformly_confluent confluent R.
    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.

Characterization of Niehren

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


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

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

Uniform Confluence and Irreducible Terms

  Section UC.
  Variable UC:uniformly_confluent.

In the following, we assume thgat the Relation is uniform 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.
    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.

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

  Lemma unif_unique x y1 y2 k1 k2: irred y1 irred y2 x >^k1 y1 x >^k2 y2 k1=k2 y1 = y2.
    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.
  End UC.
End FixX.