The Coq mailing list

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

Hi,

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.

Thanks!


Guillaume Brunerie