Remove itauto dependency as it introduces weird axioms

theories/common.v

@@ -1,4 +1,4 @@
-Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect.
+Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect ssrbool.
 From Equations Require Import Equations.
 Derive NoConfusion for nat PTag BTag PTm.
 Derive EqDec for BTag PTag PTm.
@@ -6,6 +6,7 @@ From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
 From Hammer Require Import Tactics.
+From stdpp Require Import relations (rtc(..)).
 
 Inductive lookup : nat -> list PTm -> PTm -> Prop :=
 | here A Γ : lookup 0 (cons A Γ) (ren_PTm shift A)
@@ -119,6 +120,26 @@ Definition isabs (a : PTm) :=
   | _ => false
   end.
 
+Definition tm_nonconf (a b : PTm) : bool :=
+  match a, b with
+  | PAbs _, _ => (~~ ishf b) || isabs b
+  | _, PAbs _ => ~~ ishf a
+  | VarPTm _, VarPTm _ => true
+  | PPair _ _, _ => (~~ ishf b) || ispair b
+  | _, PPair _ _ => ~~ ishf a
+  | PZero, PZero => true
+  | PSuc _, PSuc _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | PNat, PNat => true
+  | PUniv _, PUniv _ => true
+  | PBind _ _ _, PBind _ _ _ => true
+  | _,_=> false
+  end.
+
+Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
+
 Definition ishf_ren (a : PTm)  (ξ : nat -> nat) :
   ishf (ren_PTm ξ a) = ishf a.
 Proof. case : a => //=. Qed.
@@ -175,3 +196,406 @@ Module HRed.
 
     Definition nf a := forall b, ~ R a b.
 End HRed.
+
+Inductive algo_dom : PTm -> PTm -> Prop :=
+| A_AbsAbs a b :
+  algo_dom_r a b ->
+  (* --------------------- *)
+  algo_dom (PAbs a) (PAbs b)
+
+| A_AbsNeu a u :
+  ishne u ->
+  algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
+  (* --------------------- *)
+  algo_dom (PAbs a) u
+
+| A_NeuAbs a u :
+  ishne u ->
+  algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
+  (* --------------------- *)
+  algo_dom u (PAbs a)
+
+| A_PairPair a0 a1 b0 b1 :
+  algo_dom_r a0 a1 ->
+  algo_dom_r b0 b1 ->
+  (* ---------------------------- *)
+  algo_dom (PPair a0 b0) (PPair a1 b1)
+
+| A_PairNeu a0 a1 u :
+  ishne u ->
+  algo_dom_r a0 (PProj PL u) ->
+  algo_dom_r a1 (PProj PR u) ->
+  (* ----------------------- *)
+  algo_dom (PPair a0 a1) u
+
+| A_NeuPair a0 a1 u :
+  ishne u ->
+  algo_dom_r (PProj PL u) a0 ->
+  algo_dom_r (PProj PR u) a1 ->
+  (* ----------------------- *)
+  algo_dom u (PPair a0 a1)
+
+| A_ZeroZero :
+  algo_dom PZero PZero
+
+| A_SucSuc a0 a1 :
+  algo_dom_r a0 a1 ->
+  algo_dom (PSuc a0) (PSuc a1)
+
+| A_UnivCong i j :
+  (* -------------------------- *)
+  algo_dom (PUniv i) (PUniv j)
+
+| A_BindCong p0 p1 A0 A1 B0 B1 :
+  algo_dom_r A0 A1 ->
+  algo_dom_r B0 B1 ->
+  (* ---------------------------- *)
+  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
+
+| A_NatCong :
+  algo_dom PNat PNat
+
+| A_VarCong i j :
+  (* -------------------------- *)
+  algo_dom (VarPTm i) (VarPTm j)
+
+| A_AppCong u0 u1 a0 a1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r a0 a1 ->
+  (* ------------------------- *)
+  algo_dom (PApp u0 a0) (PApp u1 a1)
+
+| A_ProjCong p0 p1 u0 u1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom u0 u1 ->
+  (* ---------------------  *)
+  algo_dom (PProj p0 u0) (PProj p1 u1)
+
+| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
+  ishne u0 ->
+  ishne u1 ->
+  algo_dom_r P0 P1 ->
+  algo_dom u0 u1 ->
+  algo_dom_r b0 b1 ->
+  algo_dom_r c0 c1 ->
+  algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
+
+| A_Conf a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  tm_conf a b ->
+  algo_dom a b
+
+with algo_dom_r : PTm  -> PTm -> Prop :=
+| A_NfNf a b :
+  algo_dom a b ->
+  algo_dom_r a b
+
+| A_HRedL a a' b  :
+  HRed.R a a' ->
+  algo_dom_r a' b ->
+  (* ----------------------- *)
+  algo_dom_r a b
+
+| A_HRedR a b b'  :
+  HRed.nf a ->
+  HRed.R b b' ->
+  algo_dom_r a b' ->
+  (* ----------------------- *)
+  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.
+#[export]Hint Constructors algo_dom algo_dom_r : adom.
+
+Definition stm_nonconf a b :=
+  match a, b with
+  | PUniv _, PUniv _ => true
+  | PBind PPi _ _, PBind PPi _ _ => true
+  | PBind PSig _ _, PBind PSig _ _ => true
+  | PNat, PNat => true
+  | VarPTm _, VarPTm _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | _, _ => false
+  end.
+
+Definition neuneu_nonconf a b :=
+  match a, b with
+  | VarPTm _, VarPTm _ => true
+  | PApp _ _, PApp _ _ => true
+  | PProj _ _, PProj _ _ => true
+  | PInd _ _ _ _, PInd _ _ _ _ => true
+  | _, _ => false
+  end.
+
+Lemma stm_tm_nonconf a b :
+  stm_nonconf a b -> tm_nonconf a b.
+Proof. apply /implyP.
+       destruct a ,b =>//=; hauto lq:on inv:PTag, BTag.
+Qed.
+
+Definition stm_conf a b := ~~ stm_nonconf a b.
+
+Lemma tm_stm_conf a b :
+  tm_conf a b -> stm_conf a b.
+Proof.
+  rewrite /tm_conf /stm_conf.
+  apply /contra /stm_tm_nonconf.
+Qed.
+
+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 :
+  neuneu_nonconf a b ->
+  algo_dom a b ->
+  salgo_dom a b
+
+| S_Conf a b :
+  ishf a \/ ishne a ->
+  ishf b \/ ishne b ->
+  stm_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.
+
+#[export]Hint Constructors salgo_dom salgo_dom_r : sdom.
+Scheme salgo_ind := Induction for salgo_dom Sort Prop
+  with salgor_ind := Induction for salgo_dom_r Sort Prop.
+
+Combined Scheme salgo_dom_mutual from salgo_ind, salgor_ind.
+
+Lemma hf_no_hred (a b : PTm) :
+  ishf a ->
+  HRed.R a b ->
+  False.
+Proof. hauto l:on inv:HRed.R. Qed.
+
+Lemma hne_no_hred (a b : PTm) :
+  ishne a ->
+  HRed.R a b ->
+  False.
+Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
+
+Ltac2 destruct_salgo () :=
+  lazy_match! goal with
+  | [_ : is_true (ishne ?a) |- is_true (stm_conf ?a _) ] =>
+      if Constr.is_var a then destruct $a; ltac1:(done) else ()
+  | [|- is_true (stm_conf _ _)] =>
+      unfold stm_conf; ltac1:(done)
+  end.
+
+Ltac destruct_salgo := ltac2:(destruct_salgo ()).
+
+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 tm_conf_sym a b : tm_conf a b = tm_conf b a.
+Proof. case : a; case : b => //=. Qed.
+
+Lemma algo_dom_no_hred (a b : PTm) :
+  algo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf.
+Qed.
+
+
+Lemma A_HRedR' a b b' :
+  HRed.R b b' ->
+  algo_dom_r a b' ->
+  algo_dom_r a b.
+Proof.
+  move => hb /algo_dom_r_inv.
+  move => [a0 [b0 [h0 [h1 h2]]]].
+  have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc.
+  have ? : HRed.nf a0 by sfirstorder use:algo_dom_no_hred.
+  hauto lq:on use:A_HRedsL, A_HRedsR.
+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,A_HRedR' db:adom.
+Qed.
+
+Lemma salgo_dom_r_inv a b :
+  salgo_dom_r a b -> exists a0 b0, salgo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0.
+Proof.
+  induction 1; hauto lq:on ctrs:rtc.
+Qed.
+
+Lemma S_HRedsL a a' b :
+  rtc HRed.R a a' ->
+  salgo_dom_r a' b ->
+  salgo_dom_r a b.
+  induction 1; sfirstorder use:S_HRedL.
+Qed.
+
+Lemma S_HRedsR a b b' :
+  HRed.nf a ->
+  rtc HRed.R b b' ->
+  salgo_dom a b' ->
+  salgo_dom_r a b.
+Proof. induction 2; sauto. Qed.
+
+Lemma stm_conf_sym a b : stm_conf a b = stm_conf b a.
+Proof. case : a; case : b => //=; hauto lq:on inv:PTag, BTag. Qed.
+
+Lemma salgo_dom_no_hred (a b : PTm) :
+  salgo_dom a b ->
+  HRed.nf a /\ HRed.nf b.
+Proof.
+  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred, algo_dom_no_hred lq:on unfold:HRed.nf.
+Qed.
+
+Lemma S_HRedR' a b b' :
+  HRed.R b b' ->
+  salgo_dom_r a b' ->
+  salgo_dom_r a b.
+Proof.
+  move => hb /salgo_dom_r_inv.
+  move => [a0 [b0 [h0 [h1 h2]]]].
+  have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc.
+  have ? : HRed.nf a0 by sfirstorder use:salgo_dom_no_hred.
+  hauto lq:on use:S_HRedsL, S_HRedsR.
+Qed.
+
+Ltac solve_conf := intros; split;
+      apply S_Conf; solve [destruct_salgo | sfirstorder ctrs:salgo_dom use:hne_no_hred, hf_no_hred].
+
+Ltac solve_basic := hauto q:on ctrs:salgo_dom, salgo_dom_r, algo_dom use:algo_dom_sym.
+
+Lemma algo_dom_salgo_dom :
+  (forall a b, algo_dom a b -> salgo_dom a b /\ salgo_dom b a) /\
+    (forall a b, algo_dom_r a b -> salgo_dom_r a b /\ salgo_dom_r b a).
+Proof.
+  apply algo_dom_mutual => //=; try first [solve_conf | solve_basic].
+  - case; case; hauto lq:on ctrs:salgo_dom use:algo_dom_sym inv:HRed.R unfold:HRed.nf.
+  - move => a b ha hb hc. split;
+      apply S_Conf; hauto l:on use:tm_conf_sym, tm_stm_conf.
+  - hauto lq:on ctrs:salgo_dom_r use:S_HRedR'.
+Qed.
+
+Fixpoint hred (a : PTm) : option (PTm) :=
+    match a with
+    | VarPTm i => None
+    | PAbs a => None
+    | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
+    | PApp a b =>
+        match hred a with
+        | Some a => Some (PApp a b)
+        | None => None
+        end
+    | PPair a b => None
+    | PProj p (PPair a b) => if p is PL then Some a else Some b
+    | PProj p a =>
+        match hred a with
+        | Some a => Some (PProj p a)
+        | None => None
+        end
+    | PUniv i => None
+    | PBind p A B => None
+    | PNat => None
+    | PZero => None
+    | PSuc a => None
+    | PInd P PZero b c => Some b
+    | PInd P (PSuc a) b c =>
+        Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+    | PInd P a b c =>
+        match hred a with
+        | Some a => Some (PInd P a b c)
+        | None => None
+        end
+    end.
+
+Lemma hred_complete (a b : PTm) :
+  HRed.R a b -> hred a = Some b.
+Proof.
+  induction 1; hauto lq:on rew:off inv:HRed.R b:on.
+Qed.
+
+Lemma hred_sound (a b : PTm):
+  hred a = Some b -> HRed.R a b.
+Proof.
+  elim : a b; hauto q:on dep:on ctrs:HRed.R.
+Qed.
+
+Lemma hred_deter (a b0 b1 : PTm) :
+  HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
+Proof.
+  move /hred_complete => + /hred_complete. congruence.
+Qed.
+
+Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}.
+  destruct (hred a) eqn:eq.
+  right. exists p. by apply hred_sound in eq.
+  left. move => b /hred_complete. congruence.
+Defined.
+
+Lemma hreds_nf_refl a b  :
+  HRed.nf a ->
+  rtc HRed.R a b ->
+  a = b.
+Proof. inversion 2; sfirstorder. 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.

theories/executable.v

@@ -11,345 +11,6 @@ Set Default Proof Mode "Classic".
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
 
-Definition tm_nonconf (a b : PTm) : bool :=
-  match a, b with
-  | PAbs _, _ => (~~ ishf b) || isabs b
-  | _, PAbs _ => ~~ ishf a
-  | VarPTm _, VarPTm _ => true
-  | PPair _ _, _ => (~~ ishf b) || ispair b
-  | _, PPair _ _ => ~~ ishf a
-  | PZero, PZero => true
-  | PSuc _, PSuc _ => true
-  | PApp _ _, PApp _ _ => (~~ ishf a) && (~~ ishf b)
-  | PProj _ _, PProj _ _ => (~~ ishf a) && (~~ ishf b)
-  | PInd _ _ _ _, PInd _ _ _ _ => (~~ ishf a) && (~~ ishf b)
-  | PNat, PNat => true
-  | PUniv _, PUniv _ => true
-  | PBind _ _ _, PBind _ _ _ => true
-  | _,_=> false
-  end.
-
-Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b.
-
-Inductive eq_view : PTm -> PTm -> Type :=
-| V_AbsAbs a b :
-  eq_view (PAbs a) (PAbs b)
-| V_AbsNeu a b :
-  ~~ ishf b ->
-  eq_view (PAbs a) b
-| V_NeuAbs a b :
-  ~~ ishf a ->
-  eq_view a (PAbs b)
-| V_VarVar i j :
-  eq_view (VarPTm i) (VarPTm j)
-| V_PairPair a0 b0 a1 b1 :
-  eq_view (PPair a0 b0) (PPair a1 b1)
-| V_PairNeu a0 b0 u :
-  ~~ ishf u ->
-  eq_view (PPair a0 b0) u
-| V_NeuPair u a1 b1 :
-  ~~ ishf u ->
-  eq_view u (PPair a1 b1)
-| V_ZeroZero :
-  eq_view PZero PZero
-| V_SucSuc a b :
-  eq_view (PSuc a) (PSuc b)
-| V_AppApp u0 b0 u1 b1 :
-  eq_view (PApp u0 b0) (PApp u1 b1)
-| V_ProjProj p0 u0 p1 u1 :
-  eq_view (PProj p0 u0) (PProj p1 u1)
-| V_IndInd P0 u0 b0 c0  P1 u1 b1 c1 :
-  eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
-| V_NatNat :
-  eq_view PNat PNat
-| V_BindBind p0 A0 B0 p1 A1 B1 :
-  eq_view (PBind p0 A0 B0) (PBind p1 A1 B1)
-| V_UnivUniv i j :
-  eq_view (PUniv i) (PUniv j)
-| V_Others a b :
-  tm_conf a b ->
-  eq_view a b.
-
-Equations tm_to_eq_view (a b : PTm) : eq_view a b :=
-  tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b;
-  tm_to_eq_view (PAbs a) (PApp b0 b1) := V_AbsNeu a (PApp b0 b1) _;
-  tm_to_eq_view (PAbs a) (VarPTm i) := V_AbsNeu a (VarPTm i) _;
-  tm_to_eq_view (PAbs a) (PProj p b) := V_AbsNeu a (PProj p b) _;
-  tm_to_eq_view (PAbs a) (PInd P u b c) := V_AbsNeu a (PInd P u b c) _;
-  tm_to_eq_view (VarPTm i) (PAbs a) := V_NeuAbs (VarPTm i) a _;
-  tm_to_eq_view (PApp b0 b1) (PAbs b) := V_NeuAbs (PApp b0 b1) b _;
-  tm_to_eq_view (PProj p b) (PAbs a) := V_NeuAbs (PProj p b) a _;
-  tm_to_eq_view (PInd P u b c) (PAbs a) := V_NeuAbs (PInd P u b c) a _;
-  tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j;
-  tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1;
-  (* tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; *)
-  tm_to_eq_view (PPair a0 b0) (VarPTm i) := V_PairNeu a0 b0 (VarPTm i) _;
-  tm_to_eq_view (PPair a0 b0) (PApp c0 c1) := V_PairNeu a0 b0 (PApp c0 c1) _;
-  tm_to_eq_view (PPair a0 b0) (PProj p c) := V_PairNeu a0 b0 (PProj p c) _;
-  tm_to_eq_view (PPair a0 b0) (PInd P t0 t1 t2) := V_PairNeu a0 b0 (PInd P t0 t1 t2) _;
-  (* tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; *)
-  tm_to_eq_view (VarPTm i) (PPair a1 b1) := V_NeuPair (VarPTm i) a1 b1 _;
-  tm_to_eq_view (PApp t0 t1) (PPair a1 b1) := V_NeuPair (PApp t0 t1) a1 b1 _;
-  tm_to_eq_view (PProj t0 t1) (PPair a1 b1) := V_NeuPair (PProj t0 t1) a1 b1 _;
-  tm_to_eq_view (PInd t0 t1 t2 t3) (PPair a1 b1) := V_NeuPair (PInd t0 t1 t2 t3) a1 b1 _;
-  tm_to_eq_view PZero PZero := V_ZeroZero;
-  tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b;
-  tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1;
-  tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1;
-  tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1;
-  tm_to_eq_view PNat PNat := V_NatNat;
-  tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j;
-  tm_to_eq_view (PBind p0 A0 B0)  (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1;
-  tm_to_eq_view a b := V_Others a b _.
-
-Inductive algo_dom : PTm -> PTm -> Prop :=
-| A_AbsAbs a b :
-  algo_dom_r a b ->
-  (* --------------------- *)
-  algo_dom (PAbs a) (PAbs b)
-
-| A_AbsNeu a u :
-  ishne u ->
-  algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
-  (* --------------------- *)
-  algo_dom (PAbs a) u
-
-| A_NeuAbs a u :
-  ishne u ->
-  algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
-  (* --------------------- *)
-  algo_dom u (PAbs a)
-
-| A_PairPair a0 a1 b0 b1 :
-  algo_dom_r a0 a1 ->
-  algo_dom_r b0 b1 ->
-  (* ---------------------------- *)
-  algo_dom (PPair a0 b0) (PPair a1 b1)
-
-| A_PairNeu a0 a1 u :
-  ishne u ->
-  algo_dom_r a0 (PProj PL u) ->
-  algo_dom_r a1 (PProj PR u) ->
-  (* ----------------------- *)
-  algo_dom (PPair a0 a1) u
-
-| A_NeuPair a0 a1 u :
-  ishne u ->
-  algo_dom_r (PProj PL u) a0 ->
-  algo_dom_r (PProj PR u) a1 ->
-  (* ----------------------- *)
-  algo_dom u (PPair a0 a1)
-
-| A_ZeroZero :
-  algo_dom PZero PZero
-
-| A_SucSuc a0 a1 :
-  algo_dom_r a0 a1 ->
-  algo_dom (PSuc a0) (PSuc a1)
-
-| A_UnivCong i j :
-  (* -------------------------- *)
-  algo_dom (PUniv i) (PUniv j)
-
-| A_BindCong p0 p1 A0 A1 B0 B1 :
-  algo_dom_r A0 A1 ->
-  algo_dom_r B0 B1 ->
-  (* ---------------------------- *)
-  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
-
-| A_NatCong :
-  algo_dom PNat PNat
-
-| A_VarCong i j :
-  (* -------------------------- *)
-  algo_dom (VarPTm i) (VarPTm j)
-
-| A_ProjCong p0 p1 u0 u1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom u0 u1 ->
-  (* ---------------------  *)
-  algo_dom (PProj p0 u0) (PProj p1 u1)
-
-| A_AppCong u0 u1 a0 a1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom u0 u1 ->
-  algo_dom_r a0 a1 ->
-  (* ------------------------- *)
-  algo_dom (PApp u0 a0) (PApp u1 a1)
-
-| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
-  ishne u0 ->
-  ishne u1 ->
-  algo_dom_r P0 P1 ->
-  algo_dom u0 u1 ->
-  algo_dom_r b0 b1 ->
-  algo_dom_r c0 c1 ->
-  algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
-
-| A_Conf a b :
-  HRed.nf a ->
-  HRed.nf b ->
-  tm_conf a b ->
-  algo_dom a b
-
-with algo_dom_r : PTm  -> PTm -> Prop :=
-| A_NfNf a b :
-  algo_dom a b ->
-  algo_dom_r a b
-
-| A_HRedL a a' b  :
-  HRed.R a a' ->
-  algo_dom_r a' b ->
-  (* ----------------------- *)
-  algo_dom_r a b
-
-| A_HRedR a b b'  :
-  HRed.nf a ->
-  HRed.R b b' ->
-  algo_dom_r a b' ->
-  (* ----------------------- *)
-  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 ->
-  False.
-Proof. hauto l:on inv:HRed.R. Qed.
-
-Lemma hne_no_hred (a b : PTm) :
-  ishne a ->
-  HRed.R a b ->
-  False.
-Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
-
-Lemma algo_dom_no_hred (a b : PTm) :
-  algo_dom a b ->
-  HRed.nf a /\ HRed.nf b.
-Proof.
-  induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf.
-Qed.
-
-Derive Signature for algo_dom algo_dom_r.
-
-Fixpoint hred (a : PTm) : option (PTm) :=
-    match a with
-    | VarPTm i => None
-    | PAbs a => None
-    | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a)
-    | PApp a b =>
-        match hred a with
-        | Some a => Some (PApp a b)
-        | None => None
-        end
-    | PPair a b => None
-    | PProj p (PPair a b) => if p is PL then Some a else Some b
-    | PProj p a =>
-        match hred a with
-        | Some a => Some (PProj p a)
-        | None => None
-        end
-    | PUniv i => None
-    | PBind p A B => None
-    | PNat => None
-    | PZero => None
-    | PSuc a => None
-    | PInd P PZero b c => Some b
-    | PInd P (PSuc a) b c =>
-        Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
-    | PInd P a b c =>
-        match hred a with
-        | Some a => Some (PInd P a b c)
-        | None => None
-        end
-    end.
-
-Lemma hred_complete (a b : PTm) :
-  HRed.R a b -> hred a = Some b.
-Proof.
-  induction 1; hauto lq:on rew:off inv:HRed.R b:on.
-Qed.
-
-Lemma hred_sound (a b : PTm):
-  hred a = Some b -> HRed.R a b.
-Proof.
-  elim : a b; hauto q:on dep:on ctrs:HRed.R.
-Qed.
-
-Lemma hred_deter (a b0 b1 : PTm) :
-  HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
-Proof.
-  move /hred_complete => + /hred_complete. congruence.
-Qed.
-
-Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}.
-  destruct (hred a) eqn:eq.
-  right. exists p. by apply hred_sound in eq.
-  left. move => b /hred_complete. congruence.
-Defined.
-
 Ltac2 destruct_algo () :=
   lazy_match! goal with
   | [h : algo_dom ?a ?b |- _ ] =>
@@ -373,70 +34,79 @@ Ltac solve_check_equal :=
   | _ => idtac
   end].
 
-#[derive(equations=no)]Equations check_equal (a b : PTm) (h : algo_dom a b) :
+Global Set Transparent Obligations.
-  bool by struct h :=
-  check_equal a b h with tm_to_eq_view a b :=
-  check_equal _ _ h (V_VarVar i j) := nat_eqdec i j;
-  check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv);
-  check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv);
-  check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv);
-  check_equal _ _ h (V_PairPair a0 b0 a1 b1) :=
-    check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
-  check_equal _ _ h (V_PairNeu a0 b0 u _) :=
-    check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv);
-  check_equal _ _ h (V_NeuPair u a1 b1 _) :=
-    check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv);
-  check_equal _ _ h V_NatNat := true;
-  check_equal _ _ h V_ZeroZero := true;
-  check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv);
-  check_equal _ _ h (V_ProjProj p0 a p1 b) :=
-    PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv);
-  check_equal _ _ h (V_AppApp a0 b0 a1 b1) :=
-    check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv);
-  check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) :=
-    check_equal_r P0 P1 ltac:(check_equal_triv) &&
-      check_equal u0 u1 ltac:(check_equal_triv) &&
-      check_equal_r b0 b1 ltac:(check_equal_triv) &&
-      check_equal_r c0 c1 ltac:(check_equal_triv);
-  check_equal _ _ h (V_UnivUniv i j) := nat_eqdec i j;
-  check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) :=
-    BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv);
-  check_equal _ _ _ _ := false
 
-  (* check_equal a b h := false; *)
+Local Obligation Tactic := try solve [check_equal_triv | sfirstorder].
-  with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) :
+
-  bool by struct h0 :=
+Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool :=
-    check_equal_r a b h with (fancy_hred a) :=
+  match a, b with
-      check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _;
+  | VarPTm i, VarPTm j => nat_eqdec i j
-      check_equal_r a b h (inl h')  with (fancy_hred b) :=
+  | PAbs a, PAbs b => check_equal_r a b _
-        | inr b' := check_equal_r a (proj1_sig b') _;
+  | PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
-                 | inl h'' := check_equal a b _.
+  | PAbs a, PApp _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PInd _ _ _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | PAbs a, PProj _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
+  | VarPTm _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PApp _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PProj _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PInd _ _ _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
+  | PPair a0 b0, PPair a1 b1 =>
+      check_equal_r a0 a1 _ && check_equal_r b0 b1 _
+  | PPair a0 b0, VarPTm _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PProj _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PApp _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | PPair a0 b0, PInd _ _ _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
+  | VarPTm _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PApp _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PProj _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PInd _ _ _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
+  | PNat, PNat => true
+  | PZero, PZero => true
+  | PSuc a, PSuc b => check_equal_r a b _
+  | PProj p0 a, PProj p1 b => PTag_eqdec p0 p1 && check_equal a b _
+  | PApp a0 b0, PApp a1 b1 => check_equal a0 a1 _ && check_equal_r b0 b1 _
+  | PInd P0 u0 b0 c0, PInd P1 u1 b1 c1 =>
+      check_equal_r P0 P1 _ && check_equal u0 u1 _ && check_equal_r b0 b1 _ && check_equal_r c0 c1 _
+  | PUniv i, PUniv j => nat_eqdec i j
+  | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_eqdec p0 p1 && check_equal_r A0 A1 _ && check_equal_r B0 B1 _
+  | _, _ => false
+  end
+with check_equal_r (a b : PTm) (h : algo_dom_r a b) {struct h} : bool :=
+  match fancy_hred a with
+  | inr a' => check_equal_r (proj1_sig a') b _
+  | inl ha' => match fancy_hred b with
+            | inr b' => check_equal_r a (proj1_sig b') _
+            | inl hb' => check_equal a b _
+            end
+  end.
 
 Next Obligation.
-  intros.
+  simpl. intros. clear Heq_anonymous.  destruct a' as [a' ha']. simpl.
   inversion h; subst => //=.
-  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
-  exfalso. hauto l:on use:hred_complete unfold:HRed.nf.
-Defined.
-
-Next Obligation.
-  intros.
-  destruct h.
   exfalso. sfirstorder use:algo_dom_no_hred.
+  assert (a' = a'0) by eauto using hred_deter. by subst.
   exfalso. sfirstorder.
-  assert (  b' = b'0)by eauto using hred_deter. subst.
-  apply h.
 Defined.
 
 Next Obligation.
-  simpl. intros.
+  simpl. intros. clear Heq_anonymous Heq_anonymous0.
-  inversion h; subst =>//=.
+  destruct b' as [b' hb']. simpl.
-  exfalso. sfirstorder use:algo_dom_no_hred.
+  inversion h; subst.
-  move {h}.
+  - exfalso.
-  assert (a' = a'0) by eauto using hred_deter, hred_sound. by subst.
+    sfirstorder use:algo_dom_no_hred.
-  exfalso. sfirstorder use:hne_no_hred, hf_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_equal_abs_abs a b h : check_equal (PAbs a) (PAbs b) (A_AbsAbs a b h) = check_equal_r a b h.
 Proof. reflexivity. Qed.
@@ -491,14 +161,14 @@ Proof.
   sfirstorder use:hred_complete, hred_sound.
 Qed.
 
+Ltac simp_check_r := with_strategy opaque [check_equal] simpl in *.
+
 Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal 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.
+  simp_check_r.
-  rewrite /check_equal_r_functional.
   destruct (fancy_hred a).
-  simpl.
   destruct (fancy_hred b).
   reflexivity.
   exfalso. hauto l:on use:hred_complete.
@@ -509,11 +179,9 @@ Lemma check_equal_hredl a b a' ha doma :
   check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma.
 Proof.
   simpl.
-  rewrite /check_equal_r_functional.
   destruct (fancy_hred a).
   - hauto q:on unfold:HRed.nf.
   - destruct s as [x ?].
-    rewrite /check_equal_r_functional.
     have ? : x = a' by eauto using hred_deter. subst.
     simpl.
     f_equal.
@@ -524,7 +192,7 @@ Lemma check_equal_hredr a b b' hu r a0 :
   check_equal_r a b (A_HRedR a b b' hu r a0) =
     check_equal_r a b' a0.
 Proof.
-  simpl. rewrite /check_equal_r_functional.
+  simpl.
   destruct (fancy_hred a).
   - simpl.
     destruct (fancy_hred b) as [|[b'' hb']].
@@ -547,31 +215,51 @@ 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].
+Ltac2 destruct_salgo () :=
+  lazy_match! goal with
+  | [h : salgo_dom ?a ?b |- _ ] =>
+      if is_var a then destruct $a; ltac1:(done)  else
+        (if is_var b then destruct $b; ltac1:(done) else ())
+  end.
 
-Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} :=
+Ltac check_sub_triv :=
+  intros;subst;
+  lazymatch goal with
+  (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
+  | [_ : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
+  | _ => idtac
+  end.
+
+Local Obligation Tactic := try solve [check_sub_triv | sfirstorder].
+
+Program Fixpoint check_sub (a b : PTm) (h : salgo_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 _
+      check_sub_r A1 A0 _ && check_sub_r B0 B1 _
   | PBind PSig A0 B0, PBind PSig A1 B1 =>
-      check_sub_r q A0 A1 _ && check_sub_r q B0 B1 _
+      check_sub_r A0 A1 _ && check_sub_r B0 B1 _
   | PUniv i, PUniv j =>
-      if q then PeanoNat.Nat.leb i j else PeanoNat.Nat.leb j i
+      PeanoNat.Nat.leb i j
   | PNat, PNat => true
-  | _ ,_ => ishne a && ishne b && check_equal a b h
+  | PApp _ _ , PApp _ _ => check_equal a b _
+  | VarPTm _, VarPTm _ => check_equal a b _
+  | PInd _ _ _ _, PInd _ _ _ _ => check_equal a b _
+  | PProj _ _, PProj _ _ => check_equal a b _
+  | _, _ => false
   end
-with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} :=
+with check_sub_r (a b : PTm) (h : salgo_dom_r a b) {struct h} :=
   match fancy_hred a with
-  | inr a' => check_sub_r q (proj1_sig a') b _
+  | inr a' => check_sub_r (proj1_sig a') b _
   | inl ha' => match fancy_hred b with
-            | inr b' => check_sub_r q a (proj1_sig b') _
+            | inr b' => check_sub_r a (proj1_sig b') _
-            | inl hb' => check_sub q a b _
+            | inl hb' => check_sub  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.
+  exfalso. sfirstorder use:salgo_dom_no_hred.
   assert (a' = a'0) by eauto using hred_deter. by subst.
   exfalso. sfirstorder.
 Defined.
@@ -581,7 +269,7 @@ Next Obligation.
   destruct b' as [b' hb']. simpl.
   inversion h; subst.
   - exfalso.
-    sfirstorder use:algo_dom_no_hred.
+    sfirstorder use:salgo_dom_no_hred.
   - exfalso.
     sfirstorder.
   - assert (b' = b'0) by eauto using hred_deter. by subst.
@@ -589,34 +277,30 @@ Defined.
 
 (* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
 Next Obligation.
-  move => _ /= a b hdom ha _ hb _.
+  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 :
+Lemma check_sub_pi_pi 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 (PBind PPi A0 B0) (PBind PPi A1 B1) (S_PiCong A0 A1 B0 B1 h0 h1) =
-    check_sub_r (~~ q) A0 A1 h0 && check_sub_r q B0 B1 h1.
+    check_sub_r A1 A0 h0 && check_sub_r B0 B1 h1.
 Proof. reflexivity. Qed.
 
-Lemma check_sub_sig_sig q A0 B0  A1 B1 h0 h1 :
+Lemma check_sub_sig_sig 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 (PBind PSig A0 B0) (PBind PSig A1 B1) (S_SigCong A0 A1 B0 B1 h0 h1) =
-    check_sub_r q A0 A1 h0 && check_sub_r q B0 B1 h1.
+    check_sub_r A0 A1 h0 && check_sub_r B0 B1 h1.
-  reflexivity. Qed.
+Proof. 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.
+  check_sub (PUniv i) (PUniv j) (S_UnivCong i j) = PeanoNat.Nat.leb i j.
 Proof. reflexivity. Qed.
 
-Lemma check_sub_univ_univ' i j :
+Lemma check_sub_nfnf a b dom : check_sub_r a b (S_NfNf a b dom) = check_sub a b dom.
-  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 [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_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)=>//=.
@@ -627,8 +311,8 @@ Proof.
   hauto l:on use:hred_complete.
 Qed.
 
-Lemma check_sub_hredl q a b a' ha doma :
+Lemma check_sub_hredl 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.
+  check_sub_r a b (S_HRedL a a' b ha doma) = check_sub_r a' b doma.
 Proof.
   simpl.
   destruct (fancy_hred a).
@@ -640,9 +324,9 @@ Proof.
     apply PropExtensionality.proof_irrelevance.
 Qed.
 
-Lemma check_sub_hredr q a b b' hu r a0 :
+Lemma check_sub_hredr a b b' hu r a0 :
-  check_sub_r q a b (A_HRedR a b b' hu r a0) =
+  check_sub_r a b (S_HRedR a b b' hu r a0) =
-    check_sub_r q a b' a0.
+    check_sub_r a b' a0.
 Proof.
   simpl.
   destruct (fancy_hred a).
@@ -657,4 +341,10 @@ Proof.
     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.
+Lemma check_sub_neuneu a b i a0 : check_sub a b (S_NeuNeu a b i a0) = check_equal a b a0.
+Proof. destruct a,b => //=. Qed.
+
+Lemma check_sub_conf a b n n0 i : check_sub a b (S_Conf a b n n0 i) = false.
+Proof. destruct a,b=>//=; ecrush inv:BTag. Qed.
+
+#[export]Hint Rewrite check_sub_neuneu check_sub_conf check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop.

theories/executable_correct.v

@@ -23,6 +23,14 @@ Proof.
   inversion 3; subst => //=.
 Qed.
 
+Lemma coqeq_neuneu' u0 u1 :
+  neuneu_nonconf u0 u1 ->
+  u0 ↔ u1 ->
+  u0 ∼ u1.
+Proof.
+  induction 2 => //=; destruct u => //=.
+Qed.
+
 Lemma check_equal_sound :
   (forall a b (h : algo_dom a b), check_equal a b h -> a ↔ b) /\
   (forall a b (h : algo_dom_r a b), check_equal_r a b h -> a ⇔ b).
@@ -63,15 +71,15 @@ Proof.
   - sfirstorder.
   - move => i j /sumboolP ?.  subst.
     apply : CE_NeuNeu. apply CE_VarCong.
+  - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE.
+    rewrite check_equal_app_app in hE.
+    move /andP : hE => [h0 h1].
+    sauto lq:on use:coqeq_neuneu.
   - move => p0 p1 u0 u1 neu0 neu1 h ih he.
     apply CE_NeuNeu.
     rewrite check_equal_proj_proj in he.
     move /andP : he => [/sumboolP ? h1]. subst.
     sauto lq:on use:coqeq_neuneu.
-  - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE.
-    rewrite check_equal_app_app in hE.
-    move /andP : hE => [h0 h1].
-    sauto lq:on use:coqeq_neuneu.
   - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
     rewrite check_equal_ind_ind.
     move /andP => [/andP [/andP [h0 h1] h2 ] h3].
@@ -117,14 +125,14 @@ Proof.
   - simp check_equal. done.
   - move => i j. move => h. have {h} : ~ nat_eqdec i j by done.
     case : nat_eqdec => //=. ce_solv.
+  - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1.
+    rewrite check_equal_app_app.
+    move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu.
   - move => p0 p1 u0 u1 neu0 neu1 h ih.
     rewrite check_equal_proj_proj.
     move /negP /nandP. case.
     case : PTag_eqdec => //=. sauto lq:on.
     sauto lqb:on.
-  - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1.
-    rewrite check_equal_app_app.
-    move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu.
   - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc.
     rewrite check_equal_ind_ind.
     move => + h.
@@ -172,39 +180,31 @@ 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 : salgo_dom a b), check_sub a b h -> a ⋖ b) /\
-    (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).
+    (forall a b (h : salgo_dom_r a b), check_sub_r a b h -> a ≪ b).
 Proof.
-  apply algo_dom_mutual; try done.
+  apply salgo_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.
+  - move => A0 A1 B0 B1 s ihs s0 ihs0.
-    case : p0; case : p1; try done; simp ce_prop.
+    simp ce_prop.
-    sauto lqb:on.
+    hauto lqb:on ctrs:CoqLEq.
-    sauto lqb:on.
+  - move => A0 A1 B0 B1 s ihs s0 ihs0.
-  - hauto l:on.
+    simp ce_prop.
-  - move => i j q h.
+    hauto lqb:on ctrs:CoqLEq.
-    have {}h : nat_eqdec i j by sfirstorder.
+  - qauto ctrs:CoqLEq.
-    case : nat_eqdec h => //=; sauto lq:on.
+  - move => a b i a0.
-  - simp_sub.
+    simp ce_prop.
-    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
+    move => h. apply CLE_NeuNeu.
-  - simp_sub.
+    hauto lq:on use:check_equal_sound, coqeq_neuneu', coqeq_symmetric_mutual.
-    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
+  - move => a b n n0 i.
-  - simp_sub.
+    by simp ce_prop.
-    sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound.
+  - move => a b h ih. simp ce_prop. hauto l:on.
-  - move => a b n n0 i q h.
+  - move => a a' b hr h ih.
-    exfalso.
+    simp ce_prop.
-    destruct a, b; try done; simp_sub; hauto lb:on use:check_equal_conf.
+    sauto lq:on rew:off.
-  - move => a b doma ihdom q.
+  - move => a b b' n r dom ihdom.
-    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}.
@@ -212,91 +212,48 @@ Proof.
 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 : salgo_dom a b), check_sub a b h = false -> ~ a ⋖ b) /\
-    (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).
+    (forall a b (h : salgo_dom_r a b), check_sub_r a b h = false -> ~ a ≪ b).
 Proof.
-  apply algo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu].
+  apply salgo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu].
-  - move => i j q /=.
+  - move => i j /=.
-    sauto lq:on rew:off use:PeanoNat.Nat.leb_le.
+    move => + h. inversion h; subst => //=.
-  - move => p0 p1 A0 A1 B0 B1 a iha b ihb [].
+    sfirstorder use:PeanoNat.Nat.leb_le.
-    + move => + h. inversion h; subst; simp ce_prop.
+    hauto lq:on inv:CoqEq_Neu.
-      * move /nandP.
+  - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop.
-        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.
+    move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu.
-    case => //.
+    move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu.
-    by move /negP.
+  - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop.
-    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.
+    move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu.
-    case.
+    move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu.
-    by move/negP.
+  - move => a b i hs. simp ce_prop.
-    by move/negP.
+    move => + h. inversion h; subst => //=.
-    move /negP.
+    move => /negP h0.
-    move => h. eapply check_equal_complete in h.
+    eapply check_equal_complete in h0.
-    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
+    apply h0. by constructor.
-  - move => P0 P1 u0 u1 b0 b1 c0 c1 i i0 dom ihdom dom' ihdom' dom'' ihdom'' dom''' ihdom''' q.
+  - move => a b s ihs. simp ce_prop.
-    move /nandP.
+    move => h0 h1. apply ihs =>//.
-    case.
+    have [? ?] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
-    move /nandP.
+    inversion h1; subst.
-    case => //=.
+    hauto l:on use:hreds_nf_refl.
-    by move/negP.
+  - move => a a' b h dom.
-    by move/negP.
+    simp ce_prop => /[apply].
-    move /negP => h. eapply check_equal_complete in h.
+    move => + h1. inversion h1; subst.
-    sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on.
+    inversion H; subst.
-  - move => a b h ih q. simp ce_prop => {}/ih.
+    + sfirstorder use:coqleq_no_hred unfold:HRed.nf.
-    case : q => h0;
+    + have ? : y = a' by eauto using hred_deter. subst.
-    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.
+  - move => a b b' u hr dom ihdom.
-    inversion H1; subst. sfirstorder use:coqleq_no_hred.
+    rewrite check_sub_hredr.
-    have ? : a' = y by eauto using hred_deter. subst.
+    move => + h. inversion h; subst.
-    sauto lq:on.
+    have {}u : HRed.nf a by sfirstorder use:hne_no_hred, hf_no_hred.
-  - move => a b b' n r hr ih q.
+    move => {}/ihdom.
-    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 ? : HRed.nf b'0 by hauto l:on use:coqleq_no_hred.
-      have ? : b' = y by eauto using hred_deter. subst.
+      sfirstorder unfold:HRed.nf.
-      sauto lq:on.
+    + sauto lq:on use:hred_deter.
 Qed.

theories/fp_red.v

@@ -10,7 +10,7 @@ From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
 From Hammer Require Import Tactics.
 Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
 Require Import Btauto.
-Require Import Cdcl.Itauto.
+
 
 Ltac2 spec_refl () :=
   List.iter
@@ -2575,7 +2575,7 @@ Module LoReds.
     ~~ ishf a.
   Proof.
     move : hf_preservation. repeat move/[apply].
-    case : a; case : b => //=; itauto.
+    case : a; case : b => //=; sfirstorder b:on.
   Qed.
 
   #[local]Ltac solve_s_rec :=
@@ -2633,7 +2633,7 @@ Module LoReds.
     rtc LoRed.R (PSuc a0) (PSuc a1).
   Proof. solve_s. Qed.
 
-  Local Ltac triv := simpl in *; itauto.
+  Local Ltac triv := simpl in *; sfirstorder b:on.
 
   Lemma FromSN_mutual :
     (forall (a : PTm) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\
@@ -3048,7 +3048,7 @@ Module DJoin.
     have {h0 h1 h2 h3} : isbind c /\ isuniv c by
       hauto l:on use:REReds.bind_preservation,
           REReds.univ_preservation.
-    case : c => //=; itauto.
+    case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma hne_univ_noconf (a b : PTm) :
@@ -3078,7 +3078,7 @@ Module DJoin.
   Proof.
     move => [c [h0 h1]] h2 h3.
     have : ishne c /\ isnat c by sfirstorder use:REReds.hne_preservation, REReds.nat_preservation.
-    clear. case : c => //=; itauto.
+    clear. case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 :
@@ -3594,7 +3594,7 @@ Module Sub.
       hauto l:on use:REReds.bind_preservation,
             REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
     move : h2 h3. clear.
-    case : c => //=; itauto.
+    case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma univ_bind_noconf (a b : PTm) :
@@ -3605,7 +3605,7 @@ Module Sub.
       hauto l:on use:REReds.bind_preservation,
             REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
     move : h2 h3. clear.
-    case : c => //=; itauto.
+    case : c => //=; sfirstorder b:on.
   Qed.
 
   Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 :

theories/logrel.v

@@ -6,7 +6,7 @@ Require Import ssreflect ssrbool.
 Require Import Logic.PropExtensionality (propositional_extensionality).
 From stdpp Require Import relations (rtc(..), rtc_subrel).
 Import Psatz.
-Require Import Cdcl.Itauto.
+
 
 Definition ProdSpace (PA : PTm -> Prop)
   (PF : PTm -> (PTm -> Prop) -> Prop) b : Prop :=
@@ -355,7 +355,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : SNe H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       move : hA hAB. clear. hauto lq:on db:noconf.
       move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
       tauto.
@@ -365,7 +365,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : SNe H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       move : hAB hA h0. clear. hauto lq:on db:noconf.
       move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
       tauto.
@@ -375,7 +375,7 @@ Proof.
       have {hU} {}h : Sub.R (PBind p A B) H
         by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have{h0} : isbind H.
-      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       have : isbind (PBind p A B) by scongruence.
       move : h. clear. hauto l:on db:noconf.
       case : H h1 h => //=.
@@ -394,7 +394,7 @@ Proof.
       have {hU} {}h : Sub.R H (PBind p A B)
         by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have{h0} : isbind H.
-      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto.
+      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on.
       have : isbind (PBind p A B) by scongruence.
       move : h. clear. move : (PBind p A B). hauto lq:on db:noconf.
       case : H h1 h => //=.
@@ -413,7 +413,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : isnat H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on.
       have : @isnat PNat by simpl.
       move : h0 hAB. clear. qauto l:on db:noconf.
       case : H h1 hAB h0 => //=.
@@ -424,7 +424,7 @@ Proof.
       move => [H [/DJoin.FromRedSNs h [h1 h0]]].
       have {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
       have {}h0 : isnat H.
-      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on.
       have : @isnat PNat by simpl.
       move : h0 hAB. clear. qauto l:on db:noconf.
       case : H h1 hAB h0 => //=.
@@ -1058,7 +1058,7 @@ Definition Γ_sub' Γ Δ := forall ρ, ρ_ok Δ ρ -> ρ_ok Γ ρ.
 Definition Γ_eq' Γ Δ := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ.
 
 Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ.
-  rewrite /Γ_sub'. itauto. Qed.
+  rewrite /Γ_sub'. sfirstorder b:on. Qed.
 
 Lemma Γ_sub'_cons Γ Δ A B i j :
   Sub.R B A ->

theories/termination.v

@@ -3,280 +3,3 @@ From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
 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 /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.