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

Finish normalization

Browse source
This commit is contained in:
Yiyun Liu 2025-01-09 16:17:38 -05:00
parent 0d3b751a33
commit e75d7745fe
1 changed files with 34 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
theories/logrel.v
View file

@ -638,7 +638,7 @@ Proof.
rewrite /ρ_ok in hρ. rewrite /ρ_ok in hρ.
move => h. move => h.
rewrite /funcomp. rewrite /funcomp.
apply hρ with (m := m'). apply hρ with (k := m').
move : h. rewrite -hξ. move : h. rewrite -hξ.
by asimpl. by asimpl.
Qed. Qed.
@ -663,6 +663,17 @@ Proof.
hauto lq:on inv:option unfold:renaming_ok. hauto lq:on inv:option unfold:renaming_ok.
Qed. Qed.
Lemma SemWt_Wn n Γ (a : Tm n) A :
Γ ⊨ a ∈ A ->
wn a /\ wn A.
Proof.
move => h.
have {}/h := ρ_ok_bot _ Γ => h.
have h0 : wn (subst_Tm (fun _ : fin n => (Bot : Tm 0)) A) by hauto l:on use:adequacy.
have h1 : wn (subst_Tm (fun _ : fin n => (Bot : Tm 0)) a)by hauto l:on use:adequacy_wn.
move {h}. hauto lq:on use:wn_antirenaming.
Qed.
Lemma SemWt_Univ n Γ (A : Tm n) i : Lemma SemWt_Univ n Γ (A : Tm n) i :
Γ ⊨ A ∈ Univ i <-> Γ ⊨ A ∈ Univ i <->
forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_Tm ρ A ⟧ i ↘ S. forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_Tm ρ A ⟧ i ↘ S.
@ -787,7 +798,7 @@ Proof.
simpl in hPPi. simpl in hPPi.
move /InterpUniv_Bind_inv_nopf : hPPi. move /InterpUniv_Bind_inv_nopf : hPPi.
move => [PA [hPA [hTot ?]]]. subst=>/=. move => [PA [hPA [hTot ?]]]. subst=>/=.
rewrite /SumSpace. rewrite /SumSpace. right.
exists (subst_Tm ρ a), (subst_Tm ρ b). exists (subst_Tm ρ a), (subst_Tm ρ b).
split. split.
- hauto l:on use:Pars.substing. - hauto l:on use:Pars.substing.
@ -809,9 +820,10 @@ Proof.
move : h0 => [S][h2][h3]?. subst. move : h0 => [S][h2][h3]?. subst.
move : h1 => /=. move : h1 => /=.
rewrite /SumSpace. rewrite /SumSpace.
case; first by hauto lq:on use:adequacy_wne, wne_proj.
move => [a0 [b0 [h4 [h5 h6]]]]. move => [a0 [b0 [h4 [h5 h6]]]].
exists m, S. split => //=. exists m, S. split => //=.
have {}h4 : rtc RPar'.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPar's.ProjCong. have {}h4 : rtc RPar'.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars'.ProjCong.
have ? : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.refl, RPar'.ProjPair'. have ? : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.refl, RPar'.ProjPair'.
have : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r. have : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
move => h. move => h.
@ -837,17 +849,23 @@ Proof.
move : h0 => [S][h2][h3]?. subst. move : h0 => [S][h2][h3]?. subst.
move : h1 => /=. move : h1 => /=.
rewrite /SumSpace. rewrite /SumSpace.
move => [a0 [b0 [h4 [h5 h6]]]]. case.
specialize h3 with (1 := h5). - move => h.
move : h3 => [PB hPB]. have hp : forall p, wne (Proj p (subst_Tm ρ a)) by auto using wne_proj.
have hr : forall p, rtc RPar'.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPar's.ProjCong. have hp0 := hp PL. have hp1 := hp PR => {hp}.
have hrl : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.ProjPair', RPar'.refl. have : S (Proj PL (subst_Tm ρ a)) by hauto q:on use:adequacy_wne.
have hrr : RPar'.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar'.ProjPair', RPar'.refl. move /h3 => [PB]. asimpl. hauto lq:on use:adequacy_wne.
exists m, PB. - move => [a0 [b0 [h4 [h5 h6]]]].
asimpl. split. specialize h3 with (1 := h5).
- have h : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r. move : h3 => [PB hPB].
have {}h : rtc RPar'.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPar's. have hr : forall p, rtc RPar'.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars'.ProjCong.
move : hPB. asimpl. have hrl : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
eauto using InterpUnivN_back_preservation_star. have hrr : RPar'.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
- hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star. exists m, PB.
asimpl. split.
+ have h : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
have {}h : rtc RPar'.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPar's.
move : hPB. asimpl.
eauto using InterpUnivN_back_preservation_star.
+ hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.
Qed. Qed.