The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

2011/12/16 Adam Chlipala <adamc AT csail.mit.edu>

Guillaume Brunerie wrote:

I want to write a tactic that should match the goal against something of the form [P (x + y)] where [P], [x] and [y] are arbitrary and [P] is bound to a function.
For example if the goal is something like [2 * (1 + 1) = 4] it should succeed and bind [x] and [y] to [1] and [P] to [fun t : nat => 2 * t = 4].

Is this possible?

I tried with second order pattern matching (@?P) but it does not work (I think this is because second order pattern matching only accepts variables as arguments), and I tried with [context], but I haven't found a way to build a function out of the context I get.

If you use [context] to find the subexpression you want to abstract, you can then run [pattern] on that subexpression, which will put the conclusion into precisely the form you want.

This seems to solve my problem, thanks :-)