Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issue

Reviewed-by: gares

3 files changed, 9 insertions, 95 deletions

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 1d0c937792..33fc211fa5 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -350,11 +350,8 @@ Changes in 8.11+beta1
   `iff`. Now, it is also performed for any relation `R1` which has a
   ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance
   being also needed so :tacn:`over` can discharge the ``'Under[ _ ]``
-  goal by instantiating the hidden evar.) Also, it is now possible to
-  manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1`
-  is a `PreOrder` relation or so, thanks to extra instances proving
-  that `Under_rel` preserves the properties of the `R1` relation.
-  These two features generalizing support for setoid-like relations is
+  goal by instantiating the hidden evar.)
+  This feature generalizing support for setoid-like relations is
   enabled as soon as we do both ``Require Import ssreflect.`` and
   ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been
   added if one wants to "unprotect" the evar, and instantiate it
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v
index 609c9d5ab8..7c5cd135fe 100644
--- a/plugins/ssr/ssrsetoid.v
+++ b/plugins/ssr/ssrsetoid.v
@@ -18,9 +18,7 @@
  than [eq] or [iff], e.g. a [RewriteRelation], by doing:
  [Require Import ssreflect. Require Setoid.]
 
- This file's instances have priority 12 > other stdlib instances
- and each [Under_rel] instance comes with a [Hint Cut] directive
- (otherwise Ring_polynom.v won't compile because of unbounded search).
+ This file's instances have priority 12 > other stdlib instances.
 
  (Note: this file could be skipped when porting [under] to stdlib2.)
  *)
@@ -38,85 +36,3 @@ Instance compat_Reflexive :
     RelationClasses.Reflexive R ->
     ssrclasses.Reflexive R | 12.
 Proof. now trivial. Qed.
-
-(** Add instances so that ['Under[ F i ]] terms,
-    that is, [Under_rel T R (F i) (?G i)] terms,
-    can be manipulated with rewrite/setoid_rewrite with lemmas on [R].
-    Note that this requires that [R] is a [Prop] relation, otherwise
-    a [bool] relation may need to be "lifted": see the [TestPreOrder]
-    section in test-suite/ssr/under.v *)
-
-Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12.
-Proof. now rewrite Under_relE. Qed.
-
-(* see also Morphisms.trans_co_eq_inv_impl_morphism *)
-
-Instance Under_Reflexive {A} (R : relation A) :
-  RelationClasses.Reflexive R ->
-  RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances.
-
-(* These instances are a bit off-topic given that (Under_rel A R) will
-   typically be reflexive, to be able to trigger the [over] terminator
-
-Instance under_Irreflexive {A} (R : relation A) :
-  RelationClasses.Irreflexive R ->
-  RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances.
-
-Instance under_Asymmetric {A} (R : relation A) :
-  RelationClasses.Asymmetric R ->
-  RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances.
-
-Instance under_StrictOrder {A} (R : relation A) :
-  RelationClasses.StrictOrder R ->
-  RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances.
- *)
-
-Instance Under_Symmetric {A} (R : relation A) :
-  RelationClasses.Symmetric R ->
-  RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances.
-
-Instance Under_Transitive {A} (R : relation A) :
-  RelationClasses.Transitive R ->
-  RelationClasses.Transitive (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances.
-
-Instance Under_PreOrder {A} (R : relation A) :
-  RelationClasses.PreOrder R ->
-  RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances.
-
-Instance Under_PER {A} (R : relation A) :
-  RelationClasses.PER R ->
-  RelationClasses.PER (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_PER Under_PER] : typeclass_instances.
-
-Instance Under_Equivalence {A} (R : relation A) :
-  RelationClasses.Equivalence R ->
-  RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances.
-
-(* Don't handle Antisymmetric and PartialOrder classes for now,
-   as these classes depend on two relation symbols... *)
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index c12491138a..0312b9c733 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -313,8 +313,7 @@ Qed.
 End TestGeneric2.
 
 Section TestPreOrder.
-(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950
-   but without needing to do [rewrite UnderE] manually. *)
+(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 *)
 
 Require Import Morphisms.
 
@@ -330,7 +329,7 @@ Parameter leq_mul :
 
 Local Notation "+%N" := addn (at level 0, only parsing).
 
-(** Context lemma (could *)
+(** Context lemma *)
 Lemma leq'_big : forall I (F G : I -> nat) (r : seq I),
     (forall i : I, leq' (F i) (G i)) ->
     (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)).
@@ -370,8 +369,10 @@ have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n).
 
 under leq'_big => i.
 {
-  (* The "magic" is here: instantiate the evar with the bound "3 + n" *)
-  rewrite lem ?ltn_ord //. over.
+  rewrite UnderE.
+
+  (* instantiate the evar with the bound "3 + n" *)
+  apply: lem; exact: ltn_ord.
 }
 cbv beta.