From e1fc6b609dd69dd4ae69f6b1146eab095a923e69 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 17 Apr 2025 15:22:45 -0400 Subject: [PATCH 1/8] Add the extensional representation of pair&abs equality rules --- theories/logrel.v | 2 +- theories/typing.v | 36 +++++++++++------------------------- 2 files changed, 12 insertions(+), 26 deletions(-) diff --git a/theories/logrel.v b/theories/logrel.v index fa50b9c..e11659e 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -1701,4 +1701,4 @@ Qed. #[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv SE_Refl SE_Symmetric SE_Transitive SE_Bind SE_Abs SE_App SE_Proj1 SE_Proj2 - SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong : sem. + SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong SE_PairExt SE_FunExt : sem. diff --git a/theories/typing.v b/theories/typing.v index ae78747..e911d51 100644 --- a/theories/typing.v +++ b/theories/typing.v @@ -89,23 +89,12 @@ with Eq : list PTm -> PTm -> PTm -> PTm -> Prop := (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i -> Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i -| E_Abs Γ (a b : PTm) A B i : - Γ ⊢ PBind PPi A B ∈ (PUniv i) -> - (cons A Γ) ⊢ a ≡ b ∈ B -> - Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B - | E_App Γ i (b0 b1 a0 a1 : PTm) A B : Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B -> Γ ⊢ a0 ≡ a1 ∈ A -> Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B -| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i : - Γ ⊢ PBind PSig A B ∈ (PUniv i) -> - Γ ⊢ a0 ≡ a1 ∈ A -> - Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B -> - Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B - | E_Proj1 Γ (a b : PTm) A B : Γ ⊢ a ≡ b ∈ PBind PSig A B -> Γ ⊢ PProj PL a ≡ PProj PL b ∈ A @@ -164,16 +153,20 @@ with Eq : list PTm -> PTm -> PTm -> PTm -> Prop := (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P -(* Eta *) -| E_AppEta Γ (b : PTm) A B i : - Γ ⊢ PBind PPi A B ∈ (PUniv i) -> +| E_FunExt Γ (a b : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ PUniv i -> + Γ ⊢ a ∈ PBind PPi A B -> Γ ⊢ b ∈ PBind PPi A B -> - Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B + A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B -> + Γ ⊢ a ≡ b ∈ PBind PPi A B -| E_PairEta Γ (a : PTm ) A B i : - Γ ⊢ PBind PSig A B ∈ (PUniv i) -> +| E_PairExt Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ PUniv i -> Γ ⊢ a ∈ PBind PSig A B -> - Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR 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 with LEq : list PTm -> PTm -> PTm -> Prop := (* Structural *) @@ -242,10 +235,3 @@ Scheme wf_ind := Induction for Wff Sort Prop with le_ind := Induction for LEq Sort Prop. Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind. - -(* Lemma lem : *) -(* (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *) -(* (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...) /\ *) -(* (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *) -(* (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *) -(* Proof. apply wt_mutual. ... *) From 7c985fa58e1080e94dcbd877b9bd64df22c7183e Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 17 Apr 2025 16:42:57 -0400 Subject: [PATCH 2/8] Minor --- theories/structural.v | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/theories/structural.v b/theories/structural.v index ccb4c6f..76f679b 100644 --- a/theories/structural.v +++ b/theories/structural.v @@ -137,12 +137,12 @@ Lemma E_ProjPair2' Γ (a b : PTm) A B i U : Γ ⊢ PProj PR (PPair a b) ≡ b ∈ U. Proof. move => ->. apply E_ProjPair2. Qed. -Lemma E_AppEta' Γ (b : PTm ) A B i u : - u = (PApp (ren_PTm shift b) (VarPTm var_zero)) -> - Γ ⊢ PBind PPi A B ∈ (PUniv i) -> - Γ ⊢ b ∈ PBind PPi A B -> - Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B. -Proof. qauto l:on use:wff_mutual, E_AppEta. Qed. +(* Lemma E_AppEta' Γ (b : PTm ) A B i u : *) +(* u = (PApp (ren_PTm shift b) (VarPTm var_zero)) -> *) +(* Γ ⊢ PBind PPi A B ∈ (PUniv i) -> *) +(* Γ ⊢ b ∈ PBind PPi A B -> *) +(* Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B. *) +(* Proof. qauto l:on use:wff_mutual, E_AppEta. Qed. *) Lemma Su_Pi_Proj2' Γ (a0 a1 A0 A1 : PTm ) B0 B1 U T : U = subst_PTm (scons a0 VarPTm) B0 -> @@ -222,17 +222,7 @@ Proof. - hauto lq:on ctrs:Wt,LEq. - hauto lq:on ctrs:Eq. - hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up. - - move => Γ a b A B i hPi ihPi ha iha Δ ξ hΔ hξ. - move : ihPi (hΔ) (hξ). repeat move/[apply]. - move => /Bind_Inv [j][h0][h1]h2. - have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt. - move {hPi}. - apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up. - move => *. apply : E_App'; eauto. by asimpl. - - move => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ξ hΔ hξ. - apply : E_Pair; eauto. - move : ihb hΔ hξ. repeat move/[apply]. - by asimpl. - move => *. apply : E_Proj2'; eauto. by asimpl. - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc. move => Δ ξ hΔ hξ [:hP' hren]. @@ -302,8 +292,10 @@ Proof. move /(_ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc. move /(_ ltac:(by eauto using renaming_up)). by asimpl. - - move => *. - apply : E_AppEta'; eauto. by asimpl. + - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ. + apply : E_FunExt; eauto. move : ihe1. asimpl. apply. + admit. + by apply renaming_up. - qauto l:on use:E_PairEta. - hauto lq:on ctrs:LEq. - qauto l:on ctrs:LEq. From 87b84794b470eecb4b056a8e1c0d4fb49834645c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 18 Apr 2025 14:13:46 -0400 Subject: [PATCH 3/8] Fix structural rules --- theories/structural.v | 37 +++++++++++-------------------------- 1 file changed, 11 insertions(+), 26 deletions(-) diff --git a/theories/structural.v b/theories/structural.v index 76f679b..207447d 100644 --- a/theories/structural.v +++ b/theories/structural.v @@ -294,9 +294,10 @@ Proof. by asimpl. - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ. apply : E_FunExt; eauto. move : ihe1. asimpl. apply. - admit. + hfcrush use:Bind_Inv. by apply renaming_up. - - qauto l:on use:E_PairEta. + - move => Γ a b A B i hPi ihPi ha iha hb ihb hL ihL hR ihR Δ ξ hΔ hξ. + apply : E_PairExt; eauto. move : ihR. asimpl. by apply. - hauto lq:on ctrs:LEq. - qauto l:on ctrs:LEq. - hauto lq:on ctrs:Wff use:renaming_up, Su_Pi. @@ -439,17 +440,7 @@ Proof. - hauto lq:on ctrs:Eq. - hauto lq:on ctrs:Eq. - hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up. - - move => Γ a b A B i hPi ihPi ha iha Δ ρ hΔ hρ. - move : ihPi (hΔ) (hρ). repeat move/[apply]. - move => /Bind_Inv [j][h0][h1]h2. - have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt. - move {hPi}. - apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up. - move => *. apply : E_App'; eauto. by asimpl. - - move => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ρ hΔ hρ. - apply : E_Pair; eauto. - move : ihb hΔ hρ. repeat move/[apply]. - by asimpl. - hauto q:on ctrs:Eq. - move => *. apply : E_Proj2'; eauto. by asimpl. - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc. @@ -516,9 +507,14 @@ Proof. move /(_ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc. move /(_ ltac:(sauto l:on use:morphing_up)). asimpl. substify. by asimpl. - - move => *. - apply : E_AppEta'; eauto. by asimpl. - - qauto l:on use:E_PairEta. + - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ. + move : ihPi (hΔ) (hξ); repeat move/[apply]. move /[dup] /Bind_Inv => ihPi ?. + decompose [and ex] ihPi. + apply : E_FunExt; eauto. move : ihe1. asimpl. apply. + by eauto with wt. + by eauto using morphing_up with wt. + - move => Γ a b A B i hPi ihPi ha iha hb ihb hL ihL hR ihR Δ ξ hΔ hξ. + apply : E_PairExt; eauto. move : ihR. asimpl. by apply. - hauto lq:on ctrs:LEq. - qauto l:on ctrs:LEq. - hauto lq:on ctrs:Wff use:morphing_up, Su_Pi. @@ -659,7 +655,6 @@ Proof. sfirstorder. apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric. hauto lq:on. - - hauto lq:on ctrs:Wt,Eq. - move => n i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]] ha [iha0 [iha1 [i1 iha2]]]. repeat split. @@ -669,7 +664,6 @@ Proof. move /E_Symmetric in ha. by eauto using bind_inst. hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt. - - hauto lq:on use:bind_inst db:wt. - hauto lq:on use:Bind_Inv db:wt. - move => Γ i a b A B hS _ hab [iha][ihb][j]ihs. repeat split => //=; eauto with wt. @@ -718,15 +712,6 @@ Proof. subst Ξ. move : morphing_wt hc; repeat move/[apply]. asimpl. by apply. sauto lq:on use:substing_wt. - - move => Γ b A B i hP _ hb [i0 ihb]. - repeat split => //=; eauto with wt. - have {}hb : (cons A Γ) ⊢ ren_PTm shift b ∈ ren_PTm shift (PBind PPi A B) - by hauto lq:on use:weakening_wt, Bind_Inv. - apply : T_Abs; eauto. - apply : T_App'; eauto; rewrite-/ren_PTm. asimpl. by rewrite subst_scons_id. - apply T_Var. sfirstorder use:wff_mutual. - apply here. - - hauto lq:on ctrs:Wt. - move => Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]]. have ? : ⊢ Γ by sfirstorder use:wff_mutual. exists (max i j). From d9282fb815a8b2c18df40b573c5c2f969e908b07 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 18 Apr 2025 15:42:40 -0400 Subject: [PATCH 4/8] Finish preservation --- theories/preservation.v | 88 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 86 insertions(+), 2 deletions(-) diff --git a/theories/preservation.v b/theories/preservation.v index c8a2106..2794909 100644 --- a/theories/preservation.v +++ b/theories/preservation.v @@ -1,4 +1,4 @@ -Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red. +Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red admissible. From Hammer Require Import Tactics. Require Import ssreflect. Require Import Psatz. @@ -112,6 +112,45 @@ Proof. eauto using T_Conv. Qed. +Lemma T_Eta Γ A a B : + A :: Γ ⊢ a ∈ B -> + A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B. +Proof. + move => ha. + have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual. + have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff. + have hΓ : ⊢ Γ by hauto lq:on inv:Wff. + eapply T_App' with (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id. + apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift. + econstructor; eauto. sauto l:on use:renaming. + apply T_Var => //. + by constructor. +Qed. + +Lemma E_Abs Γ a b A B : + A :: Γ ⊢ a ≡ b ∈ B -> + Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B. +Proof. + move => h. + have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto l:on use:wff_mutual inv:Wff. + have [j hB] : exists j, A :: Γ ⊢ B ∈ PUniv j by hauto l:on use:regularity. + have hΓ : ⊢ Γ by sfirstorder use:wff_mutual. + have hΓ' : ⊢ A::Γ by eauto with wt. + set k := max i j. + have [? ?] : i <= k /\ j <= k by lia. + have {}hA : Γ ⊢ A ∈ PUniv k by hauto l:on use:T_Conv, Su_Univ. + have {}hB : A :: Γ ⊢ B ∈ PUniv k by hauto lq:on use:T_Conv, Su_Univ. + have hPi : Γ ⊢ PBind PPi A B ∈ PUniv k by eauto with wt. + apply : E_FunExt; eauto with wt. + hauto lq:on rew:off use:regularity, T_Abs. + hauto lq:on rew:off use:regularity, T_Abs. + apply : E_Transitive => /=. apply E_AppAbs. + hauto lq:on use:T_Eta, regularity. + apply /E_Symmetric /E_Transitive. apply E_AppAbs. + hauto lq:on use:T_Eta, regularity. + 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. @@ -125,6 +164,51 @@ Proof. 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 -> + Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B -> + Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B. +Proof. + move => hSig ha hb. + have [ha0 ha1] : Γ ⊢ a0 ∈ A /\ Γ ⊢ a1 ∈ A by hauto l:on use:regularity. + have [hb0 hb1] : Γ ⊢ b0 ∈ subst_PTm (scons a0 VarPTm) B /\ + Γ ⊢ b1 ∈ subst_PTm (scons a0 VarPTm) B by hauto l:on use:regularity. + have hp : Γ ⊢ PPair a0 b0 ∈ PBind PSig A B by eauto with wt. + have hp' : Γ ⊢ PPair a1 b1 ∈ PBind PSig A B. econstructor; eauto with wt; [idtac]. + apply : T_Conv; eauto. apply : Su_Sig_Proj2; by eauto using Su_Eq, E_Refl. + have ea : Γ ⊢ PProj PL (PPair a0 b0) ≡ a0 ∈ A by eauto with wt. + have : Γ ⊢ PProj PR (PPair a0 b0) ≡ b0 ∈ subst_PTm (scons a0 VarPTm) B by eauto with wt. + have : Γ ⊢ PProj PL (PPair a1 b1) ≡ a1 ∈ A by eauto using E_ProjPair1 with wt. + have : Γ ⊢ PProj PR (PPair a1 b1) ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B. + apply : E_Conv; eauto using E_ProjPair2 with wt. + apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption. + apply : E_Transitive. apply E_ProjPair1. by eauto with wt. + by eauto using E_Symmetric. + move => *. + apply : E_PairExt; eauto using E_Symmetric, E_Transitive. + apply : E_Conv. by eauto using E_Symmetric, E_Transitive. + apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption. + apply : E_Transitive. by eauto. apply /E_Symmetric /E_Transitive. + by eauto using E_ProjPair1. + eauto. +Qed. + Lemma Suc_Inv Γ (a : PTm) A : Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A. Proof. @@ -159,7 +243,7 @@ Proof. apply : Su_Sig_Proj2; eauto. move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply]. move {hS}. - move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto. + move => ?. apply : E_Conv; eauto. apply : typing.E_ProjPair2; eauto. - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero. - move => P a b c Γ A. move /Ind_Inv. From 43daff1b278f9bf21cdc89f9a69faca2b0e0b82c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 18 Apr 2025 15:46:07 -0400 Subject: [PATCH 5/8] Fix soundness --- theories/soundness.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/soundness.v b/theories/soundness.v index 7f86852..877e3fb 100644 --- a/theories/soundness.v +++ b/theories/soundness.v @@ -7,7 +7,7 @@ Theorem fundamental_theorem : (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A) /\ (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\ (forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b). - apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair]. + apply wt_mutual; eauto with sem. Unshelve. all : exact 0. Qed. From 2b92845e3e00c4a3f1385c4f1c30cdd353b1e319 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 18 Apr 2025 16:38:34 -0400 Subject: [PATCH 6/8] Add E_AppEta --- theories/admissible.v | 112 ++++++++++++++++++++++++++++++++++++++++ theories/algorithmic.v | 3 +- theories/preservation.v | 60 --------------------- 3 files changed, 114 insertions(+), 61 deletions(-) diff --git a/theories/admissible.v b/theories/admissible.v index 830ceec..48c7cea 100644 --- a/theories/admissible.v +++ b/theories/admissible.v @@ -16,6 +16,70 @@ Proof. hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs. Qed. + +Lemma App_Inv Γ (b a : PTm) U : + Γ ⊢ PApp b a ∈ U -> + exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U. +Proof. + move E : (PApp b a) => u hu. + move : b a E. elim : Γ u U / hu => //=. + - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst. + exists A,B. + repeat split => //=. + have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity. + hauto lq:on use:bind_inst, E_Refl. + - hauto lq:on rew:off ctrs:LEq. +Qed. + + +Lemma Abs_Inv Γ (a : PTm) U : + Γ ⊢ PAbs a ∈ U -> + exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U. +Proof. + move E : (PAbs a) => u hu. + move : a E. elim : Γ u U / hu => //=. + - move => Γ a A B i hP _ ha _ a0 [*]. subst. + exists A, B. repeat split => //=. + hauto lq:on use:E_Refl, Su_Eq. + - hauto lq:on rew:off ctrs:LEq. +Qed. + + + +Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm), + Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A. +Proof. + move => a b Γ A ha. + move /App_Inv : ha. + move => [A0][B0][ha][hb]hS. + move /Abs_Inv : ha => [A1][B1][ha]hS0. + have hb' := hb. + move /E_Refl in hb. + have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1. + have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0. + move : Su_Pi_Proj2 hS0 hb; repeat move/[apply]. + move : hS => /[swap]. move : Su_Transitive. repeat move/[apply]. + move => h. + apply : E_Conv; eauto. + apply : E_AppAbs; eauto. + eauto using T_Conv. +Qed. + +Lemma T_Eta Γ A a B : + A :: Γ ⊢ a ∈ B -> + A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B. +Proof. + move => ha. + have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual. + have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff. + have hΓ : ⊢ Γ by hauto lq:on inv:Wff. + eapply T_App' with (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id. + apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift. + econstructor; eauto. sauto l:on use:renaming. + apply T_Var => //. + by constructor. +Qed. + Lemma E_Bind Γ i p (A0 A1 : PTm) B0 B1 : Γ ⊢ A0 ≡ A1 ∈ PUniv i -> (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i -> @@ -46,3 +110,51 @@ Proof. have [i] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto l:on use:regularity. move : E_Proj2 h; by repeat move/[apply]. Qed. + +Lemma E_FunExt Γ (a b : PTm) A B : + Γ ⊢ a ∈ PBind PPi A B -> + Γ ⊢ b ∈ PBind PPi A B -> + A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B -> + Γ ⊢ a ≡ b ∈ PBind PPi A B. +Proof. + hauto l:on use:regularity, E_FunExt. +Qed. + +Lemma E_AppEta Γ (b : PTm) A B : + Γ ⊢ b ∈ PBind PPi A B -> + Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B. +Proof. + move => h. + have [i hPi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity. + have [j [hA hB]] : exists i, Γ ⊢ A ∈ PUniv i /\ A :: Γ ⊢ B ∈ PUniv i by hauto lq:on use:Bind_Inv. + have {i} {}hPi : Γ ⊢ PBind PPi A B ∈ PUniv j by sfirstorder use:T_Bind, wff_mutual. + have hΓ : ⊢ A :: Γ by hauto lq:on use:Bind_Inv, Wff_Cons'. + have hΓ' : ⊢ ren_PTm shift A :: A :: Γ by sauto lq:on use:renaming, renaming_shift inv:Wff. + apply E_FunExt; eauto. + apply T_Abs. + eapply T_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id. + change (PBind _ _ _) with (ren_PTm shift (PBind PPi A B)). + + eapply renaming; eauto. + apply renaming_shift. + constructor => //. + by constructor. + + apply : E_Transitive. simpl. + apply E_AppAbs' with (i := j)(A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B); eauto. + by asimpl; rewrite subst_scons_id. + hauto q:on use:renaming, renaming_shift. + constructor => //. + by constructor. + asimpl. + eapply T_App' with (A := ren_PTm shift (ren_PTm shift A)) (B := ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B)); cycle 2. + constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift. + by constructor. asimpl. substify. by asimpl. + have -> : PBind PPi (ren_PTm shift (ren_PTm shift A)) (ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B))= (ren_PTm (funcomp shift shift) (PBind PPi A B)) by asimpl. + eapply renaming; eauto. admit. + asimpl. renamify. + eapply E_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id. + hauto q:on use:renaming, renaming_shift. + sauto lq:on use:renaming, renaming_shift, E_Refl. + constructor. constructor=>//. constructor. +Admitted. diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 184872d..cca7cfa 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -586,7 +586,8 @@ Proof. have [h2 h3] : Γ ⊢ A2 ≲ A0 /\ Γ ⊢ A2 ≲ A1 by hauto l:on use:Su_Pi_Proj1. apply E_Conv with (A := PBind PPi A2 B2); cycle 1. eauto using E_Symmetric, Su_Eq. - apply : E_Abs; eauto. hauto l:on use:regularity. + apply : E_Abs; eauto. + apply iha. move /Su_Pi_Proj2_Var in hp0. apply : T_Conv; eauto. diff --git a/theories/preservation.v b/theories/preservation.v index 2794909..2722ee7 100644 --- a/theories/preservation.v +++ b/theories/preservation.v @@ -4,32 +4,6 @@ Require Import ssreflect. Require Import Psatz. Require Import Coq.Logic.FunctionalExtensionality. -Lemma App_Inv Γ (b a : PTm) U : - Γ ⊢ PApp b a ∈ U -> - exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U. -Proof. - move E : (PApp b a) => u hu. - move : b a E. elim : Γ u U / hu => //=. - - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst. - exists A,B. - repeat split => //=. - have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity. - hauto lq:on use:bind_inst, E_Refl. - - hauto lq:on rew:off ctrs:LEq. -Qed. - -Lemma Abs_Inv Γ (a : PTm) U : - Γ ⊢ PAbs a ∈ U -> - exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U. -Proof. - move E : (PAbs a) => u hu. - move : a E. elim : Γ u U / hu => //=. - - move => Γ a A B i hP _ ha _ a0 [*]. subst. - exists A, B. repeat split => //=. - hauto lq:on use:E_Refl, Su_Eq. - - hauto lq:on rew:off ctrs:LEq. -Qed. - Lemma Proj1_Inv Γ (a : PTm ) U : Γ ⊢ PProj PL a ∈ U -> exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U. @@ -93,40 +67,6 @@ Proof. - hauto lq:on rew:off ctrs:LEq. Qed. -Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm), - Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A. -Proof. - move => a b Γ A ha. - move /App_Inv : ha. - move => [A0][B0][ha][hb]hS. - move /Abs_Inv : ha => [A1][B1][ha]hS0. - have hb' := hb. - move /E_Refl in hb. - have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1. - have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0. - move : Su_Pi_Proj2 hS0 hb; repeat move/[apply]. - move : hS => /[swap]. move : Su_Transitive. repeat move/[apply]. - move => h. - apply : E_Conv; eauto. - apply : E_AppAbs; eauto. - eauto using T_Conv. -Qed. - -Lemma T_Eta Γ A a B : - A :: Γ ⊢ a ∈ B -> - A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B. -Proof. - move => ha. - have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual. - have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff. - have hΓ : ⊢ Γ by hauto lq:on inv:Wff. - eapply T_App' with (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id. - apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift. - econstructor; eauto. sauto l:on use:renaming. - apply T_Var => //. - by constructor. -Qed. - Lemma E_Abs Γ a b A B : A :: Γ ⊢ a ≡ b ∈ B -> Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B. From 8e083aad4b83f8013a80b38f7fb6df69197241ac Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sat, 19 Apr 2025 00:07:48 -0400 Subject: [PATCH 7/8] Add renaming_comp --- theories/admissible.v | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/theories/admissible.v b/theories/admissible.v index 48c7cea..e7f0769 100644 --- a/theories/admissible.v +++ b/theories/admissible.v @@ -120,6 +120,14 @@ Proof. hauto l:on use:regularity, E_FunExt. Qed. +Lemma renaming_comp Γ Δ Ξ ξ0 ξ1 : + renaming_ok Γ Δ ξ0 -> renaming_ok Δ Ξ ξ1 -> + renaming_ok Γ Ξ (funcomp ξ0 ξ1). + rewrite /renaming_ok => h0 h1 i A. + move => {}/h1 {}/h0. + by asimpl. +Qed. + Lemma E_AppEta Γ (b : PTm) A B : Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B. @@ -151,10 +159,10 @@ Proof. constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift. by constructor. asimpl. substify. by asimpl. have -> : PBind PPi (ren_PTm shift (ren_PTm shift A)) (ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B))= (ren_PTm (funcomp shift shift) (PBind PPi A B)) by asimpl. - eapply renaming; eauto. admit. + eapply renaming; eauto. by eauto using renaming_shift, renaming_comp. asimpl. renamify. eapply E_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id. hauto q:on use:renaming, renaming_shift. sauto lq:on use:renaming, renaming_shift, E_Refl. constructor. constructor=>//. constructor. -Admitted. +Qed. From 0e04a7076b069ab311fde2239ac8940eabcbdf60 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sat, 19 Apr 2025 00:24:09 -0400 Subject: [PATCH 8/8] Prove PairEta --- theories/admissible.v | 96 +++++++++++++++++++++++++++++++++++++++++ theories/algorithmic.v | 6 +-- theories/preservation.v | 73 ------------------------------- 3 files changed, 98 insertions(+), 77 deletions(-) diff --git a/theories/admissible.v b/theories/admissible.v index e7f0769..3e48d49 100644 --- a/theories/admissible.v +++ b/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. diff --git a/theories/algorithmic.v b/theories/algorithmic.v index cca7cfa..4e4e6fd 100644 --- a/theories/algorithmic.v +++ b/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}. diff --git a/theories/preservation.v b/theories/preservation.v index 2722ee7..301553e 100644 --- a/theories/preservation.v +++ b/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 ->