# 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:
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]]]]].
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']]]]].
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.

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

# Irreducibility

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.

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