Finish the soundness and completeness proof of the subtyping algorithm

theories/algorithmic.v

@@ -1050,6 +1050,12 @@ Proof.
 Qed.
 
 
+Lemma hreds_nf_refl a b  :
+  HRed.nf a ->
+  rtc HRed.R a b ->
+  a = b.
+Proof. inversion 2; sfirstorder. Qed.
+
 Lemma lored_nsteps_app_cong k (a0 a1 b : PTm) :
   nsteps LoRed.R k a0 a1 ->
   ishne a0 ->

theories/executable.v

@@ -212,6 +212,67 @@ with algo_dom_r : PTm  -> PTm -> Prop :=
   (* ----------------------- *)
   algo_dom_r a b.
 
+Scheme algo_ind := Induction for algo_dom Sort Prop
+  with algor_ind := Induction for algo_dom_r Sort Prop.
+
+Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
+
+
+(* Inductive salgo_dom : PTm -> PTm -> Prop := *)
+(* | S_UnivCong i j : *)
+(*   (* -------------------------- *) *)
+(*   salgo_dom (PUniv i) (PUniv j) *)
+
+(* | S_PiCong A0 A1 B0 B1 : *)
+(*   salgo_dom_r A1 A0 -> *)
+(*   salgo_dom_r B0 B1 -> *)
+(*   (* ---------------------------- *) *)
+(*   salgo_dom (PBind PPi A0 B0) (PBind PPi A1 B1) *)
+
+(* | S_SigCong A0 A1 B0 B1 : *)
+(*   salgo_dom_r A0 A1 -> *)
+(*   salgo_dom_r B0 B1 -> *)
+(*   (* ---------------------------- *) *)
+(*   salgo_dom (PBind PSig A0 B0) (PBind PSig A1 B1) *)
+
+(* | S_NatCong : *)
+(*   salgo_dom PNat PNat *)
+
+(* | S_NeuNeu a b : *)
+(*   ishne a -> *)
+(*   ishne b -> *)
+(*   algo_dom a b -> *)
+(*   (* ------------------- *) *)
+(*   salgo_dom *)
+
+(* | S_Conf a b : *)
+(*   HRed.nf a -> *)
+(*   HRed.nf b -> *)
+(*   tm_conf a b -> *)
+(*   salgo_dom a b *)
+
+(* with salgo_dom_r : PTm  -> PTm -> Prop := *)
+(* | S_NfNf a b : *)
+(*   salgo_dom a b -> *)
+(*   salgo_dom_r a b *)
+
+(* | S_HRedL a a' b  : *)
+(*   HRed.R a a' -> *)
+(*   salgo_dom_r a' b -> *)
+(*   (* ----------------------- *) *)
+(*   salgo_dom_r a b *)
+
+(* | S_HRedR a b b'  : *)
+(*   HRed.nf a -> *)
+(*   HRed.R b b' -> *)
+(*   salgo_dom_r a b' -> *)
+(*   (* ----------------------- *) *)
+(*   salgo_dom_r a b. *)
+
+(* Scheme salgo_ind := Induction for salgo_dom Sort Prop *)
+(*   with algor_ind := Induction for salgo_dom_r Sort Prop. *)
+
+
 Lemma hf_no_hred (a b : PTm) :
   ishf a ->
   HRed.R a b ->
@@ -351,7 +412,6 @@ Ltac solve_check_equal :=
         | inr b' := check_equal_r a (proj1_sig b') _;
                  | inl h'' := check_equal a b _.
 
-
 Next Obligation.
   intros.
   inversion h; subst => //=.
@@ -486,3 +546,115 @@ Lemma check_equal_conf a b nfa nfb nfab :
 Proof. destruct a; destruct b => //=. Qed.
 
 #[export]Hint Rewrite check_equal_abs_abs check_equal_abs_neu check_equal_neu_abs check_equal_pair_pair check_equal_pair_neu check_equal_neu_pair check_equal_bind_bind check_equal_hredl check_equal_hredr check_equal_nfnf check_equal_conf : ce_prop.
+
+Obligation Tactic := try solve [check_equal_triv | sfirstorder].
+
+Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} :=
+  match a, b with
+  | PBind PPi A0 B0, PBind PPi A1 B1 =>
+      check_sub_r (negb q) A0 A1 _ && check_sub_r q B0 B1 _
+  | PBind PSig A0 B0, PBind PSig A1 B1 =>
+      check_sub_r q A0 A1 _ && check_sub_r q B0 B1 _
+  | PUniv i, PUniv j =>
+      if q then PeanoNat.Nat.leb i j else PeanoNat.Nat.leb j i
+  | PNat, PNat => true
+  | _ ,_ => ishne a && ishne b && check_equal a b h
+  end
+with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} :=
+  match fancy_hred a with
+  | inr a' => check_sub_r q (proj1_sig a') b _
+  | inl ha' => match fancy_hred b with
+            | inr b' => check_sub_r q a (proj1_sig b') _
+            | inl hb' => check_sub q a b _
+            end
+  end.
+Next Obligation.
+  simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
+  inversion h; subst => //=.
+  exfalso. sfirstorder use:algo_dom_no_hred.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
+  exfalso. sfirstorder.
+Defined.
+
+Next Obligation.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
+  destruct b' as [b' hb']. simpl.
+  inversion h; subst.
+  - exfalso.
+    sfirstorder use:algo_dom_no_hred.
+  - exfalso.
+    sfirstorder.
+  - assert (b' = b'0) by eauto using hred_deter. by subst.
+Defined.
+
+(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
+Next Obligation.
+  move => _ /= a b hdom ha _ hb _.
+  inversion hdom; subst.
+  - assumption.
+  - exfalso; sfirstorder.
+  - exfalso; sfirstorder.
+Defined.
+
+Lemma check_sub_pi_pi q A0 B0  A1 B1 h0 h1 :
+  check_sub q (PBind PPi A0 B0) (PBind PPi A1 B1) (A_BindCong PPi PPi A0 A1 B0 B1 h0 h1) =
+    check_sub_r (~~ q) A0 A1 h0 && check_sub_r q B0 B1 h1.
+Proof. reflexivity. Qed.
+
+Lemma check_sub_sig_sig q A0 B0  A1 B1 h0 h1 :
+  check_sub q (PBind PSig A0 B0) (PBind PSig A1 B1) (A_BindCong PSig PSig A0 A1 B0 B1 h0 h1) =
+    check_sub_r q A0 A1 h0 && check_sub_r q B0 B1 h1.
+  reflexivity. Qed.
+
+Lemma check_sub_univ_univ i j :
+  check_sub true (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb i j.
+Proof. reflexivity. Qed.
+
+Lemma check_sub_univ_univ' i j :
+  check_sub false (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb j i.
+  reflexivity. Qed.
+
+Lemma check_sub_nfnf q a b dom : check_sub_r q a b (A_NfNf a b dom) = check_sub q a b dom.
+Proof.
+  have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred.
+  have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
+  simpl.
+  destruct (fancy_hred b)=>//=.
+  destruct (fancy_hred a) =>//=.
+  destruct s as [a' ha']. simpl.
+  hauto l:on use:hred_complete.
+  destruct s as [b' hb']. simpl.
+  hauto l:on use:hred_complete.
+Qed.
+
+Lemma check_sub_hredl q a b a' ha doma :
+  check_sub_r q a b (A_HRedL a a' b ha doma) = check_sub_r q a' b doma.
+Proof.
+  simpl.
+  destruct (fancy_hred a).
+  - hauto q:on unfold:HRed.nf.
+  - destruct s as [x ?].
+    have ? : x = a' by eauto using hred_deter. subst.
+    simpl.
+    f_equal.
+    apply PropExtensionality.proof_irrelevance.
+Qed.
+
+Lemma check_sub_hredr q a b b' hu r a0 :
+  check_sub_r q a b (A_HRedR a b b' hu r a0) =
+    check_sub_r q a b' a0.
+Proof.
+  simpl.
+  destruct (fancy_hred a).
+  - simpl.
+    destruct (fancy_hred b) as [|[b'' hb']].
+    + hauto lq:on unfold:HRed.nf.
+    + simpl.
+      have ? : (b'' = b') by eauto using hred_deter. subst.
+      f_equal.
+      apply PropExtensionality.proof_irrelevance.
+  - exfalso.
+    sfirstorder use:hne_no_hred, hf_no_hred.
+Qed.
+
+#[export]Hint Rewrite check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ' check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop.

theories/executable_correct.v

@@ -4,12 +4,6 @@ Require Import ssreflect ssrbool.
 From stdpp Require Import relations (rtc(..)).
 From Hammer Require Import Tactics.
 
-Scheme algo_ind := Induction for algo_dom Sort Prop
-  with algor_ind := Induction for algo_dom_r Sort Prop.
-
-Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
-
-
 Lemma coqeqr_no_hred a b : a ∼ b -> HRed.nf a /\ HRed.nf b.
 Proof. induction 1; sauto lq:on unfold:HRed.nf. Qed.
 
@@ -18,6 +12,10 @@ Proof. induction 1;
          qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf.
 Qed.
 
+Lemma coqleq_no_hred a b : a ⋖ b -> HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1; qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred, coqeqr_no_hred unfold:HRed.nf.
+Qed.
 
 Lemma coqeq_neuneu u0 u1 :
   ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1.
@@ -88,12 +86,6 @@ Proof.
     sauto lq:on rew:off.
 Qed.
 
-Lemma hreds_nf_refl a b  :
-  HRed.nf a ->
-  rtc HRed.R a b ->
-  a = b.
-Proof. inversion 2; sfirstorder. Qed.
-
 Ltac ce_solv := move => *; simp ce_prop in *; hauto qb:on rew:off inv:CoqEq, CoqEq_Neu.
 
 Lemma check_equal_complete :
@@ -177,3 +169,134 @@ Proof.
       sfirstorder unfold:HRed.nf.
     + sauto lq:on use:hred_deter.
 Qed.
+
+Ltac simp_sub := with_strategy opaque [check_equal] simpl in *.
+
+(* Reusing algo_dom results in an inefficient proof, but i'll brute force it so i can get the result more quickly *)
+Lemma check_sub_sound :
+  (forall a b (h : algo_dom a b), forall q, check_sub q a b h -> if q then a ⋖ b else b ⋖ a) /\
+    (forall a b (h : algo_dom_r a b), forall q, check_sub_r q a b h -> if q then a ≪ b else b ≪ a).
+Proof.
+  apply algo_dom_mutual; try done.
+  - move => a [] //=; hauto qb:on.
+  - move => a0 a1 []//=; hauto qb:on.
+  - simpl. move => i j [];
+    sauto lq:on use:Reflect.Nat_leb_le.
+  - move => p0 p1 A0 A1 B0 B1 a iha b ihb q.
+    case : p0; case : p1; try done; simp ce_prop.
+    sauto lqb:on.
+    sauto lqb:on.
+  - hauto l:on.
+  - move => i j q h.
+    have {}h : nat_eqdec i j by sfirstorder.
+    case : nat_eqdec h => //=; sauto lq:on.
+  - simp_sub.
+    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
+  - simp_sub.
+    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
+  - simp_sub.
+    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
+  - move => a b n n0 i q h.
+    exfalso.
+    destruct a, b; try done; simp_sub; hauto lb:on use:check_equal_conf.
+  - move => a b doma ihdom q.
+    simp ce_prop. sauto lq:on.
+  - move => a a' b hr doma ihdom q.
+    simp ce_prop. move : ihdom => /[apply]. move {doma}.
+    sauto lq:on.
+  - move => a b b' n r dom ihdom q.
+    simp ce_prop.
+    move : ihdom => /[apply].
+    move {dom}.
+    sauto lq:on rew:off.
+Qed.
+
+Lemma check_sub_complete :
+  (forall a b (h : algo_dom a b), forall q, check_sub q a b h = false -> if q then ~ a ⋖ b else ~ b ⋖ a) /\
+    (forall a b (h : algo_dom_r a b), forall q, check_sub_r q a b h = false -> if q then ~ a ≪ b else ~ b ≪ a).
+Proof.
+  apply algo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu].
+  - move => i j q /=.
+    sauto lq:on rew:off use:PeanoNat.Nat.leb_le.
+  - move => p0 p1 A0 A1 B0 B1 a iha b ihb [].
+    + move => + h. inversion h; subst; simp ce_prop.
+      * move /nandP.
+        case.
+        by move => /negbTE {}/iha.
+        by move => /negbTE {}/ihb.
+      * move /nandP.
+        case.
+        by move => /negbTE {}/iha.
+        by move => /negbTE {}/ihb.
+      * inversion H.
+    + move => + h. inversion h; subst; simp ce_prop.
+      * move /nandP.
+        case.
+        by move => /negbTE {}/iha.
+        by move => /negbTE {}/ihb.
+      * move /nandP.
+        case.
+        by move => /negbTE {}/iha.
+        by move => /negbTE {}/ihb.
+      * inversion H.
+  - simp_sub.
+    sauto lq:on use:check_equal_complete.
+  - simp_sub.
+    move => p0 p1 u0 u1 i i0 a iha q.
+    move /nandP.
+    case.
+    move /nandP.
+    case => //.
+    by move /negP.
+    by move /negP.
+    move /negP.
+    move => h. eapply check_equal_complete in h.
+    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
+  - move => u0 u1 a0 a1 i i0 a hdom ihdom hdom' ihdom'.
+    simp_sub.
+    move /nandP.
+    case.
+    move/nandP.
+    case.
+    by move/negP.
+    by move/negP.
+    move /negP.
+    move => h. eapply check_equal_complete in h.
+    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
+  - move => P0 P1 u0 u1 b0 b1 c0 c1 i i0 dom ihdom dom' ihdom' dom'' ihdom'' dom''' ihdom''' q.
+    move /nandP.
+    case.
+    move /nandP.
+    case => //=.
+    by move/negP.
+    by move/negP.
+    move /negP => h. eapply check_equal_complete in h.
+    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
+  - move => a b h ih q. simp ce_prop => {}/ih.
+    case : q => h0;
+    inversion 1; subst; hauto l:on use:algo_dom_no_hred, hreds_nf_refl.
+  - move => a a' b r dom ihdom q.
+    simp ce_prop => {}/ihdom.
+    case : q => h0.
+    inversion 1; subst.
+    inversion H0; subst. sfirstorder use:coqleq_no_hred.
+    have ? : a' = y by eauto using hred_deter. subst.
+    sauto lq:on.
+    inversion 1; subst.
+    inversion H1; subst. sfirstorder use:coqleq_no_hred.
+    have ? : a' = y by eauto using hred_deter. subst.
+    sauto lq:on.
+  - move => a b b' n r hr ih q.
+    simp ce_prop => {}/ih.
+    case : q.
+    + move => h. inversion 1; subst.
+      inversion H1; subst.
+      sfirstorder use:coqleq_no_hred.
+      have ? : b' = y by eauto using hred_deter. subst.
+      sauto lq:on.
+    + move => h. inversion 1; subst.
+      inversion H0; subst.
+      sfirstorder use:coqleq_no_hred.
+      have ? : b' = y by eauto using hred_deter. subst.
+      sauto lq:on.
+Qed.

theories/termination.v

@@ -1,14 +1,282 @@
 Require Import common Autosubst2.core Autosubst2.unscoped Autosubst2.syntax algorithmic fp_red executable.
 From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
-From stdpp Require Import relations (nsteps (..)).
+From stdpp Require Import relations (nsteps (..), rtc(..)).
+Import Psatz.
+
+Lemma tm_conf_sym a b : tm_conf a b = tm_conf b a.
+Proof. case : a; case : b => //=. Qed.
+
+#[export]Hint Constructors algo_dom algo_dom_r : adom.
+
+Lemma algo_dom_r_inv a b :
+  algo_dom_r a b -> exists a0 b0, algo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
+Proof.
+  induction 1; hauto lq:on ctrs:rtc.
+Qed.
+
+Lemma A_HRedsL a a' b :
+  rtc HRed.R a a' ->
+  algo_dom_r a' b ->
+  algo_dom_r a b.
+  induction 1; sfirstorder use:A_HRedL.
+Qed.
+
+Lemma A_HRedsR a b b' :
+  HRed.nf a ->
+  rtc HRed.R b b' ->
+  algo_dom a b' ->
+  algo_dom_r a b.
+Proof. induction 2; sauto. Qed.
+
+Lemma algo_dom_sym :
+  (forall a b (h : algo_dom a b), algo_dom b a) /\
+    (forall a b (h : algo_dom_r a b), algo_dom_r b a).
+Proof.
+  apply algo_dom_mutual; try qauto use:tm_conf_sym db:adom.
+  move => a a' b hr h ih.
+  move /algo_dom_r_inv : ih => [a0][b0][ih0][ih1]ih2.
+  have nfa0 : HRed.nf a0 by sfirstorder use:algo_dom_no_hred.
+  sauto use:A_HRedsL, A_HRedsR.
+Qed.
 
 Definition term_metric k (a b : PTm) :=
   exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
 
+Lemma term_metric_sym k (a b : PTm) :
+  term_metric k a b -> term_metric k b a.
+Proof. hauto lq:on unfold:term_metric solve+:lia. Qed.
+
+Lemma term_metric_case k (a b : PTm) :
+  term_metric k a b ->
+  (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ term_metric k' a' b /\ k' < k.
+Proof.
+  move=>[i][j][va][vb][h0] [h1][h2][h3]h4.
+  case : a h0 => //=; try firstorder.
+  - inversion h0 as [|A B C D E F]; subst.
+    hauto qb:on use:ne_hne.
+    inversion E; subst => /=.
+    + hauto lq:on use:HRed.AppAbs unfold:term_metric solve+:lia.
+    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
+    + sfirstorder qb:on use:ne_hne.
+  - inversion h0 as [|A B C D E F]; subst.
+    hauto qb:on use:ne_hne.
+    inversion E; subst => /=.
+    + hauto lq:on use:HRed.ProjPair unfold:term_metric solve+:lia.
+    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
+  - inversion h0 as [|A B C D E F]; subst.
+    hauto qb:on use:ne_hne.
+    inversion E; subst => /=.
+    + hauto lq:on use:HRed.IndZero unfold:term_metric solve+:lia.
+    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
+    + sfirstorder use:ne_hne.
+    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
+    + sfirstorder use:ne_hne.
+    + sfirstorder use:ne_hne.
+Qed.
+
+Lemma A_Conf' a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  tm_conf a b ->
+  algo_dom_r a b.
+Proof.
+  move => ha hb.
+  have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
+  have {}hb : HRed.nf b by sfirstorder use:hf_no_hred, hne_no_hred.
+  move => ?.
+  apply A_NfNf.
+  by apply A_Conf.
+Qed.
+
+Lemma term_metric_abs : forall k a b,
+    term_metric k (PAbs a) (PAbs b) ->
+    exists k', k' < k /\ term_metric k' a b.
+Proof.
+  move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_abs_inv in hva, hvb.
+  move : hva => [a'][hva]?. subst.
+  move : hvb => [b'][hvb]?. subst.
+  simpl in *. exists (k - 1).
+  hauto lq:on unfold:term_metric solve+:lia.
+Qed.
+
+Lemma term_metric_pair : forall k a0 b0 a1 b1,
+    term_metric k (PPair a0 b0) (PPair a1 b1) ->
+    exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
+Proof.
+  move => k a0 b0 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_pair_inv in hva, hvb.
+  decompose record hva => {hva}.
+  decompose record hvb => {hvb}. subst.
+  simpl in *. exists (k - 1).
+  hauto lqb:on solve+:lia.
+Qed.
+
+Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 b1,
+    term_metric k (PBind p0 a0 b0) (PBind p1 a1 b1) ->
+    exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
+Proof.
+  move => k p0 a0 b0 p1 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_bind_inv in hva, hvb.
+  decompose record hva => {hva}.
+  decompose record hvb => {hvb}. subst.
+  simpl in *. exists (k - 1).
+  hauto lqb:on solve+:lia.
+Qed.
+
+Lemma term_metric_suc : forall k a b,
+    term_metric k (PSuc a) (PSuc b) ->
+    exists k', k' < k /\ term_metric k' a b.
+Proof.
+  move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
+  apply lored_nsteps_suc_inv in hva, hvb.
+  move : hva => [a'][hva]?. subst.
+  move : hvb => [b'][hvb]?. subst.
+  simpl in *. exists (k - 1).
+  hauto lq:on unfold:term_metric solve+:lia.
+Qed.
+
+Lemma term_metric_abs_neu k (a0 : PTm) u :
+  term_metric k (PAbs a0) u ->
+  ishne u ->
+  exists j, j < k /\ term_metric j a0 (PApp (ren_PTm shift u) (VarPTm var_zero)).
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
+  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
+  move /lored_nsteps_abs_inv : h0 => [a1][h01]?. subst.
+  exists (k - 1).
+  simpl in *. split. lia.
+  exists i,j,a1,(PApp (ren_PTm shift vb) (VarPTm var_zero)).
+  repeat split => //=.
+  apply lored_nsteps_app_cong.
+  by apply lored_nsteps_renaming.
+  by rewrite ishne_ren.
+  rewrite Bool.andb_true_r.
+  sfirstorder use:ne_nf_ren.
+  rewrite size_PTm_ren. lia.
+Qed.
+
+Lemma term_metric_pair_neu k (a0 b0 : PTm) u :
+  term_metric k (PPair a0 b0) u ->
+  ishne u ->
+  exists j, j < k /\ term_metric j (PProj PL u) a0 /\ term_metric j (PProj PR u) b0.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
+  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
+  move /lored_nsteps_pair_inv : h0 => [i0][j0][a1][b1][?][?][?][?]?. subst.
+  exists (k-1). sauto qb:on use:lored_nsteps_proj_cong unfold:term_metric solve+:lia.
+Qed.
+
+Lemma term_metric_app k (a0 b0 a1 b1 : PTm) :
+  term_metric k (PApp a0 b0) (PApp a1 b1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ term_metric j a0 a1 /\ term_metric j b0 b1.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4.
+  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). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia.
+Qed.
+
+Lemma term_metric_proj k p0 p1 (a0 a1 : PTm) :
+  term_metric k (PProj p0 a0) (PProj p1 a1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ term_metric j a0 a1.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
+  move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply].
+  move => [i0][a2][hi][?]ha02. subst.
+  move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply].
+  move => [i1][a3][hj][?]ha13. subst.
+  exists (k- 1).  hauto q:on use:ne_nf solve+:lia.
+Qed.
+
+Lemma term_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 :
+  term_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
+  ishne a0 ->
+  ishne a1 ->
+  exists j, j < k /\ term_metric j P0 P1 /\ term_metric j a0 a1 /\
+         term_metric j b0 b1 /\ term_metric j c0 c1.
+Proof.
+  move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
+  move /lored_nsteps_ind_inv /(_ hne0) : h0.
+  move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst.
+  move /lored_nsteps_ind_inv /(_ hne1) : h1.
+  move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst.
+  exists (k -1). simpl in *.
+  hauto lq:on rew:off use:ne_nf b:on solve+:lia.
+Qed.
+
+
+Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b.
+Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed.
+
 Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b.
 Proof.
+  move => [:hneL].
   elim /Wf_nat.lt_wf_ind.
   move => n ih a b h.
-  case : (fancy_hred a); cycle 1.
-  move => [a' ha']. apply : A_HRedL; eauto.
+  case /term_metric_case : (h); cycle 1.
+  move => [k'][a'][h0][h1]h2.
+  by apply : A_HRedL; eauto.
+  case /term_metric_sym /term_metric_case : (h); cycle 1.
+  move => [k'][b'][hb][/term_metric_sym h0]h1.
+  move => ha. have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
+  by apply : A_HRedR; eauto.
+  move => /[swap].
+  case => hfa; case => hfb.
+  - move : hfa hfb h.
+    case : a; case : b => //=; eauto 5 using A_Conf' with adom.
+    + hauto lq:on use:term_metric_abs db:adom.
+    + hauto lq:on use:term_metric_pair db:adom.
+    + hauto lq:on use:term_metric_bind db:adom.
+    + hauto lq:on use:term_metric_suc db:adom.
+  - abstract : hneL n ih a b h hfa hfb.
+    case : a hfa h => //=.
+    + hauto lq:on use:term_metric_abs_neu db:adom.
+    + scrush use:term_metric_pair_neu db:adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+    + case : b hfb => //=; eauto 5 using A_Conf' with adom.
+  - hauto q:on use:algo_dom_sym, term_metric_sym.
+  - move {hneL}.
+    case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom.
+    + move => a0 b0 a1 b1 nfa0 nfa1.
+      move /term_metric_app /(_ nfa0  nfa1) => [j][hj][ha]hb.
+      apply A_NfNf. apply A_AppCong => //; eauto.
+      have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
+      have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
+      eauto using algo_dom_r_algo_dom.
+    + move => p0 A0 p1 A1 neA0 neA1.
+      have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred.
+      have {}nfb0 : HRed.nf A1 by sfirstorder use:hne_no_hred.
+      hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom.
+    + move => P0 a0 b0 c0 P1 a1 b1 c1 nea0 nea1.
+      have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
+      have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
+      hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
+Qed.
+
+Lemma sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b.
+Proof.
+  move /LoReds.FromSN => [va [ha0 ha1]].
+  move /LoReds.FromSN => [vb [hb0 hb1]].
+  eapply relations.rtc_nsteps in ha0.
+  eapply relations.rtc_nsteps in hb0.
+  hauto lq:on unfold:term_metric solve+:lia.
+Qed.
+
+Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b.
+Proof.
+  move : sn_term_metric; repeat move/[apply].
+  move => [k]+.
+  eauto using term_metric_algo_dom.
+Qed.