Refactor the equational theory to use the compile function

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.
+Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
-End CompilePar.
+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.

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).

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.
+  rtc RPar'.R A B -> Join.R A B.
-Proof. hauto lq:on ctrs:rtc use:RPar's_Pars. Qed.
+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{}hr : Join.R 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 : Join.R (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 {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.R 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 (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.
+    have /Join.symmetric {}h : Join.R A A0 by hauto lq:on ctrs:rtc use:RPar's_join, relations.rtc_once.
-    eauto using join_transitive.
+    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.