Merge branch 'robbert/tcsimpl' into 'master'

Add `TCSimpl` type class.

See merge request !521

CHANGELOG.md

@@ -3,7 +3,8 @@ API-breaking change is listed.
 
 ## std++ master
 
-(nothing yet)
+- Add `TCSimpl` type class that is similar to `TCEq` but performs `simpl`
+  before proving the goal by reflexivity.
 
 ## std++ 1.9.0 (2023-10-11)
 

stdpp/base.v

@@ -209,6 +209,20 @@ 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 x y] type class is similar to [TCEq] but performs [simpl]
+before proving the goal by reflexivity. Similar to [TCEq], the argument [x]
+is the input and [y] the output. When solving [TCEq x y], the argument [x]
+should be a concrete term and [y] an evar for the [simpl]ed result. *)
+Class TCSimpl {A} (x x' : A) := TCSimpl_TCEq : TCEq x x'.
+Global Hint Extern 0 (TCSimpl _ _) =>
+  (* Since the second argument should be an evar, we can call [simpl] on the
+  whole goal. *)
+  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.

tests/typeclasses.ref

+"tc_simpl_test"
+     : string
+1 goal
+  
+  P : nat → Prop
+  y : nat
+  ============================
+  P (S (S (S (S (S (S y))))))

tests/typeclasses.v

-From stdpp Require Import prelude.
+From stdpp Require Import strings.
+
+Lemma tc_simpl_test_lemma (P : nat → Prop) x y :
+  TCSimpl x y →
+  P x → P y.
+Proof. by intros ->%TCSimpl_eq. Qed.
+
+Check "tc_simpl_test".
+Lemma tc_simpl_test (P : nat → Prop) y : P (5 + S y).
+Proof.
+  apply (tc_simpl_test_lemma _ _ _ _). (* would be nicer with ssr [apply:] *)
+  Show.
+Abort.
 
 (** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
     Really, we want to set [Hint Mode Reflexive] in a way that this fails, but