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

Add lemmas that bad forms are impossible

Browse source
This commit is contained in:
Yiyun Liu 2025-01-29 12:19:45 -05:00
parent 5ea75052a5
commit a27c41c5d1
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
theories/fp_red.v
View file

@ -147,6 +147,26 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
TRedSN a b -> TRedSN a b ->
TRedSN (PProj p a) (PProj p b). TRedSN (PProj p a) (PProj p b).
Lemma PProjAbs_imp n p (a : PTm (S n)) :
~ SN (PProj p (PAbs a)).
Proof.
move E : (PProj p (PAbs a)) => u hu.
move : p a E.
elim : n u / hu=>//=.
hauto lq:on inv:SNe.
hauto lq:on inv:TRedSN.
Qed.
Lemma PProjPair_imp n (a b0 b1 : PTm n ) :
~ SN (PApp (PPair b0 b1) a).
Proof.
move E : (PApp (PPair b0 b1) a) => u hu.
move : a b0 b1 E.
elim : n u / hu=>//=.
hauto lq:on inv:SNe.
hauto lq:on inv:TRedSN.
Qed.
Scheme sne_ind := Induction for SNe Sort Prop Scheme sne_ind := Induction for SNe Sort Prop
with sn_ind := Induction for SN Sort Prop with sn_ind := Induction for SN Sort Prop
with sred_ind := Induction for TRedSN Sort Prop. with sred_ind := Induction for TRedSN Sort Prop.
@ -531,6 +551,8 @@ Proof.
- scongruence b:on. - scongruence b:on.
Qed. Qed.
Lemma η_nf'' n (a b : PTm n) : ERed'.R a b -> nf b -> nf a \/ rtc RRed.R a b. Lemma η_nf'' n (a b : PTm n) : ERed'.R a b -> nf b -> nf a \/ rtc RRed.R a b.
Proof. Proof.
move => h. move => h.