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

Add renaming_comp

Browse source
This commit is contained in:
Yiyun Liu 2025-04-19 00:07:48 -04:00
parent 2b92845e3e
commit 8e083aad4b
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
theories/admissible.v
View file

@ -120,6 +120,14 @@ Proof.
hauto l:on use:regularity, E_FunExt. hauto l:on use:regularity, E_FunExt.
Qed. 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 : Lemma E_AppEta Γ (b : PTm) A B :
Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ b ∈ PBind PPi A B ->
Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ 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. constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift.
by constructor. asimpl. substify. by asimpl. 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. 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. 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. 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. hauto q:on use:renaming, renaming_shift.
sauto lq:on use:renaming, renaming_shift, E_Refl. sauto lq:on use:renaming, renaming_shift, E_Refl.
constructor. constructor=>//. constructor. constructor. constructor=>//. constructor.
Admitted. Qed.