yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add beta and eta rules to syntactic typing

Browse source
This commit is contained in:
Yiyun Liu 2025-02-09 16:33:43 -05:00
parent 133968dd23
commit 5b925e3fa1
2 changed files with 42 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
theories/logrel.v
View file

@ -1028,9 +1028,10 @@ Lemma SE_AppEta n Γ (b : PTm n) A B i :
⊨ Γ ->
Γ ⊨ PBind PPi A B ∈ (PUniv i) ->
Γ ⊨ b ∈ PBind PPi A B ->
Γ ⊨ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ∈ PBind PPi A B.
Γ ⊨ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B.
Proof.
move => hΓ h0 h1. apply : ST_Abs; eauto.
move => hΓ h0 h1. apply SemWt_SemEq; eauto.
apply : ST_Abs; eauto.
have hA : Γ ⊨ A ∈ PUniv i by eauto using SBind_inv1.
eapply ST_App' with (A := ren_PTm shift A)(B:= ren_PTm (upRen_PTm_PTm shift) B). by asimpl.
2 : {
@ -1040,6 +1041,7 @@ Proof.
change (PBind PPi (ren_PTm shift A) (ren_PTm (upRen_PTm_PTm shift) B)) with
(ren_PTm shift (PBind PPi A B)).
apply : weakening_Sem; eauto.
hauto q:on ctrs:rtc,RERed.R.
Qed.
Lemma SE_AppAbs n Γ (a : PTm (S n)) b A B i:
@ -1310,4 +1312,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 : 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 : sem.

37
theories/typing.v
View file

@ -48,6 +48,7 @@ Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
Γ ⊢ a ∈ B
with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
(* Structural *)
| E_Refl n Γ (a : PTm n) A :
Γ ⊢ a ∈ A ->
Γ ⊢ a ≡ a ∈ A
@ -61,6 +62,7 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
Γ ⊢ b ≡ c ∈ A ->
Γ ⊢ a ≡ c ∈ A
(* Congruence *)
| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
⊢ Γ ->
Γ ⊢ A0 ∈ PUniv i ->
@ -99,12 +101,45 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
Γ ⊢ A ≲ B ->
Γ ⊢ a ≡ b ∈ B
(* Beta *)
| E_AppAbs n Γ (a : PTm (S n)) b A B i:
Γ ⊢ PBind PPi A B ∈ PUniv i ->
Γ ⊢ b ∈ A ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
| E_ProjPair1 n Γ (a b : PTm n) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ A ->
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A
| E_ProjPair2 n Γ (a b : PTm n) A B i :
Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ A ->
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
(* Eta *)
| E_AppEta n Γ (b : PTm n) A B i :
⊢ Γ ->
Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
Γ ⊢ b ∈ PBind PPi A B ->
Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
| E_PairEta n Γ (a : PTm n) 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
with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
(* Structural *)
| Su_Transitive n Γ (A B C : PTm n) :
Γ ⊢ A ≲ B ->
Γ ⊢ B ≲ C ->
Γ ⊢ A ≲ C
(* Congruence *)
| Su_Univ n Γ i j :
⊢ Γ ->
i <= j ->
@ -122,10 +157,12 @@ with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 ->
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
(* Injecting from equalities *)
| Su_Eq n Γ (A : PTm n) B i :
Γ ⊢ A ≡ B ∈ PUniv i ->
Γ ⊢ A ≲ B
(* Projection axioms *)
| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
Γ ⊢ A1 ≲ A0