[Coq-Club] folding under binders

[Abhishek Anand]

Is there a convenient way to fold a definition under binders?
(I can do a `change` of the whole term, but that is problematic when
dealing with large terms)

Consider the following example:

Definition add2 n := n +2.
Goal (fun n => n) = (fun n => n+2).

Is there a general advanced fold tactic such that `advanced_fold add2`
changes "n+2" to "add2 n"?

[Clément Pit-Claudel]

Is there a general advanced fold tactic such that `advanced_fold add2` changes "n+2" to "add2 n"?

I usually use [change (?n + 2) with (add2 n)]. It works in Coq 8.4, but unfortunately not in 8.8, apparently. I don't know when it stopped working.

Another similar example from a few months ago still works:

Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
intro.
repeat change (?a -> False) with (not a) in H.

Clément.

[Hugo Herbelin]

Hi Clément,

Thanks a lot for noticing the regression. I made a pull request on
github.com/coq/coq (PR #8553) which fixes it.

Best,

Hugo

Post by Clément Pit-Claudel

Is there a general advanced fold tactic such that `advanced_fold add2` changes "n+2" to "add2 n"?

I usually use [change (?n + 2) with (add2 n)]. It works in Coq 8.4, but unfortunately not in 8.8, apparently. I don't know when it stopped working.
Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
intro.
repeat change (?a -> False) with (not a) in H.
Clément.