The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 06 mai 2005, Hao-yang Wang wrote:

> With the following function:
> 
> Fixpoint sep (A:Set) (f:A->A) (a:A) (z:list A) {struct z}: list A :=
>      match z with
>      | nil => nil
>      | x::nil => x::nil
>      | x::(y::zs) as z1 => x::a::sep A f a z1
>      end.
> 
> The tactic "functional induction sep A f x xs" works nicely in proving
> the following theorem:
> 
>     Theorem map_sep: forall A f x xs,
>         map f (sep A f x xs) = sep A f (f x) (map f xs).
> 
> However, if I remove the parameter "f" from the above definition of sep,
> functional induction would emit a typing error.

This is due to a limitation of the tactic: variable put in argument of
functional induction are duplicated (as with the induction tactic).
Therefore A is duplicated into A0, and (f x) has not the right type. You
need to let f inside the goal (do not intro it) when you do functional
induction:

Theorem map_sep: forall A x xs f, map f (sep A x xs) = sep A (f x) (map f xs).
  intros A x xs. (* let f in the goal *)
  functional induction sep A x xs.


Cheers,

Pierre Courtieu