From f3718707f2b4668ee61ec48531a6576dbf29b123 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Mon, 20 Jan 2025 13:56:40 -0500
Subject: [PATCH 1/5] Add constants to the reduction semantics

---
 syntax.sig                   |   6 +-
 theories/Autosubst2/syntax.v |  29 +++---
 theories/fp_red.v            | 169 ++++++++++++-----------------------
 3 files changed, 74 insertions(+), 130 deletions(-)

diff --git a/syntax.sig b/syntax.sig
index 4549f7f..d268994 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -3,14 +3,14 @@ Tm(VarTm) : Type
 PTag : Type
 TTag : Type
 
-TPi : TTag
-TSig : TTag
 PL : PTag
 PR : PTag
+TPi : TTag
+TSig : TTag
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
-Bot : Tm
+Const : TTag -> Tm
 Univ : nat -> Tm
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index b972476..05fb668 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -40,7 +40,7 @@ Inductive Tm (n_Tm : nat) : Type :=
   | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
   | Proj : PTag -> Tm n_Tm -> Tm n_Tm
   | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm
-  | Bot : Tm n_Tm
+  | Const : TTag -> Tm n_Tm
   | Univ : nat -> Tm n_Tm.
 
 Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)}
@@ -83,9 +83,10 @@ exact (eq_trans
          (ap (fun x => TBind m_Tm t0 t1 x) H2)).
 Qed.
 
-Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm.
+Lemma congr_Const {m_Tm : nat} {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) :
+  Const m_Tm s0 = Const m_Tm t0.
 Proof.
-exact (eq_refl).
+exact (eq_trans eq_refl (ap (fun x => Const m_Tm x) H0)).
 Qed.
 
 Lemma congr_Univ {m_Tm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
@@ -116,7 +117,7 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | Proj _ s0 s1 => Proj n_Tm s0 (ren_Tm xi_Tm s1)
   | TBind _ s0 s1 s2 =>
       TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2)
-  | Bot _ => Bot n_Tm
+  | Const _ s0 => Const n_Tm s0
   | Univ _ s0 => Univ n_Tm s0
   end.
 
@@ -143,7 +144,7 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
   | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1)
   | TBind _ s0 s1 s2 =>
       TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2)
-  | Bot _ => Bot n_Tm
+  | Const _ s0 => Const n_Tm s0
   | Univ _ s0 => Univ n_Tm s0
   end.
 
@@ -183,7 +184,7 @@ subst_Tm sigma_Tm s = s :=
   | TBind _ s0 s1 s2 =>
       congr_TBind (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
         (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -227,7 +228,7 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
       congr_TBind (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
         (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
            (upExtRen_Tm_Tm _ _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -272,7 +273,7 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
       congr_TBind (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
         (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
            s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -317,7 +318,7 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
       congr_TBind (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
         (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
            (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -373,7 +374,7 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
         (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
         (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
            (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -450,7 +451,7 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
         (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
         (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
            (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -528,7 +529,7 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
         (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
         (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
            (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -644,7 +645,7 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
       congr_TBind (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
         (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
            (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2)
-  | Bot _ => congr_Bot
+  | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
@@ -846,7 +847,7 @@ Arguments VarTm {n_Tm}.
 
 Arguments Univ {n_Tm}.
 
-Arguments Bot {n_Tm}.
+Arguments Const {n_Tm}.
 
 Arguments TBind {n_Tm}.
 
diff --git a/theories/fp_red.v b/theories/fp_red.v
index d2fbdf6..30f3354 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -69,9 +69,8 @@ Module Par.
     R A0 A1 ->
     R B0 B1 ->
     R (TBind p A0 B0) (TBind p A1 B1)
-  (* Bot is useful for making the prov function computable  *)
-  | BotCong :
-    R Bot Bot
+  | ConstCong k :
+    R (Const k) (Const k)
   | UnivCong i :
     R (Univ i) (Univ i).
 
@@ -212,7 +211,7 @@ Module Par.
       move : ihB => [c0 [? ?]]. subst.
       eexists. split. by apply BindCong; eauto.
       by asimpl.
-    - move => n n0 ξ []//=. hauto l:on.
+    - move => n k m ξ []//=. hauto l:on.
     - move => n i n0 ξ []//=. hauto l:on.
   Qed.
 
@@ -275,10 +274,10 @@ Module Pars.
 
 End Pars.
 
-Definition var_or_bot {n} (a : Tm n) :=
+Definition var_or_const {n} (a : Tm n) :=
   match a with
   | VarTm _ => true
-  | Bot => true
+  | Const _ => true
   | _ => false
   end.
 
@@ -324,8 +323,8 @@ Module RPar.
     R A0 A1 ->
     R B0 B1 ->
     R (TBind p A0 B0) (TBind p A1 B1)
-  | BotCong :
-    R Bot Bot
+  | ConstCong k :
+    R (Const k) (Const k)
   | UnivCong i :
     R (Univ i) (Univ i).
 
@@ -571,8 +570,8 @@ Module RPar'.
     R A0 A1 ->
     R B0 B1 ->
     R (TBind p A0 B0) (TBind p A1 B1)
-  | BotCong :
-    R Bot Bot
+  | ConstCong k :
+    R (Const k) (Const k)
   | UnivCong i :
     R (Univ i) (Univ i).
 
@@ -656,16 +655,16 @@ Module RPar'.
     qauto l:on ctrs:R inv:option.
   Qed.
 
-  Lemma var_or_bot_imp {n} (a b : Tm n) :
-    var_or_bot a ->
-    a = b -> ~~ var_or_bot b -> False.
+  Lemma var_or_const_imp {n} (a b : Tm n) :
+    var_or_const a ->
+    a = b -> ~~ var_or_const b -> False.
   Proof.
     hauto lq:on inv:Tm.
   Qed.
 
-  Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
-    (forall i, var_or_bot (up_Tm_Tm ρ i)).
+  Lemma var_or_const_up n m (ρ : fin n -> Tm m) :
+    (forall i, var_or_const (ρ i)) ->
+    (forall i, var_or_const (up_Tm_Tm ρ i)).
   Proof.
     move => h /= [i|].
     - asimpl.
@@ -676,10 +675,10 @@ Module RPar'.
     - sfirstorder.
   Qed.
 
-  Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
+  Local Ltac antiimp := qauto l:on use:var_or_const_imp.
 
   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_const (ρ i)) ->
     R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
   Proof.
     move E : (subst_Tm ρ a) => u hρ h.
@@ -690,7 +689,7 @@ Module RPar'.
       case : c => //=; first by antiimp.
       move => c [?]. subst.
       spec_refl.
-      have /var_or_bot_up hρ' := hρ.
+      have /var_or_const_up hρ' := hρ.
       move : iha hρ' => /[apply] iha.
       move : ihb hρ => /[apply] ihb.
       spec_refl.
@@ -714,7 +713,7 @@ Module RPar'.
       hauto l:on.
     - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
       move => t [*]. subst.
-      have /var_or_bot_up {}/iha := hρ => iha.
+      have /var_or_const_up {}/iha := hρ => iha.
       spec_refl.
       move  :iha => [b0 [? ?]]. subst.
       eexists. split. by apply AbsCong; eauto.
@@ -750,7 +749,7 @@ Module RPar'.
                first by antiimp.
       move => ? t t0 [*]. subst.
       have {}/iha := (hρ) => iha.
-      have /var_or_bot_up {}/ihB := (hρ) => ihB.
+      have /var_or_const_up {}/ihB := (hρ) => ihB.
       spec_refl.
       move : iha => [b0 [? ?]].
       move : ihB => [c0 [? ?]]. subst.
@@ -894,8 +893,8 @@ Module EPar.
     R A0 A1 ->
     R B0 B1 ->
     R (TBind p A0 B0) (TBind p A1 B1)
-  | BotCong :
-    R Bot Bot
+  | ConstCong k :
+    R (Const k) (Const k)
   | UnivCong i :
     R (Univ i) (Univ i).
 
@@ -1070,7 +1069,7 @@ Module RPars.
   Proof. hauto lq:on use:morphing inv:option. Qed.
 
   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_const (ρ i)) ->
     rtc RPar.R (subst_Tm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_Tm ρ b0 = b.
   Proof.
     move E  :(subst_Tm ρ a) => u hρ h.
@@ -1157,7 +1156,7 @@ Module RPars'.
   Proof. hauto lq:on use:morphing inv:option. Qed.
 
   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_const (ρ i)) ->
     rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b.
   Proof.
     move E  :(subst_Tm ρ a) => u hρ h.
@@ -1444,15 +1443,15 @@ Proof.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma Bot_EPar' n (u : Tm n) :
-  EPar.R Bot u ->
-  rtc OExp.R Bot u.
-  move E : Bot => t h.
-  move : E. elim : n t u /h => //=.
-  - move => n a0 a1 h ih ?. subst.
+Lemma Const_EPar' n k (u : Tm n) :
+  EPar.R (Const k) u ->
+  rtc OExp.R (Const k) u.
+  move E : (Const k) => t h.
+  move : k E. elim : n t u /h => //=.
+  - move => n a0 a1 h ih k ?. subst.
     specialize ih with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => n a0 a1 h ih ?. subst.
+  - move => n a0 a1 h ih k ?. subst.
     specialize ih with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
   - hauto l:on ctrs:OExp.R.
@@ -1519,7 +1518,7 @@ Proof.
     move : OExp.commutativity0 h2; repeat move/[apply].
     move => [d h].
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
-  - qauto use:Bot_EPar', EPar.refl.
+  - qauto use:Const_EPar', EPar.refl.
   - qauto use:Univ_EPar', EPar.refl.
 Qed.
 
@@ -1536,7 +1535,7 @@ Function tstar {n} (a : Tm n) :=
   | Proj p (Abs a) => (Abs (Proj p (tstar a)))
   | Proj p a => Proj p (tstar a)
   | TBind p a b => TBind p (tstar a) (tstar b)
-  | Bot => Bot
+  | Const k => Const k
   | Univ i => Univ i
   end.
 
@@ -1568,7 +1567,7 @@ Function tstar' {n} (a : Tm n) :=
   | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b)
   | Proj p a => Proj p (tstar' a)
   | TBind p a b => TBind p (tstar' a) (tstar' b)
-  | Bot => Bot
+  | Const k => Const k
   | Univ i => Univ i
   end.
 
@@ -1616,63 +1615,6 @@ Proof.
   sfirstorder use:relations.diamond_confluent, EPar_diamond.
 Qed.
 
-Fixpoint depth_tm {n} (a : Tm n) :=
-  match a with
-  | VarTm _ => 1
-  | TBind _ A B => 1 + max (depth_tm A) (depth_tm B)
-  | Abs a => 1 + depth_tm a
-  | App a b => 1 + max (depth_tm a) (depth_tm b)
-  | Proj p a => 1 + depth_tm a
-  | Pair a b => 1 + max (depth_tm a) (depth_tm b)
-  | Bot => 1
-  | Univ i => 1
-  end.
-
-Lemma depth_ren n m (ξ: fin n -> fin m) a :
-  depth_tm a = depth_tm (ren_Tm ξ a).
-Proof.
-  move : m ξ. elim : n / a; scongruence.
-Qed.
-
-Lemma depth_subst n m (ρ : fin n -> Tm m) a :
-  (forall i, depth_tm (ρ i) = 1) ->
-  depth_tm a = depth_tm (subst_Tm ρ a).
-Proof.
-  move : m ρ. elim : n / a.
-  - sfirstorder.
-  - move => n a iha m ρ hρ.
-    simpl.
-    f_equal. apply iha.
-    destruct i as [i|].
-    + simpl.
-      by rewrite -depth_ren.
-    + by simpl.
-  - hauto lq:on rew:off.
-  - hauto lq:on rew:off.
-  - hauto lq:on rew:off.
-  - move => n p a iha b ihb m ρ hρ.
-    simpl. f_equal.
-    f_equal.
-    by apply iha.
-    apply ihb.
-    destruct i as [i|].
-    + simpl.
-      by rewrite -depth_ren.
-    + by simpl.
-  - sfirstorder.
-  - sfirstorder.
-Qed.
-
-Lemma depth_subst_bool n (a : Tm (S n)) :
-  depth_tm a = depth_tm (subst_Tm (scons Bot VarTm) a).
-Proof.
-  apply depth_subst.
-  destruct i as [i|] => //=.
-Qed.
-
-Local Ltac prov_tac := sfirstorder use:depth_ren.
-Local Ltac extract_tac := rewrite -?depth_subst_bool;hauto use:depth_subst_bool.
-
 Definition prov_bind {n} p0 A0 B0 (a : Tm n)  :=
   match a with
   | TBind p A B => p = p0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
@@ -1704,8 +1646,8 @@ Inductive prov {n} : Tm n -> Tm n -> Prop :=
 | P_Proj h p a :
   prov h a ->
   prov h (Proj p a)
-| P_Bot  :
-  prov Bot Bot
+| P_Const k  :
+  prov (Const k) (Const k)
 | P_Var i :
   prov (VarTm i) (VarTm i)
 | P_Univ i :
@@ -1789,7 +1731,7 @@ Proof.
   split.
   move => h. constructor. move => b. asimpl. by constructor.
   inversion 1; subst.
-  specialize H2 with (b := Bot).
+  specialize H2 with (b := Const TPi).
   move : H2. asimpl. inversion 1; subst. done.
 Qed.
 
@@ -1845,11 +1787,11 @@ Qed.
 Fixpoint extract {n} (a : Tm n) : Tm n :=
   match a with
   | TBind p A B => TBind p A B
-  | Abs a => subst_Tm (scons Bot VarTm) (extract a)
+  | Abs a => subst_Tm (scons (Const TPi) VarTm) (extract a)
   | App a b => extract a
   | Pair a b => extract a
   | Proj p a => extract a
-  | Bot => Bot
+  | Const k => Const k
   | VarTm i => VarTm i
   | Univ i => Univ i
   end.
@@ -1886,7 +1828,7 @@ Proof.
 Qed.
 
 Lemma ren_subst_bot n (a : Tm (S n)) :
-  extract (subst_Tm (scons Bot VarTm) a) = subst_Tm (scons Bot VarTm) (extract a).
+  extract (subst_Tm (scons (Const TPi) VarTm) a) = subst_Tm (scons (Const TPi) VarTm) (extract a).
 Proof.
   apply ren_morphing. destruct i as [i|] => //=.
 Qed.
@@ -1896,7 +1838,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
   | TBind p A B => exists A0 B0, extract a = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
   | Univ i => extract a = Univ i
   | VarTm i => extract a = VarTm i
-  | Bot => extract a = Bot
+  | (Const TPi) => extract a = (Const TPi)
   | _ => True
   end.
 
@@ -1909,22 +1851,22 @@ Proof.
   - move => h a ha ih.
     case : h ha ih => //=.
     + move => i ha ih.
-      move /(_ Bot) in ih.
+      move /(_ (Const TPi)) in ih.
       rewrite -ih.
       by rewrite ren_subst_bot.
     + move => p A B h ih.
-      move /(_ Bot) : ih => [A0][B0][h0][h1]h2.
+      move /(_ (Const TPi)) : ih => [A0][B0][h0][h1]h2.
       rewrite ren_subst_bot in h0.
       rewrite h0.
       eauto.
-    + move => _ /(_ Bot).
+    + move => p _ /(_ (Const TPi)).
       by rewrite ren_subst_bot.
-    + move => i h /(_ Bot).
+    + move => i h /(_ (Const TPi)).
       by rewrite ren_subst_bot => ->.
   - hauto lq:on.
   - hauto lq:on.
   - hauto lq:on.
-  - sfirstorder.
+  - case => //=.
   - sfirstorder.
   - sfirstorder.
 Qed.
@@ -2400,23 +2342,24 @@ Fixpoint ne {n} (a : Tm n) :=
   match a with
   | VarTm i => true
   | TBind _ A B => false
-  | Bot => true
   | App a b => ne a && nf b
   | Abs a => false
   | Univ _ => false
   | Proj _ a => ne a
   | Pair _ _ => false
+  | Const _ => false
   end
 with nf {n} (a : Tm n) :=
   match a with
   | VarTm i => true
   | TBind _ A B => nf A && nf B
-  | Bot => true
+  | (Const TPi) => true
   | App a b => ne a && nf b
   | Abs a => nf a
   | Univ _ => true
   | Proj _ a => ne a
   | Pair a b => nf a && nf b
+  | Const _ => true
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -2482,15 +2425,15 @@ Create HintDb nfne.
 #[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne.
 
 Lemma ne_nf_antiren n m (a : Tm n) (ρ : fin n -> Tm m) :
-  (forall i, var_or_bot (ρ i)) ->
+  (forall i, var_or_const (ρ i)) ->
   (ne (subst_Tm ρ a) -> ne a) /\ (nf (subst_Tm ρ a) -> nf a).
 Proof.
   move : m ρ. elim : n / a => //;
-   hauto b:on drew:off use:RPar.var_or_bot_up.
+   hauto b:on drew:off use:RPar.var_or_const_up.
 Qed.
 
 Lemma wn_antirenaming n m a (ρ : fin n -> Tm m) :
-  (forall i, var_or_bot (ρ i)) ->
+  (forall i, var_or_const (ρ i)) ->
   wn (subst_Tm ρ a) -> wn a.
 Proof.
   rewrite /wn => hρ.
@@ -2503,10 +2446,10 @@ Proof.
 Qed.
 
 Lemma ext_wn n (a : Tm n) :
-    wn (App a Bot) ->
+    wn (App a (Const TPi)) ->
     wn a.
 Proof.
-  move E : (App a Bot) => a0 [v [hr hv]].
+  move E : (App a (Const TPi)) => a0 [v [hr hv]].
   move : a E.
   move : hv.
   elim : a0 v / hr.
@@ -2517,9 +2460,9 @@ Proof.
     case : a0 hr0=>// => b0 b1.
     elim /RPar'.inv=>// _.
     + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
-      have ? : b3 = Bot by hauto lq:on inv:RPar'.R. subst.
+      have ? : b3 = (Const TPi) by hauto lq:on inv:RPar'.R. subst.
       suff : wn (Abs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
-      have : wn (subst_Tm (scons Bot VarTm) a3) by sfirstorder.
+      have : wn (subst_Tm (scons (Const TPi) VarTm) a3) by sfirstorder.
       move => h. apply wn_abs.
       move : h. apply wn_antirenaming.
       hauto lq:on rew:off inv:option.

From d68df5d0bc84617900727ed91a1948c360ec066b Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Mon, 20 Jan 2025 15:33:46 -0500
Subject: [PATCH 2/5] Add compile

---
 theories/compile.v | 136 +++++++++++++++++++++++++++++++++++++++++++++
 theories/fp_red.v  |  49 +++++++++++-----
 2 files changed, 172 insertions(+), 13 deletions(-)
 create mode 100644 theories/compile.v

diff --git a/theories/compile.v b/theories/compile.v
new file mode 100644
index 0000000..d9d6ca3
--- /dev/null
+++ b/theories/compile.v
@@ -0,0 +1,136 @@
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
+Require Import ssreflect ssrbool.
+From Hammer Require Import Tactics.
+
+Module Compile.
+  Fixpoint F {n} (a : Tm n) : Tm n :=
+    match a with
+    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
+    | Const k => Const k
+    | Univ i => Univ i
+    | Abs a => Abs (F a)
+    | App a b => App (F a) (F b)
+    | VarTm i => VarTm i
+    | Pair a b => Pair (F a) (F b)
+    | Proj t a => Proj t (F a)
+    end.
+
+  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
+    F (ren_Tm ξ a)= ren_Tm ξ (F a).
+  Proof. move : m ξ. elim : n  / a => //=; scongruence. Qed.
+
+  #[local]Hint Rewrite Compile.renaming : compile.
+
+  Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
+    (forall i, ρ0 i = F (ρ1 i)) ->
+    subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a).
+  Proof.
+    move : m ρ0 ρ1. elim : n / a => n//=.
+    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    - hauto lq:on rew:off.
+    - hauto lq:on rew:off.
+    - hauto lq:on.
+    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+  Qed.
+
+  Lemma substing n b (a : Tm (S n)) :
+    subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a).
+  Proof.
+    apply morphing.
+    case => //=.
+  Qed.
+
+End Compile.
+
+#[export] Hint Rewrite Compile.renaming Compile.morphing : compile.
+
+
+Module Join.
+  Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).
+
+  Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1  :
+    R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
+  Proof.
+    rewrite /R /= !join_pair_inj.
+    move => [[/join_const_inj h0 h1] h2].
+    apply abs_eq in h2.
+    evar (t : Tm (S n)).
+    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
+      apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
+    subst t. rewrite -/ren_Tm.
+    move : h2. move /join_transitive => /[apply]. asimpl => h2.
+    tauto.
+  Qed.
+
+  Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
+  Proof. hauto l:on use:join_univ_inj. Qed.
+
+End Join.
+
+Module Equiv.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (***************** Beta ***********************)
+  | AppAbs a b :
+    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
+  | ProjPair p a b :
+    R (Proj p (Pair a b)) (if p is PL then a else b)
+
+  (****************** Eta ***********************)
+  | AppEta a :
+    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
+  | PairEta a :
+    R a (Pair (Proj PL a) (Proj PR a))
+
+  (*************** Congruence ********************)
+  | Var i : R (VarTm i) (VarTm i)
+  | AbsCong a b :
+    R a b ->
+    R (Abs a) (Abs b)
+  | AppCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App a0 b0) (App a1 b1)
+  | PairCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Pair a0 b0) (Pair a1 b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (Proj p a0) (Proj p a1)
+  | BindCong p A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (TBind p A0 B0) (TBind p A1 B1)
+  | UnivCong i :
+    R (Univ i) (Univ i).
+End Equiv.
+
+Module EquivJoin.
+  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
+  Proof.
+    move => h. elim : n a b /h => n.
+    - move => a b.
+      rewrite /Join.R /join /=.
+      eexists. split. apply relations.rtc_once.
+      apply Par.AppAbs; auto using Par.refl.
+      rewrite Compile.substing.
+      apply relations.rtc_refl.
+    - move => p a b.
+      apply Join.FromPar.
+      simpl. apply : Par.ProjPair'; auto using Par.refl.
+      case : p => //=.
+    - move => a. apply Join.FromPar => /=.
+      apply : Par.AppEta'; auto using Par.refl.
+      by autorewrite with compile.
+    - move => a. apply Join.FromPar => /=.
+      apply : Par.PairEta; auto using Par.refl.
+    - hauto l:on use:Join.FromPar, Par.Var.
+    - hauto lq:on use:Join.AbsCong.
+    - qauto l:on use:Join.AppCong.
+    - qauto l:on use:Join.PairCong.
+    - qauto use:Join.ProjCong.
+    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
+      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
+    - hauto l:on.
+  Qed.
+End EquivJoin.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index 30f3354..adb05ea 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -410,16 +410,16 @@ Module RPar.
     qauto l:on ctrs:R inv:option.
   Qed.
 
-  Lemma var_or_bot_imp {n} (a b : Tm n) :
-    var_or_bot a ->
-    a = b -> ~~ var_or_bot b -> False.
+  Lemma var_or_const_imp {n} (a b : Tm n) :
+    var_or_const a ->
+    a = b -> ~~ var_or_const b -> False.
   Proof.
     hauto lq:on inv:Tm.
   Qed.
 
-  Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
-    (forall i, var_or_bot (up_Tm_Tm ρ i)).
+  Lemma var_or_const_up n m (ρ : fin n -> Tm m) :
+    (forall i, var_or_const (ρ i)) ->
+    (forall i, var_or_const (up_Tm_Tm ρ i)).
   Proof.
     move => h /= [i|].
     - asimpl.
@@ -430,10 +430,10 @@ Module RPar.
     - sfirstorder.
   Qed.
 
-  Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
+  Local Ltac antiimp := qauto l:on use:var_or_const_imp.
 
   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_const (ρ i)) ->
     R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
   Proof.
     move E : (subst_Tm ρ a) => u hρ h.
@@ -444,7 +444,7 @@ Module RPar.
       case : c => //=; first by antiimp.
       move => c [?]. subst.
       spec_refl.
-      have /var_or_bot_up hρ' := hρ.
+      have /var_or_const_up hρ' := hρ.
       move : iha hρ' => /[apply] iha.
       move : ihb hρ => /[apply] ihb.
       spec_refl.
@@ -470,7 +470,7 @@ Module RPar.
     - move => n p a0 a1 ha iha m ρ hρ []//=;
                first by antiimp.
       move => p0 []//= t [*]; first by antiimp. subst.
-      have  /var_or_bot_up {}/iha  := hρ => iha.
+      have  /var_or_const_up {}/iha  := hρ => iha.
       spec_refl. move : iha => [b0 [? ?]]. subst.
       eexists. split. apply ProjAbs; eauto. by asimpl.
     - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
@@ -488,7 +488,7 @@ Module RPar.
       hauto l:on.
     - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
       move => t [*]. subst.
-      have /var_or_bot_up {}/iha := hρ => iha.
+      have /var_or_const_up {}/iha := hρ => iha.
       spec_refl.
       move  :iha => [b0 [? ?]]. subst.
       eexists. split. by apply AbsCong; eauto.
@@ -524,7 +524,7 @@ Module RPar.
                first by antiimp.
       move => ? t t0 [*]. subst.
       have {}/iha := (hρ) => iha.
-      have /var_or_bot_up {}/ihB := (hρ) => ihB.
+      have /var_or_const_up {}/ihB := (hρ) => ihB.
       spec_refl.
       move : iha => [b0 [? ?]].
       move : ihB => [c0 [? ?]]. subst.
@@ -1838,7 +1838,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
   | TBind p A B => exists A0 B0, extract a = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
   | Univ i => extract a = Univ i
   | VarTm i => extract a = VarTm i
-  | (Const TPi) => extract a = (Const TPi)
+  | (Const i) => extract a = (Const i)
   | _ => True
   end.
 
@@ -2250,6 +2250,15 @@ Proof.
   apply prov_extract.
 Qed.
 
+Lemma pars_const_inv n i (c : Tm n) :
+  rtc Par.R (Const i) c ->
+  extract c = Const i.
+Proof.
+  have : prov (Const i) (Const i : Tm n) by sfirstorder.
+  move : prov_pars. repeat move/[apply].
+  apply prov_extract.
+Qed.
+
 Lemma pars_pi_inv n p (A : Tm n) B C :
   rtc Par.R (TBind p A B) C ->
   exists A0 B0, extract C = TBind p A0 B0 /\
@@ -2277,6 +2286,14 @@ Proof.
   sauto l:on use:pars_univ_inv.
 Qed.
 
+Lemma pars_const_inj n i j (C : Tm n) :
+  rtc Par.R (Const i) C ->
+  rtc Par.R (Const j) C ->
+  i = j.
+Proof.
+  sauto l:on use:pars_const_inv.
+Qed.
+
 Lemma pars_pi_inj n p0 p1 (A0 A1 : Tm n) B0 B1 C :
   rtc Par.R (TBind p0 A0 B0) C ->
   rtc Par.R (TBind p1 A1 B1) C ->
@@ -2314,6 +2331,12 @@ Proof.
   sfirstorder use:pars_univ_inj.
 Qed.
 
+Lemma join_const_inj n i j :
+  join (Const i : Tm n) (Const j) -> i = j.
+Proof.
+  sfirstorder use:pars_const_inj.
+Qed.
+
 Lemma join_pi_inj n p0 p1 (A0 A1 : Tm n) B0 B1 :
   join (TBind p0 A0 B0) (TBind p1 A1 B1) ->
   p0 = p1 /\ join A0 A1 /\ join B0 B1.

From 9c9ce52b63ed216299646e519e38dfb419b31ed7 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Mon, 20 Jan 2025 16:28:44 -0500
Subject: [PATCH 3/5] Recover the contra lemmas

---
 syntax.sig                   |  1 +
 theories/Autosubst2/syntax.v | 20 ++++++++-
 theories/compile.v           |  1 +
 theories/fp_red.v            | 83 ++++++++++++++++++++++++++++--------
 theories/logrel.v            | 33 +++++++++-----
 5 files changed, 110 insertions(+), 28 deletions(-)

diff --git a/syntax.sig b/syntax.sig
index d268994..3101cab 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -14,3 +14,4 @@ Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
 Const : TTag -> Tm
 Univ : nat -> Tm
+Bot : Tm
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index 05fb668..a5cb002 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -41,7 +41,8 @@ Inductive Tm (n_Tm : nat) : Type :=
   | Proj : PTag -> Tm n_Tm -> Tm n_Tm
   | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm
   | Const : TTag -> Tm n_Tm
-  | Univ : nat -> Tm n_Tm.
+  | Univ : nat -> Tm n_Tm
+  | Bot : Tm n_Tm.
 
 Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)}
   (H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0.
@@ -95,6 +96,11 @@ Proof.
 exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)).
 Qed.
 
+Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm.
+Proof.
+exact (eq_refl).
+Qed.
+
 Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -119,6 +125,7 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
       TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2)
   | Const _ s0 => Const n_Tm s0
   | Univ _ s0 => Univ n_Tm s0
+  | Bot _ => Bot n_Tm
   end.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -146,6 +153,7 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
       TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2)
   | Const _ s0 => Const n_Tm s0
   | Univ _ s0 => Univ n_Tm s0
+  | Bot _ => Bot n_Tm
   end.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -186,6 +194,7 @@ subst_Tm sigma_Tm s = s :=
         (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -230,6 +239,7 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
            (upExtRen_Tm_Tm _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -275,6 +285,7 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
            s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -320,6 +331,7 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
            (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -376,6 +388,7 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
            (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -453,6 +466,7 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
            (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -531,6 +545,7 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
            (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -647,6 +662,7 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
            (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -845,6 +861,8 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
+Arguments Bot {n_Tm}.
+
 Arguments Univ {n_Tm}.
 
 Arguments Const {n_Tm}.
diff --git a/theories/compile.v b/theories/compile.v
index d9d6ca3..3eaaf42 100644
--- a/theories/compile.v
+++ b/theories/compile.v
@@ -13,6 +13,7 @@ Module Compile.
     | VarTm i => VarTm i
     | Pair a b => Pair (F a) (F b)
     | Proj t a => Proj t (F a)
+    | Bot => Bot
     end.
 
   Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
diff --git a/theories/fp_red.v b/theories/fp_red.v
index adb05ea..6932f84 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -72,7 +72,9 @@ Module Par.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Lemma refl n (a : Tm n) : R a a.
     elim : n /a; hauto ctrs:R.
@@ -134,6 +136,7 @@ Module Par.
     - hauto l:on inv:option ctrs:R use:renaming.
     - sfirstorder.
     - sfirstorder.
+    - sfirstorder.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -213,6 +216,7 @@ Module Par.
       by asimpl.
     - move => n k m ξ []//=. hauto l:on.
     - move => n i n0 ξ []//=. hauto l:on.
+    - hauto q:on inv:Tm ctrs:R.
   Qed.
 
 End Par.
@@ -277,7 +281,7 @@ End Pars.
 Definition var_or_const {n} (a : Tm n) :=
   match a with
   | VarTm _ => true
-  | Const _ => true
+  | Bot => true
   | _ => false
   end.
 
@@ -326,7 +330,9 @@ Module RPar.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -394,6 +400,7 @@ Module RPar.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -533,6 +540,7 @@ Module RPar.
     - hauto q:on ctrs:R inv:Tm.
     - move => n i n0 ρ hρ []//=; first by antiimp.
       hauto l:on.
+    - move => n m ρ hρ []//=; hauto lq:on ctrs:R.
   Qed.
 End RPar.
 
@@ -573,7 +581,9 @@ Module RPar'.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -639,6 +649,7 @@ Module RPar'.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -758,6 +769,7 @@ Module RPar'.
     - hauto q:on ctrs:R inv:Tm.
     - move => n i n0 ρ hρ []//=; first by antiimp.
       hauto l:on.
+    - hauto q:on inv:Tm ctrs:R.
   Qed.
 End RPar'.
 
@@ -896,7 +908,9 @@ Module EPar.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Lemma refl n (a : Tm n) : EPar.R a a.
   Proof.
@@ -941,6 +955,7 @@ Module EPar.
     - hauto l:on ctrs:R use:renaming inv:option.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n a0 a1 (b0 b1 : Tm n) :
@@ -1344,6 +1359,7 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong.
   - hauto l:on ctrs:EPar.R inv:RPar.R.
   - hauto l:on ctrs:EPar.R inv:RPar.R.
+  - hauto l:on ctrs:EPar.R inv:RPar.R.
 Qed.
 
 Lemma commutativity1 n (a b0 b1 : Tm n) :
@@ -1457,6 +1473,20 @@ Lemma Const_EPar' n k (u : Tm n) :
   - hauto l:on ctrs:OExp.R.
 Qed.
 
+Lemma Bot_EPar' n (u : Tm n) :
+  EPar.R (Bot) u ->
+  rtc OExp.R (Bot) u.
+  move E : (Bot) => t h.
+  move : E. elim : n t u /h => //=.
+  - move => n a0 a1 h ih ?. subst.
+    specialize ih with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - move => n a0 a1 h ih ?. subst.
+    specialize ih with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - hauto l:on ctrs:OExp.R.
+Qed.
+
 Lemma Univ_EPar' n i (u : Tm n) :
   EPar.R (Univ i) u ->
   rtc OExp.R (Univ i) u.
@@ -1520,6 +1550,7 @@ Proof.
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
   - qauto use:Const_EPar', EPar.refl.
   - qauto use:Univ_EPar', EPar.refl.
+  - qauto use:Bot_EPar', EPar.refl.
 Qed.
 
 Function tstar {n} (a : Tm n) :=
@@ -1537,6 +1568,7 @@ Function tstar {n} (a : Tm n) :=
   | TBind p a b => TBind p (tstar a) (tstar b)
   | Const k => Const k
   | Univ i => Univ i
+  | Bot => Bot
   end.
 
 Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
@@ -1555,6 +1587,7 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
+  - hauto lq:on inv:RPar.R ctrs:RPar.R.
 Qed.
 
 Function tstar' {n} (a : Tm n) :=
@@ -1569,6 +1602,7 @@ Function tstar' {n} (a : Tm n) :=
   | TBind p a b => TBind p (tstar' a) (tstar' b)
   | Const k => Const k
   | Univ i => Univ i
+  | Bot => Bot
   end.
 
 Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
@@ -1585,6 +1619,7 @@ Proof.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
 Qed.
 
 Lemma RPar_diamond n (c a1 b1 : Tm n) :
@@ -1651,7 +1686,9 @@ Inductive prov {n} : Tm n -> Tm n -> Prop :=
 | P_Var i :
   prov (VarTm i) (VarTm i)
 | P_Univ i :
-  prov (Univ i) (Univ i).
+  prov (Univ i) (Univ i)
+| P_Bot :
+  prov Bot Bot.
 
 Lemma ERed_EPar n (a b : Tm n) : ERed.R a b -> EPar.R a b.
 Proof.
@@ -1671,6 +1708,7 @@ Proof.
   - eauto using EReds.BindCong.
   - auto using rtc_refl.
   - auto using rtc_refl.
+  - auto using rtc_refl.
 Qed.
 
 Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
@@ -1723,6 +1761,7 @@ Proof.
   - hauto lq:on ctrs:prov inv:RPar.R.
   - hauto l:on ctrs:RPar.R inv:RPar.R.
   - hauto l:on ctrs:RPar.R inv:RPar.R.
+  - hauto l:on ctrs:RPar.R inv:RPar.R.
 Qed.
 
 
@@ -1777,6 +1816,7 @@ Proof.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
+  - hauto lq:on inv:ERed.R, prov ctrs:prov.
 Qed.
 
 Lemma prov_ereds n (u : Tm n) a b : prov u a -> rtc ERed.R a b -> prov u b.
@@ -1787,13 +1827,14 @@ Qed.
 Fixpoint extract {n} (a : Tm n) : Tm n :=
   match a with
   | TBind p A B => TBind p A B
-  | Abs a => subst_Tm (scons (Const TPi) VarTm) (extract a)
+  | Abs a => subst_Tm (scons Bot VarTm) (extract a)
   | App a b => extract a
   | Pair a b => extract a
   | Proj p a => extract a
   | Const k => Const k
   | VarTm i => VarTm i
   | Univ i => Univ i
+  | Bot => Bot
   end.
 
 Lemma ren_extract n m (a : Tm n) (ξ : fin n -> fin m) :
@@ -1810,6 +1851,7 @@ Proof.
   - hauto q:on.
   - sfirstorder.
   - sfirstorder.
+  - sfirstorder.
 Qed.
 
 Lemma ren_morphing n m (a : Tm n) (ρ : fin n -> Tm m) :
@@ -1828,7 +1870,7 @@ Proof.
 Qed.
 
 Lemma ren_subst_bot n (a : Tm (S n)) :
-  extract (subst_Tm (scons (Const TPi) VarTm) a) = subst_Tm (scons (Const TPi) VarTm) (extract a).
+  extract (subst_Tm (scons Bot VarTm) a) = subst_Tm (scons Bot VarTm) (extract a).
 Proof.
   apply ren_morphing. destruct i as [i|] => //=.
 Qed.
@@ -1839,6 +1881,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
   | Univ i => extract a = Univ i
   | VarTm i => extract a = VarTm i
   | (Const i) => extract a = (Const i)
+  | Bot => extract a = Bot
   | _ => True
   end.
 
@@ -1851,24 +1894,28 @@ Proof.
   - move => h a ha ih.
     case : h ha ih => //=.
     + move => i ha ih.
-      move /(_ (Const TPi)) in ih.
+      move /(_ Bot) in ih.
       rewrite -ih.
       by rewrite ren_subst_bot.
     + move => p A B h ih.
-      move /(_ (Const TPi)) : ih => [A0][B0][h0][h1]h2.
+      move /(_ Bot) : ih => [A0][B0][h0][h1]h2.
       rewrite ren_subst_bot in h0.
       rewrite h0.
       eauto.
-    + move => p _ /(_ (Const TPi)).
+    + move => p _ /(_ Bot).
       by rewrite ren_subst_bot.
-    + move => i h /(_ (Const TPi)).
+    + move => i h /(_ Bot).
       by rewrite ren_subst_bot => ->.
+    + move /(_ Bot).
+      move => h /(_ Bot).
+      by rewrite ren_subst_bot.
   - hauto lq:on.
   - hauto lq:on.
   - hauto lq:on.
   - case => //=.
   - sfirstorder.
   - sfirstorder.
+  - sfirstorder.
 Qed.
 
 Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b :=
@@ -2072,6 +2119,7 @@ Proof.
   - sfirstorder use:ERPars.BindCong.
   - sfirstorder.
   - sfirstorder.
+  - sfirstorder.
 Qed.
 
 Lemma Pars_ERPar n (a b : Tm n) : rtc Par.R a b -> rtc ERPar.R a b.
@@ -2371,18 +2419,19 @@ Fixpoint ne {n} (a : Tm n) :=
   | Proj _ a => ne a
   | Pair _ _ => false
   | Const _ => false
+  | Bot => true
   end
 with nf {n} (a : Tm n) :=
   match a with
   | VarTm i => true
   | TBind _ A B => nf A && nf B
-  | (Const TPi) => true
   | App a b => ne a && nf b
   | Abs a => nf a
   | Univ _ => true
   | Proj _ a => ne a
   | Pair a b => nf a && nf b
   | Const _ => true
+  | Bot => true
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -2469,10 +2518,10 @@ Proof.
 Qed.
 
 Lemma ext_wn n (a : Tm n) :
-    wn (App a (Const TPi)) ->
+    wn (App a Bot) ->
     wn a.
 Proof.
-  move E : (App a (Const TPi)) => a0 [v [hr hv]].
+  move E : (App a (Bot)) => a0 [v [hr hv]].
   move : a E.
   move : hv.
   elim : a0 v / hr.
@@ -2483,9 +2532,9 @@ Proof.
     case : a0 hr0=>// => b0 b1.
     elim /RPar'.inv=>// _.
     + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
-      have ? : b3 = (Const TPi) by hauto lq:on inv:RPar'.R. subst.
+      have ? : b3 = (Bot) by hauto lq:on inv:RPar'.R. subst.
       suff : wn (Abs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
-      have : wn (subst_Tm (scons (Const TPi) VarTm) a3) by sfirstorder.
+      have : wn (subst_Tm (scons (Bot) VarTm) a3) by sfirstorder.
       move => h. apply wn_abs.
       move : h. apply wn_antirenaming.
       hauto lq:on rew:off inv:option.
diff --git a/theories/logrel.v b/theories/logrel.v
index a4b15d2..a421cda 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -1,5 +1,4 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
-Require Import fp_red.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red compile.
 From Hammer Require Import Tactics.
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
@@ -295,9 +294,9 @@ Proof.
   - hauto lq:on ctrs:prov.
   - hauto lq:on rew:off ctrs:prov b:on.
   - hauto lq:on ctrs:prov.
-  - move => n.
+  - move => n k.
     have : @prov n Bot Bot by auto using P_Bot.
-    tauto.
+    eauto.
 Qed.
 
 Lemma ne_pars_inv n (a b : Tm n) :
@@ -311,23 +310,37 @@ Lemma ne_pars_extract  n (a b : Tm n) :
   ne a -> rtc Par.R a b -> (exists i, extract b = (VarTm i)) \/ extract b = Bot.
 Proof. hauto lq:on rew:off use:ne_pars_inv, prov_extract. Qed.
 
+Lemma const_pars_extract n k b :
+  rtc Par.R (Const k : Tm n) b -> extract b = Const k.
+Proof. hauto l:on use:pars_const_inv, prov_extract. Qed.
+
+Lemma compile_ne n (a : Tm n) :
+  ne a = ne (Compile.F a) /\ nf a = nf (Compile.F a).
+Proof.
+  elim : n / a => //=; sfirstorder b:on.
+Qed.
+
 Lemma join_bind_ne_contra n p (A : Tm n) B C :
   ne C ->
-  join (TBind p A B) C -> False.
+  Join.R (TBind p A B) C -> False.
 Proof.
-  move => hC [D [h0 h1]].
-  move /pars_pi_inv : h0 => [A0 [B0 [h2 [h3 h4]]]].
+  rewrite /Join.R. move => hC /=.
+  rewrite !pair_eq.
+  move => [[[D [h0 h1]] _] _].
+  have {}hC : ne (Compile.F C) by hauto lq:on use:compile_ne.
+  have {}hC : ne (Proj PL (Proj PL (Compile.F C))) by scongruence.
   have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
+  have : extract D = Const p by eauto using const_pars_extract.
   sfirstorder.
 Qed.
 
 Lemma join_univ_ne_contra n i C :
   ne C ->
-  join (Univ i : Tm n) C -> False.
+  Join.R (Univ i : Tm n) C -> False.
 Proof.
   move => hC [D [h0 h1]].
   move /pars_univ_inv : h0 => ?.
-  have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
+  have : (exists i, extract D = (VarTm i)) \/ exists k, extract D =(Const k)  by hauto q:on use:ne_pars_extract, compile_ne.
   sfirstorder.
 Qed.
 
@@ -336,7 +349,7 @@ Qed.
 Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ B ⟧ i ;; I ↘ PB ->
-  join A B ->
+  Join.R A B ->
   PA = PB.
 Proof.
   move => h. move : B PB. elim : A PA /h.

From 78503149353745d8dd838169b9dbb6dbc3387172 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Mon, 20 Jan 2025 16:49:47 -0500
Subject: [PATCH 4/5] Add stub for par compile

---
 theories/compile.v | 15 +++++++++++++++
 theories/logrel.v  |  2 +-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/theories/compile.v b/theories/compile.v
index 3eaaf42..f063b16 100644
--- a/theories/compile.v
+++ b/theories/compile.v
@@ -66,6 +66,18 @@ Module Join.
   Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
   Proof. hauto l:on use:join_univ_inj. Qed.
 
+  Lemma transitive n (a b c : Tm n) :
+    R a b -> R b c -> R a c.
+  Proof. hauto l:on use:join_transitive unfold:R. Qed.
+
+  Lemma symmetric n (a b : Tm n) :
+    R a b -> R b a.
+  Proof. hauto l:on use:join_symmetric. Qed.
+
+  Lemma reflexive n (a : Tm n) :
+    R a a.
+  Proof. hauto l:on use:join_refl. Qed.
+
 End Join.
 
 Module Equiv.
@@ -135,3 +147,6 @@ Module EquivJoin.
     - hauto l:on.
   Qed.
 End EquivJoin.
+
+Module CompilePar.
+End CompilePar.
diff --git a/theories/logrel.v b/theories/logrel.v
index a421cda..c822d06 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -344,7 +344,7 @@ Proof.
   sfirstorder.
 Qed.
 
-#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra join_symmetric join_transitive : join.
+#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra Join.symmetric Join.transitive : join.
 
 Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->

From 36427daa61ba60fffd0308e1ec452c938ac4be43 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Mon, 20 Jan 2025 20:11:51 -0500
Subject: [PATCH 5/5] Refactor the equational theory to use the compile
 function

---
 theories/compile.v | 33 +++++++++++++++++++++++++++--
 theories/fp_red.v  | 10 ---------
 theories/logrel.v  | 52 ++++++++++++++++++++++++++++++++--------------
 3 files changed, 67 insertions(+), 28 deletions(-)

diff --git a/theories/compile.v b/theories/compile.v
index f063b16..05bc9a8 100644
--- a/theories/compile.v
+++ b/theories/compile.v
@@ -1,6 +1,7 @@
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
+From stdpp Require Import relations (rtc(..)).
 
 Module Compile.
   Fixpoint F {n} (a : Tm n) : Tm n :=
@@ -78,6 +79,16 @@ Module Join.
     R a a.
   Proof. hauto l:on use:join_refl. Qed.
 
+  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+    R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof.
+    rewrite /R.
+    rewrite /join.
+    move => [C [h0 h1]].
+    repeat (rewrite <- Compile.morphing with (ρ0 := funcomp Compile.F ρ); last by reflexivity).
+    hauto lq:on use:join_substing.
+  Qed.
+
 End Join.
 
 Module Equiv.
@@ -148,5 +159,23 @@ Module EquivJoin.
   Qed.
 End EquivJoin.
 
-Module CompilePar.
-End CompilePar.
+Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
+Proof.
+  move => h. elim : n a b /h.
+  - move => n  a0 a1 b0 b1 ha iha hb ihb /=.
+    rewrite -Compile.substing.
+    apply RPar'.AppAbs => //.
+  - hauto q:on use:RPar'.ProjPair'.
+  - qauto ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+Qed.
+
+Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b).
+Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index 6932f84..e9b5591 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -2394,16 +2394,6 @@ Proof.
   sfirstorder unfold:join.
 Qed.
 
-Lemma join_univ_pi_contra n p (A : Tm n) B i :
-  join (TBind p A B) (Univ i) -> False.
-Proof.
-  rewrite /join.
-  move => [c [h0 h1]].
-  move /pars_univ_inv : h1.
-  move /pars_pi_inv : h0.
-  hauto l:on.
-Qed.
-
 Lemma join_substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
   join a b ->
   join (subst_Tm ρ a) (subst_Tm ρ b).
diff --git a/theories/logrel.v b/theories/logrel.v
index c822d06..b9c854d 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -262,8 +262,12 @@ Lemma RPar's_Pars n (A B : Tm n) :
 Proof. hauto lq:on use:RPar'_Par, rtc_subrel. Qed.
 
 Lemma RPar's_join n (A B : Tm n) :
-  rtc RPar'.R A B -> join A B.
-Proof. hauto lq:on ctrs:rtc use:RPar's_Pars. Qed.
+  rtc RPar'.R A B -> Join.R A B.
+Proof.
+  rewrite /Join.R => h.
+  have {}h : rtc RPar'.R (Compile.F A) (Compile.F B) by eauto using compile_rpars.
+  rewrite /join. eauto using RPar's_Pars, rtc_refl.
+Qed.
 
 Lemma bindspace_iff n p (PA : Tm n -> Prop) PF PF0 b  :
   (forall (a : Tm n) (PB PB0 : Tm n -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) ->
@@ -320,6 +324,19 @@ Proof.
   elim : n / a => //=; sfirstorder b:on.
 Qed.
 
+Lemma join_univ_pi_contra n p (A : Tm n) B i :
+  Join.R (TBind p A B) (Univ i) -> False.
+Proof.
+  rewrite /Join.R /=.
+  rewrite !pair_eq.
+  move => [[h _ ]_ ].
+  move : h => [C [h0 h1]].
+  have ?  : extract C = Const p by hauto l:on use:pars_const_inv.
+  have h : prov (Univ i : Tm n) (Proj PL (Proj PL (Univ i))) by hauto lq:on ctrs:prov.
+  have {h} : prov (Univ i) C by eauto using prov_pars.
+  move /prov_extract=>/=. congruence.
+Qed.
+
 Lemma join_bind_ne_contra n p (A : Tm n) B C :
   ne C ->
   Join.R (TBind p A B) C -> False.
@@ -370,9 +387,9 @@ Proof.
       move /InterpExt_Bind_inv : hPi.
       move => [PA0][PF0][hPA0][hTot0][hRes0]?. subst.
       move => hjoin.
-      have{}hr : join U (TBind p0 A0 B0) by auto using RPar's_join.
-      have hj : join (TBind p A B) (TBind p0 A0 B0) by eauto using join_transitive.
-      have {hj} : p0 = p /\ join A A0 /\ join B B0 by hauto l:on use:join_pi_inj.
+      have{}hr : Join.R U (TBind p0 A0 B0) by auto using RPar's_join.
+      have hj : Join.R (TBind p A B) (TBind p0 A0 B0) by eauto using Join.transitive.
+      have {hj} : p0 = p /\ Join.R A A0 /\ Join.R B B0 by hauto l:on use:Join.BindInj.
       move => [? [h0 h1]]. subst.
       have ? : PA0 = PA by hauto l:on. subst.
       rewrite /ProdSpace.
@@ -381,13 +398,15 @@ Proof.
       apply bindspace_iff; eauto.
       move => a PB PB0 hPB hPB0.
       apply : ihPF; eauto.
-      by apply join_substing.
+      rewrite /Join.R.
+      rewrite -!Compile.substing.
+      hauto l:on use:join_substing.
     + move => j ?. subst.
       move => [h0 h1] h.
-      have ? : join U (Univ j) by eauto using RPar's_join.
-      have : join (TBind p A B) (Univ j) by eauto using join_transitive.
+      have ? : Join.R U (Univ j) by eauto using RPar's_join.
+      have : Join.R (TBind p A B) (Univ j) by eauto using Join.transitive.
       move => ?. exfalso.
-      eauto using join_univ_pi_contra.
+      hauto l: on use: join_univ_pi_contra.
     + move => A0 ? ? [/RPar's_join ?]. subst.
       move => _ ?. exfalso. eauto with join.
   - move => j ? B PB /InterpExtInv.
@@ -397,19 +416,19 @@ Proof.
       move /RPar's_join => *.
       exfalso. eauto with join.
     + move => m _ [/RPar's_join h0 + h1].
-      have /join_univ_inj {h0 h1} ?  : join (Univ j : Tm n) (Univ m) by eauto using join_transitive.
+      have /join_univ_inj {h0 h1} ?  : Join.R (Univ j : Tm n) (Univ m) by eauto using Join.transitive.
       subst.
       move /InterpExt_Univ_inv. firstorder.
     + move => A ? ? [/RPar's_join] *. subst. exfalso. eauto with join.
   - move => A A0 PA h.
-    have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar'_Par, relations.rtc_once.
-    eauto using join_transitive.
+    have /Join.symmetric {}h : Join.R A A0 by hauto lq:on ctrs:rtc use:RPar's_join, relations.rtc_once.
+    eauto with join.
 Qed.
 
 Lemma InterpUniv_Join n i (A B : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ i ↘ PB ->
-  join A B ->
+  Join.R A B ->
   PA = PB.
 Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed.
 
@@ -442,7 +461,7 @@ Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed.
 Lemma InterpUniv_Join' n i j (A B : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ j ↘ PB ->
-  join A B ->
+  Join.R A B ->
   PA = PB.
 Proof.
   have [? ?] : i <= max i j /\ j <= max i j by lia.
@@ -749,12 +768,12 @@ Qed.
 Lemma ST_Conv n Γ (a : Tm n) A B i :
   Γ ⊨ a ∈ A ->
   Γ ⊨ B ∈ Univ i ->
-  join A B ->
+  Join.R A B ->
   Γ ⊨ a ∈ B.
 Proof.
   move => ha /SemWt_Univ h h0.
   move => ρ hρ.
-  have {}h0 : join (subst_Tm ρ A) (subst_Tm ρ B) by eauto using join_substing.
+  have {}h0 : Join.R (subst_Tm ρ A) (subst_Tm ρ B) by eauto using Join.substing.
   move /ha : (hρ){ha} => [m [PA [h1 h2]]].
   move /h : (hρ){h} => [S hS].
   have ? : PA = S by eauto using InterpUniv_Join'. subst.
@@ -909,6 +928,7 @@ Fixpoint size_tm {n} (a : Tm n) :=
   | Proj p a => 1 + size_tm a
   | Pair a b => 1 + Nat.add (size_tm a) (size_tm b)
   | Bot => 1
+  | Const _ => 1
   | Univ _ => 1
   end.