Merge remote-tracking branch 'origin/logrel' into logrelnew

syntax.sig

@@ -16,3 +16,4 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
+PBot : PTm

theories/Autosubst2/syntax.v

@@ -40,7 +40,8 @@ Inductive PTm (n_PTm : nat) : Type :=
   | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
   | PProj : PTag -> PTm n_PTm -> PTm n_PTm
   | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm
-  | PUniv : nat -> PTm n_PTm.
+  | PUniv : nat -> PTm n_PTm
+  | PBot : PTm n_PTm.
 
 Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)}
   (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0.
@@ -89,6 +90,11 @@ Proof.
 exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)).
 Qed.
 
+Lemma congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm.
+Proof.
+exact (eq_refl).
+Qed.
+
 Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -112,6 +118,7 @@ Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat}
   | PBind _ s0 s1 s2 =>
       PBind n_PTm s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2)
   | PUniv _ s0 => PUniv n_PTm s0
+  | PBot _ => PBot n_PTm
   end.
 
 Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
@@ -142,6 +149,7 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
       PBind n_PTm s0 (subst_PTm sigma_PTm s1)
         (subst_PTm (up_PTm_PTm sigma_PTm) s2)
   | PUniv _ s0 => PUniv n_PTm s0
+  | PBot _ => PBot n_PTm
   end.
 
 Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
@@ -184,6 +192,7 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
       congr_PBind (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
         (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -229,6 +238,7 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
         (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
            (upExtRen_PTm_PTm _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
@@ -275,6 +285,7 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
         (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
            (upExt_PTm_PTm _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -322,6 +333,7 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
         (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
            (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
@@ -378,6 +390,7 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
         (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
            (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@@ -454,6 +467,7 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
         (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
            (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@@ -532,6 +546,7 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
         (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
            (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
@@ -649,6 +664,7 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
         (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
            (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2)
   | PUniv _ s0 => congr_PUniv (eq_refl s0)
+  | PBot _ => congr_PBot
   end.
 
 Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
@@ -855,6 +871,8 @@ Core.
 
 Arguments VarPTm {n_PTm}.
 
+Arguments PBot {n_PTm}.
+
 Arguments PUniv {n_PTm}.
 
 Arguments PBind {n_PTm}.

theories/fp_red.v

@@ -53,7 +53,9 @@ Module EPar.
   | BindCong p A0 A1 B0 B1 :
     R A0 A1 ->
     R B0 B1 ->
-    R (PBind p A0 B0) (PBind p A1 B1).
+    R (PBind p A0 B0) (PBind p A1 B1)
+  | BotCong :
+    R PBot PBot.
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -117,6 +119,8 @@ Inductive SNe {n} : PTm n -> Prop :=
 | N_Proj p a :
   SNe a ->
   SNe (PProj p a)
+| N_Bot :
+  SNe PBot
 with SN  {n} : PTm n -> Prop :=
 | N_Pair a b :
   SN a ->
@@ -270,6 +274,7 @@ Fixpoint ne {n} (a : PTm n) :=
   | PProj _ a => ne a
   | PUniv _ => false
   | PBind _ _ _ => false
+  | PBot => true
   end
 with nf {n} (a : PTm n) :=
   match a with
@@ -280,6 +285,7 @@ with nf {n} (a : PTm n) :=
   | PProj _ a => ne a
   | PUniv _ => true
   | PBind _ A B => nf A && nf B
+  | PBot => true
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -427,6 +433,7 @@ Proof.
   - sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
+  - sauto lq:on.
   - move => a b ha iha hb ihb b0.
     inversion 1; subst.
     + have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
@@ -595,7 +602,9 @@ Module RPar.
   | BindCong p A0 A1 B0 B1 :
     R A0 A1 ->
     R B0 B1 ->
-    R (PBind p A0 B0) (PBind p A1 B1).
+    R (PBind p A0 B0) (PBind p A1 B1)
+  | BotCong :
+    R PBot PBot.
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -690,6 +699,7 @@ Module RPar.
     | PProj p a => PProj p (tstar a)
     | PUniv i => PUniv i
     | PBind p A B => PBind p (tstar A) (tstar B)
+    | PBot => PBot
     end.
 
   Lemma triangle n (a b : PTm n) :
@@ -720,6 +730,7 @@ Module RPar.
     - hauto lq:on ctrs:R inv:R.
     - hauto lq:on ctrs:R inv:R.
     - hauto lq:on ctrs:R inv:R.
+    - hauto lq:on ctrs:R inv:R.
   Qed.
 
   Lemma diamond n (a b c : PTm n) :
@@ -736,6 +747,7 @@ Proof.
   - hauto l:on inv:RPar.R.
   - qauto l:on inv:RPar.R,SNe,SN ctrs:SNe.
   - hauto lq:on inv:RPar.R, SNe ctrs:SNe.
+  - hauto lq:on inv:RPar.R, SNe ctrs:SNe.
   - qauto l:on ctrs:SN inv:RPar.R.
   - hauto lq:on ctrs:SN inv:RPar.R.
   - hauto lq:on ctrs:SN.
@@ -874,6 +886,8 @@ Module NeEPar.
     R_nonelim A0 A1 ->
     R_nonelim B0 B1 ->
     R_nonelim (PBind p A0 B0) (PBind p A1 B1)
+  | BotCong :
+    R_nonelim PBot PBot
   with R_elim {n} : PTm n -> PTm n -> Prop :=
   | NAbsCong a0 a1 :
     R_nonelim a0 a1 ->
@@ -896,7 +910,9 @@ Module NeEPar.
   | NBindCong p A0 A1 B0 B1 :
     R_nonelim A0 A1 ->
     R_nonelim B0 B1 ->
-    R_elim (PBind p A0 B0) (PBind p A1 B1).
+    R_elim (PBind p A0 B0) (PBind p A1 B1)
+  | NBotCong :
+    R_elim PBot PBot.
 
   Scheme epar_elim_ind := Induction for R_elim Sort Prop
       with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
@@ -1165,6 +1181,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
     - hauto lq:on ctrs:rtc, NeEPar.R_nonelim.
     - hauto l:on.
     - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv.
+    - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv.
   Qed.
 
 
@@ -1272,6 +1289,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
     - hauto lq:on inv:RRed.R.
     - hauto lq:on inv:RRed.R ctrs:rtc.
     - sauto lq:on ctrs:EPar.R, rtc use:RReds.BindCong, P_BindInv, @relations.rtc_transitive.
+    - hauto lq:on inv:RRed.R ctrs:rtc.
   Qed.
 
   Lemma η_postponement_star n a b c :
@@ -1762,6 +1780,7 @@ Module LoReds.
     - hauto lq:on ctrs:rtc.
     - hauto lq:on rew:off use:LoReds.AppCong solve+:triv.
     - hauto l:on use:LoReds.ProjCong solve+:triv.
+    - hauto lq:on ctrs:rtc.
     - hauto q:on use:LoReds.PairCong solve+:triv.
     - hauto q:on use:LoReds.AbsCong solve+:triv.
     - sfirstorder use:ne_nf.
@@ -1797,6 +1816,7 @@ Fixpoint size_PTm {n} (a : PTm n) :=
   | PPair a b => 3 + Nat.add (size_PTm a) (size_PTm b)
   | PUniv _ => 3
   | PBind p A B => 3 + Nat.add (size_PTm A) (size_PTm B)
+  | PBot => 1
   end.
 
 Lemma size_PTm_ren n m (ξ : fin n -> fin m) a : size_PTm (ren_PTm ξ a) = size_PTm a.