Stream: Coq users

Topic: Protecting goal evars

view this post on Zulip Guillaume Melquiond (Jan 28 2022 at 15:57):

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?

view this post on Zulip Paolo Giarrusso (Jan 28 2022 at 22:24):

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.

view this post on Zulip Paolo Giarrusso (Jan 28 2022 at 22:26):

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

view this post on Zulip Paolo Giarrusso (Jan 29 2022 at 03:20):

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. *)

view this post on Zulip Paolo Giarrusso (Jan 29 2022 at 03:21):

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: Oct 13 2024 at 01:02 UTC