(** Lesson 5 -- Why does the triangle property help? (~35 minutes.)

    Read The Taming of the Rew, section 4.1, alongside this file, then
    The Rewster (JAR 2026), sections 4.1-4.2. See study_plan.md for the
    manuscript version and page references.
    This is a small proof about abstract relations, not a model of
    Rocq's syntax or a checker for native rules. It imports none of the
    native examples. The build checks it WITHOUT -allow-rewrite-rules.

    The key move is to find a parallel relation P and a function rho:

                          t
                         / \
                        u -> rho(t)

    Every P-successor of t can take one more P-step to the SAME rho(t).
    We prove the relational argument completely below. Constructing
    the right P and proving this premise for a type theory is the hard
    work in the paper; the premise is not assumed true of our checkout.
*)

From Corelib Require Import Init.Logic.

Set Guard Checking.
Set Universe Checking.

(** [steps R x y] means zero or more R-steps from x to y. A reflexive
    case is essential: a common reduct may already be one endpoint. *)
Inductive steps {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
| steps_refl : forall x, steps R x x
| steps_cons : forall x y z, R x y -> steps R y z -> steps R x z.

Arguments steps_refl {A R} x.
Arguments steps_cons {A R x y z} _ _.

Definition diamond {A : Type} (R : A -> A -> Prop) :=
  forall t u v, R t u -> R t v ->
    exists w, R u w /\ R v w.

Definition confluent {A : Type} (R : A -> A -> Prop) :=
  forall t u v, steps R t u -> steps R t v ->
    exists w, steps R u w /\ steps R v w.

Definition triangle {A : Type} (P : A -> A -> Prop) (rho : A -> A) :=
  (forall t, P t (rho t)) /\
  (forall t u, P t u -> P u (rho t)).

(** Exercise: hide the proof. What witness joins the two successors?
    No induction and no termination argument are needed here. *)
Lemma triangle_diamond {A : Type} (P : A -> A -> Prop) (rho : A -> A) :
  triangle P rho -> diamond P.
A: Type
P: A -> A -> Prop
rho: A -> A
triangle P rho -> diamond P
Proof.
A: Type
P: A -> A -> Prop
rho: A -> A
triangle P rho -> diamond P
  intros [_ Htriangle] t u v Htu Htv.
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
exists w : A, P u w /\ P v w
  exists (rho t).
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P u (rho t) /\ P v (rho t) split.
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P u (rho t)
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P v (rho t)
  -
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P u (rho t) apply Htriangle.
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P t u exact Htu.
  -
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P v (rho t) apply Htriangle.
A: Type
P: A -> A -> Prop
rho: A -> A
Htriangle: forall t u : A, P t u -> P u (rho t)
t, u, v: A
Htu: P t u
Htv: P t v
P t v exact Htv.
Qed.

(** The next two proofs fill a grid of diamonds. The inductions are on
    the FINITE paths supplied to the theorem. They do not assume every
    reduction sequence terminates. Step through one cons case slowly. *)
Lemma diamond_strip {A : Type} (R : A -> A -> Prop) :
  diamond R ->
  forall a b c, R a b -> steps R a c ->
    exists d, steps R b d /\ R c d.
A: Type
R: A -> A -> Prop
diamond R ->
forall a b c : A, R a b -> steps R a c -> exists d : A, steps R b d /\ R c d
Proof.
A: Type
R: A -> A -> Prop
diamond R ->
forall a b c : A, R a b -> steps R a c -> exists d : A, steps R b d /\ R c d
  intros D a b c Hab Hac.
A: Type
R: A -> A -> Prop
D: diamond R
a, b, c: A
Hab: R a b
Hac: steps R a c
exists d : A, steps R b d /\ R c d revert b Hab.
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
forall b : A, R a b -> exists d : A, steps R b d /\ R c d
  induction Hac as [a | a x c Hax Hxc IH].
A: Type
R: A -> A -> Prop
D: diamond R
a: A
forall b : A, R a b -> exists d : A, steps R b d /\ R a d
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
forall b : A, R a b -> exists d : A, steps R b d /\ R c d
  -
A: Type
R: A -> A -> Prop
D: diamond R
a: A
forall b : A, R a b -> exists d : A, steps R b d /\ R a d intros b Hab.
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: R a b
exists d : A, steps R b d /\ R a d exists b.
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: R a b
steps R b b /\ R a b split.
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: R a b
steps R b b
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: R a b
R a b
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: R a b
steps R b b apply steps_refl.
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: R a b
R a b exact Hab.
  -
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
forall b : A, R a b -> exists d : A, steps R b d /\ R c d intros b Hab.
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
exists d : A, steps R b d /\ R c d
    destruct (D a b x Hab Hax) as [w [Hbw Hxw]].
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
exists d : A, steps R b d /\ R c d
    destruct (IH w Hxw) as [d [Hwd Hcd]].
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
d: A
Hwd: steps R w d
Hcd: R c d
exists d0 : A, steps R b d0 /\ R c d0
    exists d.
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
d: A
Hwd: steps R w d
Hcd: R c d
steps R b d /\ R c d split.
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
d: A
Hwd: steps R w d
Hcd: R c d
steps R b d
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
d: A
Hwd: steps R w d
Hcd: R c d
R c d
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
d: A
Hwd: steps R w d
Hcd: R c d
steps R b d exact (steps_cons Hbw Hwd).
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, x, c: A
Hax: R a x
Hxc: steps R x c
IH: forall b : A, R x b -> exists d : A, steps R b d /\ R c d
b: A
Hab: R a b
w: A
Hbw: R b w
Hxw: R x w
d: A
Hwd: steps R w d
Hcd: R c d
R c d exact Hcd.
Qed.

Lemma diamond_confluent {A : Type} (R : A -> A -> Prop) :
  diamond R -> confluent R.
A: Type
R: A -> A -> Prop
diamond R -> confluent R
Proof.
A: Type
R: A -> A -> Prop
diamond R -> confluent R
  intros D a b c Hab.
A: Type
R: A -> A -> Prop
D: diamond R
a, b, c: A
Hab: steps R a b
steps R a c -> exists w : A, steps R b w /\ steps R c w revert c.
A: Type
R: A -> A -> Prop
D: diamond R
a, b: A
Hab: steps R a b
forall c : A, steps R a c -> exists w : A, steps R b w /\ steps R c w
  induction Hab as [a | a x b Hax Hxb IH].
A: Type
R: A -> A -> Prop
D: diamond R
a: A
forall c : A, steps R a c -> exists w : A, steps R a w /\ steps R c w
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
forall c : A, steps R a c -> exists w : A, steps R b w /\ steps R c w
  -
A: Type
R: A -> A -> Prop
D: diamond R
a: A
forall c : A, steps R a c -> exists w : A, steps R a w /\ steps R c w intros c Hac.
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
exists w : A, steps R a w /\ steps R c w exists c.
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
steps R a c /\ steps R c c split.
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
steps R a c
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
steps R c c
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
steps R a c exact Hac.
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, c: A
Hac: steps R a c
steps R c c apply steps_refl.
  -
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
forall c : A, steps R a c -> exists w : A, steps R b w /\ steps R c w intros c Hac.
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
exists w : A, steps R b w /\ steps R c w
    destruct (diamond_strip R D a x c Hax Hac) as [d [Hxd Hcd]].
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
exists w : A, steps R b w /\ steps R c w
    destruct (IH d Hxd) as [e [Hbe Hde]].
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
e: A
Hbe: steps R b e
Hde: steps R d e
exists w : A, steps R b w /\ steps R c w
    exists e.
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
e: A
Hbe: steps R b e
Hde: steps R d e
steps R b e /\ steps R c e split.
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
e: A
Hbe: steps R b e
Hde: steps R d e
steps R b e
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
e: A
Hbe: steps R b e
Hde: steps R d e
steps R c e
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
e: A
Hbe: steps R b e
Hde: steps R d e
steps R b e exact Hbe.
    +
A: Type
R: A -> A -> Prop
D: diamond R
a, x, b: A
Hax: R a x
Hxb: steps R x b
IH: forall c : A, steps R x c -> exists w : A, steps R b w /\ steps R c w
c: A
Hac: steps R a c
d: A
Hxd: steps R x d
Hcd: R c d
e: A
Hbe: steps R b e
Hde: steps R d e
steps R c e exact (steps_cons Hcd Hde).
Qed.

(** Two bookkeeping lemmas let us move between ordinary and parallel
    reduction. Their statements matter more than their proof scripts. *)
Lemma steps_trans {A : Type} (R : A -> A -> Prop) :
  forall x y z, steps R x y -> steps R y z -> steps R x z.
A: Type
R: A -> A -> Prop
forall x y z : A, steps R x y -> steps R y z -> steps R x z
Proof.
A: Type
R: A -> A -> Prop
forall x y z : A, steps R x y -> steps R y z -> steps R x z
  intros x y z Hxy Hyz.
A: Type
R: A -> A -> Prop
x, y, z: A
Hxy: steps R x y
Hyz: steps R y z
steps R x z
  induction Hxy as [x | x u y Hxu Huy IH].
A: Type
R: A -> A -> Prop
z, x: A
Hyz: steps R x z
steps R x z
A: Type
R: A -> A -> Prop
z, x, u, y: A
Hxu: R x u
Huy: steps R u y
Hyz: steps R y z
IH: steps R y z -> steps R u z
steps R x z
  -
A: Type
R: A -> A -> Prop
z, x: A
Hyz: steps R x z
steps R x z exact Hyz.
  -
A: Type
R: A -> A -> Prop
z, x, u, y: A
Hxu: R x u
Huy: steps R u y
Hyz: steps R y z
IH: steps R y z -> steps R u z
steps R x z exact (steps_cons Hxu (IH Hyz)).
Qed.

Lemma steps_simulation {A : Type} (R S : A -> A -> Prop) :
  (forall x y, R x y -> steps S x y) ->
  forall x y, steps R x y -> steps S x y.
A: Type
R, S: A -> A -> Prop
(forall x y : A, R x y -> steps S x y) ->
forall x y : A, steps R x y -> steps S x y
Proof.
A: Type
R, S: A -> A -> Prop
(forall x y : A, R x y -> steps S x y) ->
forall x y : A, steps R x y -> steps S x y
  intros embed x y Hxy.
A: Type
R, S: A -> A -> Prop
embed: forall x y : A, R x y -> steps S x y
x, y: A
Hxy: steps R x y
steps S x y
  induction Hxy as [x | x u y Hxu Huy IH].
A: Type
R, S: A -> A -> Prop
embed: forall x y : A, R x y -> steps S x y
x: A
steps S x x
A: Type
R, S: A -> A -> Prop
embed: forall x y : A, R x y -> steps S x y
x, u, y: A
Hxu: R x u
Huy: steps R u y
IH: steps S u y
steps S x y
  -
A: Type
R, S: A -> A -> Prop
embed: forall x y : A, R x y -> steps S x y
x: A
steps S x x apply steps_refl.
  -
A: Type
R, S: A -> A -> Prop
embed: forall x y : A, R x y -> steps S x y
x, u, y: A
Hxu: R x u
Huy: steps R u y
IH: steps S u y
steps S x y exact (steps_trans S x u y (embed x u Hxu) IH).
Qed.

(** The paper's bridge is R contained in P contained in R*.
    Read the three premises aloud before looking at the proof. *)
Theorem confluence_via_triangle {A : Type}
  (R P : A -> A -> Prop) (rho : A -> A) :
  (forall x y, R x y -> P x y) ->
  (forall x y, P x y -> steps R x y) ->
  triangle P rho -> confluent R.
A: Type
R, P: A -> A -> Prop
rho: A -> A
(forall x y : A, R x y -> P x y) ->
(forall x y : A, P x y -> steps R x y) -> triangle P rho -> confluent R
Proof.
A: Type
R, P: A -> A -> Prop
rho: A -> A
(forall x y : A, R x y -> P x y) ->
(forall x y : A, P x y -> steps R x y) -> triangle P rho -> confluent R
  intros include simulate Htriangle t u v Htu Htv.
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
exists w : A, steps R u w /\ steps R v w
  assert (lift_R : forall x y, R x y -> steps P x y).
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
forall x y : A, R x y -> steps P x y
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
exists w : A, steps R u w /\ steps R v w
  {
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
forall x y : A, R x y -> steps P x y intros x y Hxy.
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
x, y: A
Hxy: R x y
steps P x y
    exact (steps_cons (include x y Hxy) (steps_refl y)). }
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
exists w : A, steps R u w /\ steps R v w
  pose proof (steps_simulation R P lift_R t u Htu) as HtuP.
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
exists w : A, steps R u w /\ steps R v w
  pose proof (steps_simulation R P lift_R t v Htv) as HtvP.
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
exists w : A, steps R u w /\ steps R v w
  destruct (diamond_confluent P (triangle_diamond P rho Htriangle)
    t u v HtuP HtvP) as [w [Huw Hvw]].
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
w: A
Huw: steps P u w
Hvw: steps P v w
exists w0 : A, steps R u w0 /\ steps R v w0
  exists w.
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
w: A
Huw: steps P u w
Hvw: steps P v w
steps R u w /\ steps R v w split.
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
w: A
Huw: steps P u w
Hvw: steps P v w
steps R u w
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
w: A
Huw: steps P u w
Hvw: steps P v w
steps R v w
  -
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
w: A
Huw: steps P u w
Hvw: steps P v w
steps R u w exact (steps_simulation P R simulate u w Huw).
  -
A: Type
R, P: A -> A -> Prop
rho: A -> A
include: forall x y : A, R x y -> P x y
simulate: forall x y : A, P x y -> steps R x y
Htriangle: triangle P rho
t, u, v: A
Htu: steps R t u
Htv: steps R t v
lift_R: forall x y : A, R x y -> steps P x y
HtuP: steps P t u
HtvP: steps P t v
w: A
Huw: steps P u w
Hvw: steps P v w
steps R v w exact (steps_simulation P R simulate v w Hvw).
Qed.

Print confluence_via_triangle.
confluence_via_triangle =
fun (A : Type) (R P : A -> A -> Prop) (rho : A -> A)
  (include : forall x y : A, R x y -> P x y)
  (simulate : forall x y : A, P x y -> steps R x y)
  (Htriangle : triangle P rho) =>
(fun (t u v : A) (Htu : steps R t u) (Htv : steps R t v) =>
 let lift_R : forall x y : A, R x y -> steps P x y :=
   fun (x y : A) (Hxy : R x y) => steps_cons (include x y Hxy) (steps_refl y)
   in
 let HtuP : steps P t u := steps_simulation R P lift_R t u Htu in
 let HtvP : steps P t v := steps_simulation R P lift_R t v Htv in
 let e : exists w : A, steps P u w /\ steps P v w :=
   diamond_confluent P (triangle_diamond P rho Htriangle) t u v HtuP HtvP in
 match e with
 | ex_intro _ x x0 =>
     (fun (w : A) (H : steps P u w /\ steps P v w) =>
      match H with
      | conj x1 x2 =>
          (fun (Huw : steps P u w) (Hvw : steps P v w) =>
           ex_intro (fun w0 : A => steps R u w0 /\ steps R v w0) w
             (conj (steps_simulation P R simulate u w Huw)
                (steps_simulation P R simulate v w Hvw)))
            x1 x2
      end) x x0
 end)
:
confluent R
     : forall {A : Type} (R P : A -> A -> Prop) (rho : A -> A),
       (forall x y : A, R x y -> P x y) ->
       (forall x y : A, P x y -> steps R x y) ->
       triangle P rho -> confluent R

Arguments confluence_via_triangle {A}%_type_scope
  (R P rho _ _)%_function_scope _ t u v _ _
Print Assumptions confluence_via_triangle.
Theory:
Rewrite rules are allowed (subject reduction might be broken)

(** Checkpoint

    1. Where would a certificate have to connect to the ACTUAL native
       reduction relation? Identify all three premises above.
    2. Why is diamond stronger than local confluence? Local confluence
       allows many steps to join a ONE-step peak. It is not enough on
       its own to conclude confluence without another argument.
    3. Does this theorem require strong normalization? No: its proof
       inducts over supplied finite derivations, not an Acc proof of R.
    4. Does it certify [pplus_rules]? No P, rho, or bridge proofs have
       been supplied for Rocq's actual reduction and those rules.

    Reading exercise: Taming Example 4.3 has the same four addition
    equations as Lesson 1. Follow BOTH branches from (S m) + (S n).
    They are joinable, but the paper's chosen one-step parallel witness
    does not satisfy the triangle property. Explain how its additional
    parallel rule repairs that witness. "This criterion fails" does
    not mean "the original system is nonconfluent".

    Journal reading: Rewster 2026 Definition 1 and Theorem 2 (section
    4.2) give the criterion and triangle argument for richer patterns.
    Explain the required overlap patterns, their rule priority, and
    the one-parallel-step condition. These are premises to establish
    for the intended reduction relation, not properties checked here.

    Section 4.3 then relates reduction to alpha-cumulativity and SProp
    irrelevance. Our abstract confluence theorem does not supply those
    compatibility facts. Section 9 lists formalizing the journal's
    criteria and proofs in MetaRocq as future work; do not identify
    them with the historical Taming formalization.

    Stop here to discuss the first walkthrough. study_plan.md gives
    the next phases: modularity, dependent typing, and formal artifacts.
*)