The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

I sometimes do this (which is probably similar to what Matthieu meant):

Definition foo(n: nat): nat := n + 3.

Goal forall x, foo x + 978 <> foo x.
  intros.
  match goal with
  | |- context[?p] =>
    match p with
    | ?x + 978 =>
      let p' := eval unfold foo in p in
      change p with p'
    end
  end.

On Fri, 2018-09-28 at 21:58 -0400, Matthieu Sozeau wrote:

Hi Abishek, ssreflect’s rewrite supports contextual patterns and unfolding with “/“. Maybe with `pattern` and `eval unfold in` and `change` you could program this in Ltac as well.

Best,
— Matthieu

Le ven. 28 sept. 2018 à 15:14, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

Many times, we wish to unfold only certain occurrences of a definition.

The unfold tactic takes the occurrence number as an integer.

However, using an integer to refer to occurrence seems less robust and the integer provides less useful information when proofs break.

Is there a way to more structurally specify where to unfold?

For example, is there a way to specify where to unfold as follows:

match goal with

[|-  context[?x+978]] => unfold foo in ?x

end

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/