[ssr] under: extend ssreflect.v to generalize iff to any setoid eq

* Add an extra test with an Equivalence.

* Update the doc accordingly.

4 files changed, 98 insertions, 52 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ed980bd4de..0af23354cc 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3756,8 +3756,9 @@ involves the following steps:
    the corresponding intro pattern :n:`@i_pattern__i` in each goal.
 
 4. Then :tacn:`under` checks that the first n subgoals
-   are (quantified) equalities or double implications between a
-   term and an evar (e.g. ``m - m = ?F2 m`` in the running example).
+   are (quantified) Leibniz equalities or registered Setoid equalities
+   between a term and an evar (e.g. ``m - m = ?F2 m`` in the running
+   example).
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 71abafc22f..bd95feacd8 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -531,7 +531,7 @@ 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". *)
+(* Constants for under/over, to rewrite under binders using "context lemmas" *)
 
 Module Type UNDER_EQ.
 Parameter Under_eq :
@@ -576,54 +576,69 @@ Lemma under_eq_done :
 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 _)
+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.
+
+Module Type UNDER_REL.
+Parameter Under_rel :
+  forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A.
+Parameter Under_rel_from_rel :
+  forall (A : Type) (eqA : relation A) (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.
+Parameter over_rel :
+  forall (A : Type) (eqA : relation A) (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),
+    @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),
+    @Under_rel A eqA EeqA x x.
+Notation "''Under[' x ]" := (@Under_rel _ _ _ 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.
+End UNDER_REL.
+
+Module Export Under_rel : UNDER_REL.
+Definition Under_rel (A : Type) (eqA : relation A) (_ : Reflexive eqA) :=
+  eqA.
+Lemma Under_rel_from_rel :
+  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A),
+    @Under_rel A eqA EeqA x y -> eqA 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.
+Definition Over_rel := Under_rel.
+Lemma over_rel :
+  forall (A : Type) (eqA : relation A) (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_iff_done :
-  forall (x : Prop), @Over_iff x x.
+Lemma over_rel_done :
+  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A),
+    @Over_rel A eqA EeqA x x.
 Proof. by []. Qed.
-Lemma under_iff_done :
-  forall (x : Prop), @Under_iff x x.
+Lemma under_rel_done :
+  forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A),
+    @Under_rel A eqA EeqA x x.
 Proof. by []. Qed.
-End Under_iff.
+End Under_rel.
 
-Register Under_iff as plugins.ssreflect.Under_iff.
-Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff.
+Register Under_rel.Under_rel as plugins.ssreflect.Under_rel.
+Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel.
 
-Definition over := (over_eq, over_iff).
+Definition over := (over_eq, over_rel).
 
 Ltac over :=
   by [ apply: Under_eq.under_eq_done
-     | apply: Under_iff.under_iff_done
+     | apply: Under_rel.under_rel_done
      | rewrite over
      ].
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index cca94c8c9b..f67051eeb7 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -10,6 +10,7 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+open Ltac_plugin
 open Pp
 open Names
 open Constr
@@ -349,16 +350,25 @@ let intro_lock ipats =
         let env = Proofview.Goal.env gl in
         match EConstr.kind_of_type sigma c with
         | Term.AtomicType(hd, args) when
-            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 (Array.last args) &&
+            Ssrequality.ssr_is_setoid 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, refl =
+                  (* could raise Not_found in theory *)
+                  Rewrite.get_reflexive_proof env sigma carrier rel 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; refl|] 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|]))
         | _ ->
         let t = Reductionops.whd_all env sigma c in
         match EConstr.kind_of_type sigma t with
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index f285ad138b..b1349f287a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -228,7 +228,27 @@ Qed.
 Arguments ex_iff [R P1] P2 iffP12.
 
 Require Import Setoid.
+
 Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
 under ex_iff => n.
 by rewrite over.
-Abort.
+by move=> _.
+Qed.
+
+
+Section TestGeneric.
+Context {A B : Type} {R : nat -> relation B} `{!forall n : nat, Equivalence (R n)}.
+Variables (F : (A -> A -> B) -> B).
+Hypothesis ex_gen : forall (n : nat) (P1 P2 : A -> A -> B),
+  (forall x y : A, R n (P1 x y) (P2 x y)) -> (R n (F P1) (F P2)).
+Arguments ex_gen [n P1] P2 relP12.
+Lemma test_ex_gen (P1 P2 : A -> A -> B) (n : nat) :
+  (forall x y : A, P2 x y = P2 y x) ->
+  R n (F P1) (F P2) /\ True -> True.
+Proof.
+move=> P2C.
+under [X in R _ _ X]ex_gen => a b.
+  by rewrite P2C over.
+by move => _.
+Qed.
+End TestGeneric.