From a34afed3d52bbd4aa0f13621f5dfcfd18e13794c Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Wed, 25 Dec 2024 13:40:51 -0500
Subject: [PATCH] Add ERPar

---
 theories/fp_red.v | 59 +++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 54 insertions(+), 5 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index b1e17d5..0fa38aa 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -1114,11 +1114,6 @@ Proof.
   - qauto rew:db:prov.
 Qed.
 
-Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
-Proof.
-  move => h. elim : n a b /h; qauto ctrs:Par.R.
-Qed.
-
 Lemma prov_par n (A : Tm n) B a b : prov A B a -> Par.R a b -> prov A B b.
 Proof.
   move => + h. move : A B.
@@ -1199,6 +1194,60 @@ Proof.
   exists A2, B2. hauto l:on.
 Qed.
 
+Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
+Proof.
+  move => h. elim : n a b /h; qauto ctrs:Par.R.
+Qed.
+
+Lemma RPar_Par n (a b : Tm n) : RPar.R a b -> Par.R a b.
+Proof.
+  move => h. elim : n a b /h; hauto lq:on ctrs:Par.R.
+Qed.
+
+Module ERPar.
+  Inductive R {n} (a b : Tm n) : Prop :=
+  | RPar : RPar.R a b -> R a b
+  | EPar : EPar.R a b -> R a b.
+End ERPar.
+
+Lemma ERPar_Par n (a b : Tm n) : ERPar.R a b -> Par.R a b.
+Proof.
+  sfirstorder inv:ERPar.R use:EPar_Par, RPar_Par.
+Qed.
+
+Lemma Par_ERPar n (a b : Tm n) : Par.R a b -> rtc ERPar.R a b.
+Proof.
+  move => h. elim : n a b /h.
+  - move => n a0 a1 b0 b1 ha iha hb ihb.
+    apply : rtc_l. apply ERPar.RPar.
+    apply RPar.AppAbs; eauto using RPar.refl.
+    (* congruence *)
+    admit.
+  - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc.
+    apply : rtc_l. apply ERPar.RPar.
+    apply RPar.AppPair; eauto using RPar.refl.
+    admit.
+  - move => n p a0 a1 ha iha.
+    apply : rtc_l. apply ERPar.RPar. apply RPar.ProjAbs; eauto using RPar.refl.
+    admit.
+  - move => n p a0 a1 b0 b1 ha iha hb ihb.
+    apply : rtc_l. apply ERPar.RPar. apply RPar.ProjPair; eauto using RPar.refl.
+    admit.
+  - move => n a0 a1 ha iha.
+    apply : rtc_l. apply ERPar.EPar. apply EPar.AppEta; eauto using EPar.refl.
+    admit.
+  - move => n a0 a1 ha iha.
+    apply : rtc_l. apply ERPar.EPar. apply EPar.PairEta; eauto using EPar.refl.
+    admit.
+  - sfirstorder.
+  - admit.
+  - admit.
+  - admit.
+  - admit.
+  - admit.
+  - sfirstorder.
+Admitted.
+
 Lemma Par_confluent n (c a1 b1 : Tm n) :
   rtc Par.R c a1 ->
   rtc Par.R c b1 ->