Finish injectivity for pairs

theories/algorithmic.v

@@ -771,12 +771,56 @@ Proof.
   lia.
 Qed.
 
+Lemma lored_nsteps_pair_inv k n (a0 b0 C : PTm n) :
+    nsteps LoRed.R k (PPair a0 b0) C ->
+    exists i j a1 b1,
+      i <= k /\ j <= k /\
+        C = PPair a1 b1 /\
+        nsteps LoRed.R i a0 a1 /\
+        nsteps LoRed.R j b0 b1.
+  move E : (PPair 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 : ih => [i][j][a1][b1][?][?][?][h0]h1.
+    subst. exists (S i),j,a1,b1. sauto lq:on solve+:lia.
+    spec_refl.
+    move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
+    exists i, (S j), a1, b1. sauto lq:on solve+:lia.
+Qed.
+
+Lemma algo_metric_join n k (a b : PTm n) :
+  algo_metric k a b ->
+  DJoin.R a b.
+  rewrite /algo_metric.
+  move => [i][j][va][vb][h0][h1][h2][h3][[v [h40 h41]]]h5.
+  have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps.
+  have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps.
+  apply REReds.FromEReds in h40,h41.
+  apply LoReds.ToRReds in h0,h1.
+  apply REReds.FromRReds in h0,h1.
+  rewrite /DJoin.R. exists v. sfirstorder use:@relations.rtc_transitive.
+Qed.
+
 Lemma algo_metric_pair n k (a0 b0 a1 b1 : PTm n) :
   SN (PPair a0 b0) ->
   SN (PPair a1 b1) ->
   algo_metric k (PPair a0 b0) (PPair a1 b1) ->
   exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
-Admitted.
+  move => sn0 sn1 /[dup] /algo_metric_join hj.
+  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
+  move : lored_nsteps_pair_inv h0;repeat move/[apply].
+  move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
+  move : lored_nsteps_pair_inv h1;repeat move/[apply].
+  move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
+  simpl in *. exists (k - 1).
+  move /andP : h2 => [h20 h21].
+  move /andP : h3 => [h30 h31].
+  suff : EJoin.R a2 a3 /\ EJoin.R b2 b3 by hauto lq:on solve+:lia.
+  hauto l:on use:DJoin.ejoin_pair_inj.
+Qed.
 
 Lemma algo_metric_neu_abs n k (a0 : PTm (S n)) u :
   algo_metric k u (PAbs a0) ->
@@ -836,19 +880,6 @@ Proof.
   - exists i1,j1,b2,b3. sfirstorder b:on solve+:lia.
 Qed.
 
-Lemma algo_metric_join n k (a b : PTm n) :
-  algo_metric k a b ->
-  DJoin.R a b.
-  rewrite /algo_metric.
-  move => [i][j][va][vb][h0][h1][h2][h3][[v [h40 h41]]]h5.
-  have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps.
-  have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps.
-  apply REReds.FromEReds in h40,h41.
-  apply LoReds.ToRReds in h0,h1.
-  apply REReds.FromRReds in h0,h1.
-  rewrite /DJoin.R. exists v. sfirstorder use:@relations.rtc_transitive.
-Qed.
-
 Lemma T_Univ_Raise n Γ (a : PTm n) i j :
   Γ ⊢ a ∈ PUniv i ->
   i <= j ->

theories/fp_red.v

@@ -262,6 +262,12 @@ end.
 Lemma ne_nf n a : @ne n a -> nf a.
 Proof. elim : a => //=. Qed.
 
+Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
+  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
+Proof.
+  move : m ξ. elim : n / a => //=; solve [hauto b:on].
+Qed.
+
 Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop :=
 | T_Refl :
   TRedSN' a a
@@ -842,12 +848,6 @@ Module RReds.
 End RReds.
 
 
-Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
-  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
-Proof.
-  move : m ξ. elim : n / a => //=; solve [hauto b:on].
-Qed.
-
 Module NeEPar.
   Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -1446,6 +1446,14 @@ Module ERed.
     all : hauto lq:on ctrs:R.
   Qed.
 
+  Lemma nf_preservation n (a b : PTm n) :
+    ERed.R a b -> (nf a -> nf b) /\ (ne a -> ne b).
+  Proof.
+    move => h.
+    elim : n a b /h => //=;
+                        hauto lqb:on use:ne_nf_ren,ne_nf.
+  Qed.
+
 End ERed.
 
 Module EReds.
@@ -1829,6 +1837,14 @@ Module REReds.
     hauto l:on use:substing.
   Qed.
 
+  Lemma ToEReds n (a b : PTm n) :
+    nf a ->
+    rtc RERed.R a b -> rtc ERed.R a b.
+  Proof.
+    move => + h.
+    induction h; hauto lq:on rew:off ctrs:rtc use:RERed.ToBetaEta, RReds.nf_refl, @rtc_once, ERed.nf_preservation.
+  Qed.
+
 End REReds.
 
 Module LoRed.
@@ -2215,6 +2231,12 @@ Module DJoin.
   Lemma refl n (a : PTm n) : R a a.
   Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
 
+  Lemma FromEJoin n (a b : PTm n) : EJoin.R a b -> DJoin.R a b.
+  Proof. hauto q:on use:REReds.FromEReds. Qed.
+
+  Lemma ToEJoin n (a b : PTm n) : nf a -> nf b -> DJoin.R a b -> EJoin.R a b.
+  Proof. hauto q:on use:REReds.ToEReds. Qed.
+
   Lemma symmetric n (a b : PTm n) : R a b -> R b a.
   Proof. sfirstorder unfold:R. Qed.
 
@@ -2381,6 +2403,45 @@ Module DJoin.
     hauto q:on ctrs:rtc inv:option use:REReds.cong.
   Qed.
 
+  Lemma pair_inj n (a0 a1 b0 b1 : PTm n) :
+    SN (PPair a0 b0) ->
+    SN (PPair a1 b1) ->
+    R (PPair a0 b0) (PPair a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    move => sn0 sn1.
+    have [? [? [? ?]]] : SN a0 /\ SN b0 /\ SN a1 /\ SN b1 by sfirstorder use:SN_NoForbid.P_PairInv.
+    have ? : SN (PProj PL (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PL (PPair a1 b1)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a1 b1)) by hauto lq:on db:sn.
+    have h0L : RRed.R (PProj PL (PPair a0 b0)) a0 by eauto with red.
+    have h0R : RRed.R (PProj PR (PPair a0 b0)) b0 by eauto with red.
+    have h1L : RRed.R (PProj PL (PPair a1 b1)) a1 by eauto with red.
+    have h1R : RRed.R (PProj PR (PPair a1 b1)) b1 by eauto with red.
+    move => h2.
+    move /ProjCong in h2.
+    have h2L := h2 PL.
+    have {h2}h2R := h2 PR.
+    move /FromRRed1 in h0L.
+    move /FromRRed0 in h1L.
+    move /FromRRed1 in h0R.
+    move /FromRRed0 in h1R.
+    split; eauto using transitive.
+  Qed.
+
+  Lemma ejoin_pair_inj n (a0 a1 b0 b1 : PTm n) :
+    nf a0 -> nf b0 -> nf a1 -> nf b1 ->
+    EJoin.R (PPair a0 b0) (PPair a1 b1) ->
+    EJoin.R a0 a1 /\ EJoin.R b0 b1.
+  Proof.
+    move => h0 h1 h2 h3 /FromEJoin.
+    have [? ?] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move => ?.
+    have : R a0 a1 /\ R b0 b1 by hauto l:on use:pair_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
   Lemma abs_inj n (a0 a1 : PTm (S n)) :
     SN a0 -> SN a1 ->
     R (PAbs a0) (PAbs a1) ->