fix: Shorten ssrsetoid.v

* This patch is a quick fix that removes part of the features of coq/coq#10022,
  namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
  relation R. This just means we'll need to do an extra step [rewrite UnderE.]
  which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
  feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23

2 files changed, 7 insertions, 90 deletions

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.