autorewrite should not exploit hypothesis H while rewriting hypothesis H

[fpottier]

Is your feature request related to a problem?

Hi! My feature request is as follows: when autorewrite applies a rewrite rule inside a hypothesis H, if this rewrite rule has side conditions (subgoals), then the hypothesis H should be cleared while attempting to prove these subgoals. In the absence of this protection, autorewrite can destroy information. Here are two examples:

From Stdlib Require Import Lia ZArith ZArithRing.
Open Scope Z_scope.

(* There is an interesting problem with [Z.max_r] and friends.
   Although these rewriting rules are very useful, they can
   cause a phenomenon where rewriting destroys information.

   Here is an example. The following lemma is true: *)

Goal forall a, Z.max a 0 = 0 <-> a <= 0.
Proof. lia. Qed.

(* Yet, unfortunately, rewriting with [Z.max_r] can transform
   a valid goal into an unsatisfiable goal: *)

Goal forall a, Z.max a 0 = 0 -> a <= 0.
Proof.
  intros. rewrite Z.max_r in H by lia.
  (* We are dead! The problem is that the information contained in the
     equation [a `max` 0 = 0] is used to simplify this equation itself
     into [0 = 0], thereby destroying this information. *)
Restart.
  (* A defense is to clear [H] while proving the premise: *)
  intros. Fail rewrite Z.max_r in H by (clear H; lia).
Abort.

(* Unfortunately [autorewrite] does not offer such a defense.

   Such a defense would work as follows: when [autorewrite] applies a
   rewrite rule inside a hypothesis H, if this rewrite rule has side
   conditions (subgoals), then H should be cleared while attempting to
   prove these subgoals. *)

(* A similar issue arises with other rewrite rules, such as
   [sub_diag']. *)

Lemma sub_diag' x y : x = y -> x - y = 0.
Proof. lia. Qed.

Goal forall x y, x - y = 0 -> x = y.
Proof.
  (* This goal is true. *)
  lia.
Restart.
  (* Yet rewriting with [sub_diag'] makes it unsatisfiable: *)
  intros. rewrite sub_diag' in H by lia.
  (* We are dead! *)
Abort.

This is not an artificial example! Rewriting with a database that contains Z.max_r (and many other rules) can be very useful in practice.

Proposed solution

No response

Alternative solutions

No response

Additional context

No response

[fpottier]

Come to think of it, a similar request concerns rewrite ... in * by foo. When this tactic wants to rewrite inside a hypothesis H, it could (should) clear H before calling foo to prove the subgoals.