Generalize Pi to TBind so we have both sigma and pi

syntax.sig

@@ -1,13 +1,16 @@
 nat  : Type
 Tm(VarTm) : Type
 PTag : Type
+TTag : Type
 
+TPi : TTag
+TSig : TTag
 PL : PTag
 PR : PTag
 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
+TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
 Bot : Tm
 Univ : nat -> Tm

theories/Autosubst2/syntax.v

@@ -19,13 +19,27 @@ Proof.
 exact (eq_refl).
 Qed.
 
+Inductive TTag : Type :=
+  | TPi : TTag
+  | TSig : TTag.
+
+Lemma congr_TPi : TPi = TPi.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_TSig : TSig = TSig.
+Proof.
+exact (eq_refl).
+Qed.
+
 Inductive Tm (n_Tm : nat) : Type :=
   | VarTm : fin n_Tm -> Tm n_Tm
   | Abs : Tm (S n_Tm) -> Tm n_Tm
   | 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
+  | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm
   | Bot : Tm n_Tm
   | Univ : nat -> Tm n_Tm.
 
@@ -59,12 +73,14 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj m_Tm x s1) H0))
          (ap (fun x => Proj m_Tm t0 x) H1)).
 Qed.
 
-Lemma congr_Pi {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm (S m_Tm)} {t0 : Tm m_Tm}
+Lemma congr_TBind {m_Tm : nat} {s0 : TTag} {s1 : Tm m_Tm} {s2 : Tm (S m_Tm)}
-  {t1 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1) :
+  {t0 : TTag} {t1 : Tm m_Tm} {t2 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1)
-  Pi m_Tm s0 s1 = Pi m_Tm t0 t1.
+  (H2 : s2 = t2) : TBind m_Tm s0 s1 s2 = TBind m_Tm t0 t1 t2.
 Proof.
-exact (eq_trans (eq_trans eq_refl (ap (fun x => Pi m_Tm x s1) H0))
+exact (eq_trans
-         (ap (fun x => Pi m_Tm t0 x) H1)).
+         (eq_trans (eq_trans eq_refl (ap (fun x => TBind m_Tm x s1 s2) H0))
+            (ap (fun x => TBind m_Tm t0 x s2) H1))
+         (ap (fun x => TBind m_Tm t0 t1 x) H2)).
 Qed.
 
 Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm.
@@ -98,7 +114,8 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | App _ s0 s1 => App n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
   | 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)
+  | 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
   | Univ _ s0 => Univ n_Tm s0
   end.
@@ -124,8 +141,8 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
   | App _ s0 s1 => App n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
   | Pair _ s0 s1 => Pair n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
   | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      Pi n_Tm (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
+      TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2)
   | Bot _ => Bot n_Tm
   | Univ _ s0 => Univ n_Tm s0
   end.
@@ -163,9 +180,9 @@ subst_Tm sigma_Tm s = s :=
       congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0)
         (idSubst_Tm sigma_Tm Eq_Tm s1)
   | Proj _ s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (idSubst_Tm sigma_Tm Eq_Tm s0)
+      congr_TBind (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
-        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
+        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -206,10 +223,10 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
         (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
   | Proj _ s0 s1 =>
       congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+      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) s1)
+           (upExtRen_Tm_Tm _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -251,10 +268,10 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
       congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
         (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
   | Proj _ s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+      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)
-           s1)
+           s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -296,10 +313,10 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
         (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
   | Proj _ s0 s1 =>
       congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+      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) s1)
+           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -351,10 +368,11 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
   | Proj _ s0 s1 =>
       congr_Proj (eq_refl s0)
         (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+      congr_TBind (eq_refl s0)
+        (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) s1)
+           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -427,10 +445,11 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
   | Proj _ s0 s1 =>
       congr_Proj (eq_refl s0)
         (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+      congr_TBind (eq_refl s0)
+        (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) s1)
+           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -504,10 +523,11 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
   | Proj _ s0 s1 =>
       congr_Proj (eq_refl s0)
         (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+      congr_TBind (eq_refl s0)
+        (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) s1)
+           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -620,10 +640,10 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
         (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
   | Proj _ s0 s1 =>
       congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
-  | Pi _ s0 s1 =>
+  | TBind _ s0 s1 s2 =>
-      congr_Pi (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+      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) s1)
+           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
@@ -828,7 +848,7 @@ Arguments Univ {n_Tm}.
 
 Arguments Bot {n_Tm}.
 
-Arguments Pi {n_Tm}.
+Arguments TBind {n_Tm}.
 
 Arguments Proj {n_Tm}.
 

theories/fp_red.v

@@ -68,10 +68,10 @@ Module Par.
   | ProjCong p a0 a1 :
     R a0 a1 ->
     R (Proj p a0) (Proj p a1)
-  | PiCong A0 A1 B0 B1:
+  | BindCong p A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
-    R (Pi A0 B0) (Pi A1 B1)
+    R (TBind p A0 B0) (TBind p A1 B1)
   (* Bot is useful for making the prov function computable  *)
   | BotCong :
     R Bot Bot
@@ -209,11 +209,11 @@ Module Par.
       move : iha => [b0 [? ?]]. subst.
       eexists. split. by apply ProjCong; eauto.
       by asimpl.
-    - move => n A0 A1 B0 B1 ha iha hB ihB m ξ []//= t t0 [*]. subst.
+    - move => n p A0 A1 B0 B1 ha iha hB ihB m ξ []//= ? t t0 [*]. subst.
       spec_refl.
       move : iha => [b0 [? ?]].
       move : ihB => [c0 [? ?]]. subst.
-      eexists. split. by apply PiCong; eauto.
+      eexists. split. by apply BindCong; eauto.
       by asimpl.
     - move => n n0 ξ []//=. hauto l:on.
     - move => n i n0 ξ []//=. hauto l:on.
@@ -286,7 +286,7 @@ Module RPar.
   | ProjCong p a0 a1 :
     R a0 a1 ->
     R (Proj p a0) (Proj p a1)
-  | PiCong A0 A1 B0 B1:
+  | BindCong A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
     R (Pi A0 B0) (Pi A1 B1)
@@ -404,7 +404,7 @@ Module EPar.
   | ProjCong p a0 a1 :
     R a0 a1 ->
     R (Proj p a0) (Proj p a1)
-  | PiCong A0 A1 B0 B1:
+  | BindCong A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
     R (Pi A0 B0) (Pi A1 B1)
@@ -533,7 +533,7 @@ Module RPars.
     rtc RPar.R (App a0 b0) (App a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma PiCong n (a0 a1 : Tm n) b0 b1 :
+  Lemma BindCong n (a0 a1 : Tm n) b0 b1 :
     rtc RPar.R a0 a1 ->
     rtc RPar.R b0 b1 ->
     rtc RPar.R (Pi a0 b0) (Pi a1 b1).
@@ -754,7 +754,7 @@ Proof.
       exists d. split => //.
       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 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.
 Qed.
@@ -927,7 +927,7 @@ Proof.
   - move => n a0 a1 b0 b1 ha iha hb ihb c.
     move /Pi_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}.
     have : EPar.R (Pi a2 b2)(Pi a3 b3)
-      by hauto l:on use:EPar.PiCong.
+      by hauto l:on use:EPar.BindCong.
     move : OExp.commutativity0 h2; repeat move/[apply].
     move => [d h].
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
@@ -1375,24 +1375,24 @@ Module ERPar.
     - sfirstorder use:EPar.AppCong, @rtc_once.
   Qed.
 
-  Lemma PiCong n (a0 a1 : Tm n) b0 b1:
+  Lemma BindCong n (a0 a1 : Tm n) b0 b1:
     R a0 a1 ->
     R b0 b1 ->
     rtc R (Pi a0 b0) (Pi a1 b1).
   Proof.
     move => [] + [].
-    - sfirstorder use:RPar.PiCong, @rtc_once.
+    - sfirstorder use:RPar.BindCong, @rtc_once.
     - move => h0 h1.
       apply : rtc_l.
-      left. apply RPar.PiCong; eauto; apply RPar.refl.
+      left. apply RPar.BindCong; eauto; apply RPar.refl.
       apply rtc_once.
-      hauto l:on use:EPar.PiCong, EPar.refl.
+      hauto l:on use:EPar.BindCong, EPar.refl.
     - move => h0 h1.
       apply : rtc_l.
-      left. apply RPar.PiCong; eauto; apply RPar.refl.
+      left. apply RPar.BindCong; eauto; apply RPar.refl.
       apply rtc_once.
-      hauto l:on use:EPar.PiCong, EPar.refl.
+      hauto l:on use:EPar.BindCong, EPar.refl.
-    - sfirstorder use:EPar.PiCong, @rtc_once.
+    - sfirstorder use:EPar.BindCong, @rtc_once.
   Qed.
 
   Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
@@ -1423,7 +1423,7 @@ Module ERPar.
 
 End ERPar.
 
-Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong ERPar.PiCong : erpar.
+Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong ERPar.BindCong : erpar.
 
 Module ERPars.
   #[local]Ltac solve_s_rec :=
@@ -1454,7 +1454,7 @@ Module ERPars.
     rtc ERPar.R (Proj p a0) (Proj p a1).
   Proof. solve_s. Qed.
 
-  Lemma PiCong n (a0 a1 : Tm n) b0 b1:
+  Lemma BindCong n (a0 a1 : Tm n) b0 b1:
     rtc ERPar.R a0 a1 ->
     rtc ERPar.R b0 b1 ->
     rtc ERPar.R (Pi a0 b0) (Pi a1 b1).
@@ -1512,7 +1512,7 @@ Proof.
   - sfirstorder use:ERPars.AppCong.
   - sfirstorder use:ERPars.PairCong.
   - sfirstorder use:ERPars.ProjCong.
-  - sfirstorder use:ERPars.PiCong.
+  - sfirstorder use:ERPars.BindCong.
   - sfirstorder.
   - sfirstorder.
 Qed.