[ssr] Refactor under's Setoid generalization to ease stdlib2 porting

Changes:
* Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive];
* Add ssrsetoid.v that links
  [ssrclasses.Reflexive] and [RelationClasses.Reflexive];
* Add [Require Coq.ssr.ssrsetoid] in Setoid.v;
* Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that
  ports some non-exported material from rewrite.ml;
* Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin;
* Update doc and tests as well.

Summary:
* We can now use the under tactic in two flavors:
 - with the [eq] or [iff] relations: [Require Import ssreflect.]
 - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.]
   (while [ssreflect] does not require [RelationClasses] nor [Setoid],
   and conversely [Setoid] does not require [ssreflect]).
* The file ssrsetoid.v could be skipped when porting under to stdlib2.

7 files changed, 159 insertions, 18 deletions

diff --git a/plugins/ssr/ssrclasses.ml b/plugins/ssr/ssrclasses.ml
new file mode 100644
index 0000000000..6cf5ffe201
--- /dev/null
+++ b/plugins/ssr/ssrclasses.ml
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Compatibility layer for [under] and [setoid_rewrite]; see [ssrclasses.v]. *)
+
+(* Clone of [Rewrite.find_global] not using [Coqlib.find_reference] (deprec.) *)
+let find_global s =
+  let gr = lazy (Coqlib.lib_ref s) in
+    fun (evd,cstrs) ->
+      let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in
+        (evd, cstrs), c
+
+(* Copy of [Rewrite.app_poly_check] *)
+let app_poly_check env evars f args =
+  let (evars, cstrs), fc = f evars in
+  let evars, t = Typing.solve_evars env evars (EConstr.mkApp (fc, args)) in
+  (evars, cstrs), t
+
+(* Copy of [Rewrite.goalevars], [Rewrite.cstrevars] *)
+let goalevars evars = fst evars
+let cstrevars evars = snd evars
+
+(* Copy of [Rewrite.extends_undefined] *)
+let extends_undefined evars evars' =
+  let f ev evi found = found || not (Evd.mem evars ev)
+  in Evd.fold_undefined f evars' false
+
+(* Copy of [Rewrite.find_class_proof] *)
+let find_class_proof proof_type proof_method env evars carrier relation =
+  try
+    let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in
+    let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in
+      if extends_undefined (goalevars evars) evars' then raise Not_found
+      else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
+  with e when Logic.catchable_exception e -> raise Not_found
+
+(* Copy of [Rewrite.get_lemma_proof *)
+let get_lemma_proof f env evm x y =
+  let (evm, _), c = f env (evm,Evar.Set.empty) x y in
+    evm, c
+
+(* Clone of [Rewrite.PropGlobal.get_reflexive_proof] *)
+let get_reflexive_proof_aux env =
+  let reflexive_type = find_global "plugins.ssreflect.reflexive_type" in
+  let reflexive_proof = find_global "plugins.ssreflect.reflexive_proof" in
+  find_class_proof reflexive_type reflexive_proof env
+
+(* Clone of [Rewrite.get_reflexive_proof],
+   using [Coq.ssr.ssrclasses.Reflexive]
+   instead of [Coq.Classes.RelationClasses.Reflexive] *)
+let get_reflexive_proof_ssr =
+  get_lemma_proof get_reflexive_proof_aux
diff --git a/plugins/ssr/ssrclasses.mli b/plugins/ssr/ssrclasses.mli
new file mode 100644
index 0000000000..a0a1f40d9d
--- /dev/null
+++ b/plugins/ssr/ssrclasses.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Clone of [Rewrite.get_reflexive_proof],
+    using [Coq.ssr.ssrclasses.Reflexive]
+    instead of [Coq.Classes.RelationClasses.Reflexive] *)
+val get_reflexive_proof_ssr :
+  Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr
diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v
new file mode 100644
index 0000000000..ed9ae0ce17
--- /dev/null
+++ b/plugins/ssr/ssrclasses.v
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+
+(** Compatibility layer for [under] and [setoid_rewrite].
+
+ Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing
+ [Require Import ssreflect] does not [Require Import RelationClasses],
+ and conversely. **)
+
+Section Defs.
+  Context {A : Type}.
+  Class Reflexive (R : A -> A -> Prop) :=
+    reflexivity : forall x : A, R x x.
+End Defs.
+
+Register Reflexive as plugins.ssreflect.reflexive_type.
+Register reflexivity as plugins.ssreflect.reflexive_proof.
+
+Instance iff_Reflexive : Reflexive iff := iff_refl.
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index bd95feacd8..fd73c86fb3 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -579,54 +579,53 @@ End Under_eq.
 Register Under_eq.Under_eq as plugins.ssreflect.Under_eq.
 Register Under_eq.Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq.
 
-Require Import Coq.Relations.Relation_Definitions.
-Require Import RelationClasses.
+Require Import ssrclasses.
 
 Module Type UNDER_REL.
 Parameter Under_rel :
-  forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A.
+  forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop.
 Parameter Under_rel_from_rel :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A),
     @Under_rel A eqA EeqA x y -> eqA x y.
 
 (** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *)
 Parameter Over_rel :
-  forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A.
+  forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop.
 Parameter over_rel :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A),
     @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y.
 Parameter over_rel_done :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
     @Over_rel A eqA EeqA x x.
 Hint Extern 0 (@Over_rel _ _ _ _ _) => solve [ apply over_rel_done ] : core.
 Hint Resolve over_rel_done : core.
 
 (** [under_rel_done]: for Ltac-style over *)
 Parameter under_rel_done :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
     @Under_rel A eqA EeqA x x.
 Notation "''Under[' x ]" := (@Under_rel _ _ _ x _)
   (at level 8, format "''Under['  x  ]", only printing).
 End UNDER_REL.
 
 Module Export Under_rel : UNDER_REL.
-Definition Under_rel (A : Type) (eqA : relation A) (_ : Reflexive eqA) :=
+Definition Under_rel (A : Type) (eqA : A -> A -> Prop) (_ : Reflexive eqA) :=
   eqA.
 Lemma Under_rel_from_rel :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A),
     @Under_rel A eqA EeqA x y -> eqA x y.
 Proof. by []. Qed.
 Definition Over_rel := Under_rel.
 Lemma over_rel :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A),
     @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y.
 Proof. by []. Qed.
 Lemma over_rel_done :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
     @Over_rel A eqA EeqA x x.
 Proof. by []. Qed.
 Lemma under_rel_done :
-  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A),
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
     @Under_rel A eqA EeqA x x.
 Proof. by []. Qed.
 End Under_rel.
diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack
index 824348fee7..66aa6b3e67 100644
--- a/plugins/ssr/ssreflect_plugin.mlpack
+++ b/plugins/ssr/ssreflect_plugin.mlpack
@@ -7,7 +7,7 @@ Ssrview
 Ssrbwd
 Ssrequality
 Ssripats
+Ssrclasses
 Ssrfwd
 Ssrparser
 Ssrvernac
-
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index f67051eeb7..3401a49bf3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -10,7 +10,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open Ltac_plugin
 open Pp
 open Names
 open Constr
@@ -351,7 +350,14 @@ let intro_lock ipats =
         match EConstr.kind_of_type sigma c with
         | Term.AtomicType(hd, args) when
             Array.length args >= 2 && is_app_evar sigma (Array.last args) &&
-            Ssrequality.ssr_is_setoid env sigma hd args ->
+            Ssrequality.ssr_is_setoid env sigma hd args
+            (* if the last condition above [ssr_is_setoid ...] holds
+            then [Coq.Classes.RelationClasses] has been required *)
+            ||
+            (* if this is not the case, the tactic can still succeed
+            when the considered relation is [Coq.Init.Logic.iff] *)
+            Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") &&
+            Array.length args = 2 && is_app_evar sigma args.(1) ->
               Tactics.New.refine ~typecheck:true (fun sigma ->
                 let lm2 = Array.length args - 2 in
                 let sigma, carrier =
@@ -359,8 +365,9 @@ let intro_lock ipats =
                 let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in
                 let rel_args = Array.sub args lm2 2 in
                 let sigma, refl =
-                  (* could raise Not_found in theory *)
-                  Rewrite.get_reflexive_proof env sigma carrier rel in
+                  (* this could raise Not_found, but this should never occur in
+                     practice given ssrclasses.v, so we put no try/with block *)
+                  Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel in
                 let sigma, under_rel =
                   Ssrcommon.mkSsrConst "Under_rel" env sigma in
                 let sigma, under_from_rel =
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v
new file mode 100644
index 0000000000..75653be0c5
--- /dev/null
+++ b/plugins/ssr/ssrsetoid.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+
+(** Compatibility layer for [under] and [setoid_rewrite].
+
+ This file is intended to be required by [Require Import Setoid] or so
+ in order to reconcile [Coq.Classes.RelationClasses.Reflexive] with
+ [Coq.ssr.ssrclasses.Reflexive].
+
+ We can thus use the [under] tactic with other relations than [eq],
+ such as [iff] or a [RewriteRelation], by doing:
+ [Require Import ssreflect. Require Setoid.]
+
+ (Note: this file could be skipped when porting [under] to stdlib2.)
+ *)
+
+Require Import ssrclasses.
+Require Import RelationClasses.
+
+Instance compat_Reflexive :
+  forall {A} {R : A -> A -> Prop},
+    RelationClasses.Reflexive R ->
+    ssrclasses.Reflexive R.
+Proof. now trivial. Qed.