[Coq-Club] structural specification of where to unfold

[Abhishek Anand]

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/

[Matthieu Sozeau]

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

Post by Abhishek Anand
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?
match goal with
[|- context[?x+978]] => unfold foo in ?x
end
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Enrico Tassi]

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.

For reference: https://hal.inria.fr/hal-00652286v2

Best

[Samuel Gruetter]

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 <***@gmail.com<mailto:***@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/