Diamond property implies confluence

Using Coq
1

So I’ve been working on formalizing a proof of the Church-Rosser theorem for beta-reduction in the untyped lambda calculus following Peter Selinger’s Lecture notes on the Lambda Calculus, and I’ve managed to do so for all the major lemmas leading up to the main theorem, but somehow, I spent hours on trying to prove that “diamond property implies confluence” (probably the last step to completing the proof for the main theorem) to no avail, even though its informal proof is already given as a nice little diagram in Figure 3. I’m probably missing something obvious here, so any hints on how to proceed would be much appreciated.

Here is a minimal reproducible snippet of my code:

From Coq Require Import Relations.

Ltac inv H := inversion H; subst; clear H.

Hint Constructors clos_refl_trans_1n.

Lemma diamond_property_implies_confluence :
  forall {A : Type} (R : A -> A -> Prop),
  (forall x y z,
    R x y ->
    R x z ->
    exists w, R y w /\ R z w) ->
  forall x y z,
    clos_refl_trans_1n A R x y ->
    clos_refl_trans_1n A R x z ->
    exists w, clos_refl_trans_1n A R y w /\
      clos_refl_trans_1n A R z w.
Proof.
  intros.
  generalize dependent z.
  induction H0; intros; eauto.
  inv H2; eauto.
  destruct (H _ _ _ H0 H3) as [? [? ?]].
  (* TODO *)
Admitted.

Specifically, I am stuck at the following context:

1 subgoal
A : Type
R : A -> A -> Prop
H : forall x y z : A,
    R x y -> R x z -> exists w : A, R y w /\ R z w
x, y, z : A
H0 : R x y
H1 : clos_refl_trans_1n A R y z
IHclos_refl_trans_1n : forall z0 : A,
                       clos_refl_trans_1n A R y z0 ->
                       exists w : A,
                         clos_refl_trans_1n A R z
                           w /\
                         clos_refl_trans_1n A R z0
                           w
z0, y0 : A
H3 : R x y0
H4 : clos_refl_trans_1n A R y0 z0
x0 : A
H2 : R y x0
H5 : R y0 x0
______________________________________(1/1)
exists w : A,
  clos_refl_trans_1n A R z w /\
  clos_refl_trans_1n A R z0 w

Directly applying the inductive hypothesis at this stage to transform the goal to clos_refl_trans_1n A R y z0 seems like a dead end. The other thing that I tried was show that clos_refl_trans_1n A R y x0 and then apply the induction hypothesis to that to yield two new hypotheses clos_refl_trans_1n A R z w and clos_refl_trans_1n A R x0 w for some w, but that doesn’t seem to lead me to a proof of clos_refl_trans_1n A R z0 w either.

1 Like
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
3

Funny, I happen to be working on proving the Church-Rosser theorem as well! Though I’m not as far along as you are. Thank you @gasche for the help, I’m sure it will come in handy for me too.

4

@DonaldKellett pardon me if this is straying from the topic of your question, but I’m curious as to how you’re dealing with generating fresh variable names when doing capture-avoiding substitution. I’m myself working with DeBruijn notation, which avoids this issue. But I’m very intrigued as to how to do a more human-friendly notation in Coq.

5

Many thanks for your proof sketch - I went with the clever approach and was able to prove that diamond property implies confluence in just a few lines, which subsequently enabled me to complete my proof of the Church-Rosser theorem :heart:

6

Incidentally, I was also working with deBruijn indices so I’m afraid I do not have an answer to your question.

7

I figured it’s not necessary to switch up the definition for reflexive-transitive closure (R x y /\ R* y z one is fine). The important thing that made the ‘clever’ proof go through is on_the_left, doing just a ‘row’ of the rectangle. It’s the intermediate induction hypothesis that made ‘induction on one side, then the other’ the proof go through.

1 Like
8

@DonaldKellett I happen to also be formalizing Church-Rosser with those lecture notes (I’m using de Bruijn indices). I managed to show that the diamond property implies confluence, however I got really stuck on lemma 4.7, and that’s the only remaining lemma left for me. What auxiliary lemmas helped?

9

Yeah, this is a tricky one - in my proof, it only directly depends on two lemmas but those two lemmas depend in turn on a number of other lemmas.

I suppose you are getting stuck dealing with complex expressions involving lifting and substitution. In that case, I would recommend reading How I learned to stop worrying and love deBrujin indices if you haven’t done so already, and then whenever you encounter a syntactic mismatch between the lifting and substitution expressions in the hypotheses and conclusion, try to draw (a) diagram(s) to see why/whether the two expressions are actually equivalent, and work from there to figure out the intermediate lemmas you need to prove.

On a side note, if you’d like to share your results once you’ve figured out the final piece of the puzzle and learn from others, you may be interested in this Kata.

1 Like
10

For anyone curious, with the right lemmas and after working through some of them, it was pretty straightforward. I cleaned up parts of the proof over the last few days.

1 Like
11

@DonaldKellett how do you draw substitution? That article makes lifting nice and visual but I can’t seem to work through how substitution and lifting interact graphically.

12

You’re right that substitution is not depicted in the article. IIRC I figured it out myself by thinking about how substitution works and drawing some inspiration from how lifting is visualized. I wish I could give you a more specific answer, but unfortunately I did not keep my diagrams once I was done with the formalization :sweat_smile: