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

One remaining case for eta postponement

Browse source
This commit is contained in:
Yiyun Liu 2025-02-22 00:10:18 -05:00
parent 29d05befe9
commit d9d0e9cdd4
1 changed files with 22 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

31
theories/fp_red.v
View file

@ -1273,6 +1273,7 @@ Module Type NoForbid.
Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b.
Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a.
Axiom P_SucInv : forall n (a : PTm n), P (PSuc a) -> P a.
Axiom P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B. Axiom P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B.
Axiom P_IndInv : forall n Q (a : PTm n) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c. Axiom P_IndInv : forall n Q (a : PTm n) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c.
@ -1342,6 +1343,9 @@ Module SN_NoForbid <: NoForbid.
move : p A B E. elim : n u /hu=>//=;sauto lq:on rew:off. move : p A B E. elim : n u /hu=>//=;sauto lq:on rew:off.
Qed. Qed.
Lemma P_SucInv : forall n (a : PTm n), P (PSuc a) -> P a.
Proof. sauto lq:on. Qed.
Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a.
Proof. Proof.
move => n a. move E : (PAbs a) => u h. move => n a. move E : (PAbs a) => u h.
@ -1488,7 +1492,6 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
move => [b01][ihb0]ihb1. move => [b01][ihb0]ihb1.
move : ihc => /[apply]. move : ihc => /[apply].
move => [c01][ihc0]ihc1. move => [c01][ihc0]ihc1.
exists
case /orP : (orNb (ishf a01)) => [h|]. case /orP : (orNb (ishf a01)) => [h|].
+ eexists. split. by eauto using RReds.IndCong. + eexists. split. by eauto using RReds.IndCong.
hauto q:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf. hauto q:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
@ -1497,16 +1500,15 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
* move /norP. * move /norP.
have : P (PInd P01 a01 b01 c01) by eauto using P_RReds, RReds.IndCong. have : P (PInd P01 a01 b01 c01) by eauto using P_RReds, RReds.IndCong.
hauto lq:on use:PInd_imp. hauto lq:on use:PInd_imp.
* case /orP. * move => ha01.
admit. eexists. split. eauto using RReds.IndCong.
move {h}. apply NeEPar.IndCong; eauto.
case : a01 iha0 iha1 => //=. move : iha1 ha01. clear.
inversion 1; subst => //=; hauto lq:on ctrs:NeEPar.R_elim.
best b:on use:PInd_imp. - hauto l:on.
- hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.SucCong, P_SucInv.
Qed. Qed.
Lemma eta_postponement n a b c : Lemma eta_postponement n a b c :
@P n a -> @P n a ->
EPar.R a b -> EPar.R a b ->
@ -1612,6 +1614,17 @@ best b:on use:PInd_imp.
- hauto lq:on inv:RRed.R ctrs:rtc. - hauto lq:on inv:RRed.R ctrs:rtc.
- sauto lq:on ctrs:EPar.R, rtc use:RReds.BindCong, P_BindInv, @relations.rtc_transitive. - sauto lq:on ctrs:EPar.R, rtc use:RReds.BindCong, P_BindInv, @relations.rtc_transitive.
- hauto lq:on inv:RRed.R ctrs:rtc. - hauto lq:on inv:RRed.R ctrs:rtc.
- hauto q:on ctrs:rtc inv:RRed.R.
- move => n P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc u.
admit.
- hauto lq:on inv:RRed.R ctrs:rtc, EPar.R.
- move => n a0 a1 ha iha u /P_SucInv ha0.
elim /RRed.inv => //= _ a2 a3 h [*]. subst.
move : iha (ha0) (h); repeat move/[apply].
move => [a2 [ih0 ih1]].
exists (PSuc a2).
split. by apply RReds.SucCong.
by apply EPar.SucCong.
Qed. Qed.
Lemma η_postponement_star n a b c : Lemma η_postponement_star n a b c :