Prove structural properties of DJoin

theories/fp_red.v

@@ -229,7 +229,7 @@ Ltac2 rec solve_anti_ren () :=
   let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
   intro $x;
   lazy_match! Constr.type (Control.hyp x) with
-  | fin ?x -> _ ?y => (ltac1:(case;qauto depth:2 db:sn))
+  | fin _ -> _ _ => (ltac1:(case;qauto depth:2 db:sn))
   | _ => solve_anti_ren ()
   end.
 
@@ -431,34 +431,32 @@ Module RRed.
     all : qauto ctrs:R.
   Qed.
 
+  Ltac2 rec solve_anti_ren () :=
+    let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
+    intro $x;
+    lazy_match! Constr.type (Control.hyp x) with
+    | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2 ctrs:RRed.R))
+    | _ => solve_anti_ren ()
+    end.
+
+  Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
     R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
   Proof.
     move E : (ren_PTm ξ a) => u h.
-    move : n ξ a E. elim : m u b/h.
+    move : n ξ a E. elim : m u b/h; try solve_anti_ren.
     - move => n a b m ξ []//=. move => []//= t t0 [*]. subst.
       eexists. split. apply AppAbs. by asimpl.
     - move => n p a b m ξ []//=.
       move => p0 []//=. hauto q:on ctrs:R.
-    - move => n a0 a1 ha iha m ξ []//=.
-      move => p [*]. subst.
-      spec_refl.
-      move : iha => [t [h0 h1]]. subst.
-      eexists. split. eauto using AbsCong.
-      by asimpl.
-    - move => n a0 a1 b ha iha m ξ []//=.
-      hauto lq:on ctrs:R.
-    - move => n a b0 b1 h ih m ξ []//=.
-      hauto lq:on ctrs:R.
-    - move => n a0 a1 b ha iha m ξ []//=.
-      hauto lq:on ctrs:R.
-    - move => n a b0 b1 h ih m ξ []//=.
-      hauto lq:on ctrs:R.
-    - move => n p a0 a1 ha iha m ξ []//=.
-      hauto lq:on ctrs:R.
   Qed.
 
+  Lemma nf_imp n (a b : PTm n) :
+    nf a ->
+    R a b -> False.
+  Proof. move/[swap]. induction 1; hauto qb:on inv:PTm. Qed.
+
 End RRed.
 
 Module RPar.
@@ -574,6 +572,48 @@ Module RPar.
     induction 1; qauto l:on use:RPar.refl ctrs:RPar.R.
   Qed.
 
+  Function tstar {n} (a : PTm n) :=
+    match a with
+    | VarPTm i => a
+    | PAbs a => PAbs (tstar a)
+    | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a)
+    | PApp a b => PApp (tstar a) (tstar b)
+    | PPair a b => PPair (tstar a) (tstar b)
+    | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b)
+    | PProj p a => PProj p (tstar a)
+    end.
+
+  Lemma triangle n (a b : PTm n) :
+    RPar.R a b -> RPar.R b (tstar a).
+  Proof.
+    move : b.
+    apply tstar_ind => {}n{}a.
+    - hauto lq:on ctrs:R inv:R.
+    - hauto lq:on ctrs:R inv:R.
+    - hauto lq:on rew:off inv:R use:cong ctrs:R.
+    - hauto lq:on ctrs:R inv:R.
+    - hauto lq:on ctrs:R inv:R.
+    - move => p a0 b ? ? ih b0. subst.
+      elim /inv => //=_.
+      + move => p a1 a2 b1 b2 h0 h1[*]. subst.
+        by apply ih.
+      + move => p a1 a2 ha [*]. subst.
+        elim /inv : ha => //=_.
+        move => a1 a3 b0 b1 h0 h1 [*]. subst.
+        apply : ProjPair'; eauto using refl.
+    - move => p a0 b ? p0 ?. subst.
+      case : p0 => //= _.
+      move => ih b0. elim /inv => //=_.
+      + hauto l:on.
+      + move => p a1 a2 ha [*]. subst.
+        elim /inv : ha => //=_ > ? ? [*]. subst.
+        apply : ProjPair'; eauto using refl.
+    - hauto lq:on ctrs:R inv:R.
+  Qed.
+
+  Lemma diamond n (a b c : PTm n) :
+    R a b -> R a c -> exists d, R b d /\ R c d.
+  Proof. eauto using triangle. Qed.
 End RPar.
 
 Lemma red_sn_preservation n :
@@ -610,46 +650,6 @@ Proof.
   - sauto.
 Qed.
 
-Function tstar {n} (a : PTm n) :=
-  match a with
-  | VarPTm i => a
-  | PAbs a => PAbs (tstar a)
-  | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a)
-  | PApp a b => PApp (tstar a) (tstar b)
-  | PPair a b => PPair (tstar a) (tstar b)
-  | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b)
-  | PProj p a => PProj p (tstar a)
-  end.
-
-Module TStar.
-  Lemma renaming n m (ξ : fin n -> fin m) (a : PTm n) :
-    tstar (ren_PTm ξ a) = ren_PTm ξ (tstar a).
-  Proof.
-    move : m ξ.
-    apply tstar_ind => {}n {}a => //=.
-    - hauto lq:on.
-    - scongruence.
-    - move => a0 b ? h ih m ξ.
-      rewrite ih.
-      asimpl; congruence.
-    - qauto l:on.
-    - scongruence.
-    - hauto q:on.
-    - qauto l:on.
-  Qed.
-
-  Lemma pair n (a b : PTm n) :
-    tstar (PPair a b) = PPair (tstar a) (tstar b).
-    reflexivity. Qed.
-End TStar.
-
-Definition isPair {n} (a : PTm n) := if a is PPair _ _ then true else false.
-
-Lemma tstar_proj n (a : PTm n) :
-  ((~~ isPair a) /\ forall p, tstar (PProj p a) = PProj p (tstar a)) \/
-    exists a0 b0, a = PPair a0 b0 /\ forall p, tstar (PProj p a) = (if p is PL then (tstar a0) else (tstar b0)).
-Proof. sauto lq:on. Qed.
-
 Module EPar'.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -732,6 +732,7 @@ Module EPars.
     rtc EPar'.R a0 a1 ->
     rtc EPar'.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
+
 End EPars.
 
 Module RReds.
@@ -771,6 +772,31 @@ Module RReds.
     move => h. move : m ξ. elim : a b /h; hauto lq:on ctrs:rtc use:RRed.renaming.
   Qed.
 
+  Lemma FromRPar n (a b : PTm n) (h : RPar.R a b) :
+    rtc RRed.R a b.
+  Proof.
+    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl.
+    move => n a0 a1 b0 b1 ha iha hb ihb.
+    apply : rtc_r; last by apply RRed.AppAbs.
+    by eauto using AppCong, AbsCong.
+
+    move => n p a0 a1 b0 b1 ha iha hb ihb.
+    apply : rtc_r; last by apply RRed.ProjPair.
+    by eauto using PairCong, ProjCong.
+  Qed.
+
+  Lemma RParIff n (a b : PTm n) :
+    rtc RRed.R a b <-> rtc RPar.R a b.
+  Proof.
+    split.
+    induction 1; hauto l:on ctrs:rtc use:RPar.FromRRed, @relations.rtc_transitive.
+    induction 1; hauto l:on ctrs:rtc use:FromRPar, @relations.rtc_transitive.
+  Qed.
+
+  Lemma nf_refl n (a b : PTm n) :
+    rtc RRed.R a b -> nf a -> a = b.
+  Proof. induction 1; sfirstorder use:RRed.nf_imp. Qed.
+
 End RReds.
 
 
@@ -1272,7 +1298,7 @@ Module ERed.
     let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
     intro $x;
     lazy_match! Constr.type (Control.hyp x) with
-    | fin ?x -> _ ?y => (ltac1:(case;qauto depth:2 ctrs:ERed.R))
+    | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2 ctrs:ERed.R))
     | _ => solve_anti_ren ()
     end.
 
@@ -1282,36 +1308,134 @@ Module ERed.
   (*   destruct a. *)
   (*   exact (ξ f). *)
 
+  Lemma up_injective n m (ξ : fin n -> fin m) :
+    (forall i j, ξ i = ξ j -> i = j) ->
+    forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+  Proof.
+    sblast inv:option.
+  Qed.
+
+  Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+    (forall i j, ξ i = ξ j -> i = j) ->
+    ren_PTm ξ a = ren_PTm ξ b ->
+    a = b.
+  Proof.
+    move : m ξ b.
+    elim : n / a => //; try solve_anti_ren.
+
+    move => n a iha m ξ []//=.
+    move => u hξ [h].
+    apply iha in h. by subst.
+    destruct i, j=>//=.
+    hauto l:on.
+  Qed.
+
+  Lemma AppEta' n a u :
+    u = (@PApp (S n) (ren_PTm shift a) (VarPTm var_zero)) ->
+    R (PAbs u) a.
+  Proof. move => ->. apply AppEta. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h.
+
+    move => n a m ξ /=.
+    apply AppEta'; eauto. by asimpl.
+    all : qauto ctrs:R.
+  Qed.
+
   (* Need to generalize to injective renaming *)
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
+    (forall i j, ξ i = ξ j -> i = j) ->
     R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
   Proof.
+    move => hξ.
     move E : (ren_PTm ξ a) => u hu.
-    move : n ξ a E.
+    move : n ξ a hξ E.
     elim : m u b / hu; try solve_anti_ren.
     - move => n a m ξ []//=.
-      move => u [].
+      move => u hξ [].
       case : u => //=.
       move => u0 u1 [].
       case : u1 => //=.
       move => i /[swap] [].
       case : i => //= _ h.
-      apply f_equal with (f := subst_PTm (scons (PAbs (VarPTm var_zero)) VarPTm)) in h.
-      move : h. asimpl. move => ?. subst.
-      admit.
+      have : exists p, ren_PTm shift p = u0 by admit.
+      move => [p ?]. subst.
+      move : h. asimpl.
+      replace (ren_PTm (funcomp shift ξ) p) with
+        (ren_PTm shift (ren_PTm ξ p)); last by asimpl.
+      move /ren_injective.
+      move /(_ ltac:(hauto l:on)).
+      move => ?. subst.
+      exists p. split=>//. apply AppEta.
     - move => n a m ξ [] //=.
-      move => u u0 [].
+      move => u u0 hξ [].
       case : u => //=.
       case : u0 => //=.
-      move => p p0 p1 p2 [? ?] [? ?]. subst.
-
-
-
-
+      move => p p0 p1 p2 [? ?] [? h]. subst.
+      have ? : p0 = p2 by eauto using ren_injective. subst.
+      hauto l:on.
+    - move => n a0 a1 ha iha m ξ []//= p hξ [?]. subst.
+      sauto lq:on use:up_injective.
+  Admitted.
 
 
 End ERed.
 
+Module EReds.
+
+  #[local]Ltac solve_s_rec :=
+  move => *; eapply rtc_l; eauto;
+         hauto lq:on ctrs:ERed.R.
+
+  #[local]Ltac solve_s :=
+    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+
+  Lemma AbsCong n (a b : PTm (S n)) :
+    rtc ERed.R a b ->
+    rtc ERed.R (PAbs a) (PAbs b).
+  Proof. solve_s. Qed.
+
+  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+    rtc ERed.R a0 a1 ->
+    rtc ERed.R b0 b1 ->
+    rtc ERed.R (PApp a0 b0) (PApp a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+    rtc ERed.R a0 a1 ->
+    rtc ERed.R b0 b1 ->
+    rtc ERed.R (PPair a0 b0) (PPair a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma ProjCong n p (a0 a1  : PTm n) :
+    rtc ERed.R a0 a1 ->
+    rtc ERed.R (PProj p a0) (PProj p a1).
+  Proof. solve_s. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    rtc ERed.R a b -> rtc ERed.R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof. induction 1; hauto l:on use:ERed.renaming ctrs:rtc. Qed.
+
+  Lemma FromEPar n (a b : PTm n) :
+    EPar.R a b ->
+    rtc ERed.R a b.
+  Proof.
+    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl.
+    - move => n a0 a1 _ h.
+      have {}h : rtc ERed.R (ren_PTm shift a0) (ren_PTm shift a1) by apply renaming.
+      apply : rtc_r. apply AbsCong. apply AppCong; eauto. apply rtc_refl.
+      apply ERed.AppEta.
+    - move => n a0 a1 _ h.
+      apply : rtc_r.
+      apply PairCong; eauto using ProjCong.
+      apply ERed.PairEta.
+  Qed.
+End EReds.
+
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
 
 
@@ -1355,6 +1479,14 @@ Module RERed.
     ERed.R a b \/ RRed.R a b.
   Proof. induction 1; hauto lq:on db:red. Qed.
 
+  Lemma FromBeta n (a b : PTm n) :
+    RRed.R a b -> RERed.R a b.
+  Proof. induction 1; qauto l:on ctrs:R. Qed.
+
+  Lemma FromEta n (a b : PTm n) :
+    ERed.R a b -> RERed.R a b.
+  Proof. induction 1; qauto l:on ctrs:R. Qed.
+
   Lemma ToBetaEtaPar n (a b : PTm n) :
     R a b ->
     EPar.R a b \/ RRed.R a b.
@@ -1362,8 +1494,33 @@ Module RERed.
     hauto q:on use:ERed.ToEPar, ToBetaEta.
   Qed.
 
+  Lemma sn_preservation n (a b : PTm n) :
+    R a b ->
+    SN a ->
+    SN b.
+  Proof. hauto q:on use:ToBetaEtaPar, epar_sn_preservation, red_sn_preservation, RPar.FromRRed. Qed.
+
 End RERed.
 
+Module REReds.
+  Lemma sn_preservation n (a b : PTm n) :
+    rtc RERed.R a b ->
+    SN a ->
+    SN b.
+  Proof. induction 1; eauto using RERed.sn_preservation. Qed.
+
+  Lemma FromRReds n (a b : PTm n) :
+    rtc RRed.R a b ->
+    rtc RERed.R a b.
+  Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.FromBeta. Qed.
+
+  Lemma FromEReds n (a b : PTm n) :
+    rtc ERed.R a b ->
+    rtc RERed.R a b.
+  Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.FromEta. Qed.
+
+End REReds.
+
 Module LoRed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (****************** Beta ***********************)
@@ -1405,6 +1562,11 @@ Module LoRed.
     move => h. elim : n a b /h=>//=.
   Qed.
 
+  Lemma ToRRed n (a b : PTm n) :
+    LoRed.R a b ->
+    RRed.R a b.
+  Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
+
 End LoRed.
 
 Module LoReds.
@@ -1459,7 +1621,7 @@ Module LoReds.
 
   Local Ltac triv := simpl in *; itauto.
 
-  Lemma FromSN : forall n,
+  Lemma FromSN_mutual : forall n,
     (forall (a : PTm n) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\
     (forall (a : PTm n) (_ : SN a), exists v, rtc LoRed.R a v /\ nf v) /\
     (forall (a b : PTm n) (_ : TRedSN a b), LoRed.R a b).
@@ -1483,6 +1645,12 @@ Module LoReds.
       hauto lq:on ctrs:LoRed.R.
   Qed.
 
+  Lemma FromSN : forall n a, @SN n a -> exists v, rtc LoRed.R a v /\ nf v.
+  Proof. firstorder using FromSN_mutual. Qed.
+
+  Lemma ToRReds : forall n (a b : PTm n), rtc LoRed.R a b -> rtc RRed.R a b.
+  Proof. induction 1; hauto lq:on ctrs:rtc use:LoRed.ToRRed. Qed.
+
 End LoReds.
 
 
@@ -1531,74 +1699,166 @@ Proof.
     + move => a0 a1 ha [*]. subst.
       elim /ERed.inv : ha => //= _.
       * move => a0 a2 b0 ha [*]. subst. rename a2 into a1.
-        have [a2 [h0 h1]] : exists a2, ERed.R a2 a /\ a1 = ren_PTm shift a2 by admit. subst.
-        eexists. split; cycle 1.
-        apply : relations.rtc_r; cycle 1.
-        apply ERed.AppEta.
-        apply rtc_refl.
-        eauto using relations.rtc_once.
+        move /ERed.antirenaming : ha.
+        move /(_ ltac:(hauto lq:on)) => [a' [h0 h1]]. subst.
+        hauto lq:on ctrs:rtc, ERed.R.
       * hauto q:on ctrs:rtc, ERed.R inv:ERed.R.
   - move => a c ha.
     elim /ERed.inv : ha => //= _.
     + hauto l:on.
-    + move => a0 a1 b0 ha ? [*]. subst.
+    + move => a0 a1 b0 ha [*]. subst.
       elim /ERed.inv : ha => //= _.
-      move => p a1 a2 ha ? [*]. subst.
-      exists a1. split. by apply relations.rtc_once.
-      apply : rtc_l. apply ERed.PairEta.
-      apply : rtc_l. apply ERed.PairCong1. eauto using ERed.ProjCong.
-      apply rtc_refl.
-    + move => a0 b0 b1 ha ? [*]. subst.
-      elim /ERed.inv : ha => //= _ p a0 a1 h ? [*]. subst.
-      exists a0. split; first by apply relations.rtc_once.
-      apply : rtc_l; first by apply ERed.PairEta.
-      apply relations.rtc_once.
-      hauto lq:on ctrs:ERed.R.
+      move => p a0 a2 ha [*]. subst.
+      hauto q:on ctrs:rtc, ERed.R.
+    + move => a0 b0 b1 ha [*]. subst.
+      elim /ERed.inv : ha => //= _.
+      move => p a0 a2 ha [*]. subst.
+      hauto q:on ctrs:rtc, ERed.R.
   - move => a0 a1 ha iha c.
     elim /ERed.inv => //= _.
-    + move => a2 ? [*]. subst.
+    + move => a2 [*]. subst.
       elim /ERed.inv : ha => //=_.
-      * move => a1 a2 b0 ha ? [*] {iha}. subst.
-        have [a0 [h0 h1]] : exists a0, ERed.R a0 c /\ a1 = ren_Tm shift a0 by admit. subst.
+      * move => a0 a2 b0 ha [*] {iha}. subst.
+        have [a0 [h0 h1]] : exists a0, ERed.R c a0 /\ a2 = ren_PTm shift a0 by hauto lq:on use:ERed.antirenaming. subst.
         exists a0. split; last by apply relations.rtc_once.
         apply relations.rtc_once. apply ERed.AppEta.
       * hauto q:on inv:ERed.R.
-    + hauto l:on use:EReds.AbsCong.
+    + hauto lq:on use:EReds.AbsCong.
   - move => a0 a1 b ha iha c.
     elim /ERed.inv => //= _.
     + hauto lq:on ctrs:rtc use:EReds.AppCong.
     + hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
   - move => a b0 b1 hb ihb c.
     elim /ERed.inv => //=_.
-    + move => a0 a1 a2 ha ? [*]. subst.
-      move {ihb}. exists (App a0 b0).
+    + move => a0 a1 a2 ha [*]. subst.
+      move {ihb}. exists (PApp a1 b1).
       hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
     + hauto lq:on ctrs:rtc use:EReds.AppCong.
   - move => a0 a1 b ha iha c.
     elim /ERed.inv => //= _.
-    + move => ? ?[*]. subst.
-      elim /ERed.inv : ha => //= _ p a1 a2 h ? [*]. subst.
-      exists a1. split; last by apply relations.rtc_once.
-      apply : rtc_l. apply ERed.PairEta.
-      apply relations.rtc_once. hauto lq:on ctrs:ERed.R.
+    + sauto lq:on.
     + hauto lq:on ctrs:rtc use:EReds.PairCong.
     + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
   - move => a b0 b1 hb hc c. elim /ERed.inv => //= _.
-    + move => ? ? [*]. subst.
-      elim /ERed.inv : hb => //= _ p a0 a1 ha ? [*]. subst.
-      move {hc}.
-      exists a0. split; last by apply relations.rtc_once.
-      apply : rtc_l; first by apply ERed.PairEta.
-      hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+    + move => ? [*]. subst.
+      sauto lq:on.
     + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
     + hauto lq:on ctrs:rtc use:EReds.PairCong.
   - qauto l:on inv:ERed.R use:EReds.ProjCong.
-  - move => p A0 A1 B hA ihA.
-    move => c. elim/ERed.inv => //=.
-    + hauto lq:on ctrs:rtc use:EReds.BindCong.
-    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-  - move => p A B0 B1 hB ihB c.
-    elim /ERed.inv => //=.
-    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
-    + hauto lq:on ctrs:rtc use:EReds.BindCong.
-Admitted.
+Qed.
+
+Lemma ered_confluence n (a b c : PTm n) :
+  rtc ERed.R a b ->
+  rtc ERed.R a c ->
+  exists d, rtc ERed.R b d  /\ rtc ERed.R c d.
+Proof.
+  sfirstorder use:relations.locally_confluent_confluent, ered_sn, ered_local_confluence.
+Qed.
+
+Lemma red_confluence n (a b c : PTm n) :
+  rtc RRed.R a b ->
+  rtc RRed.R a c ->
+  exists d, rtc RRed.R b d  /\ rtc RRed.R c d.
+  suff : rtc RPar.R a b -> rtc RPar.R a c -> exists d : PTm n, rtc RPar.R b d /\ rtc RPar.R c d
+             by hauto lq:on use:RReds.RParIff.
+  apply relations.diamond_confluent.
+  rewrite /relations.diamond.
+  eauto using RPar.diamond.
+Qed.
+
+Lemma red_uniquenf n (a b c : PTm n) :
+  rtc RRed.R a b ->
+  rtc RRed.R a c ->
+  nf b ->
+  nf c ->
+  b = c.
+Proof.
+  move : red_confluence; repeat move/[apply].
+  move => [d [h0 h1]].
+  move => *.
+  suff [] : b = d /\ c = d by congruence.
+  sfirstorder use:RReds.nf_refl.
+Qed.
+
+Module NeEPars.
+  Lemma R_nonelim_nf n (a b : PTm n) :
+    rtc NeEPar.R_nonelim a b ->
+    nf b ->
+    nf a.
+  Proof. induction 1; sfirstorder use:NeEPar.R_elim_nf. Qed.
+
+  Lemma ToEReds : forall n, (forall (a b : PTm n), rtc NeEPar.R_nonelim a b -> rtc ERed.R a b).
+  Proof.
+    induction 1; hauto l:on use:NeEPar.ToEPar, EReds.FromEPar, @relations.rtc_transitive.
+  Qed.
+End NeEPars.
+
+
+Lemma rered_standardization n (a c : PTm n) :
+  SN a ->
+  rtc RERed.R a c ->
+  exists b, rtc RRed.R a b /\ rtc NeEPar.R_nonelim b c.
+Proof.
+  move => + h. elim : a c /h.
+  by eauto using rtc_refl.
+  move => a b c.
+  move /RERed.ToBetaEtaPar.
+  case.
+  - move => h0 h1 ih hP.
+    have  : SN b by qauto use:epar_sn_preservation.
+    move => {}/ih [b' [ihb0 ihb1]].
+    hauto lq:on ctrs:rtc use:SN_UniqueNF.η_postponement_star'.
+  - hauto lq:on ctrs:rtc use:red_sn_preservation, RPar.FromRRed.
+Qed.
+
+Lemma rered_confluence n (a b c : PTm n) :
+  SN a ->
+  rtc RERed.R a b ->
+  rtc RERed.R a c ->
+  exists d, rtc RERed.R b d  /\ rtc RERed.R c d.
+Proof.
+  move => hP hb hc.
+  have [] : SN b /\ SN c by qauto use:REReds.sn_preservation.
+  move => /LoReds.FromSN [bv [/LoReds.ToRReds /REReds.FromRReds hbv  hbv']].
+  move => /LoReds.FromSN [cv [/LoReds.ToRReds /REReds.FromRReds hcv  hcv']].
+  have [] : SN b /\ SN c by sfirstorder use:REReds.sn_preservation.
+  move : rered_standardization hbv; repeat move/[apply]. move => [bv' [hb0 hb1]].
+  move : rered_standardization hcv; repeat move/[apply]. move => [cv' [hc0 hc1]].
+
+  have [] : rtc RERed.R a bv' /\ rtc RERed.R a cv'
+    by sfirstorder use:@relations.rtc_transitive, REReds.FromRReds.
+  move : rered_standardization (hP). repeat move/[apply]. move => [bv'' [hb3 hb4]].
+  move : rered_standardization (hP). repeat move/[apply]. move => [cv'' [hc3 hc4]].
+  have hb2 : rtc NeEPar.R_nonelim bv'' bv by hauto lq:on use:@relations.rtc_transitive.
+  have hc2 : rtc NeEPar.R_nonelim cv'' cv by hauto lq:on use:@relations.rtc_transitive.
+  have [hc5 hb5] : nf cv'' /\ nf bv'' by sfirstorder use:NeEPars.R_nonelim_nf.
+  have ? : bv'' = cv'' by sfirstorder use:red_uniquenf. subst.
+  apply NeEPars.ToEReds in hb2, hc2.
+  move : ered_confluence (hb2) (hc2); repeat move/[apply].
+  move => [v [hv hv']].
+  exists v. split.
+  move /NeEPars.ToEReds /REReds.FromEReds : hb1.
+  move /REReds.FromRReds : hb0. move /REReds.FromEReds : hv. eauto using relations.rtc_transitive.
+  move /NeEPars.ToEReds /REReds.FromEReds : hc1.
+  move /REReds.FromRReds : hc0. move /REReds.FromEReds : hv'. eauto using relations.rtc_transitive.
+Qed.
+
+(* "Declarative" Joinability *)
+Module DJoin.
+  Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c.
+
+  Lemma refl n (a : PTm n) : R a a.
+  Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
+
+  Lemma symmetric n (a b : PTm n) : R a b -> R b a.
+  Proof. sfirstorder unfold:R. Qed.
+
+  Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c.
+  Proof.
+    rewrite /R.
+    move => + [ab [ha +]] [bc [+ hc]].
+    move : rered_confluence; repeat move/[apply].
+    move => [v [h0 h1]].
+    exists v. sfirstorder use:@relations.rtc_transitive.
+  Qed.
+End DJoin.