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

Add syntactic typing rules

Browse source
This commit is contained in:
Yiyun Liu 2025-02-25 16:06:04 -05:00
parent 4dd2cd7cd8
commit b2aec9c6ce
2 changed files with 21 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
theories/logrel.v
View file

@ -1722,4 +1722,4 @@ Qed.
#[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv #[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_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 : 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 : sem.

20
theories/typing.v
View file

@ -115,6 +115,13 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
Γ ⊢ a ≡ b ∈ PBind PSig A B -> Γ ⊢ a ≡ b ∈ PBind PSig A B ->
Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
| E_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
Γ ⊢ a0 ≡ a1 ∈ PNat ->
Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
| E_Conv n Γ (a b : PTm n) A B : | E_Conv n Γ (a b : PTm n) A B :
Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ≡ b ∈ A ->
Γ ⊢ A ≲ B -> Γ ⊢ A ≲ B ->
@ -139,6 +146,19 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
| E_IndZero n Γ P i (b : PTm n) c :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P
| E_IndSuc s Γ P (a : PTm s) b c i :
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
Γ ⊢ a ∈ PNat ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons 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 *) (* Eta *)
| E_AppEta n Γ (b : PTm n) A B i : | E_AppEta n Γ (b : PTm n) A B i :
⊢ Γ -> ⊢ Γ ->