From 90b24b259b7e2fd1f5005cf0c78106c7a8285b5c Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Tue, 24 Dec 2024 00:52:06 -0500
Subject: [PATCH] Add confluence proof for EPar and RPar

---
 theories/fp_red.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 2ea5afd..44b7d16 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -690,3 +690,26 @@ Lemma RPar_diamond n (c a1 b1 : Tm n) :
   RPar.R c b1 ->
   exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
 Proof. hauto l:on use:RPar_triangle. Qed.
+
+Lemma RPar_confluent n (c a1 b1 : Tm n) :
+  rtc RPar.R c a1 ->
+  rtc RPar.R c b1 ->
+  exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2.
+Proof.
+  sfirstorder use:relations.diamond_confluent, RPar_diamond.
+Qed.
+
+Lemma EPar_confluent n (c a1 b1 : Tm n) :
+  rtc EPar.R c a1 ->
+  rtc EPar.R c b1 ->
+  exists d2, rtc EPar.R a1 d2 /\ rtc EPar.R b1 d2.
+Proof.
+  sfirstorder use:relations.diamond_confluent, EPar_diamond.
+Qed.
+
+Lemma Par_confluent n (c a1 b1 : Tm n) :
+  rtc Par.R c a1 ->
+  rtc Par.R c b1 ->
+  exists d2, rtc Par.R a1 d2 /\ rtc Par.R b1 d2.
+Proof.
+Admitted.