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 way to achieve this is:
Apply f_equal f:=(g b z).

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

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

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 ?

After written the draft of the above message, I searched the mailing list and found that Pierre Courtieu has discussed the similar problem in his message
Re: [Coq-Club] Rewriting terms in the conclusion.
12 Dec 2002

He has defined a tactic Decompeq
to deal with the problem. Actually, I wrote a similar tactic too.
The problem is that both tactics failed for functions with three
arguments like the above one, but they succeeded on functions with one or two arguments.

Gang Chen