[ssr] Refactor/Simplify the implementation of under

* Preserve the same behavior/interface but merge the two Module Types
  (UNDER_EQ and) UNDER_REL.
* Remove the "Reflexive" argument in Under_rel.Under_rel
* Update plugin code (ssrfwd.ml) & Factor-out the main step
* Update the Hint (viz. apply over_rel_done => apply: over_rel_done)
* All the tests still pass!

Credits to @CohenCyril for suggesting this enhancement

3 files changed, 44 insertions, 110 deletions

diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v
index ed9ae0ce17..29486ff4cf 100644
--- a/plugins/ssr/ssrclasses.v
+++ b/plugins/ssr/ssrclasses.v
@@ -25,4 +25,5 @@ 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 c98d872a9c..a19aade6e9 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -533,111 +533,61 @@ Proof. by move=> /(_ P); apply. Qed.
 (*****************************************************************************)
 (* Constants for under/over, to rewrite under binders using "context 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.
-Parameter Under_eqE :
-  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.
-Lemma Under_eqE (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.Under_eq as plugins.ssreflect.Under_eq.
-Register Under_eq.Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq.
-
 Require Import ssrclasses.
 
 Module Type UNDER_REL.
 Parameter Under_rel :
-  forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop.
+  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
 Parameter Under_rel_from_rel :
-  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A),
-    @Under_rel A eqA EeqA x y -> eqA x y.
+  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) (EeqA : Reflexive eqA) (x y : A),
-    @Under_rel A eqA EeqA x y = eqA x y.
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y = eqA x y.
 
 (** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *)
 Parameter Over_rel :
-  forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop.
+  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
 Parameter over_rel :
-  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.
+  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 EeqA x x.
-Hint Extern 0 (@Over_rel _ _ _ _ _) => solve [ apply over_rel_done ] : core.
+    @Over_rel A eqA 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 : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Under_rel A eqA EeqA x x.
-Notation "''Under[' x ]" := (@Under_rel _ _ _ x _)
+    @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) (_ : Reflexive eqA) :=
+Definition Under_rel (A : Type) (eqA : A -> A -> Prop) :=
   eqA.
 Lemma Under_rel_from_rel :
-  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A),
-    @Under_rel A eqA EeqA x y -> eqA x y.
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y -> eqA x y.
 Proof. by []. Qed.
-Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A) :
-  @Under_rel A eqA EeqA x y = eqA x y.
+Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (x y : A) :
+  @Under_rel A eqA x y = eqA x y.
 Proof. by []. Qed.
 Definition Over_rel := Under_rel.
 Lemma over_rel :
-  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.
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y = @Over_rel A eqA x y.
 Proof. by []. Qed.
 Lemma over_rel_done :
   forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Over_rel A eqA EeqA x x.
-Proof. by []. Qed.
+    @Over_rel A eqA x x.
+Proof. by rewrite /Over_rel. Qed.
 Lemma under_rel_done :
   forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Under_rel A eqA EeqA x x.
+    @Under_rel A eqA x x.
 Proof. by []. Qed.
 End Under_rel.
 
@@ -645,18 +595,17 @@ 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_eq, over_rel).
+Definition over := over_rel.
 
 (** Closing tactic *)
 Ltac over :=
-  by [ apply: Under_eq.under_eq_done
-     | apply: Under_rel.under_rel_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_eqE, Under_relE).
+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.
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 485ec667d6..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 ())])
@@ -358,45 +373,14 @@ let intro_lock ipats =
             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 =
-                  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 =
-                  try
-                    Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel
-                  (* could raise Not_found--this can't occur actually:
-                     at that point, either [Ssrequality.ssr_is_setoid]
-                     holds or the relation is [Coq.Init.Logic.iff],
-                     and [Coq.ssr.ssrclasses] was necessarily required
-                     so we know that in the environment, the relation
-                     has an instance of [Coq.ssr.ssrclasses.Reflexive]
-                   *)
-                  with Not_found -> assert false 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|]))
+          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));