Diamond property implies confluence

Using Rocq
2

The problem is that the proof is actually a bit tricky in stating exactly what we are inducing over. Note that this is not specific to Coq, you would hit the same issue if trying to do a pen-and-paper proof carefully. The lecture notes do a “graphical proof” which makes these difficulties invisible.

The statement that you are trying to prove says in essence: for any x, all pairs of paths out of x can be closed into a diamond. It is natural to try to do this by induction over the paths. But, given the definitions that you are using, you end up in situations where you would have to use an induction hypothesis on a pair of (shorter) paths out of another point; the induction hypothesis is only about paths out of x, so you are stuck.

If you look at the details, the reason why paths out of another point come up in the proof is the definition of the reflexive-transitive closure R* of a relation R. The non-base-case definition says that R* x z holds when R x y and R* y z for some y; in the corresponding case of the proof, you have to work with pairs of paths starting from y.

There are two ways out of this problem:

  • The general approach: instead of doing an induction on a reduction sequence, do an induction on the length of induction sequences: “forall n, all n-length diamonds can be closed”. This is what a pen-and-paper mathematician would do in this situation, because they are typically more familiar with induction on numbers.
  • The clever approach, which is to change the definition of reflexive-transitive closure to make the proof go through.

Once the equivalence between the two forms of reflexive-transitive closure is done, the proofs with the clever approach are nicer than with the general approach, because you do the induction directly on the inductive structure of interest (the reduction sequence), instead of doing an induction on a natural number and then an inversion on the reduction sequence.

I have done both to answer your question. Here are my definitions and lemma statements – I thought you may prefer to have to write the proofs yourself.

Common definitions and statements

Definition diamond_property {A : Type}
           (R1 R2 : A -> A -> Prop)  :=
forall x y z,
    R1 x y ->
    R2 x z ->
    exists w, R2 y w /\ R1 z w.

Lemma diamond_symmetric : forall {A : Type} (R1 R2 : A -> A -> Prop),
  diamond_property R1 R2 -> diamond_property R2 R1.

General approach

Inductive star {A : Type} (R : A -> A -> Prop) : nat -> A -> A -> Prop :=
| Zero : forall x, star R 0 x x
| Step : forall x y, R x y -> forall n z, star R n y z -> star R (S n) x z.

Lemma clos_refl_star : forall {A} R x y, clos_refl_trans_1n A R x y <-> exists n, star R n x y.

Lemma on_the_left :
  forall {A : Type} (R1 R2 : A -> A -> Prop),
  diamond_property R1 R2 -> forall n, diamond_property (star R1 n) R2.

Lemma on_the_right :                     
  forall {A : Type} (R1 R2 : A -> A -> Prop),
  diamond_property R1 R2 -> forall n, diamond_property R1 (star R2 n).

Lemma diamond_property_implies_mn_confluence :
  forall {A : Type} (R : A -> A -> Prop),
  diamond_property R R -> forall m n, diamond_property (star R m) (star R n).

Theorem diamond_property_implies_confluence :
  forall {A : Type} (R : A -> A -> Prop),
  diamond_property R R -> diamond_property (clos_refl_trans_1n A R) (clos_refl_trans_1n A R).

Clever approach

Inductive clos_refl_trans {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
| Zero : forall x, clos_refl_trans R x x
| Step : forall x y, clos_refl_trans R x y -> forall z, R y z -> clos_refl_trans R x z.

Lemma snoc_clos_refl_trans_1n {A : Type} (R : A -> A -> Prop) :
  forall x y, clos_refl_trans_1n A R x y -> forall z, R y z -> clos_refl_trans_1n A R x z.

Lemma cons_clos_refl_trans {A : Type} (R : A -> A -> Prop) :
  forall y z, clos_refl_trans R y z -> forall x, R x y -> clos_refl_trans R x z.

Lemma clos_refl_trans_equiv {A : Type} R :
  forall x y, clos_refl_trans R x y <-> clos_refl_trans_1n A R x y.

Lemma on_the_left :
  forall {A : Type} (R1 R2 : A -> A -> Prop),
  diamond_property R1 R2 -> diamond_property (clos_refl_trans R1) R2.

(The rest of the proof is exactly similar to the general approach.)

4 Likes