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

Finish soundness proof

Browse source
This commit is contained in:
Yiyun Liu 2025-02-08 22:52:50 -05:00
parent 0c83044d72
commit 932662d5d9
2 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
theories/logrel.v
View file

@ -1120,7 +1120,7 @@ Proof.
qauto l:on use:SemWt_SemLEq, Sub.transitive. qauto l:on use:SemWt_SemLEq, Sub.transitive.
Qed. Qed.
Lemma ST_Univ n Γ i j : Lemma ST_Univ' n Γ i j :
i < j -> i < j ->
Γ ⊨ PUniv i : PTm n ∈ PUniv j. Γ ⊨ PUniv i : PTm n ∈ PUniv j.
Proof. Proof.
@ -1128,6 +1128,12 @@ Proof.
apply SemWt_Univ. move => ρ hρ. eexists. by apply InterpUniv_Univ. apply SemWt_Univ. move => ρ hρ. eexists. by apply InterpUniv_Univ.
Qed. Qed.
Lemma ST_Univ n Γ i :
Γ ⊨ PUniv i : PTm n ∈ PUniv (S i).
Proof.
apply ST_Univ'. lia.
Qed.
Lemma SSu_Univ n Γ i j : Lemma SSu_Univ n Γ i j :
i <= j -> i <= j ->
Γ ⊨ PUniv i : PTm n ≲ PUniv j. Γ ⊨ PUniv i : PTm n ≲ PUniv j.
@ -1227,4 +1233,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 SemWff_nil SemWff_cons : 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 : sem.

7
theories/soundness.v
View file

@ -5,7 +5,8 @@ From Hammer Require Import Tactics.
Theorem fundamental_theorem : Theorem fundamental_theorem :
(forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\ (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\
(forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A) /\ (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A) /\
(forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A). (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
apply wt_mutual; eauto with sem;[idtac]. (forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
hauto l:on use:SE_Pair. apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
Unshelve. all : exact 0.
Qed. Qed.