Finish the enhanced eta postponement

theories/fp_red.v

@@ -144,16 +144,6 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
 
 Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop.
 
-Inductive SNe' {n} : PTm n -> Prop :=
-| N_Var' i :
-  SNe' (VarPTm i)
-| N_App' a b :
-  SNe a ->
-  SNe' (PApp a b)
-| N_Proj' p a :
-  SNe a ->
-  SNe' (PProj p a).
-
 Lemma PProjAbs_imp n p (a : PTm (S n)) :
   ~ SN (PProj p (PAbs a)).
 Proof.
@@ -895,6 +885,12 @@ Module NeERed.
     move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_nonelim.
   Qed.
 
+  Lemma ToERed : forall n, (forall (a b : PTm n), R_elim a b -> ERed.R a b) /\
+                 (forall (a b : PTm n), R_nonelim a b -> ERed.R a b).
+  Proof.
+    apply ered_mutual; qauto l:on ctrs:ERed.R.
+  Qed.
+
 End NeERed.
 
 Module Type NoForbid.
@@ -1091,6 +1087,141 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
     - hauto lq:on ctrs:rtc, NeERed.R_nonelim.
   Qed.
 
+
+  Lemma eta_postponement n a b c :
+    @P n a ->
+    ERed.R a b ->
+    RRed.R b c ->
+    exists d, rtc RRed.R a d /\ ERed.R d c.
+  Proof.
+    move => + h.
+    move : c.
+    elim : n a b /h => //=.
+    - move => n a0 a1 ha iha c /[dup] hP /P_AbsInv /P_AppInv [/P_renaming hP' _] hc.
+      move : iha (hP') (hc); repeat move/[apply].
+      move => [d [h0 h1]].
+      exists  (PAbs (PApp (ren_PTm shift d) (VarPTm var_zero))).
+      split. hauto lq:on rew:off ctrs:rtc use:RReds.AbsCong, RReds.AppCong, RReds.renaming.
+      hauto lq:on ctrs:ERed.R.
+    - move => n a0 a1 ha iha c /P_PairInv [/P_ProjInv + _].
+      move /iha => /[apply].
+      move => [d [h0 h1]].
+      exists (PPair (PProj PL d) (PProj PR d)).
+      hauto lq:on ctrs:ERed.R use:RReds.PairCong, RReds.ProjCong.
+    - move => n a0 a1 ha iha c  /P_AbsInv /[swap].
+      elim /RRed.inv => //=_.
+      move => a2 a3 + [? ?]. subst.
+      move : iha; repeat move/[apply].
+      hauto lq:on use:RReds.AbsCong ctrs:ERed.R.
+    - move => n a0 a1 b0 b1 ha iha hb ihb c hP.
+      elim /RRed.inv => //= _.
+      + move => a2 b2 [*]. subst.
+        have [hP' hP''] : P a0 /\ P b0 by sfirstorder use:P_AppInv.
+        move {iha ihb}.
+        move /η_split /(_ hP') : ha.
+        move => [b [h0 h1]].
+        inversion h1; subst.
+        * inversion H0; subst.
+          exists (subst_PTm (scons b0 VarPTm) a3).
+          split; last by scongruence use:ERed.morphing.
+          apply : relations.rtc_transitive.
+          apply RReds.AppCong.
+          eassumption.
+          apply rtc_refl.
+          apply : rtc_l.
+          apply RRed.AppCong0. apply RRed.AbsCong. simpl. apply RRed.AppAbs.
+          asimpl.
+          apply rtc_once.
+          apply RRed.AppAbs.
+        * exfalso.
+          move : hP h0. clear => hP h0.
+          have : rtc RRed.R (PApp a0 b0) (PApp (PPair (PProj PL a1) (PProj PR a1)) b0)
+            by qauto l:on ctrs:rtc use:RReds.AppCong.
+          move : P_RReds hP. repeat move/[apply].
+          sfirstorder use:P_AppPair.
+        * exists (subst_PTm (scons b0 VarPTm) a1).
+          split.
+          apply : rtc_r; last by apply RRed.AppAbs.
+          hauto lq:on ctrs:rtc use:RReds.AppCong.
+          hauto l:on inv:option use:ERed.morphing,NeERed.ToERed.
+      + move => a2 a3 b2 ha2 [*]. subst.
+        move : iha (ha2) {ihb} => /[apply].
+        have : P a0 by sfirstorder use:P_AppInv.
+        move /[swap]/[apply].
+        move => [d [h0 h1]].
+        exists (PApp d b0).
+        hauto lq:on ctrs:ERed.R, rtc use:RReds.AppCong.
+      + move => a2 b2 b3 hb2 [*]. subst.
+        move {iha}.
+        have : P b0 by sfirstorder use:P_AppInv.
+        move : ihb hb2; repeat move /[apply].
+        hauto lq:on rew:off ctrs:ERed.R, rtc use:RReds.AppCong.
+    - move => n a0 a1 b0 b1 ha iha hb ihb c /P_PairInv [hP hP'].
+      elim /RRed.inv => //=_;
+        hauto lq:on rew:off ctrs:ERed.R, rtc use:RReds.PairCong.
+    - move => n p a0 a1 ha iha c /[dup] hP /P_ProjInv hP'.
+      elim / RRed.inv => //= _.
+      + move => p0 a2 b0 [*]. subst.
+        move : η_split hP'  ha; repeat move/[apply].
+        move => [a1 [h0 h1]].
+        inversion h1; subst.
+        * qauto l:on ctrs:rtc use:RReds.ProjCong, P_ProjAbs, P_RReds.
+        * inversion H0; subst.
+          exists (if p is PL then a1 else b1).
+          split; last by scongruence use:NeERed.ToERed.
+          apply : relations.rtc_transitive.
+          apply RReds.ProjCong; eauto.
+          apply : rtc_l.
+          apply RRed.ProjCong.
+          apply RRed.PairCong0.
+          apply RRed.ProjPair.
+          apply : rtc_l.
+          apply RRed.ProjCong.
+          apply RRed.PairCong1.
+          apply RRed.ProjPair.
+          apply rtc_once. apply RRed.ProjPair.
+        * exists (if p is PL then a3 else b1).
+          split; last by hauto lq:on use:NeERed.ToERed.
+          apply : relations.rtc_transitive.
+          eauto using RReds.ProjCong.
+          apply rtc_once.
+          apply RRed.ProjPair.
+      + move => p0 a2 a3 h0 [*]. subst.
+        move : iha hP' h0;repeat move/[apply].
+        hauto lq:on ctrs:rtc, ERed.R use:RReds.ProjCong.
+    - 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) :