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

Finish the enhanced eta postponement

Browse source
This commit is contained in:
Yiyun Liu 2025-01-30 23:29:25 -05:00
parent 51ac5ffbd6
commit 5a7f46a8a1
1 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
theories/fp_red.v
View file

@ -1192,6 +1192,36 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
- hauto lq:on inv:RRed.R.
Qed.
Lemma η_postponement_star n a b c :
@P n a ->
ERed.R a b ->
rtc RRed.R b c ->
exists d, rtc RRed.R a d /\ ERed.R d c.
Proof.
move => + + h. move : a.
elim : b c / h.
- sfirstorder.
- move => a0 a1 a2 ha ha' iha u hu hu'.
move : eta_postponement (hu) ha hu'; repeat move/[apply].
move => [d [h0 h1]].
have : P d by sfirstorder use:P_RReds.
move : iha h1; repeat move/[apply].
sfirstorder use:@relations.rtc_transitive.
Qed.
Lemma η_postponement_star' n a b c :
@P n a ->
ERed.R a b ->
rtc RRed.R b c ->
exists d, rtc RRed.R a d /\ NeERed.R_nonelim d c.
Proof.
move => h0 h1 h2.
have : exists d, rtc RRed.R a d /\ ERed.R d c by eauto using η_postponement_star.
move => [d [h3 /η_split]].
move /(_ ltac:(eauto using P_RReds)).
sfirstorder use:@relations.rtc_transitive.
Qed.
End UniqueNF.
Lemma η_nf_to_ne n (a0 a1 : PTm n) :