Stop automatically using assumption in replace

Close #17959

doc/sphinx/proofs/writing-proofs/equality.rst

@@ -248,8 +248,6 @@ Rewriting with Leibniz and setoid equality
    as a subgoal. (Note the generated equality is reversed with respect
    to the order of the two terms in the tactic syntax; see
    issue `#13480 <https://github.com/coq/coq/issues/13480>`_.)
-   This equality is automatically solved if it occurs among
-   the hypotheses, or if its symmetric form occurs.
 
    The second form, with `->` or no arrow, replaces :n:`@one_term__from`
    with :n:`@term__to` using
@@ -267,6 +265,14 @@ Rewriting with Leibniz and setoid equality
    .. exn:: Terms do not have convertible types.
       :undocumented:
 
+   .. flag:: Replace Use Assumption
+
+      This deprecated flag is off by default. Turning it on makes
+      :tacn:`replace` automatically solve the generated equality if it
+      or its symmetric form occur among the hypotheses. When :n:`by
+      @ltac_expr3` is provided the automatic assumption search is
+      tried before the :n:`@ltac_expr3`.
+
    .. tacn:: cutrewrite {? {| -> | <- } } @one_type {? in @ident }
 
       Where :n:`@one_type` is an equality.

tactics/equality.ml

@@ -619,6 +619,12 @@ let replace_core clause l2r eq =
    tac : Used to prove the equality c1 = c2
    gl : goal *)
 
+let since_8_19 = Deprecation.make ~since:"8.19" ()
+
+let {Goptions.get = replace_use_assum} =
+  Goptions.declare_bool_option_and_ref ~depr:since_8_19 ~key:["Replace";"Use";"Assumption"]
+    ~value:false ()
+
 let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let try_prove_eq =
     match try_prove_eq_opt with
@@ -648,13 +654,18 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     Tacticals.pf_constr_of_global sym >>= fun sym ->
     Tacticals.pf_constr_of_global e >>= fun e ->
     let eq = applist (e, [t1;c1;c2]) in
+    let solve_tac =
+      if replace_use_assum () then
+      tclFIRST
+        [assumption;
+         tclTHEN (apply sym) assumption;
+         try_prove_eq
+        ]
+      else try_prove_eq
+    in
     tclTHENLAST
       (replace_core clause l2r eq)
-      (tclFIRST
-         [assumption;
-          tclTHEN (apply sym) assumption;
-          try_prove_eq
-         ])
+      solve_tac
   end
 
 let replace c1 c2 =

theories/Compat/Coq818.v

@@ -11,3 +11,5 @@
 (** Compatibility file for making Coq act similar to Coq v8.18 *)
 
 Require Export Coq.Compat.Coq819.
+
+#[export] Set Replace Use Assumption.

theories/Reals/RiemannInt_SF.v

@@ -676,7 +676,7 @@ Proof.
         (Int_SF lf1 (cons r1 r2) = Int_SF (cons r3 lf2) (cons r1 (cons s2 s3)))
     ; apply H0 with r1 b.
     { unfold adapted_couple in H2; decompose [and] H2; clear H2;
-        replace b with (Rmax a b);
+        replace b with (Rmax a b) by assumption;
       rewrite <- H12; apply RList_P7;
         [ assumption | simpl; right; left; reflexivity ]. }
     { eapply StepFun_P7.
@@ -730,7 +730,7 @@ Proof.
   rewrite H9; rewrite H10; rewrite H6; apply Rplus_eq_compat_l; rewrite <- H10;
     apply H0 with r1 b.
   { unfold adapted_couple in H2; decompose [and] H2; clear H2;
-    replace b with (Rmax a b).
+    replace b with (Rmax a b) by assumption.
     rewrite <- H12; apply RList_P7;
     [ assumption | simpl; right; left; reflexivity ]. }
   { eapply StepFun_P7.
@@ -1525,7 +1525,8 @@ Proof.
   2:discrR.
   rewrite Rmult_1_l; rewrite <-Rplus_diag; assert (H5 : r0 <= b).
   { replace b with
-      (pos_Rl (cons r (cons r0 r1)) (pred (length (cons r (cons r0 r1))))).
+      (pos_Rl (cons r (cons r0 r1)) (pred (length (cons r (cons r0 r1)))))
+    by assumption.
     replace r0 with (pos_Rl (cons r (cons r0 r1)) 1).
     { elim (RList_P6 (cons r (cons r0 r1))); intros; apply H5.
       { assumption. }

vernac/auto_ind_decl.ml

@@ -867,6 +867,20 @@ let destruct_ind env sigma c =
 let bl_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 
+let sym_assumption =
+  let open Proofview in
+  let open Proofview.Notations in
+  tclUNIT () >>= fun () ->
+  let sym = try Coqlib.lib_ref "core.eq.sym"
+    with Coqlib.NotFoundRef _ ->
+    try Coqlib.lib_ref "core.identity.sym"
+    with Coqlib.NotFoundRef _ ->
+      CErrors.user_err
+        Pp.(str "Scheme Equality needs core.eq.sym or core.identity.sym to be registered.")
+  in
+  Tacticals.pf_constr_of_global sym >>= fun sym ->
+  Tactics.apply sym <*> Tactics.assumption
+
 (*
   In the following, avoid is the list of names to avoid.
   If the args of the Inductive type are A1 ... An
@@ -920,7 +934,7 @@ let do_replace_lb handle aavoid narg p q =
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
            in
            Tacticals.tclTHENLIST [
-             Equality.replace p q ; Tactics.apply app ; Auto.default_auto]
+             Equality.replace_by p q sym_assumption; Tactics.apply app ; Auto.default_auto]
   end
 
 (* used in the bool -> leb side *)