theories/fp_red.v

@@ -144,6 +144,16 @@ 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.
@@ -885,12 +895,6 @@ 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.
@@ -1087,141 +1091,6 @@ 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) :