From 76f8c32dad6befa32f1a514f0b7b48ba8056cf0d Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Wed, 5 Feb 2025 21:14:31 -0500
Subject: [PATCH] Finish the hard fun case for interpuniv_join

---
 theories/logrel.v | 47 ++++++++++++++++++++++++++++-------------------
 1 file changed, 28 insertions(+), 19 deletions(-)

diff --git a/theories/logrel.v b/theories/logrel.v
index bcc06be..bb7571e 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -294,6 +294,27 @@ Proof.
   subst. hauto lq:on inv:TRedSN.
 Qed.
 
+Lemma bindspace_iff n p (PA : PTm n -> Prop) PF PF0 b  :
+  (forall (a : PTm n) (PB PB0 : PTm n -> Prop), PA a -> PF a PB -> PF0 a PB0 -> PB = PB0) ->
+  (forall a, PA a -> exists PB, PF a PB) ->
+  (forall a, PA a -> exists PB0, PF0 a PB0) ->
+  (BindSpace p PA PF b <-> BindSpace p PA PF0 b).
+Proof.
+  rewrite /BindSpace => h hPF hPF0.
+  case : p => /=.
+  - rewrite /ProdSpace.
+    split.
+    move => h1 a PB ha hPF'.
+    specialize hPF with (1 := ha).
+    specialize hPF0 with (1 := ha).
+    sblast.
+    move => ? a PB ha.
+    specialize hPF with (1 := ha).
+    specialize hPF0 with (1 := ha).
+    sblast.
+  - rewrite /SumSpace.
+    hauto lq:on rew:off.
+Qed.
 
 Lemma InterpUniv_Join n i (A B : PTm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
@@ -331,26 +352,14 @@ Proof.
     move => a PB PB' ha hPB hPB'. apply : ihPF; eauto.
     have hj0 : DJoin.R (PAbs B) (PAbs B0) by eauto using DJoin.AbsCong.
     have {}hj0 : DJoin.R (PApp (PAbs B) a) (PApp (PAbs B0) a) by eauto using DJoin.AppCong, DJoin.refl.
-    have ? : SN (PApp (PAbs B) a)
-      by hauto lq:on rew:off use:N_Exp, N_β, adequacy.
-    have ? : SN (PApp (PAbs B0) a)
-      by hauto lq:on rew:off use:N_Exp, N_β, adequacy.
-    have : DJoin.R (PApp (PAbs B0) a) (subst_PTm (scons a VarPTm) B0)
-      by hauto lq:on ctrs:RRed.R use:DJoin.FromRRed0.
-    have : DJoin.R (subst_PTm (scons a VarPTm) B) (PApp (PAbs B) a)
-      by hauto lq:on ctrs:RRed.R use:DJoin.FromRRed1.
+    have [? ?] : SN (PApp (PAbs B) a) /\ SN (PApp (PAbs B0) a) by
+      hauto lq:on rew:off use:N_Exp, N_β, adequacy.
+    have [? ?] : DJoin.R (PApp (PAbs B0) a) (subst_PTm (scons a VarPTm) B0) /\
+           DJoin.R (subst_PTm (scons a VarPTm) B) (PApp (PAbs B) a)
+      by hauto lq:on ctrs:RRed.R use:DJoin.FromRRed0, DJoin.FromRRed1.
     eauto using DJoin.transitive.
-
-    move => hI.
-    case : p0 => //=.
-    + rewrite /ProdSpace.
-      extensionality b.
-      apply propositional_extensionality.
-      split.
-      move =>  hPF a PB.
-
-      move => a PB hPB.
-
+    move => h. extensionality b. apply propositional_extensionality.
+    hauto l:on use:bindspace_iff.
   - move => i j jlti ih B PB hPB.
     have ? : SN B by hauto l:on use:adequacy.
     move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].