The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 05.04.2013 16:21, schrieb Kenneth Roe:

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

The main problem is, as Mr. Chlipala mentioned, hat 10! is just a very large number.

I believe, however, that you don't actually need to fully beta-reduce the term in question.
Probably unfold does what you want:


Goal fact 10 = 10 * fact 9.
unfold fact. reflexivity. Qed.

Jonas