Prove injectivity of Pair and Lambdas

README.md

@@ -0,0 +1 @@
+This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.

syntax.sig

@@ -1,8 +1,16 @@
+nat  : Type
 Tm(VarTm) : Type
--- nat : 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
-Proj1 : Tm -> Tm
-Proj2 : Tm -> Tm
+Proj : PTag -> Tm -> Tm
+TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
+Bot : Tm
+Univ : nat -> Tm

theories/Autosubst2/syntax.v

@@ -5,13 +5,43 @@ Require Import Setoid Morphisms Relation_Definitions.
 
 Module Core.
 
+Inductive PTag : Type :=
+  | PL : PTag
+  | PR : PTag.
+
+Lemma congr_PL : PL = PL.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_PR : PR = PR.
+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
-  | Proj1 : Tm n_Tm -> Tm n_Tm
-  | Proj2 : Tm n_Tm -> Tm n_Tm.
+  | Proj : PTag -> Tm 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.
 
 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.
@@ -35,16 +65,33 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair m_Tm x s1) H0))
          (ap (fun x => Pair m_Tm t0 x) H1)).
 Qed.
 
-Lemma congr_Proj1 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
-  Proj1 m_Tm s0 = Proj1 m_Tm t0.
+Lemma congr_Proj {m_Tm : nat} {s0 : PTag} {s1 : Tm m_Tm} {t0 : PTag}
+  {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) :
+  Proj m_Tm s0 s1 = Proj m_Tm t0 t1.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => Proj1 m_Tm x) H0)).
+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_Proj2 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
-  Proj2 m_Tm s0 = Proj2 m_Tm t0.
+Lemma congr_TBind {m_Tm : nat} {s0 : TTag} {s1 : Tm m_Tm} {s2 : Tm (S m_Tm)}
+  {t0 : TTag} {t1 : Tm m_Tm} {t2 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1)
+  (H2 : s2 = t2) : TBind m_Tm s0 s1 s2 = TBind m_Tm t0 t1 t2.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => Proj2 m_Tm x) H0)).
+exact (eq_trans
+         (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.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_Univ {m_Tm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
+  Univ m_Tm s0 = Univ m_Tm t0.
+Proof.
+exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)).
 Qed.
 
 Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
@@ -66,8 +113,11 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | Abs _ s0 => Abs n_Tm (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
   | 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)
-  | Proj1 _ s0 => Proj1 n_Tm (ren_Tm xi_Tm s0)
-  | Proj2 _ s0 => Proj2 n_Tm (ren_Tm xi_Tm s0)
+  | Proj _ s0 s1 => Proj n_Tm s0 (ren_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.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -90,8 +140,11 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
   | Abs _ s0 => Abs n_Tm (subst_Tm (up_Tm_Tm sigma_Tm) s0)
   | 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)
-  | Proj1 _ s0 => Proj1 n_Tm (subst_Tm sigma_Tm s0)
-  | Proj2 _ s0 => Proj2 n_Tm (subst_Tm sigma_Tm s0)
+  | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -126,8 +179,12 @@ subst_Tm sigma_Tm s = s :=
   | Pair _ s0 s1 =>
       congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0)
         (idSubst_Tm sigma_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (idSubst_Tm sigma_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (idSubst_Tm sigma_Tm Eq_Tm s0)
+  | Proj _ s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      congr_TBind (eq_refl s0) (idSubst_Tm sigma_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.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -164,8 +221,14 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | Pair _ s0 s1 =>
       congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
         (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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) s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -204,8 +267,13 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
   | Pair _ s0 s1 =>
       congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
         (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+  | Proj _ s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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)
+           s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -243,8 +311,14 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
   | Pair _ s0 s1 =>
       congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
         (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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) s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -291,10 +365,16 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
   | Pair _ s0 s1 =>
       congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
-  | Proj1 _ s0 =>
-      congr_Proj1 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
-  | Proj2 _ s0 =>
-      congr_Proj2 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0)
+        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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) s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -362,10 +442,16 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
   | Pair _ s0 s1 =>
       congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
         (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
-  | Proj1 _ s0 =>
-      congr_Proj1 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
-  | Proj2 _ s0 =>
-      congr_Proj2 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0)
+        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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) s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -434,10 +520,16 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
   | Pair _ s0 s1 =>
       congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
-  | Proj1 _ s0 =>
-      congr_Proj1 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
-  | Proj2 _ s0 =>
-      congr_Proj2 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0)
+        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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) s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -546,8 +638,14 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
   | Pair _ s0 s1 =>
       congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
         (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
+  | TBind _ s0 s1 s2 =>
+      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) s2)
+  | Bot _ => congr_Bot
+  | Univ _ s0 => congr_Univ (eq_refl s0)
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -746,9 +844,13 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
-Arguments Proj2 {n_Tm}.
+Arguments Univ {n_Tm}.
 
-Arguments Proj1 {n_Tm}.
+Arguments Bot {n_Tm}.
+
+Arguments TBind {n_Tm}.
+
+Arguments Proj {n_Tm}.
 
 Arguments Pair {n_Tm}.
 

theories/diagram.txt

@@ -0,0 +1,20 @@
+a0 --> a3
+|      |
+|      |
+v      v
+a1 --> a4
+
+
+(Abs a3) >>* a2
+
+Abs a0 ----> (Abs a3) >>* a2
+  |             |
+  |             |
+Abs a1 ----> (Abs a4) >>*
+
+
+a0 >> a1
+|     |
+|     |
+v     v
+b0 >> b1