Suppose I have a goal `foo x -> ?Goal{x:=x}`

and I do `replace x with y`

. This gives `foo y -> ?Goal{x:=y}`

. Unfortunately, at this point, the goal is broken and no longer provable. What I really wanted to obtain was `foo y -> ?Goal{x:=x}`

. Obviously, I could solve the issue by using `pattern x at 1; replace x with y`

. But I am in a context where `replace`

is actually an arbitrary user-provided tactic, so `pattern`

is not a solution. Is there some way to protect `?Goal`

from any unfortunate side-effect?

If remember or set aren't enough, I've seen coq-ext-lib's hiding tactic to do sort-of (reversible) sealing on the spot. Of course that's not literally safe for arbitrary user-defined tactics, just for everything that doesn't unseal.

Guessing the evar instead of spelling it out requires some ltac, matching subterms and using is_evar...

Regarding ext-lib:

```
From Coq Require Import Utf8.
Require Import ExtLib.Tactics.Hide.
Axiom foo : nat -> nat -> Prop.
Goal ∀ x y, x = 1 -> ∃ (P : Prop), foo x y -> P.
Proof.
intros x y Heq. eexists ?[P].
subst.
remember ?P@{x:=1} eqn:H.
hide_hyp H.
replace y with 1. (* Does not affect evar. *)
```

but `hide_hyp H.`

is just `apply hidden in H`

with `Inductive Hidden (P : Type) : Prop := hidden : P → Hidden P`

, so it's not hard to reverse.

Last updated: Jun 18 2024 at 21:01 UTC