Need to tweak the definition of Prov

syntax.sig

@@ -7,4 +7,5 @@ Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
-Pi : Tm -> (bind Tm in Tm) -> Tm
+Pi : Tm -> (bind Tm in Tm) -> Tm
+Bot : Tm

theories/Autosubst2/syntax.v

@@ -25,7 +25,8 @@ Inductive Tm (n_Tm : nat) : Type :=
   | App : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
   | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
   | Proj : PTag -> Tm n_Tm -> Tm n_Tm
-  | Pi : Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm.
+  | Pi : Tm n_Tm -> Tm (S n_Tm) -> 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.
@@ -65,6 +66,11 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => Pi m_Tm x s1) H0))
          (ap (fun x => Pi m_Tm t0 x) H1)).
 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.
@@ -86,6 +92,7 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | Pair _ s0 s1 => Pair n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
   | Proj _ s0 s1 => Proj n_Tm s0 (ren_Tm xi_Tm s1)
   | Pi _ s0 s1 => Pi n_Tm (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1)
+  | Bot _ => Bot n_Tm
   end.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -111,6 +118,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)
   | Pi _ s0 s1 =>
       Pi n_Tm (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
+  | Bot _ => Bot n_Tm
   end.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -149,6 +157,7 @@ subst_Tm sigma_Tm s = s :=
   | Pi _ s0 s1 =>
       congr_Pi (idSubst_Tm sigma_Tm Eq_Tm s0)
         (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -191,6 +200,7 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
       congr_Pi (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
         (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
            (upExtRen_Tm_Tm _ _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -234,6 +244,7 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
       congr_Pi (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
         (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
            s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -277,6 +288,7 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
       congr_Pi (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
         (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
            (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -330,6 +342,7 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
       congr_Pi (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
            (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -404,6 +417,7 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
       congr_Pi (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
         (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
            (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -479,6 +493,7 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
       congr_Pi (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
            (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -593,6 +608,7 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
       congr_Pi (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
         (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
            (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1)
+  | Bot _ => congr_Bot
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -791,6 +807,8 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
+Arguments Bot {n_Tm}.
+
 Arguments Pi {n_Tm}.
 
 Arguments Proj {n_Tm}.

theories/fp_red.v

@@ -3,6 +3,7 @@ Require Import FunInd.
 From stdpp Require Import relations (rtc (..), rtc_once, rtc_r).
 From Hammer Require Import Tactics.
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+From Equations Require Import Equations.
 
 
 (* Trying my best to not write C style module_funcname *)
@@ -53,7 +54,9 @@ Module Par.
   | PiCong A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
-    R (Pi A0 B0) (Pi A1 B1).
+    R (Pi A0 B0) (Pi A1 B1)
+  | BotCong :
+    R Bot Bot.
 End Par.
 
 (***************** Beta rules only ***********************)
@@ -97,7 +100,9 @@ Module RPar.
   | PiCong A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
-    R (Pi A0 B0) (Pi A1 B1).
+    R (Pi A0 B0) (Pi A1 B1)
+  | BotCong :
+    R Bot Bot.
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -163,6 +168,7 @@ Module RPar.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R use:morphing_up.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -209,7 +215,9 @@ Module EPar.
   | PiCong A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
-    R (Pi A0 B0) (Pi A1 B1).
+    R (Pi A0 B0) (Pi A1 B1)
+  | BotCong :
+    R Bot Bot.
 
   Lemma refl n (a : Tm n) : EPar.R a a.
   Proof.
@@ -252,6 +260,7 @@ Module EPar.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
     - hauto l:on ctrs:R use:renaming inv:option.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n a0 a1 (b0 b1 : Tm n) :
@@ -551,6 +560,7 @@ Proof.
       hauto lq:on use:RPars.ProjCong, relations.rtc_transitive.
     + hauto lq:on ctrs:EPar.R use:RPars.ProjCong.
   - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.PiCong.
+  - hauto l:on ctrs:EPar.R inv:RPar.R.
 Qed.
 
 Lemma commutativity1 n (a b0 b1 : Tm n) :
@@ -650,6 +660,20 @@ 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.
+    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 EPar_diamond n (c a1 b1 : Tm n) :
   EPar.R c a1 ->
   EPar.R c b1 ->
@@ -697,6 +721,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.
 Qed.
 
 Function tstar {n} (a : Tm n) :=
@@ -712,6 +737,7 @@ Function tstar {n} (a : Tm n) :=
   | Proj p (Abs a) => (Abs (Proj p (tstar a)))
   | Proj p a => Proj p (tstar a)
   | Pi a b => Pi (tstar a) (tstar b)
+  | Bot => Bot
   end.
 
 Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
@@ -728,6 +754,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) :
@@ -752,14 +779,53 @@ Proof.
   sfirstorder use:relations.diamond_confluent, EPar_diamond.
 Qed.
 
-Fixpoint prov {n} A B (a : Tm n) : Prop :=
+Fixpoint depth_tm {n} (a : Tm n) :=
   match a with
-  | Pi A0 B0 => rtc Par.R A A0 /\ rtc Par.R B B0
+  | VarTm _ => 1
-  | App a b => prov A B a
+  | Pi A B => 1 + max (depth_tm A) (depth_tm B)
-  | Abs a => prov A B (subst_Tm (scons A VarTm) a)
+  | Abs a => 1 + depth_tm a
-  | _ => True
+  | 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
   end.
 
+Equations prov {n} (A : Tm n) (B : Tm (S n)) (a : Tm n) : Prop by wf (depth_tm a) lt :=
+  prov A B (Pi A0 B0) := rtc Par.R A A0 /\ rtc Par.R B B0;
+  prov A B (Abs a) := prov A B (subst_Tm (scons Bot VarTm) a);
+  prov A B (App a b) := prov A B a;
+  prov A B (Pair a b) := prov A B a /\ prov A B b;
+  prov A B (Proj p a) := prov A B a;
+  prov A B Bot := False;
+  prov A B (VarTm _) := False.
+Next Obligation.
+Admitted.
+
+Next Obligation.
+  sfirstorder.
+Qed.
+
+Next Obligation.
+  sfirstorder.
+Qed.
+
+Next Obligation.
+  sfirstorder.
+Qed.
+
+Lemma prov_par n (A : Tm n) B a b : prov A B a -> EPar.R a b -> prov A B b.
+Proof.
+  move => + h. move : A B.
+  elim : n a b /h.
+  - move => n a0 a1 ha iha A B. simp prov. move /iha.
+    asimpl. simp prov.
+  - hauto l:on rew:db:prov.
+  - simp prov.
+  - move => n a0 a1 ha iha A B. simp prov.
+
+
+
+
 Lemma Par_confluent n (c a1 b1 : Tm n) :
   rtc Par.R c a1 ->
   rtc Par.R c b1 ->