The Coq mailing list

["Hao-yang Wang" <hywang AT pobox.com>]

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.

(By the way, this example comes from the textbook "Isabelle/HOL" by Nipkow,
Paulson, and Wenzel, Section 3.5.4. Earlier in Section 3.4.4, I discovered
that a two-line proof in Isabelle/HOL could become a full-page essay in coq,
while in Section 3.5.2, I discovered that the proof of termination can be
done very elegantly in coq, if I let the "refine" tactic to fill in the
blanks. :-)

Cheers,
Hao-yang Wang