Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) relation

Reviewed-by: gares

7 files changed, 278 insertions, 109 deletions

diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v
new file mode 100644
index 0000000000..0ae3f8c6a5
--- /dev/null
+++ b/plugins/ssr/ssrclasses.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   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].
+
+ Note: this file does not require [ssreflect]; it is both required by
+ [ssrsetoid] and required by [ssrunder].
+
+ 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 eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A.
+Instance iff_Reflexive : Reflexive iff := iff_refl.
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 9ebdf71329..bc4a57dedd 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -530,102 +530,32 @@ Lemma abstract_context T (P : T -> Type) x :
 Proof. by move=> /(_ P); apply. Qed.
 
 (*****************************************************************************)
-(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *)
-
-Module Type UNDER_EQ.
-Parameter Under_eq :
-  forall (R : Type), R -> R -> Prop.
-Parameter Under_eq_from_eq :
-  forall (T : Type) (x y : T), @Under_eq T x y -> x = y.
-
-(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *)
-Parameter Over_eq :
-  forall (R : Type), R -> R -> Prop.
-Parameter over_eq :
-  forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y.
-Parameter over_eq_done :
-  forall (T : Type) (x : T), @Over_eq T x x.
-(* We need both hints below, otherwise the test-suite does not pass *)
-Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core.
-(* => for [test-suite/ssr/under.v:test_big_patt1] *)
-Hint Resolve over_eq_done : core.
-(* => for [test-suite/ssr/over.v:test_over_1_1] *)
-
-(** [under_eq_done]: for Ltac-style over *)
-Parameter under_eq_done :
-  forall (T : Type) (x : T), @Under_eq T x x.
-Notation "''Under[' x ]" := (@Under_eq _ x _)
-  (at level 8, format "''Under['  x  ]", only printing).
-End UNDER_EQ.
-
-Module Export Under_eq : UNDER_EQ.
-Definition Under_eq := @eq.
-Lemma Under_eq_from_eq (T : Type) (x y : T) :
-  @Under_eq T x y -> x = y.
-Proof. by []. Qed.
-Definition Over_eq := Under_eq.
-Lemma over_eq :
-  forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y.
-Proof. by []. Qed.
-Lemma over_eq_done :
-  forall (T : Type) (x : T), @Over_eq T x x.
-Proof. by []. Qed.
-Lemma under_eq_done :
-  forall (T : Type) (x : T), @Under_eq T x x.
-Proof. by []. Qed.
-End Under_eq.
-
-Register Under_eq as plugins.ssreflect.Under_eq.
-Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq.
-
-Module Type UNDER_IFF.
-Parameter Under_iff : Prop -> Prop -> Prop.
-Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
-
-(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *)
-Parameter Over_iff : Prop -> Prop -> Prop.
-Parameter over_iff :
-  forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
-Parameter over_iff_done :
-  forall (x : Prop), @Over_iff x x.
-Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core.
-Hint Resolve over_iff_done : core.
-
-(** [under_iff_done]: for Ltac-style over *)
-Parameter under_iff_done :
-  forall (x : Prop), @Under_iff x x.
-Notation "''Under[' x ]" := (@Under_iff x _)
-  (at level 8, format "''Under['  x  ]", only printing).
-End UNDER_IFF.
-
-Module Export Under_iff : UNDER_IFF.
-Definition Under_iff := iff.
-Lemma Under_iff_from_iff (x y : Prop) :
-  @Under_iff x y -> x <-> y.
-Proof. by []. Qed.
-Definition Over_iff := Under_iff.
-Lemma over_iff :
-  forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
-Proof. by []. Qed.
-Lemma over_iff_done :
-  forall (x : Prop), @Over_iff x x.
-Proof. by []. Qed.
-Lemma under_iff_done :
-  forall (x : Prop), @Under_iff x x.
-Proof. by []. Qed.
-End Under_iff.
-
-Register Under_iff as plugins.ssreflect.Under_iff.
-Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff.
-
-Definition over := (over_eq, over_iff).
+(* Material for under/over (to rewrite under binders using "context lemmas") *)
 
+Require Export ssrunder.
+
+Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) =>
+  solve [ apply: Under_rel.over_rel_done ] : core.
+Hint Resolve Under_rel.over_rel_done : core.
+
+Register Under_rel.Under_rel as plugins.ssreflect.Under_rel.
+Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel.
+
+(** Closing rewrite rule *)
+Definition over := over_rel.
+
+(** Closing tactic *)
 Ltac over :=
-  by [ apply: Under_eq.under_eq_done
-     | apply: Under_iff.under_iff_done
+  by [ apply: Under_rel.under_rel_done
      | rewrite over
      ].
 
+(** Convenience rewrite rule to unprotect evars, e.g., to instantiate
+    them in another way than with reflexivity. *)
+Definition UnderE := Under_relE.
+
+(*****************************************************************************)
+
 (** An interface for non-Prop types; used to avoid improper instantiation
     of polymorphic lemmas with on-demand implicits when they are used as views.
     For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y.
diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack
index 824348fee7..46669998b9 100644
--- a/plugins/ssr/ssreflect_plugin.mlpack
+++ b/plugins/ssr/ssreflect_plugin.mlpack
@@ -10,4 +10,3 @@ Ssripats
 Ssrfwd
 Ssrparser
 Ssrvernac
-
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index 43aeeb2dae..baf5288725 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -42,6 +42,9 @@ val mk_rwarg :
 val norwmult : ssrdir * ssrmult
 val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option
 
+val ssr_is_setoid :
+  Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool
+
 val ssrinstancesofrule :
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssrdir ->
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index cca94c8c9b..b0f56c423f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -340,6 +340,21 @@ let intro_lock ipats =
   let hnf' = Proofview.numgoals >>= fun ng ->
              Proofview.tclDISPATCH
                (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
+  let protect_subgoal env sigma hd args =
+    Tactics.New.refine ~typecheck:true (fun sigma ->
+        let lm2 = Array.length args - 2 in
+        let sigma, carrier =
+          Typing.type_of env sigma args.(lm2) in
+        let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in
+        let rel_args = Array.sub args lm2 2 in
+        let sigma, under_rel =
+          Ssrcommon.mkSsrConst "Under_rel" env sigma in
+        let sigma, under_from_rel =
+          Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in
+        let under_rel_args = Array.append [|carrier; rel|] rel_args in
+        let ty = EConstr.mkApp (under_rel, under_rel_args) in
+        let sigma, t = Evarutil.new_evar env sigma ty in
+        sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) in
   let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
     Proofview.tclORELSE
       (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
@@ -349,30 +364,23 @@ let intro_lock ipats =
         let env = Proofview.Goal.env gl in
         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
+            (* 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 sigma, under_iff =
-                 Ssrcommon.mkSsrConst "Under_iff" env sigma in
-               let sigma, under_from_iff =
-                 Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in
-               let ty = EConstr.mkApp (under_iff,args) in
-               let sigma, t = Evarutil.new_evar env sigma ty in
-               sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|]))
+            Array.length args = 2 && is_app_evar sigma args.(1) ->
+          protect_subgoal env sigma hd args
         | _ ->
         let t = Reductionops.whd_all env sigma c in
         match EConstr.kind_of_type sigma t with
         | Term.AtomicType(hd, args) when
             Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
             Array.length args = 3 && is_app_evar sigma args.(2) ->
-              Tactics.New.refine ~typecheck:true (fun sigma ->
-                let sigma, under =
-                  Ssrcommon.mkSsrConst "Under_eq" env sigma in
-                let sigma, under_from_eq =
-                  Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in
-                let ty = EConstr.mkApp (under,args) in
-                let sigma, t = Evarutil.new_evar env sigma ty in
-                sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
+          protect_subgoal env sigma hd args
         | _ ->
     ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
 
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v
new file mode 100644
index 0000000000..609c9d5ab8
--- /dev/null
+++ b/plugins/ssr/ssrsetoid.v
@@ -0,0 +1,122 @@
+(************************************************************************)
+(*         *   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].
+
+ In particular, we can use the [under] tactic with other relations
+ 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).
+
+ (Note: this file could be skipped when porting [under] to stdlib2.)
+ *)
+
+Require Import ssrclasses.
+Require Import ssrunder.
+Require Import RelationClasses.
+Require Import Relation_Definitions.
+
+(** Reconcile [Coq.Classes.RelationClasses.Reflexive] with
+    [Coq.ssr.ssrclasses.Reflexive] *)
+
+Instance compat_Reflexive :
+  forall {A} {R : relation A},
+    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/plugins/ssr/ssrunder.v b/plugins/ssr/ssrunder.v
new file mode 100644
index 0000000000..7c529a6133
--- /dev/null
+++ b/plugins/ssr/ssrunder.v
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*         *   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># **)
+
+(** Constants for under/over, to rewrite under binders using "context lemmas"
+
+ Note: this file does not require [ssreflect]; it is both required by
+ [ssrsetoid] and *exported* by [ssrunder].
+
+ This preserves the following feature: we can use [Setoid] without
+ requiring [ssreflect] and use [ssreflect] without requiring [Setoid].
+*)
+
+Require Import ssrclasses.
+
+Module Type UNDER_REL.
+Parameter Under_rel :
+  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
+Parameter Under_rel_from_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y -> eqA x y.
+Parameter Under_relE :
+  forall (A : Type) (eqA : A -> A -> Prop),
+    @Under_rel A eqA = eqA.
+
+(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *)
+Parameter Over_rel :
+  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
+Parameter over_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y = @Over_rel A eqA x y.
+Parameter over_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Over_rel A eqA x x.
+
+(** [under_rel_done]: for Ltac-style over *)
+Parameter under_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Under_rel A eqA 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 : A -> A -> Prop) :=
+  eqA.
+Lemma Under_rel_from_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y -> eqA x y.
+Proof. now trivial. Qed.
+Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) :
+  @Under_rel A eqA = eqA.
+Proof. now trivial. Qed.
+Definition Over_rel := Under_rel.
+Lemma over_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y = @Over_rel A eqA x y.
+Proof. now trivial. Qed.
+Lemma over_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Over_rel A eqA x x.
+Proof. now unfold Over_rel. Qed.
+Lemma under_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Under_rel A eqA x x.
+Proof. now trivial. Qed.
+End Under_rel.