The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Consider the following Coq declarations:

    Fixpoint fact (x : nat) := match x with
                               | 0 => 1
                               | (S y) => (S y) * (fact y)
                               end.

    Definition z := fact 10.

    Theorem q: (fact 10)=10*(fact 9).
    Proof.
        simpl.

The definition of "z" happens very quickly.  However, the "simpl" at the very end takes a long time.  And in fact generates a "Stack overflow" error.  However, the only meaningful operation of simpl is to do an evaluation of the "fact" function.  Is there an alternative to using "simpl" that is faster?  What else can I do to speed up performance?

          - Ken