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

Repair epar sn preservation

Browse source
This commit is contained in:
Yiyun Liu 2025-02-21 15:11:12 -05:00
parent 396bddc8b3
commit 2af49373e3
1 changed files with 21 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

21
theories/fp_red.v
View file

@ -517,6 +517,14 @@ Proof.
hauto lq:on rew:off inv:TRedSN db:sn. hauto lq:on rew:off inv:TRedSN db:sn.
Qed. Qed.
Lemma SN_IndInv : forall n P (a : PTm n) b c, SN (PInd P a b c) -> SN P /\ SN a /\ SN b /\ SN c.
Proof.
move => n P a b c. move E : (PInd P a b c) => u hu. move : P a b c E.
elim : n u / hu => //=.
hauto lq:on rew:off inv:SNe db:sn.
hauto lq:on rew:off inv:TRedSN db:sn.
Qed.
Lemma epar_sn_preservation n : Lemma epar_sn_preservation n :
(forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\ (forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\
(forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\ (forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\
@ -527,6 +535,7 @@ Proof.
- sauto lq:on. - sauto lq:on.
- sauto lq:on. - sauto lq:on.
- sauto lq:on. - sauto lq:on.
- sauto lq:on.
- move => a b ha iha hb ihb b0. - move => a b ha iha hb ihb b0.
inversion 1; subst. inversion 1; subst.
+ have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on. + have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
@ -545,6 +554,9 @@ Proof.
- sauto lq:on. - sauto lq:on.
- sauto lq:on. - sauto lq:on.
- sauto lq:on. - sauto lq:on.
- sauto lq:on.
- sauto lq:on.
- sauto lq:on.
- move => a b ha iha c h0. - move => a b ha iha c h0.
inversion h0; subst. inversion h0; subst.
inversion H1; subst. inversion H1; subst.
@ -576,6 +588,15 @@ Proof.
sauto lq:on. sauto lq:on.
+ sauto lq:on. + sauto lq:on.
- sauto. - sauto.
- sauto q:on.
- move => P a b c hP ihP ha iha hb ihb hc ihc u.
elim /EPar.inv => //=_.
move => P0 P1 a0 a1 b0 b1 c0 c1 hP0 ha0 hb0 hc0 [*]. subst.
elim /EPar.inv : ha0 => //=_.
move => a0 a2 ha0 [*]. subst.
eexists. split. apply T_Once. apply N_IndSuc; eauto.
hauto q:on ctrs:EPar.R use:EPar.morphing, EPar.refl inv:option.
- sauto q:on.
Qed. Qed.
Module RRed. Module RRed.