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

Add back preservation lemma for ered
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source 
Needed for justifying that the extended algorithm
This commit is contained in:
Yiyun Liu 2025-05-20 14:41:09 -04:00
parent 4c527c1b81
commit d2576f21fc
1 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
theories/fp_red.v
View file

@ -719,6 +719,8 @@ Module RRed.
move => */=; apply : IndSuc'; eauto. by asimpl.
Qed.
Lemma abs_preservation a b : isabs a -> R a b -> isabs b. hauto q:on inv:R. Qed.
End RRed.
Module RPar.
@ -1004,6 +1006,9 @@ Qed.
Module RReds.
Lemma abs_preservation a b : isabs a -> rtc RRed.R a b -> isabs b.
induction 2; hauto lq:on use:RRed.abs_preservation. Qed.
#[local]Ltac solve_s_rec :=
move => *; eapply rtc_l; eauto;
hauto lq:on ctrs:RRed.R.
@ -1755,6 +1760,15 @@ Module ERed.
Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
Lemma abs_back_preservation (a b : PTm) :
SN a -> R a b -> isabs b -> isabs a.
Proof.
move => + h.
elim : a b /h => //=.
case => //=. move => p. move /SN_NoForbid.P_PairInv.
sfirstorder use:SN_NoForbid.PProj_imp.
Qed.
Lemma ToEPar (a b : PTm) :
ERed.R a b -> EPar.R a b.
Proof.
@ -3292,7 +3306,6 @@ Module DJoin.
Qed.
End DJoin.
Module Sub1.
Inductive R : PTm -> PTm -> Prop :=
| Refl a :