DecSyn.algorithmic

Definition of Coquand's algorithm and its correctness


Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax
  common typing preservation admissible fp_red structural soundness.
From Hammer Require Import Tactics.
Require Import ssreflect ssrbool.
Require Import Psatz.
From stdpp Require Import relations (rtc(..), nsteps(..)).

Properties about weak-head reduction

Module HRed.
  Lemma ToRRed (a b : PTm) : HRed.R a b RRed.R a b.
  Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.

  Lemma preservation Γ (a b A : PTm) : Γ ⊢ a ∈ A HRed.R a b Γ ⊢ b ∈ A.
  Proof.
    sfirstorder use:subject_reduction, ToRRed.
  Qed.

  Lemma ToEq Γ (a b : PTm ) A : Γ ⊢ a ∈ A HRed.R a b Γ ⊢ a ≡ b ∈ A.
  Proof. sfirstorder use:ToRRed, RRed_Eq. Qed.

End HRed.

Module HReds.
  Lemma preservation Γ (a b A : PTm) : Γ ⊢ a ∈ A rtc HRed.R a b Γ ⊢ b ∈ A.
  Proof. induction 2; sfirstorder use:HRed.preservation. Qed.

  Lemma ToEq Γ (a b : PTm) A : Γ ⊢ a ∈ A rtc HRed.R a b Γ ⊢ a ≡ b ∈ A.
  Proof.
    induction 2; sauto lq:on use:HRed.ToEq, E_Transitive, HRed.preservation.
  Qed.
End HReds.

Lemma T_Conv_E Γ (a : PTm) A B i :
  Γ ⊢ a ∈ A
  Γ ⊢ A ≡ B ∈ PUniv i Γ ⊢ B ≡ A ∈ PUniv i
  Γ ⊢ a ∈ B.
Proof. qauto use:T_Conv, Su_Eq, E_Symmetric. Qed.

Lemma E_Conv_E Γ (a b : PTm) A B i :
  Γ ⊢ a ≡ b ∈ A
  Γ ⊢ A ≡ B ∈ PUniv i Γ ⊢ B ≡ A ∈ PUniv i
  Γ ⊢ a ≡ b ∈ B.
Proof. qauto use:E_Conv, Su_Eq, E_Symmetric. Qed.

Lemma lored_embed Γ (a b : PTm) A :
  Γ ⊢ a ∈ A LoRed.R a b Γ ⊢ a ≡ b ∈ A.
Proof. sfirstorder use:LoRed.ToRRed, RRed_Eq. Qed.

Lemma loreds_embed Γ (a b : PTm ) A :
  Γ ⊢ a ∈ A rtc LoRed.R a b Γ ⊢ a ≡ b ∈ A.
Proof.
  move + h. move : Γ A.
  elim : a b /h.
  - sfirstorder use:E_Refl.
  - move a b c ha hb ih Γ A hA.
    have ? : Γ ⊢ a ≡ b ∈ A by sfirstorder use:lored_embed.
    have ? : Γ ⊢ b ∈ A by hauto l:on use:regularity.
    hauto lq:on ctrs:Eq.
Qed.

Lemma Zero_Inv Γ U :
  Γ ⊢ PZero ∈ U
  Γ ⊢ PNat ≲ U.
Proof.
  move E : PZero u hu.
  move : E.
  elim : Γ u U /hu//=.
  by eauto using Su_Eq, E_Refl, T_Nat'.
  hauto lq:on rew:off ctrs:LEq.
Qed.

Lemma Sub_Bind_InvR Γ p (A : PTm ) B C :
  Γ ⊢ PBind p A B ≲ C
   i A0 B0, Γ ⊢ C ≡ PBind p ∈ PUniv i.
Proof.
  move /[dup] h.
  move /synsub_to_usub.
  move [ [ ]].
  move /LoReds.FromSN : .
  move [C' [ ]].
  have [i hC] : i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
  have hE : Γ ⊢ C ≡ C' ∈ PUniv i by sfirstorder use:loreds_embed.
  have : Γ ⊢ PBind p A B ≲ C' by eauto using Su_Transitive, Su_Eq.
  move : hE . clear.
  case : C' //=.
  - move k _ _ /synsub_to_usub.
    clear. move [_ [_ h]]. exfalso.
    rewrite /Sub.R in h.
    move : h [c][d][+ []].
    move /REReds.bind_inv ?.
    move /REReds.var_inv ?.
    sauto lq:on.
  - move h. exfalso.
    have {h} : Γ ⊢ PAbs ∈ PUniv i by hauto l:on use:regularity.
    move /Abs_Inv [][][_]/synsub_to_usub.
    hauto l:on use:Sub.bind_univ_noconf.
  - move u v hC /andP [ ] /synsub_to_usub ?.
    exfalso.
    suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf.
    eapply ne_nf_embed //=. sfirstorder b:on.
  - move hC h ?. exfalso.
    have {hC} : Γ ⊢ PPair ∈ PUniv i by hauto l:on use:regularity.
    hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
  - move _ + /synsub_to_usub.
    hauto lq:on use:Sub.bind_sne_noconf, ne_nf_embed.
  - move b /[dup] /synsub_to_usub *.
    have ? : b = p by hauto l:on use:Sub.bind_inj. subst.
    eauto.
  - hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf.
  - move _ _ /synsub_to_usub [_ [_ h]]. exfalso.
    apply Sub.nat_bind_noconf in h //=.
  - move h.
    have {}h : Γ ⊢ PZero ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move : h. clear.
    move /Zero_Inv /synsub_to_usub.
    hauto l:on use:Sub.univ_nat_noconf.
  - move a h.
    have {}h : Γ ⊢ PSuc a ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move /Suc_Inv : h [_ /synsub_to_usub].
    hauto lq:on use:Sub.univ_nat_noconf.
  - move /synsub_to_usub [_ [_ ]].
    set u := PInd _ _ _ _ in .
    have hne : SNe u by sfirstorder use:ne_nf_embed.
    exfalso. move : hne. hauto l:on use:Sub.bind_sne_noconf.
Qed.

Lemma Sub_Univ_InvR Γ i C :
  Γ ⊢ PUniv i ≲ C
   j k, Γ ⊢ C ≡ PUniv j ∈ PUniv k.
Proof.
  move /[dup] h.
  move /synsub_to_usub.
  move [ [ ]].
  move /LoReds.FromSN : .
  move [C' [ ]].
  have [j hC] : i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
  have hE : Γ ⊢ C ≡ C' ∈ PUniv j by sfirstorder use:loreds_embed.
  have : Γ ⊢ PUniv i ≲ C' by eauto using Su_Transitive, Su_Eq.
  move : hE . clear.
  case : C' //=.
  - move f _ _ /synsub_to_usub.
    move [_ [_]].
    move [][][/REReds.univ_inv + [/REReds.var_inv ]].
    hauto lq:on inv:Sub1.R.
  - move p hC.
    have {hC} : Γ ⊢ PAbs p ∈ PUniv j by hauto l:on use:regularity.
    hauto lq:on rew:off use:Abs_Inv, synsub_to_usub,
            Sub.bind_univ_noconf.
  - hauto q:on use:synsub_to_usub, Sub.univ_sne_noconf, ne_nf_embed.
  - move a b hC.
    have {hC} : Γ ⊢ PPair a b ∈ PUniv j by hauto l:on use:regularity.
    hauto lq:on rew:off use:Pair_Inv, synsub_to_usub,
            Sub.bind_univ_noconf.
  - hauto q:on use:synsub_to_usub, Sub.univ_sne_noconf, ne_nf_embed.
  - hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
  - sfirstorder.
  - hauto q:on use:synsub_to_usub, Sub.nat_univ_noconf.
  - move h.
    have {}h : Γ ⊢ PZero ∈ PUniv j by hauto l:on use:regularity.
    exfalso. move : h. clear.
    move /Zero_Inv /synsub_to_usub.
    hauto l:on use:Sub.univ_nat_noconf.
  - move a h.
    have {}h : Γ ⊢ PSuc a ∈ PUniv j by hauto l:on use:regularity.
    exfalso. move /Suc_Inv : h [_ /synsub_to_usub].
    hauto lq:on use:Sub.univ_nat_noconf.
  - move /synsub_to_usub [_ [_ ]].
    set u := PInd _ _ _ _ in .
    have hne : SNe u by sfirstorder use:ne_nf_embed.
    exfalso. move : hne. hauto l:on use:Sub.univ_sne_noconf.
Qed.

Lemma Sub_Bind_InvL Γ p (A : PTm) B C :
  Γ ⊢ C ≲ PBind p A B
   i A0 B0, Γ ⊢ PBind p ≡ C ∈ PUniv i.
Proof.
  move /[dup] h.
  move /synsub_to_usub.
  move [ [ ]].
  move /LoReds.FromSN : .
  move [C' [ ]].
  have [i hC] : i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
  have hE : Γ ⊢ C ≡ C' ∈ PUniv i by sfirstorder use:loreds_embed.
  have : Γ ⊢ C' ≲ PBind p A B by eauto using Su_Transitive, Su_Eq, E_Symmetric.
  move : hE . clear.
  case : C' //=.
  - move k _ _ /synsub_to_usub.
    clear. move [_ [_ h]]. exfalso.
    rewrite /Sub.R in h.
    move : h [c][d][+ []].
    move /REReds.var_inv ?.
    move /REReds.bind_inv ?.
    hauto lq:on inv:Sub1.R.
  - move h. exfalso.
    have {h} : Γ ⊢ PAbs ∈ PUniv i by hauto l:on use:regularity.
    move /Abs_Inv [][][_]/synsub_to_usub.
    hauto l:on use:Sub.bind_univ_noconf.
  - move u v hC /andP [ ] /synsub_to_usub ?.
    exfalso.
    suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf.
    eapply ne_nf_embed //=. sfirstorder b:on.
  - move hC h ?. exfalso.
    have {hC} : Γ ⊢ PPair ∈ PUniv i by hauto l:on use:regularity.
    hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
  - move _ + /synsub_to_usub.
    hauto lq:on use:Sub.sne_bind_noconf, ne_nf_embed.
  - move b /[dup] /synsub_to_usub *.
    have ? : b = p by hauto l:on use:Sub.bind_inj. subst.
    eauto using E_Symmetric.
  - hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
  - move _ _ /synsub_to_usub [_ [_ h]]. exfalso.
    apply Sub.bind_nat_noconf in h //=.
  - move h.
    have {}h : Γ ⊢ PZero ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move : h. clear.
    move /Zero_Inv /synsub_to_usub.
    hauto l:on use:Sub.univ_nat_noconf.
  - move a h.
    have {}h : Γ ⊢ PSuc a ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move /Suc_Inv : h [_ /synsub_to_usub].
    hauto lq:on use:Sub.univ_nat_noconf.
  - move /synsub_to_usub [_ [_ ]].
    set u := PInd _ _ _ _ in .
    have hne : SNe u by sfirstorder use:ne_nf_embed.
    exfalso. move : hne. subst u.
    hauto l:on use:Sub.sne_bind_noconf.
Qed.

Lemma T_Abs_Inv Γ (a0 a1 : PTm) U :
  Γ ⊢ PAbs ∈ U
  Γ ⊢ PAbs ∈ U
   Δ V, Δ ⊢ ∈ V Δ ⊢ ∈ V.
Proof.
  move /Abs_Inv [][][].
  move /Abs_Inv [][][].
  move /Sub_Bind_InvR : () [i][][]hE.
  have hSu : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Eq, Su_Transitive.
  have hSu' : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Eq, Su_Transitive.
  exists ((cons Γ)), .
  have [k ?] : k, Γ ⊢ ∈ PUniv k by hauto lq:on use:regularity, Bind_Inv.
  split.
  - have /Su_Pi_Proj2_Var ? := hSu'.
    have /Su_Pi_Proj1 ? := hSu'.
    move /regularity_sub0 : hSu' [j] /Bind_Inv [ [? ?]].
    apply T_Conv with (A := ); eauto.
    apply : ctx_eq_subst_one; eauto.
  - have /Su_Pi_Proj2_Var ? := hSu.
    have /Su_Pi_Proj1 ? := hSu.
    move /regularity_sub0 : hSu [j] /Bind_Inv [ [? ?]].
    apply T_Conv with (A := ); eauto.
    apply : ctx_eq_subst_one; eauto.
Qed.

Lemma Abs_Pi_Inv Γ (a : PTm) A B :
  Γ ⊢ PAbs a ∈ PBind PPi A B
  (cons A Γ) ⊢ a ∈ B.
Proof.
  move h.
  have [i hi] : i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto use:regularity.
  have [{}i {}hi] : i, Γ ⊢ A ∈ PUniv i by hauto use:Bind_Inv.
  apply : subject_reduction; last apply RRed.AppAbs'.
  apply : T_App'; cycle 1.
  apply : weakening_wt'; cycle 2. apply hi.
  apply h. reflexivity. reflexivity. rewrite -/ren_PTm.
  apply T_Var with (i := var_zero).
  by eauto using Wff_Cons'.
  apply here.
  rewrite -/ren_PTm.
  by asimpl; rewrite subst_scons_id.
  rewrite -/ren_PTm.
  by asimpl; rewrite subst_scons_id.
Qed.

Lemma T_Abs_Neu_Inv Γ (a u : PTm) U :
  Γ ⊢ PAbs a ∈ U
  Γ ⊢ u ∈ U
   Δ V, Δ ⊢ a ∈ V Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ V.
Proof.
  move /[dup] ha' + hu.
  move /Abs_Inv [][][ha]hSu.
  move /Sub_Bind_InvR : (hSu) [i][][]hE.
  have {}hu : Γ ⊢ u ∈ PBind PPi by eauto using T_Conv_E.
  have ha'' : Γ ⊢ PAbs a ∈ PBind PPi by eauto using T_Conv_E.
  have {}hE : Γ ⊢ PBind PPi ∈ PUniv i
    by hauto l:on use:regularity.
  have {i} [j {}hE] : j, Γ ⊢ ∈ PUniv j
      by qauto l:on use:Bind_Inv.
  have hΓ : ⊢ cons Γ by eauto using Wff_Cons'.
  set Δ := cons _ _ in hΓ.
  have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ .
  apply : T_App'; cycle 1. apply : weakening_wt' //=; eauto.
  reflexivity.
  rewrite -/ren_PTm.
  apply T_Var; eauto using here.
  rewrite -/ren_PTm. by asimpl; rewrite subst_scons_id.
  exists Δ, . split //.
  by move /Abs_Pi_Inv in ha''.
Qed.

Lemma T_Univ_Raise Γ (a : PTm) i j :
  Γ ⊢ a ∈ PUniv i
  i j
  Γ ⊢ a ∈ PUniv j.
Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.

Lemma Bind_Univ_Inv Γ p (A : PTm) B i :
  Γ ⊢ PBind p A B ∈ PUniv i
  Γ ⊢ A ∈ PUniv i (cons A Γ) ⊢ B ∈ PUniv i.
Proof.
  move /Bind_Inv.
  move [][hA][hB]h.
  move /synsub_to_usub : h [_ [_ /Sub.univ_inj ? ]].
  sfirstorder use:T_Univ_Raise.
Qed.

Lemma Pair_Sig_Inv Γ (a b : PTm) A B :
  Γ ⊢ PPair a b ∈ PBind PSig A B
  Γ ⊢ a ∈ A Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B.
Proof.
  move /[dup] .
  have [i hr] : i, Γ ⊢ PBind PSig A B ∈ PUniv i by sfirstorder use:regularity.
  move /T_Proj1 in .
  move /T_Proj2 in .
  split.
  hauto lq:on use:subject_reduction ctrs:RRed.R.
  have hE : Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A by
    hauto lq:on use:RRed_Eq ctrs:RRed.R.
  apply : T_Conv.
  move /subject_reduction : . apply.
  apply RRed.ProjPair.
  apply : bind_inst; eauto.
Qed.

Coquand's algorithm for equalities

Reserved Notation "a ∼ b" (at level 70).
Reserved Notation "a ↔ b" (at level 70).
Reserved Notation "a ⇔ b" (at level 70).
Inductive CoqEq : PTm PTm Prop :=
| CE_ZeroZero :
  PZero ↔ PZero

| CE_SucSuc a b :
  a ⇔ b
  (* ------------- *)
  PSuc a ↔ PSuc b

| CE_AbsAbs a b :
  a ⇔ b
  (* --------------------- *)
  PAbs a ↔ PAbs b

| CE_AbsNeu a u :
  ishne u
  a ⇔ PApp (ren_PTm shift u) (VarPTm var_zero)
  (* --------------------- *)
  PAbs a ↔ u

| CE_NeuAbs a u :
  ishne u
  PApp (ren_PTm shift u) (VarPTm var_zero) ⇔ a
  (* --------------------- *)
  u ↔ PAbs a

| CE_PairPair a0 a1 b0 b1 :
   ⇔
   ⇔
  (* ---------------------------- *)
  PPair ↔ PPair

| CE_PairNeu a0 a1 u :
  ishne u
   ⇔ PProj PL u
   ⇔ PProj PR u
  (* ----------------------- *)
  PPair ↔ u

| CE_NeuPair a0 a1 u :
  ishne u
  PProj PL u ⇔
  PProj PR u ⇔
  (* ----------------------- *)
  u ↔ PPair

| CE_UnivCong i :
  (* -------------------------- *)
  PUniv i ↔ PUniv i

| CE_BindCong p A0 A1 B0 B1 :
   ⇔
   ⇔
  (* ---------------------------- *)
  PBind p ↔ PBind p

| CE_NatCong :
  (* ------------------ *)
  PNat ↔ PNat

| CE_NeuNeu a0 a1 :
   ∼
   ↔

with CoqEq_Neu : PTm PTm Prop :=
| CE_VarCong i :
  (* -------------------------- *)
  VarPTm i ∼ VarPTm i

| CE_ProjCong p u0 u1 :
  ishne
  ishne
   ∼
  (* ---------------------  *)
  PProj p ∼ PProj p

| CE_AppCong u0 u1 a0 a1 :
  ishne
  ishne
   ∼
   ⇔
  (* ------------------------- *)
  PApp ∼ PApp

| CE_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
  ishne
  ishne
   ⇔
   ∼
   ⇔
   ⇔
  (* ----------------------------------- *)
  PInd ∼ PInd

with CoqEq_R : PTm PTm Prop :=
| CE_HRed a a' b b' :
  rtc HRed.R a a'
  rtc HRed.R b b'
  a' ↔ b'
  (* ----------------------- *)
  a ⇔ b
where "a ↔ b" := (CoqEq a b) and "a ⇔ b" := (CoqEq_R a b) and "a ∼ b" := (CoqEq_Neu a b).

Lemma CE_HRedL (a a' b : PTm) :
  HRed.R a a'
  a' ⇔ b
  a ⇔ b.
Proof.
  hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
Qed.

Lemma CE_HRedR (a b b' : PTm) :
  HRed.R b b'
  a ⇔ b'
  a ⇔ b.
Proof.
  hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
Qed.

Lemma CE_Nf a b :
  a ↔ b a ⇔ b.
Proof. hauto l:on ctrs:rtc. Qed.

Scheme
  coqeq_neu_ind := Induction for CoqEq_Neu Sort Prop
  with coqeq_ind := Induction for CoqEq Sort Prop
  with coqeq_r_ind := Induction for CoqEq_R Sort Prop.

Combined Scheme coqeq_mutual from coqeq_neu_ind, coqeq_ind, coqeq_r_ind.

Lemma coqeq_symmetric_mutual :
    ( (a b : PTm), a ∼ b b ∼ a)
    ( (a b : PTm), a ↔ b b ↔ a)
    ( (a b : PTm), a ⇔ b b ⇔ a).
Proof. apply coqeq_mutual; qauto l:on ctrs:CoqEq,CoqEq_R, CoqEq_Neu. Qed.

Soundness of Coquand's equality algorithm

Lemma coqeq_sound_mutual :
    ( (a b : PTm ), a ∼ b Γ A B, Γ ⊢ a ∈ A Γ ⊢ b ∈ B C,
       Γ ⊢ C ≲ A Γ ⊢ C ≲ B Γ ⊢ a ≡ b ∈ C)
    ( (a b : PTm ), a ↔ b Γ A, Γ ⊢ a ∈ A Γ ⊢ b ∈ A Γ ⊢ a ≡ b ∈ A)
    ( (a b : PTm ), a ⇔ b Γ A, Γ ⊢ a ∈ A Γ ⊢ b ∈ A Γ ⊢ a ≡ b ∈ A).
Proof.
  move [:hAppL hPairL].
  apply coqeq_mutual.
  - move i Γ A B .
    move /Var_Inv : [hΓ [C [ ]]].
    move /Var_Inv : [_ [ [ ]]].
    have ? : = C by eauto using lookup_deter. subst.
    exists C.
    repeat split //=.
    apply E_Refl. eauto using T_Var.
  - move [] hu ihu Γ A B .
    + move /Proj1_Inv : .
      move [][][].
      move /Proj1_Inv : .
      move [][][].
      specialize ihu with (1 := ) (2 := ).
      move : ihu.
      move [C][][]ih.
      have [i[[ ]]] : i A2 B2, Γ ⊢ PBind PSig ≡ C ∈ PUniv i by sfirstorder use:Sub_Bind_InvL.
      exists .
      have [ ] : Γ ⊢ PBind PSig ≲ PBind PSig Γ ⊢ PBind PSig ≲ PBind PSig by qauto l:on use:Su_Eq, Su_Transitive.
      repeat split;
        eauto using Su_Sig_Proj1, Su_Transitive;[idtac].
      apply E_Proj1 with (B := ); eauto using E_Conv_E.
    + move /Proj2_Inv : .
      move [][][].
      move /Proj2_Inv : .
      move [][][].
      specialize ihu with (1 := ) (2 := ).
      move : ihu.
      move [C][][]ih.
      have [ [ [i hi]]] : A2 B2 i, Γ ⊢ PBind PSig ≡ C ∈ PUniv i by hauto q:on use:Sub_Bind_InvL.
      have [ ] : Γ ⊢ PBind PSig ≲ PBind PSig Γ ⊢ PBind PSig ≲ PBind PSig by qauto l:on use:Su_Eq, Su_Transitive.
      have : Γ ⊢ ≡ ∈ PBind PSig by eauto using E_Conv_E.
      exists (subst_PTm (scons (PProj PL ) VarPTm) ).
      have [? ?] : Γ ⊢ ∈ PBind PSig Γ ⊢ ∈ PBind PSig by hauto l:on use:regularity.
      repeat split //=.
      apply : Su_Transitive ;eauto.
      apply : Su_Sig_Proj2; eauto.
      apply E_Refl. eauto using T_Proj1.
      apply : Su_Transitive ;eauto.
      apply : Su_Sig_Proj2; eauto.
      apply : E_Proj1; eauto.
      apply : E_Proj2; eauto.
  - move hu ihu ha iha Γ A B .
    move /App_Inv : [][][][]hU.
    move /App_Inv : [][][][].
    move : ihu . repeat move/[apply].
    move [C][][].
    have [i [ [ hPi]]] : i A2 B2, Γ ⊢ PBind PPi ≡ C ∈ PUniv i by sfirstorder use:Sub_Bind_InvL.
    have ? : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Eq, Su_Transitive.
    have h : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Eq, Su_Transitive.
    have ha' : Γ ⊢ ≡ ∈ by
      sauto lq:on use:Su_Transitive, Su_Pi_Proj1.
    have hwf : Γ ⊢ PBind PPi ∈ PUniv i by hauto l:on use:regularity.
    have [j hj'] : j,Γ ⊢ ∈ PUniv j by hauto l:on use:regularity.
    have ? : ⊢ Γ by sfirstorder use:wff_mutual.
    exists (subst_PTm (scons VarPTm) ).
    repeat split. apply : Su_Transitive; eauto.
    apply : Su_Pi_Proj2'; eauto using E_Refl.
    apply : Su_Transitive; eauto.
    have ? : Γ ⊢ ≲ by eauto using Su_Pi_Proj1.
    apply Su_Transitive with (B := subst_PTm (scons VarPTm) );
      first by sfirstorder use:bind_inst.
    apply : Su_Pi_Proj2'; eauto using E_Refl.
    apply E_App with (A := ); eauto using E_Conv_E.
  - move {hAppL hPairL} hP ihP hu ihu hb ihb hc ihc Γ A B.
    move /Ind_Inv [][][][][].
    move /Ind_Inv [][][][][].
    move : ihu ; do!move/[apply]. move ihu.
    have {}ihu : Γ ⊢ ≡ ∈ PNat by hauto l:on use:E_Conv.
    have wfΓ : ⊢ Γ by hauto use:wff_mutual.
    have wfΓ' : ⊢ (cons PNat Γ) by hauto lq:on use:Wff_Cons', T_Nat'.
    move [:sigeq].
    have sigeq' : Γ ⊢ PBind PSig PNat ≡ PBind PSig PNat ∈ PUniv (max ).
    apply E_Bind. by eauto using T_Nat, E_Refl.
    abstract : sigeq. hauto lq:on use:T_Univ_Raise solve+:lia.
    have sigleq : Γ ⊢ PBind PSig PNat ≲ PBind PSig PNat .
    apply Su_Sig with (i := 0)//. by apply T_Nat'. by eauto using Su_Eq, T_Nat', E_Refl.
    apply Su_Eq with (i := max ). apply sigeq.
    exists (subst_PTm (scons VarPTm) ). repeat split //.
    suff : Γ ⊢ subst_PTm (scons VarPTm) ≲ subst_PTm (scons VarPTm) by eauto using Su_Transitive.
    by eauto using Su_Sig_Proj2.
    apply E_IndCong with (i := max ); eauto. move :sigeq; clear; hauto q:on use:regularity.
    apply ihb; eauto. apply : T_Conv; eauto. eapply morphing. apply : Su_Eq. apply E_Symmetric. apply sigeq.
    done. apply morphing_ext. apply morphing_id. done. by apply T_Zero.
    apply ihc; eauto.
    eapply T_Conv; eauto.
    eapply ctx_eq_subst_one; eauto. apply : Su_Eq; apply sigeq.
    eapply weakening_su; eauto.
    eapply morphing; eauto. apply : Su_Eq. apply E_Symmetric. apply sigeq.
    apply morphing_ext. set x := {1}(funcomp _ shift).
    have : x = funcomp (ren_PTm shift) VarPTm by asimpl.
    apply : morphing_ren; eauto. apply : renaming_shift; eauto. by apply morphing_id.
    apply T_Suc. apply T_Var; eauto using here.
  - hauto lq:on use:Zero_Inv db:wt.
  - hauto lq:on use:Suc_Inv db:wt.
  - move a b ha iha Γ A .
    move /Abs_Inv : [][][].
    move /Abs_Inv : [][][].
    have [i [ [ h]]] : i A2 B2, Γ ⊢ A ≡ PBind PPi ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
    have : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Transitive, Su_Eq.
    have : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Transitive, Su_Eq.
    have [j ?] : j, Γ ⊢ ∈ PUniv j by eapply wff_mutual in ; inversion ; subst; eauto.
    have [k ?] : j, Γ ⊢ ∈ PUniv j by eapply wff_mutual in ; inversion ; subst; eauto.
    have [l ?] : j, Γ ⊢ ∈ PUniv j by hauto lq:on rew:off use:regularity, Bind_Inv.
    have [ ] : Γ ⊢ ≲ Γ ⊢ ≲ by hauto l:on use:Su_Pi_Proj1.
    apply E_Conv with (A := PBind PPi ); cycle 1.
    eauto using E_Symmetric, Su_Eq.
    apply : E_Abs; eauto.

    apply iha.
    move /Su_Pi_Proj2_Var in .
    apply : T_Conv; eauto.
    eapply ctx_eq_subst_one with ( := ); eauto.
    move /Su_Pi_Proj2_Var in .
    apply : T_Conv; eauto.
    eapply ctx_eq_subst_one with ( := ); eauto.
  - abstract : hAppL.
    move a u hneu ha iha Γ A wta wtu.
    move /Abs_Inv : wta [][][wta]hPi.
    have [i [ [ h]]] : i A2 B2, Γ ⊢ A ≡ PBind PPi ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
    have hPi'' : Γ ⊢ PBind PPi ≲ A by eauto using Su_Eq, Su_Transitive, E_Symmetric.
    have [ ?] : j0, Γ ⊢ ∈ PUniv by move /regularity_sub0 in hPi; hauto lq:on use:Bind_Inv.
    have [ ?] : j0, Γ ⊢ ∈ PUniv by move /regularity_sub0 in hPi''; hauto lq:on use:Bind_Inv.
    have hPi' : Γ ⊢ PBind PPi ≲ PBind PPi by eauto using Su_Eq, Su_Transitive.
    have hPidup := hPi'.
    apply E_Conv with (A := PBind PPi ); eauto.
    have /regularity_sub0 [i' ] := hPi.
    have : Γ ⊢ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ≡ u ∈ PBind PPi .
    apply : E_AppEta; eauto.
    apply T_Conv with (A := A);eauto.
    eauto using Su_Eq.
    move ?.
    suff : Γ ⊢ PAbs a ≡ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ∈ PBind PPi
      by eauto using E_Transitive.
    apply : E_Abs; eauto.
    apply iha.
    move /Su_Pi_Proj2_Var in hPi'.
    apply : T_Conv; eauto.
    eapply ctx_eq_subst_one with ( := ); eauto.
    sfirstorder use:Su_Pi_Proj1.
    eapply T_App' with (A := ren_PTm shift ) (B := ren_PTm (upRen_PTm_PTm shift) ).
    by asimpl; rewrite subst_scons_id.
    eapply weakening_wt' with (a := u) (A := PBind PPi );eauto.
    by eauto using T_Conv_E. apply T_Var. apply : Wff_Cons'; eauto.
    apply here.
  (* Mirrors the last case *)
  - move a u hu ha iha Γ A .
    apply E_Symmetric.
    apply : hAppL; eauto.
    sfirstorder use:coqeq_symmetric_mutual.
    sfirstorder use:E_Symmetric.
  - move {hAppL hPairL} ha iha hb ihb Γ A.
    move /Pair_Inv [][][][].
    move /Pair_Inv [][][][].
    have [i[[ ]]] : i A2 B2, Γ ⊢ A ≡ PBind PSig ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
    apply E_Conv with (A := PBind PSig ); last by eauto using E_Symmetric, Su_Eq.
    have : Γ ⊢ PBind PSig ≲ PBind PSig by eauto using Su_Transitive, Su_Eq, E_Symmetric.
    have : Γ ⊢ PBind PSig ≲ PBind PSig by eauto using Su_Transitive, Su_Eq, E_Symmetric.
    have /Su_Sig_Proj1 := .
    have /Su_Sig_Proj1 := .
    move [:eqa].
    apply : E_Pair; eauto. hauto l:on use:regularity.
    abstract : eqa. apply iha; eauto using T_Conv.
    apply ihb.
    + apply T_Conv with (A := subst_PTm (scons VarPTm) ); eauto.
      have : Γ ⊢ ≡ ∈ by eauto using E_Refl.
      hauto l:on use:Su_Sig_Proj2.
    + apply T_Conv with (A := subst_PTm (scons VarPTm) ); eauto; cycle 1.
      move /E_Symmetric in eqa.
      have ? : Γ ⊢ PBind PSig ∈ PUniv i by hauto use:regularity.
      apply:bind_inst; eauto.
      apply : T_Conv; eauto.
      have : Γ ⊢ ≡ ∈ by eauto using E_Refl.
      hauto l:on use:Su_Sig_Proj2.
  - move {hAppL}.
    abstract : hPairL.
    move {hAppL}.
    move u neu Γ A ha hu.
    move /Pair_Inv : ha [][][][]ha.
    have [i [ [ hA]]] : i A2 B2, Γ ⊢ A ≡ PBind PSig ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
    have hA' : Γ ⊢ PBind PSig ≲ A by eauto using E_Symmetric, Su_Eq.
    move /E_Conv : (hA'). apply.
    have hSig : Γ ⊢ PBind PSig ≲ PBind PSig by eauto using E_Symmetric, Su_Eq, Su_Transitive.
    have : Γ ⊢ ≲ by sfirstorder use:Su_Sig_Proj1.
    have hu' : Γ ⊢ u ∈ PBind PSig by eauto using T_Conv_E.
    move [:].
    apply : E_Transitive; last (apply : E_PairEta).
    apply : E_Pair; eauto. hauto l:on use:regularity.
    abstract : .
    apply . apply : T_Conv; eauto.
    by eauto using T_Proj1.
    apply . apply : T_Conv; eauto.
    move /E_Refl in .
    hauto l:on use:Su_Sig_Proj2.
    move /T_Proj2 in hu'.
    apply : T_Conv; eauto.
    move /E_Symmetric in .
    move /regularity_sub0 in hA'.
    hauto l:on use:bind_inst.
    eassumption.
  (* Same as before *)
  - move {hAppL}.
    move *. apply E_Symmetric. apply : hPairL;
      sfirstorder use:coqeq_symmetric_mutual, E_Symmetric.
  - sfirstorder use:E_Refl.
  - move {hAppL hPairL} p hA ihA hB ihB Γ A .
    move /Bind_Inv : [i][][]hU.
    move /Bind_Inv : [j][][].
    have [l [k hk]] : l k, Γ ⊢ A ≡ PUniv k ∈ PUniv l
        by hauto lq:on use:Sub_Univ_InvR.
    have hjk : Γ ⊢ PUniv j ≲ PUniv k by eauto using Su_Eq, Su_Transitive.
    have hik : Γ ⊢ PUniv i ≲ PUniv k by eauto using Su_Eq, Su_Transitive.
    apply E_Conv with (A := PUniv k); last by eauto using Su_Eq, E_Symmetric.
    move [:eqA].
    apply E_Bind. abstract : eqA. apply ihA.
    apply T_Conv with (A := PUniv i); eauto.
    apply T_Conv with (A := PUniv j); eauto.
    apply ihB.
    apply T_Conv with (A := PUniv i); eauto.
    move : weakening_su hik . by repeat move/[apply].
    apply T_Conv with (A := PUniv j); eauto.
    apply : ctx_eq_subst_one; eauto. apply : Su_Eq; apply eqA.
    move : weakening_su hjk . by repeat move/[apply].
  - hauto lq:on ctrs:Eq,LEq,Wt.
  - hauto lq:on ctrs:Eq,LEq,Wt.
  - move => a a' b b' ha hb hab ihab Γ A .
    have [*] : Γ ⊢ a' ∈ A Γ ⊢ b' ∈ A by eauto using HReds.preservation.
    hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive.
Qed.

Goguen's termination metric for equalities

Our goal here is to hide the rather messy arithmetic behind the nicer Bove-Capretta domain algo_dom_r
Definition term_metric k (a b : PTm) :=
   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 ne_hne (a : PTm) : ne a ishne a.
Proof. elim : a //=; sfirstorder b:on. Qed.

Lemma hf_hred_lored (a b : PTm) :
  ~~ ishf a
  LoRed.R a b
  HRed.R a b ishne a.
Proof.
  move + h. elim : a b/ h//=.
  - hauto l:on use:HRed.AppAbs.
  - hauto l:on use:HRed.ProjPair.
  - hauto lq:on ctrs:HRed.R.
  - hauto lq:on ctrs:HRed.R.
  - hauto lq:on ctrs:HRed.R.
  - sfirstorder use:ne_hne.
  - hauto lq:on ctrs:HRed.R.
  - sfirstorder use:ne_hne.
  - hauto q:on ctrs:HRed.R.
  - hauto lq:on use:ne_hne.
  - hauto lq:on use:ne_hne.
Qed.

Lemma term_metric_case k (a b : PTm) :
  term_metric k a b
  (ishf a ishne a) k' a', HRed.R a a' term_metric k' a' b k' < k.
Proof.
  move[i][j][va][vb][] [][][].
  case : a //=; try firstorder.
  - inversion 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 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 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.
  move ?.
  apply A_NfNf.
  apply A_Conf; sfirstorder use:hf_no_hred, hne_no_hred.
Qed.

Lemma hne_nf_ne (a : PTm ) :
  ishne a nf a ne a.
Proof. case : a //=. Qed.

Lemma lored_nsteps_renaming k (a b : PTm) (ξ : ) :
  nsteps LoRed.R k a b
  nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b).
Proof.
  induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming.
Qed.

Lemma hred_hne (a b : PTm) :
  HRed.R a b
  ishne a
  False.
Proof. induction 1; sfirstorder. Qed.

Lemma hf_not_hne (a : PTm) :
  ishf a ishne a False.
Proof. case : a => //=. Qed.

Helpers for inverting derivations and ruling out impossible cases


Lemma T_AbsPair_Imp Γ a (b0 b1 : PTm) A :
  Γ ⊢ PAbs a ∈ A
  Γ ⊢ PPair ∈ A
  False.
Proof.
  move /Abs_Inv [][][_]haU.
  move /Pair_Inv [][][_][_]hbU.
  move /Sub_Bind_InvR : haU [i][][].
  have : Γ ⊢ PBind PSig ≲ PBind PPi by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_inj.
Qed.

Lemma T_AbsZero_Imp Γ a (A : PTm) :
  Γ ⊢ PAbs a ∈ A
  Γ ⊢ PZero ∈ A
  False.
Proof.
  move /Abs_Inv [][][_]haU.
  move /Zero_Inv hbU.
  move /Sub_Bind_InvR : haU [i][][].
  have : Γ ⊢ PNat ≲ PBind PPi by eauto using Su_Transitive, Su_Eq.
  clear. hauto lq:on use:synsub_to_usub, Sub.bind_nat_noconf.
Qed.

Lemma T_AbsSuc_Imp Γ a b (A : PTm) :
  Γ ⊢ PAbs a ∈ A
  Γ ⊢ PSuc b ∈ A
  False.
Proof.
  move /Abs_Inv [][][_]haU.
  move /Suc_Inv [_ hbU].
  move /Sub_Bind_InvR : haU [i][][].
  have {hbU } : Γ ⊢ PNat ≲ PBind PPi by eauto using Su_Transitive, Su_Eq.
  hauto lq:on use:Sub.bind_nat_noconf, synsub_to_usub.
Qed.

Lemma Nat_Inv Γ A:
  Γ ⊢ PNat ∈ A
   i, Γ ⊢ PUniv i ≲ A.
Proof.
  move E : PNat u hu.
  move : E.
  elim : Γ u A / hu//=.
  - hauto lq:on use:E_Refl, T_Univ, Su_Eq.
  - hauto lq:on ctrs:LEq.
Qed.

Lemma T_AbsNat_Imp Γ a (A : PTm ) :
  Γ ⊢ PAbs a ∈ A
  Γ ⊢ PNat ∈ A
  False.
Proof.
  move /Abs_Inv [][][_]haU.
  move /Nat_Inv [i hA].
  move /Sub_Univ_InvR : hA [j][k]hA.
  have : Γ ⊢ PBind PPi ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub.
Qed.

Lemma T_PairBind_Imp Γ (a0 a1 : PTm ) p A0 B0 U :
  Γ ⊢ PPair ∈ U
  Γ ⊢ PBind p ∈ U
  False.
Proof.
  move /Pair_Inv [][][_][_]hbU.
  move /Bind_Inv [i][_ [_ haU]].
  move /Sub_Univ_InvR : haU [j][k]hU.
  have : Γ ⊢ PBind PSig ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
Qed.

Lemma T_PairNat_Imp Γ (a0 a1 : PTm) U :
  Γ ⊢ PPair ∈ U
  Γ ⊢ PNat ∈ U
  False.
Proof.
  move/Pair_Inv [][][_][_]hbU.
  move /Nat_Inv [i]/Sub_Univ_InvR[j][k]hU.
  have : Γ ⊢ PBind PSig ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
Qed.

Lemma T_PairZero_Imp Γ (a0 a1 : PTm ) U :
  Γ ⊢ PPair ∈ U
  Γ ⊢ PZero ∈ U
  False.
Proof.
  move/Pair_Inv[][][_][_]hbU.
  move/Zero_Inv. move/Sub_Bind_InvR : hbU[i][][]*.
  have : Γ ⊢ PNat ≲ PBind PSig by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_nat_noconf.
Qed.

Lemma T_PairSuc_Imp Γ (a0 a1 : PTm ) b U :
  Γ ⊢ PPair ∈ U
  Γ ⊢ PSuc b ∈ U
  False.
Proof.
  move/Pair_Inv[][][_][_]hbU.
  move/Suc_Inv[_ hU]. move/Sub_Bind_InvR : hbU[i][][]*.
  have : Γ ⊢ PNat ≲ PBind PSig by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_nat_noconf.
Qed.

Lemma Univ_Inv Γ i U :
  Γ ⊢ PUniv i ∈ U
  Γ ⊢ PUniv i ∈ PUniv (S i) Γ ⊢ PUniv (S i) ≲ U.
Proof.
  move E : (PUniv i) u hu.
  move : i E. elim : Γ u U / hu n //=.
  - hauto l:on use:E_Refl, Su_Eq, T_Univ.
  - hauto lq:on rew:off ctrs:LEq.
Qed.

Lemma T_PairUniv_Imp Γ (a0 a1 : PTm) i U :
  Γ ⊢ PPair ∈ U
  Γ ⊢ PUniv i ∈ U
  False.
Proof.
  move /Pair_Inv [][][_][_]hbU.
  move /Univ_Inv [ ].
  move /Sub_Univ_InvR : [j [k hU]].
  have : Γ ⊢ PBind PSig ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub.
  hauto lq:on use:Sub.bind_univ_noconf.
Qed.

Lemma T_AbsUniv_Imp Γ a i (A : PTm) :
  Γ ⊢ PAbs a ∈ A
  Γ ⊢ PUniv i ∈ A
  False.
Proof.
  move /Abs_Inv [][][_]haU.
  move /Univ_Inv [ ].
  move /Sub_Univ_InvR : [j [k hU]].
  have : Γ ⊢ PBind PPi ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub.
  hauto lq:on use:Sub.bind_univ_noconf.
Qed.

Lemma T_AbsUniv_Imp' Γ (a : PTm) i :
  Γ ⊢ PAbs a ∈ PUniv i False.
Proof.
  hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Abs_Inv.
Qed.

Lemma T_ZeroUniv_Imp' Γ i :
  Γ ⊢ PZero ∈ PUniv i False.
Proof.
  hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Zero_Inv.
Qed.

Lemma T_SucUniv_Imp' Γ (a : PTm) i :
  Γ ⊢ PSuc a ∈ PUniv i False.
Proof.
  hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Suc_Inv.
Qed.

Lemma T_PairUniv_Imp' Γ (a b : PTm) i :
  Γ ⊢ PPair a b ∈ PUniv i False.
Proof.
  hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Pair_Inv.
Qed.

Lemma T_AbsBind_Imp Γ a p A0 B0 (U : PTm ) :
  Γ ⊢ PAbs a ∈ U
  Γ ⊢ PBind p ∈ U
  False.
Proof.
  move /Abs_Inv [][][_ ha].
  move /Bind_Inv [i [_ [_ h]]].
  move /Sub_Univ_InvR : h [j [k hU]].
  have : Γ ⊢ PBind PPi ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub.
  hauto lq:on use:Sub.bind_univ_noconf.
Qed.

Lemma lored_nsteps_suc_inv k (a : PTm ) b :
  nsteps LoRed.R k (PSuc a) b b', nsteps LoRed.R k a b' b = PSuc b'.
Proof.
  move E : (PSuc a) u hu.
  move : a E.
  elim : u b /hu.
  - hauto l:on.
  - scrush ctrs:nsteps inv:LoRed.R.
Qed.

Lemma lored_nsteps_abs_inv k (a : PTm) b :
  nsteps LoRed.R k (PAbs a) b b', nsteps LoRed.R k a b' b = PAbs b'.
Proof.
  move E : (PAbs a) u hu.
  move : a E.
  elim : u b /hu.
  - hauto l:on.
  - scrush ctrs:nsteps inv:LoRed.R.
Qed.

Lemma lored_hne_preservation (a b : PTm) :
    LoRed.R a b ishne a ishne b.
Proof. induction 1; sfirstorder. Qed.

Lemma loreds_hne_preservation (a b : PTm ) :
  rtc LoRed.R a b ishne a ishne b.
Proof. induction 1; hauto lq:on ctrs:rtc use:lored_hne_preservation. Qed.

Lemma lored_nsteps_bind_inv k p (a0 : PTm ) b0 C :
    nsteps LoRed.R k (PBind p ) C
     i j a1 b1,
      i k j k
        C = PBind p
        nsteps LoRed.R i
        nsteps LoRed.R j .
Proof.
  move E : (PBind p ) u hu. move : p E.
  elim : k u C / hu.
  - sauto lq:on.
  - move k ha ha' ih p ?. subst.
    inversion ha; subst //=;
    spec_refl.
    move : ih [i][j][][][?][?][?][]. subst.
    exists (S i),j,,. sauto lq:on solve+:lia.
    move : ih [i][j][][][?][?][?][]. subst.
    exists i,(S j),,. sauto lq:on solve+:lia.
Qed.

Lemma lored_nsteps_ind_inv k P0 (a0 : PTm) b0 c0 U :
  nsteps LoRed.R k (PInd ) U
  ishne
   iP ia ib ic P1 a1 b1 c1,
    iP k ia k ib k ic k
      U = PInd
      nsteps LoRed.R iP
      nsteps LoRed.R ia
      nsteps LoRed.R ib
      nsteps LoRed.R ic .
Proof.
  move E : (PInd ) u hu.
  move : E.
  elim : k u U / hu.
  - sauto lq:on.
  - move k ih ? . subst.
    inversion ; subst //=; spec_refl.
    * move /(_ ltac:(done)) : ih.
      move [iP][ia][ib][ic].
      exists (S iP), ia, ib, ic. sauto lq:on solve+:lia.
    * move /(_ ltac:(sfirstorder use:lored_hne_preservation)) : ih.
      move [iP][ia][ib][ic].
      exists iP, (S ia), ib, ic. sauto lq:on solve+:lia.
    * move /(_ ltac:(done)) : ih.
      move [iP][ia][ib][ic].
      exists iP, ia, (S ib), ic. sauto lq:on solve+:lia.
    * move /(_ ltac:(done)) : ih.
      move [iP][ia][ib][ic].
      exists iP, ia, ib, (S ic). sauto lq:on solve+:lia.
Qed.

Lemma lored_nsteps_app_inv k (a0 b0 C : PTm) :
    nsteps LoRed.R k (PApp ) C
    ishne
     i j a1 b1,
      i k j k
        C = PApp
        nsteps LoRed.R i
        nsteps LoRed.R j .
Proof.
  move E : (PApp ) u hu. move : E.
  elim : k u C / hu.
  - sauto lq:on.
  - move k ih ?. subst.
    inversion ; subst //=.
    spec_refl.
    move h.
    have : ishne by sfirstorder use:lored_hne_preservation.
    move : ih /[apply]. move [i][j][][][?][?][?][].
    subst. exists (S i),j,,. sauto lq:on solve+:lia.
    spec_refl. move : ih /[apply].
    move [i][j][][][?][?][?][]. subst.
    exists i, (S j), , . sauto lq:on solve+:lia.
Qed.

Lemma lored_nsteps_proj_inv k p (a0 C : PTm) :
    nsteps LoRed.R k (PProj p ) C
    ishne
     i a1,
      i k
        C = PProj p
        nsteps LoRed.R i .
Proof.
  move E : (PProj p ) u hu. move : E.
  elim : k u C / hu.
  - sauto lq:on.
  - move k ih ?. subst.
    inversion ; subst //=.
    spec_refl.
    move h.
    have : ishne by sfirstorder use:lored_hne_preservation.
    move : ih /[apply]. move [i][][?][?]. subst.
    exists (S i), . hauto lq:on ctrs:nsteps solve+:lia.
Qed.

Lemma lored_nsteps_app_cong k (a0 a1 b : PTm) :
  nsteps LoRed.R k
  ishne
  nsteps LoRed.R k (PApp b) (PApp b).
  move h. move : b.
  elim : k / h.
  - sauto.
  - move m ih.
    move b hneu.
    apply : nsteps_l; eauto using LoRed.AppCong0.
    apply LoRed.AppCong0;eauto. move : hneu. clear. case : //=.
    apply ih. sfirstorder use:lored_hne_preservation.
Qed.

Lemma lored_nsteps_proj_cong k p (a0 a1 : PTm) :
  nsteps LoRed.R k
  ishne
  nsteps LoRed.R k (PProj p ) (PProj p ).
  move h. move : p.
  elim : k / h.
  - sauto.
  - move m ih p hneu.
    apply : nsteps_l; eauto using LoRed.ProjCong.
    apply LoRed.ProjCong;eauto. move : hneu. clear. case : //=.
    apply ih. sfirstorder use:lored_hne_preservation.
Qed.

Lemma lored_nsteps_pair_inv k (a0 b0 C : PTm ) :
    nsteps LoRed.R k (PPair ) C
     i j a1 b1,
      i k j k
        C = PPair
        nsteps LoRed.R i
        nsteps LoRed.R j .
  move E : (PPair ) u hu. move : E.
  elim : k u C / hu.
  - sauto lq:on.
  - move k ih ?. subst.
    inversion ; subst //=.
    spec_refl.
    move : ih [i][j][][][?][?][?][].
    subst. exists (S i),j,,. sauto lq:on solve+:lia.
    spec_refl.
    move : ih [i][j][][][?][?][?][]. subst.
    exists i, (S j), , . sauto lq:on solve+:lia.
Qed.

Lemma term_metric_abs : k a b,
    term_metric k (PAbs a) (PAbs b)
     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 : k a0 b0 a1 b1,
    term_metric k (PPair ) (PPair )
     k', k' < k term_metric k' term_metric k' .
Proof.
  move k [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 : k p0 a0 b0 p1 a1 b1,
    term_metric k (PBind ) (PBind )
     k', k' < k term_metric k' term_metric k' .
Proof.
  move k [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 : k a b,
    term_metric k (PSuc a) (PSuc b)
     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 ) u
  ishne u
   j, j < k term_metric j (PApp (ren_PTm shift u) (VarPTm var_zero)).
Proof.
  move [i][j][va][vb][][][][] neu.
  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
  move /lored_nsteps_abs_inv : [][]?. subst.
  exists (k - 1).
  simpl in *. split. lia.
  exists i,j,,(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 ) u
  ishne u
   j, j < k term_metric j (PProj PL u) term_metric j (PProj PR u) .
Proof.
  move [i][j][va][vb][][][][] neu.
  have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
  move /lored_nsteps_pair_inv : [][][][][?][?][?][?]?. 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 ) (PApp )
  ishne
  ishne
   j, j < k term_metric j term_metric j .
Proof.
  move [i][j][va][vb][][][][].
  move .
  move : lored_nsteps_app_inv ();repeat move/[apply].
  move [][][][][?][?][?][]. subst.
  move : lored_nsteps_app_inv ();repeat move/[apply].
  move [][][][][?][?][?][]. 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 ) (PProj )
  ishne
  ishne
   j, j < k term_metric j .
Proof.
  move [i][j][va][vb][][][][] .
  move : lored_nsteps_proj_inv ();repeat move/[apply].
  move [][][hi][?]. subst.
  move : lored_nsteps_proj_inv ();repeat move/[apply].
  move [][][hj][?]. 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 ) (PInd )
  ishne
  ishne
   j, j < k term_metric j term_metric j
         term_metric j term_metric j .
Proof.
  move => [i][j][va][vb][][][][] .
  move /lored_nsteps_ind_inv /(_ ) : .
  move =>[iP][ia][ib][ic][][][][][?][?][?][?][?][?][?][?]?. subst.
  move /lored_nsteps_ind_inv /(_ ) : .
  move =>[][][][][][][][][?][?][?][?][?][?][?][?]?. subst.
  exists (k -1). simpl in *.
  hauto lq:on rew:off use:ne_nf b:on solve+:lia.
Qed.

Lemma that hides the arithmetic of term_metric

Lemma term_metric_algo_dom : 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'][][].
  by apply : A_HRedL; eauto.
  case /term_metric_sym /term_metric_case : (h); cycle 1.
  move [k'][b'][hb][/term_metric_sym ].
  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 .
      move /term_metric_app /(_ ) [j][hj][ha]hb.
      apply A_NfNf.
      (* apply A_NfNf. apply A_NeuNeu. apply A_AppCong => //; eauto. *)
      have : HRed.nf by sfirstorder use:hne_no_hred.
      have : HRed.nf by sfirstorder use:hne_no_hred.
      have : algo_dom by eauto using algo_dom_r_algo_dom.
      constructor //. eauto.
    + move .
      have {} : HRed.nf by sfirstorder use:hne_no_hred.
      have {} : HRed.nf by sfirstorder use:hne_no_hred.
      hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom.
    + move .
      have {} : HRed.nf by sfirstorder use:hne_no_hred.
      have {} : HRed.nf by sfirstorder use:hne_no_hred.
      hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
Qed.

Lemma ce_neu_neu_helper a b :
  ishne a ishne b
  ( Γ A B, Γ ⊢ a ∈ A Γ ⊢ b ∈ B a ∼ b) ( Γ A, Γ ⊢ a ∈ A Γ ⊢ b ∈ A a ⇔ b) ( Γ A B, ishne a ishne b Γ ⊢ a ∈ A Γ ⊢ b ∈ B a ∼ b).
Proof. sauto lq:on. Qed.

Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 :
  ishne ishne
  DJoin.R (PInd ) (PInd )
  DJoin.R DJoin.R DJoin.R DJoin.R .
Proof. hauto q:on use:REReds.hne_ind_inv. Qed.

Completeness of Coquand's equality algorithm

Lemma coqeq_complete' :
  ( a b, algo_dom a b DJoin.R a b ( Γ A, Γ ⊢ a ∈ A Γ ⊢ b ∈ A a ⇔ b) ( Γ A B, ishne a ishne b Γ ⊢ a ∈ A Γ ⊢ b ∈ B a ∼ b))
    ( a b, algo_dom_r a b DJoin.R a b Γ A, Γ ⊢ a ∈ A Γ ⊢ b ∈ A a ⇔ b).
  move [:hConfNeuNf hhPairNeu hhAbsNeu].
  apply algo_dom_mutual.
  - move a b h ih hj. split //.
    move Γ A. move : T_Abs_Inv; repeat move/[apply].
    move [Δ][V][].
    have [? ?] : SN a SN b by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply CE_Nf. constructor. apply : ih; eauto using DJoin.abs_inj.
  - abstract : hhAbsNeu.
    move a u hu ha iha hj //.
    split //= Γ A.
    move + h. have ? : SN u by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    move : T_Abs_Neu_Inv h; repeat move/[apply].
    move [Δ][V][ha']hu'.
    apply CE_Nf. constructor //. apply : iha; eauto.
    apply DJoin.abs_inj.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply : DJoin.transitive; eauto.
    apply DJoin.symmetric. apply DJoin.FromEJoin. eexists. split. apply relations.rtc_once.
    apply ERed.AppEta. apply rtc_refl.
  - hauto q:on use:coqeq_symmetric_mutual, DJoin.symmetric, algo_dom_sym.
  - move {hhAbsNeu hhPairNeu hConfNeuNf}.
    move doma iha domb ihb /DJoin.pair_inj hj.
    split //.
    move Γ A .
    have [] : SN (PPair ) SN (PPair ) by hauto lq:on use:logrel.SemWt_SN, fundamental_theorem.
    move : hj; repeat move/[apply].
    move [hja hjb].
    move /Pair_Inv : [][][][].
    move /Pair_Inv : [][][][].
    move /Sub_Bind_InvR : ().
    move [i][][]hE.
    have : Γ ⊢ PBind PSig ≲ PBind PSig
      by eauto using Su_Transitive, Su_Eq.
    have : Γ ⊢ PBind PSig ≲ PBind PSig
      by eauto using Su_Transitive, Su_Eq.
    have : Γ ⊢ ≲ by eauto using Su_Sig_Proj1.
    have : Γ ⊢ ≲ by eauto using Su_Sig_Proj1.
    have ha0A2 : Γ ⊢ ∈ by eauto using T_Conv.
    have ha1A2 : Γ ⊢ ∈ by eauto using T_Conv.
    move : iha (ha0A2) (ha1A2) hja; repeat move/[apply].
    move h.
    apply CE_Nf.
    apply CE_PairPair //.
    have {}haE : Γ ⊢ ≡ ∈
      by hauto l:on use:coqeq_sound_mutual.
    have {} : Γ ⊢ ∈ subst_PTm (scons VarPTm) .
    apply : T_Conv; eauto.
    move /E_Refl in . hauto l:on use:Su_Sig_Proj2.
    eapply ihb; cycle -1; eauto.
    apply : T_Conv; eauto.
    apply Su_Transitive with (B := subst_PTm (scons VarPTm) ).
    move /E_Refl in . hauto l:on use:Su_Sig_Proj2.
    move : hE haE. clear.
    move h.
    eapply regularity in h.
    move : h [_ [hB _]].
    eauto using bind_inst.
  - abstract : hhPairNeu. move {hConfNeuNf}.
    move u neu doma iha domb ihb hj.
    split // Γ A /[dup] wt /Pair_Inv
               [][][][]hU.
    move wtu.
    move /Sub_Bind_InvR : (hU) [i][][]hE.
    have {}wt : Γ ⊢ PPair ∈ PBind PSig by sauto lq:on.
    have {}hu : Γ ⊢ u ∈ PBind PSig by eauto using T_Conv_E.
    move /Pair_Sig_Inv : wt [{} {}].
    have /T_Proj1 huL := hu.
    have /T_Proj2 {hu} huR := hu.
    have heL : ⇔ PProj PL u . apply : iha; eauto.
    apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto.
    apply : N_Exp; eauto. apply N_ProjPairL.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply DJoin.FromRRed1. apply RRed.ProjPair.
    eapply CE_HRed; eauto using rtc_refl.
    apply CE_PairNeu; eauto.
    eapply ihb; eauto.
    apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto.
    apply : N_Exp; eauto. apply N_ProjPairR.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply DJoin.FromRRed1. apply RRed.ProjPair.
    apply : T_Conv; eauto.
    have {}hE : Γ ⊢ PBind PSig ∈ PUniv i
      by hauto l:on use:regularity.
    have /E_Symmetric : Γ ⊢ ≡ PProj PL u ∈ by
      hauto l:on use:coqeq_sound_mutual.
    hauto l:on use:bind_inst.
  - move {hhAbsNeu}.
    move u hu ha iha hb ihb /DJoin.symmetric hj. split // *.
    eapply coqeq_symmetric_mutual.
    eapply algo_dom_sym in ha, hb.
    eapply hhPairNeu //=; eauto; hauto lq:on use:DJoin.symmetric, coqeq_symmetric_mutual.
  - move {hhPairNeu hhAbsNeu}. hauto l:on.
  - move {hhPairNeu hhAbsNeu}.
    move ha iha /DJoin.suc_inj hj. split //.
    move Γ A /Suc_Inv ? /Suc_Inv ?. apply CE_Nf. hauto lq:on ctrs:CoqEq.
  - move i j /DJoin.univ_inj ?. subst.
    split //. hauto l:on.
  - move {hhPairNeu hhAbsNeu} .
    move hA ihA hB ihB /DJoin.bind_inj. move [?][hjA]hjB. subst.
    split // Γ A.
    move .
    have {} : i, Γ ⊢ PBind ∈ PUniv i by move /Bind_Inv in ; qauto use:T_Bind.
    move [i] .
    have {} : i, Γ ⊢ PBind ∈ PUniv i by move /Bind_Inv in ; qauto use:T_Bind.
    move [j] .
    have /Bind_Univ_Inv {} [? ?] : Γ ⊢ PBind ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
    have /Bind_Univ_Inv {} [? ?] : Γ ⊢ PBind ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
    move [:eqa].
    apply CE_Nf. constructor; first by abstract : eqa; eauto.
    eapply ihB; eauto. apply : ctx_eq_subst_one; eauto.
    apply : Su_Eq; eauto. sfirstorder use:coqeq_sound_mutual.
  - hauto l:on.
  - move {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper // Γ A B.
    move /Var_Inv [h [ [ ]]].
    move /Var_Inv [h' [ [ ]]].
    by constructor.
  - move domu ihu doma iha. move /DJoin.hne_app_inj /(_ ) [hju hja].
    apply ce_neu_neu_helper //= Γ A B.
    move /App_Inv [][][][].
    move /App_Inv [][][][].
    move /(_ hju) : ihu.
    move [_ ihb].
    move : ihb () () () (). repeat move/[apply].
    move ihb.
    have : C, Γ ⊢ C ≲ PBind PPi Γ ⊢ C ≲ PBind PPi
        by hauto lq:on use:coqeq_sound_mutual.
    move [C][].
    move /Sub_Bind_InvL : ().
    move [i][][]hE.
    have : Γ ⊢ PBind PPi ≲ PBind PPi by
      eauto using Su_Eq, Su_Transitive.
    have : Γ ⊢ PBind PPi ≲ PBind PPi by
      eauto using Su_Eq, Su_Transitive.
    have : Γ ⊢ ≲ by sfirstorder use:Su_Pi_Proj1.
    have : Γ ⊢ ≲ by sfirstorder use:Su_Pi_Proj1.
    have : Γ ⊢ ∈ by eauto using T_Conv.
    have : Γ ⊢ ∈ by eauto using T_Conv.
    move : iha hja. repeat move/[apply].
    move iha.
    move : iha () (); repeat move/[apply].
    move iha.
    hauto lq:on ctrs:CoqEq_Neu.
  - move doma iha /DJoin.hne_proj_inj /(_ ) [? hja]. subst.
    move : iha hja; repeat move/[apply].
    move [_ iha]. apply ce_neu_neu_helper // Γ A B.
    move : iha () ();repeat move/[apply].
    move ih.
    case : .
    ** move .
       move /Proj1_Inv : . move [][][].
       move /Proj1_Inv : . move [][][].
       move : ih () () () (); repeat move/[apply].
       move ih .
       have [C [ ]] : C, Γ ⊢ C ≲ PBind PSig Γ ⊢ C ≲ PBind PSig
           by hauto lq:on use:coqeq_sound_mutual.
       move /Sub_Bind_InvL : () [i][][].
       have : Γ ⊢ PBind PSig ≲ PBind PSig
         by eauto using Su_Transitive, Su_Eq.
       have : Γ ⊢ PBind PSig ≲ PBind PSig
         by eauto using Su_Transitive, Su_Eq.
       hauto lq:on ctrs:CoqEq_Neu.
    ** move .
       move /Proj2_Inv : . move [][][].
       move /Proj2_Inv : . move [][][].
       move : ih () () () (); repeat move/[apply]. move ih .
       have [C [ ]] : C, Γ ⊢ C ≲ PBind PSig Γ ⊢ C ≲ PBind PSig
           by hauto lq:on use:coqeq_sound_mutual.
       move /Sub_Bind_InvL : () [i][][].
       hauto lq:on ctrs:CoqEq_Neu.
  - move {hhPairNeu hhAbsNeu}.
    move domP ihP domu ihu domb ihb domc ihc /hne_ind_inj.
    move /(_ ) [hjP][hju][hjb]hjc.
    apply ce_neu_neu_helper // Γ A B.
    move /Ind_Inv [][][][][].
    move /Ind_Inv [][][][][].
    have {}iha : ∼ by qauto l:on.
    have [] : max max by lia.
    move : T_Univ_Raise ; repeat move/[apply]. move .
    move : T_Univ_Raise ; repeat move/[apply]. move .
    have {}ihP : ⇔ by qauto l:on.
    set Δ := cons _ _ in , , , .
    have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
    have hPE : Δ ⊢ ≡ ∈ PUniv (max )
      by hauto l:on use:coqeq_sound_mutual.
    have haE : Γ ⊢ ≡ ∈ PNat
      by hauto l:on use:coqeq_sound_mutual.
    have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
    have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) ≡ subst_PTm (scons PZero VarPTm) ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max )).
    eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
    have {} : Γ ⊢ ∈ subst_PTm (scons PZero VarPTm)
      by eauto using T_Conv_E.
    have {}ihb : ⇔ by hauto l:on.
    have hPSig : Γ ⊢ PBind PSig PNat ≡ PBind PSig PNat ∈ PUniv (Nat.max ) by eauto with wt.
    set T := ren_PTm shift _ in .
    have : (cons Δ) ⊢ ∈ T.
    apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
    apply : Su_Eq; eauto.
    subst T. apply : weakening_su; eauto.
    eapply morphing. apply : Su_Eq. apply E_Symmetric. by eauto.
    hauto l:on use:wff_mutual.
    apply morphing_ext. set x := funcomp _ _.
    have : x = funcomp (ren_PTm shift) VarPTm by asimpl.
    apply : morphing_ren; eauto using renaming_shift. by apply morphing_id.
    apply T_Suc. apply T_Var //=. apply here. subst T {}.
    have {}ihc : ⇔ by qauto l:on.
    hauto q:on ctrs:CoqEq_Neu.
  - move a b ha hb.
    move {hhPairNeu hhAbsNeu}.
    case : hb; case : ha.
    + move {hConfNeuNf}.
      move . split; last by sfirstorder use:hf_not_hne.
      move : .
      case : b; case : a //= *; try by (exfalso; eauto 2 using T_AbsPair_Imp, T_AbsUniv_Imp, T_AbsBind_Imp, T_AbsNat_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_PairUniv_Imp, T_PairBind_Imp, T_PairNat_Imp, T_PairZero_Imp, T_PairSuc_Imp).
      sfirstorder use:DJoin.bind_univ_noconf.
      hauto q:on use:REReds.nat_inv, REReds.bind_inv.
      hauto q:on use:REReds.zero_inv, REReds.bind_inv.
      hauto q:on use:REReds.suc_inv, REReds.bind_inv.
      hauto q:on use:REReds.bind_inv, REReds.univ_inv.
      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv.
      hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv.
      hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
      hauto lq:on rew:off use:REReds.bind_inv, REReds.nat_inv.
      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv.
      hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv.
      hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv.
      hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv.
      hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv.
      hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv.
      hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv.
      hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv.
      hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
      hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv.
      hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
    + abstract : hConfNeuNf a b.
      move . split; last by sfirstorder use:hf_not_hne.
      move : .
      case : b; case : a //=; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv, REReds.bind_inv, REReds.nat_inv, REReds.univ_inv, REReds.zero_inv, REReds.suc_inv.
    + rewrite tm_conf_sym.
      move /DJoin.symmetric hb.
      move : hConfNeuNf hb; repeat move/[apply].
      qauto l:on use:coqeq_symmetric_mutual.
    + move neua neub hconf hj.
      move {hConfNeuNf}.
      exfalso.
      move : neua neub hconf hj.
      case : b; case : a //=*; exfalso; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv.
  - sfirstorder.
  - move {hConfNeuNf hhPairNeu hhAbsNeu}.
    move a a' b hr ha iha hj Γ A wta wtb.
    apply : CE_HRedL; eauto.
    apply : iha; eauto; last by sfirstorder use:HRed.preservation.
    apply : DJoin.transitive; eauto.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply DJoin.FromRRed1. by apply HRed.ToRRed.
  - move {hConfNeuNf hhPairNeu hhAbsNeu}.
    move a b b' nfa hr h ih j Γ A wta wtb.
    apply : CE_HRedR; eauto.
    apply : ih; eauto; last by eauto using HRed.preservation.
    apply : DJoin.transitive; eauto.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply DJoin.FromRRed0. by apply HRed.ToRRed.
Qed.

Lemma coqeq_sound : Γ (a b : PTm) A,
    Γ ⊢ a ∈ A Γ ⊢ b ∈ A a ⇔ b Γ ⊢ a ≡ b ∈ A.
Proof. sfirstorder use:coqeq_sound_mutual. Qed.

Lemma sn_term_metric (a b : PTm) : SN a SN b k, term_metric k a b.
Proof.
  move /LoReds.FromSN [va [ ]].
  move /LoReds.FromSN [vb [ ]].
  eapply relations.rtc_nsteps in .
  eapply relations.rtc_nsteps in .
  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.

Lemma coqeq_complete Γ (a b A : PTm) :
  Γ ⊢ a ≡ b ∈ A a ⇔ b.
Proof.
  move => h.
  have : algo_dom_r a b DJoin.R a b by
    hauto lq:on use:fundamental_theorem, logrel.SemEq_SemWt, logrel.SemWt_SN, sn_algo_dom.
  hauto lq:on use:regularity, coqeq_complete'.
Qed.

Coquand's algorithm extended with subtyping

Reserved Notation "a ≪ b" (at level 70).
Reserved Notation "a ⋖ b" (at level 70).
Inductive CoqLEq : PTm PTm Prop :=
| CLE_UnivCong i j :
  i j
  (* -------------------------- *)
  PUniv i ⋖ PUniv j

| CLE_PiCong A0 A1 B0 B1 :
   ≪
   ≪
  (* ---------------------------- *)
  PBind PPi ⋖ PBind PPi

| CLE_SigCong A0 A1 B0 B1 :
   ≪
   ≪
  (* ---------------------------- *)
  PBind PSig ⋖ PBind PSig

| CLE_NatCong :
  PNat ⋖ PNat

| CLE_NeuNeu a0 a1 :
   ∼
   ⋖

with CoqLEq_R : PTm PTm Prop :=
| CLE_HRed a a' b b' :
  rtc HRed.R a a'
  rtc HRed.R b b'
  a' ⋖ b'
  (* ----------------------- *)
  a ≪ b
where "a ≪ b" := (CoqLEq_R a b) and "a ⋖ b" := (CoqLEq a b).

Scheme coqleq_ind := Induction for CoqLEq Sort Prop
  with coqleq_r_ind := Induction for CoqLEq_R Sort Prop.

Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind.

Soundness of Coquand's algorithm extended with subtyping

Lemma coqleq_sound_mutual :
    ( (a b : PTm), a ⋖ b Γ i, Γ ⊢ a ∈ PUniv i Γ ⊢ b ∈ PUniv i Γ ⊢ a ≲ b )
    ( (a b : PTm), a ≪ b Γ i, Γ ⊢ a ∈ PUniv i Γ ⊢ b ∈ PUniv i Γ ⊢ a ≲ b ).
Proof.
  apply coqleq_mutual.
  - hauto lq:on use:wff_mutual ctrs:LEq.
  - move hA ihA hB ihB Γ i.
    move /Bind_Univ_Inv [] /Bind_Univ_Inv [].
    have hlA : Γ ⊢ ≲ by sfirstorder.
    have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
    apply Su_Transitive with (B := PBind PPi ).
    by apply : Su_Pi; eauto using E_Refl, Su_Eq.
    apply : Su_Pi; eauto using E_Refl, Su_Eq.
    apply : ihB; eauto using ctx_eq_subst_one.
  - move hA ihA hB ihB Γ i.
    move /Bind_Univ_Inv [] /Bind_Univ_Inv [].
    have hlA : Γ ⊢ ≲ by sfirstorder.
    have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
    apply Su_Transitive with (B := PBind PSig ).
    apply : Su_Sig; eauto using E_Refl, Su_Eq.
    apply : ihB; by eauto using ctx_eq_subst_one.
    apply : Su_Sig; eauto using E_Refl, Su_Eq.
  - sauto lq:on use:coqeq_sound_mutual, Su_Eq.
  - sauto lq:on use:coqeq_sound_mutual, Su_Eq.
  - move a a' b b' ? ? ? ih Γ i ha hb.
    have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq.
    have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq.
    suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive.
    eauto using HReds.preservation.
Qed.

Lemma CLE_HRedL (a a' b : PTm ) :
  HRed.R a a'
  a' ≪ b
  a ≪ b.
Proof.
  hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
Qed.

Lemma CLE_HRedR (a a' b : PTm) :
  HRed.R a a'
  b ≪ a'
  b ≪ a.
Proof.
  hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
Qed.

Lemma subvar_inj (i j : ) :
    Sub.R (VarPTm i) (VarPTm j) i = j.
Proof.
  rewrite /Sub.R.
  move [c][d][][].
  apply REReds.var_inv in , . subst.
  inversion ; by subst.
Qed.

Lemma algo_dom_hf_hne (a b : PTm) :
  algo_dom a b
  (ishf a ishne a) (ishf b ishne b).
Proof.
  inversion 1;subst //=; by sfirstorder b:on.
Qed.

Lemma algo_dom_neu_neu_nonconf a b :
  algo_dom a b
  neuneu_nonconf a b
  ishne a ishne b.
Proof.
  move /algo_dom_hf_hne h.
  move .
  destruct a,b => //=; sfirstorder b:on.
Qed.

Completeness of Coquand's algorithm extended with subtyping

Lemma coqleq_complete' :
  ( a b, salgo_dom a b Sub.R a b Γ i, Γ ⊢ a ∈ PUniv i Γ ⊢ b ∈ PUniv i a ⋖ b)
  ( a b, salgo_dom_r a b Sub.R a b Γ i, Γ ⊢ a ∈ PUniv i Γ ⊢ b ∈ PUniv i a ≪ b).
Proof.
  apply salgo_dom_mutual.
  - move i j /Sub.univ_inj.
    hauto lq:on ctrs:CoqLEq.
  - move hA ihA hB ihB /Sub.bind_inj. move [_][hjA]hjB Γ i.
    move /Bind_Univ_Inv [ ] /Bind_Univ_Inv [ ].
    have {}ihA : ≪ by hauto l:on.
    constructor //.
    have ihA' : Γ ⊢ ≲ by hauto l:on use:coqleq_sound_mutual.
    suff : (cons Γ) ⊢ ∈ PUniv i
      by hauto l:on.
    eauto using ctx_eq_subst_one.
  - move hA ihA hB ihB /Sub.bind_inj. move [_][hjA]hjB Γ i.
    move /Bind_Univ_Inv [ ] /Bind_Univ_Inv [ ].
    have {}ihA : ≪ by hauto l:on.
    constructor //.
    have ihA' : Γ ⊢ ≲ by hauto l:on use:coqleq_sound_mutual.
    suff : (cons Γ) ⊢ ∈ PUniv i
      by hauto l:on.
    eauto using ctx_eq_subst_one.
  - sfirstorder.
  - move a b hconf hdom.
    have [? ?] : ishne a ishne b by sfirstorder use:algo_dom_neu_neu_nonconf.
    move h. apply Sub.ToJoin in h; last by tauto.
    move Γ i ha hb.
    apply CLE_NeuNeu. hauto q:on use:coqeq_complete'.
  - move [:neunf] a b.
    case ha; case hb.
    move : ha hb.
    + case : a //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
      * case : b //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
        case + + []//=.
        hauto lq:on rew:off use:Sub.bind_inj.
        hauto lq:on rew:off use:Sub.bind_inj.
        hauto lq:on use:Sub.bind_univ_noconf.
        hauto lq:on use:Sub.nat_bind_noconf.
      * case : b //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
        hauto lq:on use:Sub.univ_bind_noconf.
        hauto lq:on use:Sub.nat_univ_noconf.
      * case : b //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
        hauto lq:on use:Sub.bind_nat_noconf.
        hauto lq:on use:Sub.univ_nat_noconf.
    + move .
      apply Sub.ToJoin in ; last by tauto.
      move Γ i wta wtb. exfalso.
      abstract : neunf a b ha hb Γ i wta wtb.
      case : a ha wta //=; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'.
      sfirstorder use: DJoin.hne_bind_noconf.
      sfirstorder use: DJoin.hne_univ_noconf.
      sfirstorder use:DJoin.hne_nat_noconf.
    + move . apply Sub.ToJoin in ; last by tauto.
      hauto drew:off use:DJoin.symmetric, stm_conf_sym.
    + move Γ i wta wtb.
      apply CLE_NeuNeu.
      apply Sub.ToJoin in ; last by tauto.
      eapply coqeq_complete'; eauto.
      apply algo_dom_r_algo_dom.
      sfirstorder use:hne_no_hred.
      sfirstorder use:hne_no_hred.
      hauto lq:on use:sn_algo_dom, logrel.SemWt_SN, fundamental_theorem.
  - hauto l:on.
  - move a a' b hr ha iha hj Γ A wta wtb.
    apply : CLE_HRedL; eauto.
    apply : iha; eauto; last by sfirstorder use:HRed.preservation.
    apply : Sub.transitive; eauto.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply /Sub.FromJoin /DJoin.FromRRed1. by apply HRed.ToRRed.
  - move a b b' nfa hr h ih j Γ A wta wtb.
    apply : CLE_HRedR; eauto.
    apply : ih; eauto; last by eauto using HRed.preservation.
    apply : Sub.transitive; eauto.
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
    apply /Sub.FromJoin /DJoin.FromRRed0. by apply HRed.ToRRed.
Qed.

Putting everything together

Lemma coqleq_complete_unty Γ (A B : PTm) i :
  Γ ⊢ A ∈ PUniv i
  Γ ⊢ B ∈ PUniv i
  Sub.R A B
  A ≪ B.
Proof.
  move h *.
  have : salgo_dom_r A B by
    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN, sn_algo_dom, algo_dom_salgo_dom.
  hauto lq:on use:coqleq_complete'.
Qed.

Lemma coqleq_complete Γ (a b : PTm) :
  Γ ⊢ a ≲ b a ≪ b.
Proof.
  hauto use:coqleq_complete_unty, regularity, logrel.SemLEq_SemWt, fundamental_theorem.
Qed.

Lemma coqleq_sound : Γ (a b : PTm) i j,
    Γ ⊢ a ∈ PUniv i Γ ⊢ b ∈ PUniv j a ≪ b Γ ⊢ a ≲ b.
Proof.
  move Γ a b i j.
  have [*] : i i + j j i + j by lia.
  have : Γ ⊢ a ∈ PUniv (i + j) Γ ⊢ b ∈ PUniv (i + j)
    by sfirstorder use:T_Univ_Raise.
  sfirstorder use:coqleq_sound_mutual.
Qed.

On pen and paper, the three equivalence results from above, when combined with the termination of reduction, allows us to conclude the decidability of type conversion. In Rocq, we need to go through the Bove-Capretta method to obtain the executable function DecSyn.conv_dec.Conv_dec.