[ssr] under: Add a contrived example to test under/over with Setoids

* Borrow ideas from the Setoid refman documentation:
  https://coq.inria.fr/refman/addendum/generalized-rewriting.html#first-class-setoids-and-morphisms

* Introduce a relation with the following signature:
  [Rel : forall (m n : nat) (s : Setoid m n), car s -> car s -> Prop]

1 files changed, 43 insertions, 0 deletions

diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 7a723b2c5e..2ef2690252 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -260,3 +260,46 @@ under [X in R _ _ X]ex_gen => a b.
 by move => _.
 Qed.
 End TestGeneric.
+
+Import Setoid.
+(* to expose [Coq.Relations.Relation_Definitions.reflexive],
+   [Coq.Classes.RelationClasses.RewriteRelation], and so on. *)
+
+Section TestGeneric2.
+(* Some toy abstract example with a parameterized setoid type *)
+Record Setoid (m n : nat) : Type :=
+  { car : Type
+  ; Rel : car -> car -> Prop
+  ; refl : reflexive _ Rel
+  ; sym : symmetric _ Rel
+  ; trans : transitive _ Rel
+  }.
+
+Context {m n : nat}.
+Add Parametric Relation (s : Setoid m n) : (car s) (@Rel _ _ s)
+  reflexivity proved by (@refl _ _ s)
+  symmetry proved by (@sym _ _ s)
+  transitivity proved by (@trans _ _ s)
+  as eq_rel.
+
+Context {A : Type} {s1 s2 : Setoid m n}.
+
+Let B := @car m n s1.
+Let C := @car m n s2.
+Variable (F : C -> (A -> A -> B) -> C).
+Hypothesis rel2_gen :
+  forall (c1 c2 : C) (P1 P2 : A -> A -> B),
+    Rel c1 c2 ->
+    (forall a b : A, Rel (P1 a b) (P2 a b)) ->
+    Rel (F c1 P1) (F c2 P2).
+Arguments rel2_gen [c1] c2 [P1] P2 relc12 relP12.
+Lemma test_rel2_gen (c : C) (P : A -> A -> B)
+  (toy_hyp : forall a b, P a b = P b a) :
+  Rel (F c P) (F c (fun a b => P b a)).
+Proof.
+under [here in Rel _ here]rel2_gen.
+- over.
+- by move=> a b; rewrite toy_hyp over.
+- reflexivity.
+Qed.
+End TestGeneric2.