The Coq mailing list

[GANGCHEN5 AT aol.com]

Hello,

I have a goal (g b z x)=(g b z y) and I want to derive a subgoal

x = y

One can use the tactic to achieve this:
Apply f_equal f:=(g3 b z).

But I want to find a more automatic way to do this kind of job, so I define a
tactic:

Definition Tactics F_equal =
Match Context With
   [  |- (?1 ?2 ?3 ?4) = (?1 ?2 ?3 ?5) ] ->
        Apply f_equal with f := [u](g3 b z u).

When I use this tactic, the system replies:

Error: No matching clauses for Match Context

What's wrong with this ?

In general, when the goal is  F[e1] = F[e2} where F is an
_expression_ with a hole, we would like to derive a subgoal e1 = e2.
What is the best way to do this ?

Thank you.

Gang Chen