From 9d3c3726dd0fb28d254963e6c3612c3e4197c9f9 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Tue, 8 Apr 2025 16:53:58 -0400
Subject: [PATCH] The proof is miserable

---
 theories/confluence.v | 58 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 57 insertions(+), 1 deletion(-)

diff --git a/theories/confluence.v b/theories/confluence.v
index 4fabdb6..7424be0 100644
--- a/theories/confluence.v
+++ b/theories/confluence.v
@@ -118,6 +118,9 @@ Module IPar.
     βηPar.R a0 a1 ->
     R (App (Abs b0) a0) (subst_Tm (scons a1 VarTm) b1).
   Derive Inversion inv with (forall a b, R a b).
+
+  Lemma ToβηPar a b : R a b -> βηPar.R a b.
+  Proof. induction 1; hauto lq:on ctrs:βηPar.R. Qed.
 End IPar.
 
 Module OExp.
@@ -125,8 +128,23 @@ Module OExp.
   | AbsEta b :
     R b (Abs (App (ren_Tm shift b) (VarTm var_zero))).
 
+  Derive Inversion inv with (forall a b, R a b).
 End OExp.
 
+Lemma βηO_commute a b c :
+  βηPar.R a b -> OExp.R a c ->
+  exists d, OExp.R b d /\ βηPar.R c d.
+Proof.
+  hauto lq:on inv:OExp.R ctrs:OExp.R,βηPar.R use:βηPar.renaming, βηPar.refl.
+Qed.
+
+Lemma βηO_commute0 a b c :
+  βηPar.R a b -> rtc OExp.R a c ->
+  exists d, rtc OExp.R b d /\ βηPar.R c d.
+Proof.
+  move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:βηO_commute.
+Qed.
+
 Lemma IO_factorization a c :
   βηPar.R a c -> exists b, IPar.R a b /\ rtc OExp.R b c.
 Proof.
@@ -158,6 +176,32 @@ Lemma IO_merge' a b c :
   βηPar.R a b -> rtc OExp.R b c -> βηPar.R a c.
 Proof. induction 2; hauto l:on use:IO_merge. Qed.
 
+
+(* Lemma AppAbsEta b0 a0 b1 a1 : *)
+(*   βηPar.R b0 (Abs b1) -> *)
+(*   βηPar.R a0 a1 -> *)
+(*   βηPar.R  *)
+
+Lemma diamond a b c : IPar.R a b  -> IPar.R a c -> exists d, IPar.R b d /\ IPar.R c d.
+Proof.
+  elim : a b c.
+  - hauto lq:on inv:IPar.R ctrs:IPar.R.
+  - move => a iha b c.
+    elim /IPar.inv => //=_.
+    move => a0 a1 + [?]?. subst.
+    move => /[swap]. elim /IPar.inv => //=_.
+    move => a0 a2 + [?]?. subst.
+    move /IO_factorization.
+    move => [a3 [h0 h1]].
+    move /IO_factorization.
+    move => [a4 [h2 h3]].
+    move : iha h0 h2. repeat move/[apply].
+    move => [d [h2 h4]].
+    move :
+
+
+
+
 Lemma diamond a b0 b1 :
   βηPar.R a b0 -> βηPar.R a b1 -> exists c, βηPar.R b0 c /\ βηPar.R b1 c.
 Proof.
@@ -176,4 +220,16 @@ Proof.
     + move => b3 b4 a2 a3 hb' ha' [*]. subst.
       have {}/ihb [b14 [ihb0 ihb1]] := hb'.
       have {}/iha [a13 [iha0 iha1]] := ha'.
-      exists (App b14 a13). split. by constructor.
+      set q := (App _ _) in h1.
+      have : βηPar.R q (App b14 a13) by constructor.
+      move : βηO_commute0 h1. subst q. repeat move/[apply].
+      move => [d [h0 h1]].
+      exists d.
+      split => //.
+      apply : IO_merge'; eauto using βηPar.AppCong.
+    + move => b3 b4 a2 a3 hb' ha' [*]. subst.
+      move /IO_factorization : hb.
+      move => [b []].
+      elim /IPar.inv => //=_ a2 b5 hb'' [?]? ho. subst.
+      move /βηPar.AbsCong : hb'. move => {}/ihb. move => [b14 [ihb0 ihb1]].
+      move : iha ha'  => /[apply]. move => [a13 [iha0 iha1]].