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

Write down the statement for ST_Ind

Browse source
This commit is contained in:
Yiyun Liu 2025-02-23 16:01:45 -05:00
parent 4e9a5582d2
commit 8df64ef989
1 changed files with 37 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

37
theories/logrel.v
View file

@ -1282,6 +1282,43 @@ Proof.
apply ST_Univ'. lia.
Qed.
Lemma ST_Nat n Γ i :
Γ ⊨ PNat : PTm n ∈ PUniv i.
Proof.
move => ?. apply SemWt_Univ. move => ρ hρ.
eexists. by apply InterpUniv_Nat.
Qed.
Lemma ST_Zero n Γ :
Γ ⊨ PZero : PTm n ∈ PNat.
Proof.
move => ρ hρ. exists 0, SNat. simpl. split.
apply InterpUniv_Nat.
apply S_Zero.
Qed.
Lemma ST_Suc n Γ (a : PTm n) :
Γ ⊨ a ∈ PNat ->
Γ ⊨ PSuc a ∈ PNat.
Proof.
move => ha ρ.
move : ha => /[apply] /=.
move => [k][PA][h0 h1].
move /InterpUniv_Nat_inv : h0 => ?. subst.
exists 0, SNat. split. apply InterpUniv_Nat.
eauto using S_Suc.
Qed.
Lemma ST_Ind n Γ P (a : PTm n) 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 a b c ∈ subst_PTm (scons a VarPTm) P.
Proof.
Admitted.
Lemma SSu_Univ n Γ i j :
i <= j ->
Γ ⊨ PUniv i : PTm n ≲ PUniv j.