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

Finish the split lemma up to strong normalization

Browse source
This commit is contained in:
Yiyun Liu 2025-01-29 15:52:05 -05:00
parent 710b59fd8f
commit 5f619c0980
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
theories/fp_red.v
View file

@ -699,7 +699,23 @@ Proof.
* admit. * admit.
- hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong. - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong.
- move => n p a0 a1 ha [a2 [iha0 iha1]]. - move => n p a0 a1 ha [a2 [iha0 iha1]].
case /orP : (orNb (ishf a2)) => [h|].
exists (PProj p a2).
split. eauto using RReds.ProjCong.
qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf.
case : a2 iha0 iha1 => //=.
+ move => u iha0 iha1 _.
(* Impossible by SN *)
admit.
+ move => u0 u1 iha0 iha1 _.
inversion iha1; subst.
* exists (PProj p a2). split.
apply : rtc_r.
apply RReds.ProjCong; eauto.
clear. hauto l:on inv:PTag.
hauto lq:on ctrs:NeERed.R_nonelim.
* hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong.
- hauto lq:on ctrs:rtc, NeERed.R_nonelim. - hauto lq:on ctrs:rtc, NeERed.R_nonelim.
Admitted. Admitted.