Add some more injection lemmas for neutrals

theories/algorithmic.v

@@ -567,6 +567,53 @@ Proof.
   - hauto lq:on ctrs:nsteps inv:LoRed.R.
 Qed.
 
+Lemma lored_hne_preservation n (a b : PTm n) :
+    LoRed.R a b -> ishne a -> ishne b.
+Proof.  induction 1; sfirstorder. Qed.
+
+Lemma lored_nsteps_app_inv k n (a0 b0 C : PTm n) :
+    nsteps LoRed.R k (PApp a0 b0) C ->
+    ishne a0 ->
+    exists i j a1 b1,
+      i <= k /\ j <= k /\
+        C = PApp a1 b1 /\
+        nsteps LoRed.R i a0 a1 /\
+        nsteps LoRed.R j b0 b1.
+Proof.
+  move E : (PApp a0 b0) => u hu. move : a0 b0 E.
+  elim : k u C / hu.
+  - sauto lq:on.
+  - move => k a0 a1 a2 ha01 ha12 ih a3 b0 ?.  subst.
+    inversion ha01; subst => //=.
+    spec_refl.
+    move => h.
+    have : ishne a4 by sfirstorder use:lored_hne_preservation.
+    move : ih => /[apply]. move => [i][j][a1][b1][?][?][?][h0]h1.
+    subst. exists (S i),j,a1,b1. sauto lq:on solve+:lia.
+    spec_refl. move : ih => /[apply].
+    move => [i][j][a1][b1][?][?][?][h0]h1. subst.
+    exists i, (S j), a1, b1. sauto lq:on solve+:lia.
+Qed.
+
+Lemma algo_metric_app n k (a0 b0 a1 b1 : PTm n) :
+  algo_metric k (PApp a0 b0) (PApp a1 b1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
+Proof.
+  move => [i][j][va][vb][v][h0][h1][h2][h3][h4][h5]h6.
+  move => hne0 hne1.
+  move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply].
+  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
+  move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply].
+  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
+  simpl in *. exists (k - 1).
+  split. lia.
+  split.
+  + rewrite /algo_metric.
+    have : exists a4 b4, rtc ERed.R a2 a4 /\ ERed.R
+    exists i0,i1,a2,b2.
+
 Lemma algo_metric_join n k (a b : PTm n) :
   algo_metric k a b ->
   DJoin.R a b.
@@ -663,6 +710,12 @@ Proof.
       * move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB.
         move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0.
         move /App_Inv : wtB => [A1][B1][hb1][ha1]hS1.
+        have : DJoin.R (PApp b0 a0) (PApp b1 a1)
+          by hauto l:on use:algo_metric_join.
+        move : DJoin.hne_app_inj (hne0) (hne1). repeat move/[apply].
+        move => [hjb hja].
+        split. apply CE_AppCong => //=.
+        eapply ih; eauto.
         admit.
       * admit.
       * sfirstorder use:T_Bot_Imp.

theories/fp_red.v

@@ -20,7 +20,7 @@ Ltac2 spec_refl () :=
                try (specialize $h with (1 := eq_refl))
            end)  (Control.hyps ()).
 
-Ltac spec_refl := ltac2:(spec_refl ()).
+Ltac spec_refl := ltac2:(Control.enter spec_refl).
 
 Module EPar.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -1510,10 +1510,45 @@ Module EReds.
     induction 1; hauto lq:on ctrs:rtc use:ERed.substing.
   Qed.
 
+  Lemma app_inv n (a0 b0 C : PTm n) :
+    rtc ERed.R (PApp a0 b0) C ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc ERed.R a0 a1 /\
+               rtc ERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma proj_inv n p (a C : PTm n) :
+    rtc ERed.R (PProj p a) C ->
+    exists c, C = PProj p c /\ rtc ERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,ERed.R inv:ERed.R.
+  Qed.
+
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
 
+Module EJoin.
+  Definition R {n} (a b : PTm n) := exists c, rtc ERed.R a c /\ rtc ERed.R b c.
+
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:EReds.app_inv.
+  Qed.
+
+End EJoin.
 
 Module RERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -1602,6 +1637,10 @@ Module RERed.
     hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing.
   Qed.
 
+  Lemma hne_preservation n (a b : PTm n) :
+    RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; sfirstorder. Qed.
+
 End RERed.
 
 Module REReds.
@@ -1694,6 +1733,32 @@ Module REReds.
     move : i E. elim : u C /hu; hauto lq:on rew:off inv:RERed.R.
   Qed.
 
+  Lemma hne_app_inv n (a0 b0 C : PTm n) :
+    rtc RERed.R (PApp a0 b0) C ->
+    ishne a0 ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc RERed.R a0 a1 /\
+               rtc RERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
+  Lemma hne_proj_inv n p (a C : PTm n) :
+    rtc RERed.R (PProj p a) C ->
+    ishne a ->
+    exists c, C = PProj p c /\ rtc RERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
   Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
     rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof.
@@ -2206,6 +2271,24 @@ Module DJoin.
     sauto lq:on rew:off use:REReds.univ_inv.
   Qed.
 
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    ishne a0 ->
+    ishne a1 ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:REReds.hne_app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    ishne a0 ->
+    ishne a1 ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    sauto lq:on use:REReds.hne_proj_inv.
+  Qed.
+
   Lemma FromRRed0 n (a b : PTm n) :
     RRed.R a b -> R a b.
   Proof.