From 3732757abec3352a01838296c74b4e72e7d5e65b Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Sun, 12 Jan 2025 19:22:06 -0500
Subject: [PATCH] Parallelize cred

---
 theories/fp_red.v | 111 ++++++++++++++++++++++++++++------------------
 1 file changed, 69 insertions(+), 42 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 5840512..db3e761 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -378,66 +378,93 @@ Definition var_or_bot {n} (a : Tm n) :=
 Module CRed.
   Inductive R {n} : Tm n -> Tm n ->  Prop :=
   (****************** Eta ***********************)
-  | IfApp a b c d :
-    R (If (App a b) c d) (App (If a c d) b)
-  | IfProj p a b c :
-    R (If (Proj p a) b c) (Proj p (If a b c))
-
+  | IfApp a0 a1 b0 b1 c0 c1 d0 d1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R d0 d1 ->
+    R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1)
+  | IfProj p a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1))
   (*************** Congruence ********************)
+  | Var i : R (VarTm i) (VarTm i)
   | AbsCong a0 a1 :
     R a0 a1 ->
     R (Abs a0) (Abs a1)
-  | AppCong0 a0 a1 b :
+  | AppCong a0 a1 b0 b1 :
     R a0 a1 ->
-    R (App a0 b) (App a1 b)
-  | AppCong1 a b0 b1 :
     R b0 b1 ->
-    R (App a b0) (App a b1)
-  | PairCong0 a0 a1 b :
+    R (App a0 b0) (App a1 b1)
+  | PairCong a0 a1 b0 b1 :
     R a0 a1 ->
-    R (Pair a0 b) (Pair a1 b)
-  | PairCong1 a b0 b1 :
     R b0 b1 ->
-    R (Pair a b0) (Pair a b1)
+    R (Pair a0 b0) (Pair a1 b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
     R (Proj p a0) (Proj p a1)
-  | BindCong0 p A0 A1 B:
+  | BindCong p A0 A1 B0 B1:
     R A0 A1 ->
-    R (TBind p A0 B) (TBind p A1 B)
-  | BindCong1 p A B0 B1:
     R B0 B1 ->
-    R (TBind p A B0) (TBind p A B1).
+    R (TBind p A0 B0) (TBind p A1 B1)
+  | BotCong :
+    R Bot Bot
+  | UnivCong i :
+    R (Univ i) (Univ i)
+  | BoolCong :
+    R Bool Bool
+  | BValCong b :
+    R (BVal b) (BVal b)
+  | IfCong a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If a0 b0 c0) (If a1 b1 c1).
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
-  Lemma diamond n (a b c : Tm n) : R a b -> R a c -> exists d, clos_refl R b d /\ clos_refl R c d.
+  Lemma refl n (a : Tm n) : R a a.
+  Proof. elim : n / a; hauto lq:on ctrs:R. Qed.
+
+  Function tstar {n} (a : Tm n) :=
+    match a with
+    | VarTm i => a
+    | Abs a => Abs (tstar a)
+    | App a b => App (tstar a) (tstar b)
+    | Pair a b => Pair (tstar a) (tstar b)
+    | Proj p a => Proj p (tstar a)
+    | TBind p a b => TBind p (tstar a) (tstar b)
+    | Bot => Bot
+    | Univ i => Univ i
+    | Bool => Bool
+    | If (Proj p a) b c => Proj p (If (tstar a) (tstar b) (tstar c))
+    | If (App a d) b c => App (If (tstar a) (tstar b) (tstar c)) (tstar d)
+    | If a b c => If (tstar a) (tstar b) (tstar c)
+    | BVal v => BVal v
+    end.
+
+  Lemma triangle n (a : Tm n) : forall b, R a b -> R b (tstar a).
   Proof.
-    move => h. move : c. elim : n a b /h.
-    - hauto l:on ctrs:R inv:R.
-    - hauto l:on ctrs:R inv:R.
-    - move => n a0 a1 ha iha c.
-      elim /inv => //= _.
-      move => a2 a3 ha' [*]. subst.
-      apply iha in ha'.
-      move : ha' => [d [h0 h1]].
-      exists (Abs d).
-      hauto q:on ctrs:clos_refl,R inv:clos_refl.
-    - hauto q:on ctrs:clos_refl,R inv:clos_refl, R.
-    - hauto q:on ctrs:clos_refl,R inv:clos_refl, R.
-    - hauto q:on ctrs:clos_refl,R inv:clos_refl, R.
-    - hauto q:on ctrs:clos_refl,R inv:clos_refl, R.
-    - hauto q:on ctrs:clos_refl,R inv:clos_refl, R.
-    - hauto q:on ctrs:clos_refl,R inv:clos_refl, R.
-    - move => n p A B0 B1 hB ihB C.
-      elim /inv => //= _.
-      move => p0 A0 A1 B hA [*]. subst.
-      + hauto lq:on ctrs:clos_refl,R inv:clos_refl.
-      + move => p0 A0 B2 B3 h [*]. subst.
-        move /ihB : h{ihB}.
-        move => [B4 [h0 h1]].
-        exists (TBind p A B4). qauto l:on ctrs:clos_refl, R inv:clos_refl.
+    apply tstar_ind => {n a}.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on rew:off ctrs:R inv:R.
+    - hauto lq:on rew:off inv:R ctrs:R.
+    - hauto lq:on rew:off inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on ctrs:R inv:R.
+    - hauto lq:on drew:off ctrs:R inv:R.
+    - hauto lq:on drew:off ctrs:R inv:R.
   Qed.
+
+  Lemma diamond n (a b c : Tm n) : R a b -> R a c -> exists d, R b d /\ R c d.
+  Proof. sfirstorder use:triangle. Qed.
 End CRed.
 
 (***************** Beta rules only ***********************)