Prove PairEta

theories/admissible.v

@@ -120,6 +120,13 @@ Proof.
   hauto l:on use:regularity, E_FunExt.
 Qed.
 
+Lemma E_PairExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B. hauto l:on use:regularity, E_PairExt. Qed.
+
 Lemma renaming_comp Γ Δ Ξ ξ0 ξ1 :
   renaming_ok Γ Δ ξ0 -> renaming_ok Δ Ξ ξ1 ->
   renaming_ok Γ Ξ (funcomp ξ0 ξ1).
@@ -166,3 +173,92 @@ Proof.
   sauto lq:on use:renaming, renaming_shift, E_Refl.
   constructor. constructor=>//. constructor.
 Qed.
+
+Lemma Proj1_Inv Γ (a : PTm ) U :
+  Γ ⊢ PProj PL a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
+Proof.
+  move E : (PProj PL a) => u hu.
+  move :a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    eapply regularity in ha.
+    move : ha => [i].
+    move /Bind_Inv => [j][h _].
+    by move /E_Refl /Su_Eq in h.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Proj2_Inv Γ (a : PTm) U :
+  Γ ⊢ PProj PR a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
+Proof.
+  move E : (PProj PR a) => u hu.
+  move :a E. elim : Γ u U / hu => //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    have ha' := ha.
+    eapply regularity in ha.
+    move : ha => [i ha].
+    move /T_Proj1 in ha'.
+    apply : bind_inst; eauto.
+    apply : E_Refl ha'.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Pair_Inv Γ (a b : PTm ) U :
+  Γ ⊢ PPair a b ∈ U ->
+  exists A B, Γ ⊢ a ∈ A /\
+         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
+         Γ ⊢ PBind PSig A B ≲ U.
+Proof.
+  move E : (PPair a b) => u hu.
+  move : a b E. elim : Γ u U / hu => //=.
+  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
+    exists A,B. repeat split => //=.
+    move /E_Refl /Su_Eq : hS. apply.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+Proof.
+  move => a b Γ A.
+  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move /Su_Sig_Proj1 in hS.
+  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair1; eauto.
+Qed.
+
+Lemma E_ProjPair2 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PR (PPair a b) ∈ A -> Γ ⊢ PProj PR (PPair a b) ≡ b ∈ A.
+Proof.
+  move => a b Γ A. move /Proj2_Inv.
+  move => [A0][B0][ha]h.
+  have hr := ha.
+  move /Pair_Inv : ha => [A1][B1][ha][hb]hU.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity.
+  have /E_Symmetric : Γ ⊢ (PProj PL (PPair a b)) ≡ a ∈ A1 by eauto using  E_ProjPair1 with wt.
+  move /Su_Sig_Proj2 : hU. repeat move/[apply]. move => hB.
+  apply : E_Conv; eauto.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair2; eauto.
+Qed.
+
+
+Lemma E_PairEta Γ a A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PPair (PProj PL a) (PProj PR a) ≡ a ∈ PBind PSig A B.
+Proof.
+  move => h.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto use:regularity.
+  apply E_PairExt => //.
+  eapply T_Pair; eauto with wt.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto with wt.
+  apply E_ProjPair2.
+  apply : T_Proj2; eauto with wt.
+Qed.

theories/algorithmic.v

@@ -608,13 +608,12 @@ Proof.
     have /regularity_sub0 [i' hPi0] := hPi.
     have : Γ ⊢ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ≡ u ∈ PBind PPi A2 B2.
     apply : E_AppEta; eauto.
-    hauto l:on use:regularity.
     apply T_Conv with (A := A);eauto.
     eauto using Su_Eq.
     move => ?.
     suff : Γ ⊢ PAbs a ≡ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ∈ PBind PPi A2 B2
       by eauto using E_Transitive.
-    apply : E_Abs; eauto. hauto l:on use:regularity.
+    apply : E_Abs; eauto.
     apply iha.
     move /Su_Pi_Proj2_Var in hPi'.
     apply : T_Conv; eauto.
@@ -666,7 +665,7 @@ Proof.
     have hA02 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Sig_Proj1.
     have hu'  : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
     move => [:ih0'].
-    apply : E_Transitive; last (apply E_Symmetric; apply : E_PairEta).
+    apply : E_Transitive; last (apply : E_PairEta).
     apply : E_Pair; eauto. hauto l:on use:regularity.
     abstract : ih0'.
     apply ih0. apply : T_Conv; eauto.
@@ -679,7 +678,6 @@ Proof.
     move /E_Symmetric in ih0'.
     move /regularity_sub0 in hA'.
     hauto l:on use:bind_inst.
-    hauto l:on use:regularity.
     eassumption.
   (* Same as before *)
   - move {hAppL}.

theories/preservation.v

@@ -4,51 +4,6 @@ Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Lemma Proj1_Inv Γ (a : PTm ) U :
-  Γ ⊢ PProj PL a ∈ U ->
-  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
-Proof.
-  move E : (PProj PL a) => u hu.
-  move :a E. elim : Γ u U / hu => //=.
-  - move => Γ a A B ha _ a0 [*]. subst.
-    exists A, B. split => //=.
-    eapply regularity in ha.
-    move : ha => [i].
-    move /Bind_Inv => [j][h _].
-    by move /E_Refl /Su_Eq in h.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Proj2_Inv Γ (a : PTm) U :
-  Γ ⊢ PProj PR a ∈ U ->
-  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
-Proof.
-  move E : (PProj PR a) => u hu.
-  move :a E. elim : Γ u U / hu => //=.
-  - move => Γ a A B ha _ a0 [*]. subst.
-    exists A, B. split => //=.
-    have ha' := ha.
-    eapply regularity in ha.
-    move : ha => [i ha].
-    move /T_Proj1 in ha'.
-    apply : bind_inst; eauto.
-    apply : E_Refl ha'.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
-
-Lemma Pair_Inv Γ (a b : PTm ) U :
-  Γ ⊢ PPair a b ∈ U ->
-  exists A B, Γ ⊢ a ∈ A /\
-         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
-         Γ ⊢ PBind PSig A B ≲ U.
-Proof.
-  move E : (PPair a b) => u hu.
-  move : a b E. elim : Γ u U / hu => //=.
-  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
-    exists A,B. repeat split => //=.
-    move /E_Refl /Su_Eq : hS. apply.
-  - hauto lq:on rew:off ctrs:LEq.
-Qed.
 
 Lemma Ind_Inv Γ P (a : PTm) b c U :
   Γ ⊢ PInd P a b c ∈ U ->
@@ -91,34 +46,6 @@ Proof.
   asimpl. rewrite !subst_scons_id. by apply E_Symmetric.
 Qed.
 
-Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
-    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
-Proof.
-  move => a b Γ A.
-  move /Proj1_Inv. move => [A0][B0][hab]hA0.
-  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
-  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
-  move /Su_Sig_Proj1 in hS.
-  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
-  apply : E_Conv; eauto.
-  apply : E_ProjPair1; eauto.
-Qed.
-
-Lemma E_ProjPair2 : forall (a b : PTm) Γ (A : PTm),
-    Γ ⊢ PProj PR (PPair a b) ∈ A -> Γ ⊢ PProj PR (PPair a b) ≡ b ∈ A.
-Proof.
-  move => a b Γ A. move /Proj2_Inv.
-  move => [A0][B0][ha]h.
-  have hr := ha.
-  move /Pair_Inv : ha => [A1][B1][ha][hb]hU.
-  have [i hSig] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity.
-  have /E_Symmetric : Γ ⊢ (PProj PL (PPair a b)) ≡ a ∈ A1 by eauto using  E_ProjPair1 with wt.
-  move /Su_Sig_Proj2 : hU. repeat move/[apply]. move => hB.
-  apply : E_Conv; eauto.
-  apply : E_Conv; eauto.
-  apply : E_ProjPair2; eauto.
-Qed.
-
 Lemma E_Pair Γ a0 b0 a1 b1 A B i :
   Γ ⊢ PBind PSig A B ∈ PUniv i ->
   Γ ⊢ a0 ≡ a1 ∈ A ->