From fb6e1fc314193b39d1c3bf8ed9707100a4fc29fe Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 16 Jul 2024 12:43:40 -0400
Subject: [PATCH 1/8] working on subtyping impl

---
 theories/Extraction/Subtyping.v | 61 +++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 theories/Extraction/Subtyping.v

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
new file mode 100644
index 00000000..4a69d4a2
--- /dev/null
+++ b/theories/Extraction/Subtyping.v
@@ -0,0 +1,61 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Algorithmic Require Import Subtyping.Definitions.
+From Mcltt.Core Require Import NbE.
+From Mcltt.Extraction Require Import NbE.
+From Equations Require Import Equations.
+Import Domain_Notations.
+
+
+Equations subtyping_nf_impl (A B : nf) : bool :=
+| n{{{ Type@i }}}, n{{{ Type@j }}} with Compare_dec.le_lt_dec i j => {
+  | left _ => true;
+  | right _ => false
+  }
+| n{{{ Π A B }}}, n{{{ Π A' B' }}} with nf_eq_dec A A' => {
+  | left _ => subtyping_nf_impl B B'
+  | right _ => false
+  }
+| A, B with nf_eq_dec A B => {
+  | left _ => true
+  | right _ => false
+  }.
+
+Theorem subtyping_nf_impl_sound : forall A B,
+    subtyping_nf_impl A B = true ->
+    alg_subtyping_nf A B.
+Proof.
+  intros. funelim (subtyping_nf_impl A B); mauto 2.
+  all:simp subtyping_nf_impl in *;
+    repeat match goal with
+      | H : _ = _ |- _ => rewrite H in *
+      end;
+    subst;
+    simpl in *;
+    try congruence.
+  all:try solve [econstructor; simpl; trivial].
+  mauto.
+Qed.
+
+Theorem subtyping_nf_impl_complete : forall A B,
+    alg_subtyping_nf A B ->
+    subtyping_nf_impl A B = true.
+Proof.
+  induction 1; subst.
+  - destruct (nf_eq_dec N N) eqn:?; try congruence.
+    destruct N; simp subtyping_nf_impl;
+      try rewrite Heqs;
+      simpl in *;
+      try contradiction;
+      trivial.
+  - simp subtyping_nf_impl.
+    destruct (Compare_dec.le_lt_dec i j);
+      simpl; lia.
+  - simp subtyping_nf_impl.
+    destruct (nf_eq_dec A' A'); simpl; congruence.
+Qed.
+
+
+(* Equations subtyping_impl Γ A B : bool := *)
+(* | Γ, A, B => { *)
+(*     let (w, _) := nbe_impl Γ  *)
+(*   } *)

From ae65659f85829e9c8a9d8a7a9b0f8b7740519a72 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 11:05:07 -0400
Subject: [PATCH 2/8] fux subtyping impl

---
 theories/Extraction/Subtyping.v | 66 +++++++++++++--------------------
 theories/_CoqProject            |  1 +
 2 files changed, 27 insertions(+), 40 deletions(-)

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index 4a69d4a2..e6850b2e 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -6,53 +6,39 @@ From Equations Require Import Equations.
 Import Domain_Notations.
 
 
-Equations subtyping_nf_impl (A B : nf) : bool :=
+#[local]
+  Ltac subtyping_tac :=
+  lazymatch goal with
+  | |- {{ ⊢anf ~_ ⊆ ~_ }} =>
+      subst;
+      mauto 4;
+      try congruence;
+      econstructor; simpl; trivial
+  | |- ~ {{ ⊢anf ~_ ⊆ ~_ }} =>
+      let H := fresh "H" in
+      intro H; dependent destruction H; simpl in *;
+      try lia;
+      try congruence
+  end.
+
+#[tactic="subtyping_tac"]
+Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆ B }} } :=
 | n{{{ Type@i }}}, n{{{ Type@j }}} with Compare_dec.le_lt_dec i j => {
-  | left _ => true;
-  | right _ => false
+  | left _ => left _;
+  | right _ => right _
   }
 | n{{{ Π A B }}}, n{{{ Π A' B' }}} with nf_eq_dec A A' => {
-  | left _ => subtyping_nf_impl B B'
-  | right _ => false
+  | left _ with subtyping_nf_impl B B' => {
+    | left _ => left _
+    | right _ => right _
+    }
+  | right _ => right _
   }
 | A, B with nf_eq_dec A B => {
-  | left _ => true
-  | right _ => false
+  | left _ => left _
+  | right _ => right _
   }.
 
-Theorem subtyping_nf_impl_sound : forall A B,
-    subtyping_nf_impl A B = true ->
-    alg_subtyping_nf A B.
-Proof.
-  intros. funelim (subtyping_nf_impl A B); mauto 2.
-  all:simp subtyping_nf_impl in *;
-    repeat match goal with
-      | H : _ = _ |- _ => rewrite H in *
-      end;
-    subst;
-    simpl in *;
-    try congruence.
-  all:try solve [econstructor; simpl; trivial].
-  mauto.
-Qed.
-
-Theorem subtyping_nf_impl_complete : forall A B,
-    alg_subtyping_nf A B ->
-    subtyping_nf_impl A B = true.
-Proof.
-  induction 1; subst.
-  - destruct (nf_eq_dec N N) eqn:?; try congruence.
-    destruct N; simp subtyping_nf_impl;
-      try rewrite Heqs;
-      simpl in *;
-      try contradiction;
-      trivial.
-  - simp subtyping_nf_impl.
-    destruct (Compare_dec.le_lt_dec i j);
-      simpl; lia.
-  - simp subtyping_nf_impl.
-    destruct (nf_eq_dec A' A'); simpl; congruence.
-Qed.
 
 
 (* Equations subtyping_impl Γ A B : bool := *)
diff --git a/theories/_CoqProject b/theories/_CoqProject
index eaee3ea6..1c123f27 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -77,4 +77,5 @@
 ./Extraction/NbE.v
 ./Extraction/Readback.v
 ./Extraction/TypeCheck.v
+./Extraction/Subtyping.v
 ./LibTactics.v

From 30f229af5cc8deaecdb75b42acbc8ab1fbf4ff11 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 11:11:08 -0400
Subject: [PATCH 3/8] implement an NbE for types

---
 theories/Extraction/NbE.v | 126 +++++++++++++++++++++++++++++++-------
 1 file changed, 103 insertions(+), 23 deletions(-)

diff --git a/theories/Extraction/NbE.v b/theories/Extraction/NbE.v
index b23d7645..01ee2441 100644
--- a/theories/Extraction/NbE.v
+++ b/theories/Extraction/NbE.v
@@ -107,45 +107,125 @@ Qed.
 #[local]
   Hint Resolve nbe_order_sound : mcltt.
 
-#[local]
-  Ltac impl_obl_tac1 :=
+Section NbEDef.
+
+  #[local]
+    Ltac impl_obl_tac1 :=
   match goal with
   | H : nbe_order _ _ _ |- _ => progressive_invert H
   end.
 
+  #[local]
+    Ltac impl_obl_tac :=
+    repeat impl_obl_tac1; try econstructor; mauto.
+
+  #[tactic="impl_obl_tac"]
+    Equations nbe_impl G M A (H : nbe_order G M A) : { w | nbe G M A w } by struct H :=
+  | G, M, A, H =>
+      let (p, Hp) := initial_env_impl G _ in
+      let (a, Ha) := eval_exp_impl A p _ in
+      let (m, Hm) := eval_exp_impl M p _ in
+      let (w, Hw) := read_nf_impl (length G) d{{{ ⇓ a m }}} _ in
+      exist _ w _.
+
+  Lemma nbe_impl_complete' : forall G M A w,
+      nbe G M A w ->
+      forall (H : nbe_order G M A),
+      exists H', nbe_impl G M A H = exist _ w H'.
+  Proof.
+    induction 1;
+      pose proof initial_env_impl_complete';
+      pose proof eval_exp_impl_complete';
+      pose proof read_nf_impl_complete';
+      intros; simp nbe_impl;
+      repeat complete_tac;
+      eauto.
+  Qed.
+
+End NbEDef.
+
 #[local]
-  Ltac impl_obl_tac :=
-  repeat impl_obl_tac1; try econstructor; mauto.
-
-#[tactic="impl_obl_tac"]
-  Equations nbe_impl G M A (H : nbe_order G M A) : { w | nbe G M A w } by struct H :=
-| G, M, A, H =>
-    let (p, Hp) := initial_env_impl G _ in
-    let (a, Ha) := eval_exp_impl A p _ in
-    let (m, Hm) := eval_exp_impl M p _ in
-    let (w, Hw) := read_nf_impl (length G) d{{{ ⇓ a m }}} _ in
-    exist _ w _.
-
-Lemma nbe_impl_complete' : forall G M A w,
+  Hint Resolve nbe_impl_complete' : mcltt.
+
+Lemma nbe_impl_complete : forall G M A w,
     nbe G M A w ->
-    forall (H : nbe_order G M A),
-      exists H', nbe_impl G M A H = exist _ w H'.
+      exists H H', nbe_impl G M A H = exist _ w H'.
+Proof.
+  repeat unshelve mauto.
+Qed.
+
+
+Inductive nbe_ty_order G A : Prop :=
+| nbe_ty_order_run :
+  `( initial_env_order G ->
+     (forall p, initial_env G p ->
+           eval_exp_order A p) ->
+     (forall p a,
+         initial_env G p ->
+         {{ ⟦ A ⟧ p ↘ a }} ->
+         read_typ_order (length G) a) ->
+     nbe_ty_order G A ).
+
+#[local]
+  Hint Constructors nbe_ty_order : mcltt.
+
+
+Lemma nbe_ty_order_sound : forall G A w,
+    nbe_ty G A w ->
+    nbe_ty_order G A.
+Proof with (econstructor; intros;
+            functional_initial_env_rewrite_clear;
+            functional_eval_rewrite_clear;
+            functional_read_rewrite_clear;
+            mauto).
+  induction 1...
+Qed.
+
+#[local]
+  Hint Resolve nbe_ty_order_sound : mcltt.
+
+Section NbETyDef.
+
+  #[local]
+    Ltac impl_obl_tac1 :=
+  match goal with
+  | H : nbe_ty_order _ _ |- _ => progressive_invert H
+  end.
+
+  #[local]
+    Ltac impl_obl_tac :=
+    repeat impl_obl_tac1; try econstructor; mauto.
+
+  #[tactic="impl_obl_tac"]
+    Equations nbe_ty_impl G A (H : nbe_ty_order G A) : { w | nbe_ty G A w } by struct H :=
+  | G, A, H =>
+      let (p, Hp) := initial_env_impl G _ in
+      let (a, Ha) := eval_exp_impl A p _ in
+      let (w, Hw) := read_typ_impl (length G) a _ in
+      exist _ w _.
+
+End NbETyDef.
+
+Lemma nbe_ty_impl_complete' : forall G A w,
+    nbe_ty G A w ->
+    forall (H : nbe_ty_order G A),
+      exists H', nbe_ty_impl G A H = exist _ w H'.
 Proof.
   induction 1;
     pose proof initial_env_impl_complete';
     pose proof eval_exp_impl_complete';
-    pose proof read_nf_impl_complete';
-    intros; simp nbe_impl;
+    pose proof read_typ_impl_complete';
+    intros; simp nbe_ty_impl;
     repeat complete_tac;
     eauto.
 Qed.
 
 #[local]
-  Hint Resolve nbe_impl_complete' : mcltt.
+  Hint Resolve nbe_ty_impl_complete' : mcltt.
 
-Lemma nbe_impl_complete : forall G M A w,
-    nbe G M A w ->
-      exists H H', nbe_impl G M A H = exist _ w H'.
+Lemma nbe_ty_impl_complete : forall G A w,
+    nbe_ty G A w ->
+      exists H H', nbe_ty_impl G A H = exist _ w H'.
 Proof.
   repeat unshelve mauto.
 Qed.

From 358c3db1771ad6ad092fc211febf88181db6f7c8 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 11:42:27 -0400
Subject: [PATCH 4/8] what's wrong with Equations

---
 theories/Extraction/Subtyping.v | 31 +++++++++++++++++++++++++++----
 1 file changed, 27 insertions(+), 4 deletions(-)

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index e6850b2e..15b93ccc 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -40,8 +40,31 @@ Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆
   }.
 
 
+Inductive subtyping_order G A B :=
+| subtyping_order_run :
+  nbe_ty_order G A ->
+  nbe_ty_order G B ->
+  subtyping_order G A B.
+#[local]
+  Hint Constructors subtyping_order : mcltt.
+
+#[local]
+  Ltac subtyping_impl_tac1 :=
+  match goal with
+  | H : subtyping_order _ _ _ |- _ => progressive_invert H
+  end.
 
-(* Equations subtyping_impl Γ A B : bool := *)
-(* | Γ, A, B => { *)
-(*     let (w, _) := nbe_impl Γ  *)
-(*   } *)
+#[local]
+  Ltac subtyping_impl_tac :=
+  repeat subtyping_impl_tac1; try econstructor; mauto.
+
+Equations? subtyping_impl G A B (H1 : nbe_ty_order G A) (H2 : nbe_ty_order G B) :
+  { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
+| G, A, B with nbe_ty_impl G A H1 => {
+  | @exist a _ with nbe_ty_impl G B H2 => {
+    | @exist b _ with subtyping_nf_impl a b => {
+      | left _ => _;
+      | right _ => _
+      }
+    }
+  }.

From 6ae9082960e84c71760678c219c11483f6dd56ef Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 14:19:55 -0400
Subject: [PATCH 5/8] define subtyping

---
 theories/Extraction/Subtyping.v | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index 15b93ccc..c51a272a 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -52,19 +52,26 @@ Inductive subtyping_order G A B :=
   Ltac subtyping_impl_tac1 :=
   match goal with
   | H : subtyping_order _ _ _ |- _ => progressive_invert H
+  | H : nbe_ty_order _ _ |- _ => progressive_invert H
   end.
 
 #[local]
   Ltac subtyping_impl_tac :=
   repeat subtyping_impl_tac1; try econstructor; mauto.
 
-Equations? subtyping_impl G A B (H1 : nbe_ty_order G A) (H2 : nbe_ty_order G B) :
+#[tactic="subtyping_impl_tac"]
+Equations subtyping_impl G A B (H : subtyping_order G A B) :
   { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
-| G, A, B with nbe_ty_impl G A H1 => {
-  | @exist a _ with nbe_ty_impl G B H2 => {
+| G, A, B, H with nbe_ty_impl G A _ => {
+  | @exist a _ with nbe_ty_impl G B _ => {
     | @exist b _ with subtyping_nf_impl a b => {
-      | left _ => _;
-      | right _ => _
+      | left _ => left _;
+      | right _ => right _
       }
     }
   }.
+Next Obligation.
+  progressive_inversion.
+  functional_nbe_rewrite_clear.
+  contradiction.
+Qed.

From c8eee0b1d08aa07e171a4b2ad1fa63ff2f7f22f9 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 14:40:55 -0400
Subject: [PATCH 6/8] finish subtyping

---
 theories/Extraction/Subtyping.v | 78 +++++++++++++++++++++++++++++----
 1 file changed, 69 insertions(+), 9 deletions(-)

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index c51a272a..3099ee18 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -1,7 +1,7 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Algorithmic Require Import Subtyping.Definitions.
 From Mcltt.Core Require Import NbE.
-From Mcltt.Extraction Require Import NbE.
+From Mcltt.Extraction Require Import Evaluation NbE.
 From Equations Require Import Equations.
 Import Domain_Notations.
 
@@ -39,6 +39,31 @@ Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆
   | right _ => right _
   }.
 
+Theorem subtyping_nf_impl_complete : forall A B,
+    {{ ⊢anf A ⊆ B }} ->
+    exists H, subtyping_nf_impl A B = left H.
+Proof.
+  induction 1; subst;
+    simp subtyping_nf_impl.
+  - destruct (nf_eq_dec N N) eqn:Heq;
+      [| congruence].
+    destruct N; try contradiction;
+      simp subtyping_nf_impl;
+      rewrite Heq;
+      simpl; eauto.
+  - destruct (Compare_dec.le_lt_dec i j);
+      simp subtyping_nf_impl;
+      eauto.
+    lia.
+  - destruct_all.
+    destruct (nf_eq_dec A' A');
+      [ |congruence].
+    simp subtyping_nf_impl.
+    bulky_rewrite.
+    simp subtyping_nf_impl.
+    eauto.
+Qed.
+
 
 Inductive subtyping_order G A B :=
 | subtyping_order_run :
@@ -48,6 +73,16 @@ Inductive subtyping_order G A B :=
 #[local]
   Hint Constructors subtyping_order : mcltt.
 
+
+Lemma subtyping_order_sound : forall G A B,
+    {{ G ⊢a A ⊆ B }} ->
+    subtyping_order G A B.
+Proof.
+  intros * H.
+  dependent destruction H.
+  mauto using nbe_ty_order_sound.
+Qed.
+
 #[local]
   Ltac subtyping_impl_tac1 :=
   match goal with
@@ -59,19 +94,44 @@ Inductive subtyping_order G A B :=
   Ltac subtyping_impl_tac :=
   repeat subtyping_impl_tac1; try econstructor; mauto.
 
+
 #[tactic="subtyping_impl_tac"]
 Equations subtyping_impl G A B (H : subtyping_order G A B) :
   { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
-| G, A, B, H with nbe_ty_impl G A _ => {
-  | @exist a _ with nbe_ty_impl G B _ => {
-    | @exist b _ with subtyping_nf_impl a b => {
-      | left _ => left _;
-      | right _ => right _
-      }
-    }
-  }.
+| G, A, B, H =>
+    let (a, Ha) := nbe_ty_impl G A _ in
+    let (b, Hb) := nbe_ty_impl G B _ in
+    match subtyping_nf_impl a b with
+    | left _ => left _
+    | right _ => right _
+    end.
 Next Obligation.
   progressive_inversion.
   functional_nbe_rewrite_clear.
   contradiction.
 Qed.
+
+Theorem subtyping_impl_complete' : forall G A B,
+    {{G ⊢a A ⊆ B}} ->
+    forall (H : subtyping_order G A B),
+      exists H', subtyping_impl G A B H = left H'.
+Proof.
+  intros * Hsub H.
+  dependent destruction Hsub.
+  simp subtyping_impl.
+  pose proof nbe_ty_impl_complete';
+    repeat complete_tac;
+    eauto.
+  edes_rewrite subtyping_nf_impl_complete;
+    eauto.
+Qed.
+
+#[local]
+ Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt.
+
+Theorem subtyping_impl_complete : forall G A B,
+    {{G ⊢a A ⊆ B}} ->
+    exists H H', subtyping_impl G A B H = left H'.
+Proof.
+  repeat unshelve mauto.
+Qed.

From 5728c0ebd9ccc683631cc4bb77b9787b0e414712 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 14:44:10 -0400
Subject: [PATCH 7/8] simplify proofs

---
 theories/Extraction/Subtyping.v | 33 ++++++---------------------------
 1 file changed, 6 insertions(+), 27 deletions(-)

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index 3099ee18..61b87abf 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -43,25 +43,9 @@ Theorem subtyping_nf_impl_complete : forall A B,
     {{ ⊢anf A ⊆ B }} ->
     exists H, subtyping_nf_impl A B = left H.
 Proof.
-  induction 1; subst;
-    simp subtyping_nf_impl.
-  - destruct (nf_eq_dec N N) eqn:Heq;
-      [| congruence].
-    destruct N; try contradiction;
-      simp subtyping_nf_impl;
-      rewrite Heq;
-      simpl; eauto.
-  - destruct (Compare_dec.le_lt_dec i j);
-      simp subtyping_nf_impl;
-      eauto.
-    lia.
-  - destruct_all.
-    destruct (nf_eq_dec A' A');
-      [ |congruence].
-    simp subtyping_nf_impl.
-    bulky_rewrite.
-    simp subtyping_nf_impl.
-    eauto.
+  intros.
+  destruct (subtyping_nf_impl A B) eqn:Heq; eauto.
+  contradiction.
 Qed.
 
 
@@ -116,14 +100,9 @@ Theorem subtyping_impl_complete' : forall G A B,
     forall (H : subtyping_order G A B),
       exists H', subtyping_impl G A B H = left H'.
 Proof.
-  intros * Hsub H.
-  dependent destruction Hsub.
-  simp subtyping_impl.
-  pose proof nbe_ty_impl_complete';
-    repeat complete_tac;
-    eauto.
-  edes_rewrite subtyping_nf_impl_complete;
-    eauto.
+  intros.
+  destruct (subtyping_impl G A B H0) eqn:Heq; eauto.
+  contradiction.
 Qed.
 
 #[local]

From ad31732ab1f7e9ade7e6e9d7c19155319edac5f1 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 20 Aug 2024 14:48:27 -0400
Subject: [PATCH 8/8] further improvement

---
 theories/Extraction/Subtyping.v |  9 +++------
 theories/LibTactics.v           | 13 +++++++++++++
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index 61b87abf..c99e48d1 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -43,9 +43,7 @@ Theorem subtyping_nf_impl_complete : forall A B,
     {{ ⊢anf A ⊆ B }} ->
     exists H, subtyping_nf_impl A B = left H.
 Proof.
-  intros.
-  destruct (subtyping_nf_impl A B) eqn:Heq; eauto.
-  contradiction.
+  intros; dec_complete.
 Qed.
 
 
@@ -95,14 +93,13 @@ Next Obligation.
   contradiction.
 Qed.
 
+
 Theorem subtyping_impl_complete' : forall G A B,
     {{G ⊢a A ⊆ B}} ->
     forall (H : subtyping_order G A B),
       exists H', subtyping_impl G A B H = left H'.
 Proof.
-  intros.
-  destruct (subtyping_impl G A B H0) eqn:Heq; eauto.
-  contradiction.
+  intros; dec_complete.
 Qed.
 
 #[local]
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 206857fe..8ecf9077 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -486,3 +486,16 @@ Ltac bulky_rewrite_in1 HT :=
   end.
 
 Ltac bulky_rewrite_in HT := repeat (bulky_rewrite_in1 HT; mauto 2).
+
+
+(** This tactic provides a trivial proof for the completeness of a decision procedure. *)
+Ltac dec_complete :=
+  lazymatch goal with
+  | |- exists _, ?L = _ =>
+      lazymatch type of L with
+      | sumbool _ _ =>
+          let Heq := fresh "Heq" in
+          destruct L eqn:Heq; eauto;
+          contradiction
+      end
+  end.