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

Finish all Bind proj lemmas

Browse source
This commit is contained in:
Yiyun Liu 2025-02-06 16:20:56 -05:00
parent c25bac311c
commit e7a26e6bd6
1 changed files with 21 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
theories/logrel.v
View file

@ -926,41 +926,34 @@ Lemma SBind_inv1 n Γ i p (A : PTm n) B :
hauto lq:on rew:off use:InterpUniv_Bind_inv.
Qed.
Lemma SBind_inv2 n Γ i p (A : PTm n) B :
Γ ⊨ PBind p A B ∈ PUniv i ->
funcomp (ren_PTm shift) (scons A Γ) ⊨ B ∈ PUniv i.
move /SemWt_Univ => h. apply SemWt_Univ.
move => ρ hρ.
set ρ' := funcomp ρ shift.
move /(_ ρ') : h.
have : ρ_ok Γ ρ'.
move => k.
subst ρ'.
rewrite /ρ_ok in hρ.
move => l PA. move => /(_ (shift k) l PA) in hρ.
move : hρ. asimpl. rewrite /funcomp. hauto lq:on.
move /[swap]/[apply].
move => /= [S hS].
move /InterpUniv_Bind_inv_nopf : hS.
move => [PA][hPA][hPF]?. subst.
subst ρ'.
Qed.
Lemma Bind_Proj1 n Γ p (A0 A1 : PTm n) B0 B1 i :
Γ ⊨ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i ->
Γ ⊨ A0 ≡ A1 ∈ PUniv i.
Proof.
move /SemEq_SemWt => [h0][h1]he.
apply SemWt_SemEq; eauto using SBind_inv.
apply SemWt_SemEq; eauto using SBind_inv1.
move /DJoin.bind_inj : he. tauto.
Qed.
Lemma Bind_Proj2' n Γ p (A0 A1 : PTm n) B0 B1 i :
Lemma Bind_Proj2 n Γ p (a0 a1 A0 A1 : PTm n) B0 B1 i :
Γ ⊨ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i ->
funcomp (ren_PTm shift) (scons A0 Γ) ⊨ B0 ≡ B1 ∈ PUniv i.
Γ ⊨ a0 ≡ a1 ∈ A0 ->
Γ ⊨ subst_PTm (scons a0 VarPTm) B0 ≡ subst_PTm (scons a1 VarPTm) B1 ∈ PUniv i.
Proof.
move /SemEq_SemWt => [h0][h1]he.
apply SemWt_SemEq; last by hauto l:on use:DJoin.bind_inj.
move /SemEq_SemWt => [hA][hB]/DJoin.bind_inj [_ [h1 h2]] /SemEq_SemWt [ha0][ha1]ha.
move : h2 => [B [h2 h2']].
move : ha => [c [ha ha']].
apply SemWt_SemEq; eauto using SBind_inst.
apply SBind_inst with (p := p) (A := A1); eauto.
apply : ST_Conv; eauto. hauto l:on use:SBind_inv1.
rewrite /DJoin.R.
eexists. split.
apply : relations.rtc_transitive.
apply REReds.substing. apply h2.
apply REReds.cong.
have : forall i0, rtc RERed.R (scons a0 VarPTm i0) (scons c VarPTm i0) by hauto q:on ctrs:rtc inv:option.
apply.
apply : relations.rtc_transitive. apply REReds.substing; eauto.
apply REReds.cong.
hauto lq:on ctrs:rtc inv:option.
Qed.