The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr> (by way of Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>)]

GANGCHEN5 AT aol.com
 wrote:
> In a message dated 7/31/2003 4:30:05 AM Eastern Daylight Time, 
> Pierre.Courtieu AT sophia.inria.fr
>  writes:
> 
> > Can you show the tatic you wrote? Decompeq seems to be what you need.
> 
> Decompeq is what I need. But it does not work for my example. Maybe there 
> is 
> a bug in coq. Here is a complete example:
> 
> Variable A : Set.
> Variable x,y,z : A.
> Variable g : A->A.
> Variable g2 : A->A->A.
> Variable B : Set.
> Set Implicit Arguments.
> Variable g3 : (A:Set)B->A->A->A.
> Implicits g3.
> ...

> Lemma F_equal_test : x=y->(g3 b z x)=(g3 b z y).
> Intro.
> Decompeq.
> (* Failed : 

g3 takes 4 arguments! It works with Decompeq, it should also work with
your tactic if you add cases to it.

> My tactic is as follows, it failed in the last example too.
> Tactic Definition F_equal :=
>  Match Context With 
>     [  |- (?1 ?2) = (?1 ?3) ] -> 
>       Apply f_equal with f:=?1
> 
>   | [  |- (?1 ?2 ?4) = (?1 ?2 ?5) ] -> 
>       Apply f_equal with f:=(?1 ?2)
>   | [  |- (?1 ?2 ?4) = (?1 ?3 ?4) ] -> 
>       Apply f_equal with f:=[z](?1 z ?4)
> 
>   | [  |- (?1 ?2 ?3 ?6) = (?1 ?2 ?3 ?7) ] -> 
>       Apply f_equal with f:=[zz](?1 ?2 ?3 zz)
>   | [  |- (?1 ?2 ?6 ?3 ) = (?1 ?2 ?7 ?3 ) ] -> 
>       Apply f_equal with f:=[z](?1 ?2 z ?3)
>   | [  |- (?1 ?6 ?2 ?3 ) = (?1 ?7 ?2 ?3) ] -> 
>       Apply f_equal with f:=[z](?1 ?2 ?3 z).

add one more group with (?1 ?2 ?3 ?6 ?8)