From 903bfaa4516a4348100febc73993dc156917be0e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 11:45:21 +0200
Subject: [PATCH] Add `TCSimpl` type class.

---
 stdpp/base.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/stdpp/base.v b/stdpp/base.v
index 2d2482ca..361276b1 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -209,6 +209,16 @@ Global Hint Mode TCEq ! - - : typeclass_instances.
 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
 Proof. split; destruct 1; reflexivity. Qed.
 
+(** The [TCSimpl] type class is similar to [TCEq] but performs [simpl] before
+proving the goal by reflexivity. *)
+Class TCSimpl {A} (x x' : A) := TCSimpl_TCEq : TCEq x x'.
+Global Hint Extern 0 (TCSimpl _ _) =>
+  simpl; notypeclasses refine (TCEq_refl _) : typeclass_instances.
+Global Hint Mode TCSimpl ! - - : typeclass_instances.
+
+Lemma TCSimpl_eq {A} (x1 x2 : A) : TCSimpl x1 x2 ↔ x1 = x2.
+Proof. apply TCEq_eq. Qed.
+
 Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
-- 
GitLab