Add pi type

syntax.sig

@@ -7,3 +7,4 @@ 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

theories/Autosubst2/syntax.v

@@ -24,7 +24,8 @@ Inductive Tm (n_Tm : nat) : Type :=
   | 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.
+  | Proj : PTag -> Tm n_Tm -> Tm n_Tm
+  | Pi : Tm n_Tm -> Tm (S n_Tm) -> 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.
@@ -56,6 +57,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}
+  {t1 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1) :
+  Pi m_Tm s0 s1 = Pi m_Tm t0 t1.
+Proof.
+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 upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -76,6 +85,7 @@ 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)
   end.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -99,6 +109,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 =>
+      Pi n_Tm (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
   end.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -134,6 +146,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 =>
+      congr_Pi (idSubst_Tm sigma_Tm Eq_Tm s0)
+        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
   end.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -172,6 +187,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 =>
+      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)
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -211,6 +230,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 =>
+      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)
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -250,6 +273,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 =>
+      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)
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -299,6 +326,10 @@ 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 =>
+      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)
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -369,6 +400,10 @@ 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 =>
+      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)
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -440,6 +475,10 @@ 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 =>
+      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)
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -550,6 +589,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 =>
+      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)
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -748,6 +791,8 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
+Arguments Pi {n_Tm}.
+
 Arguments Proj {n_Tm}.
 
 Arguments Pair {n_Tm}.

theories/fp_red.v

@@ -49,7 +49,11 @@ Module Par.
     R (Pair a0 b0) (Pair a1 b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (Proj p a0) (Proj p a1).
+    R (Proj p a0) (Proj p a1)
+  | PiCong A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (Pi A0 B0) (Pi A1 B1).
 End Par.
 
 (***************** Beta rules only ***********************)
@@ -89,7 +93,11 @@ Module RPar.
     R (Pair a0 b0) (Pair a1 b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (Proj p a0) (Proj p a1).
+    R (Proj p a0) (Proj p a1)
+  | PiCong A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (Pi A0 B0) (Pi A1 B1).
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -154,6 +162,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 use:morphing_up.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -196,7 +205,11 @@ Module EPar.
     R (Pair a0 b0) (Pair a1 b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (Proj p a0) (Proj p a1).
+    R (Proj p a0) (Proj p a1)
+  | PiCong A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (Pi A0 B0) (Pi A1 B1).
 
   Lemma refl n (a : Tm n) : EPar.R a a.
   Proof.
@@ -238,6 +251,7 @@ Module EPar.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
+    - hauto l:on ctrs:R use:renaming inv:option.
   Qed.
 
   Lemma substing n a0 a1 (b0 b1 : Tm n) :
@@ -315,6 +329,12 @@ Module RPars.
     rtc RPar.R (App a0 b0) (App a1 b1).
   Proof. solve_s. Qed.
 
+  Lemma PiCong 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).
+  Proof. solve_s. Qed.
+
   Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R b0 b1 ->
@@ -530,6 +550,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.
 Qed.
 
 Lemma commutativity1 n (a b0 b1 : Tm n) :
@@ -599,6 +620,21 @@ Proof.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
+Lemma Pi_EPar' n (a : Tm n) b u  :
+  EPar.R (Pi a b) u ->
+  (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (Pi a0 b0) u).
+Proof.
+  move E : (Pi a b) => t h.
+  move : a b E. elim : n t u /h => //=.
+  - move => n a0 a1 ha iha a b ?. subst.
+    specialize iha with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - move => n a0 a1 ha iha a b ?. subst.
+    specialize iha with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - hauto l:on ctrs:OExp.R.
+Qed.
+
 Lemma Pair_EPar' n (a b u : Tm n) :
   EPar.R (Pair a b) u ->
   exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (Pair a0 b0) u.
@@ -654,6 +690,13 @@ Proof.
     move : OExp.commutativity0 h1; repeat move/[apply].
     move => [d1 h1].
     exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
+  - 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.
+    move : OExp.commutativity0 h2; repeat move/[apply].
+    move => [d h].
+    exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
 Qed.
 
 Function tstar {n} (a : Tm n) :=
@@ -668,6 +711,7 @@ Function tstar {n} (a : Tm n) :=
   | Proj p (Pair a b) => if p is PL then (tstar a) else (tstar b)
   | Proj p (Abs a) => (Abs (Proj p (tstar a)))
   | Proj p a => Proj p (tstar a)
+  | Pi a b => Pi (tstar a) (tstar b)
   end.
 
 Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
@@ -683,6 +727,7 @@ Proof.
   - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'.
   - 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) :