From 2b92845e3e00c4a3f1385c4f1c30cdd353b1e319 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 18 Apr 2025 16:38:34 -0400 Subject: [PATCH] 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.