The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

Kenneth,

Defining z as (fact 10) does not actually evaluates (fact 10). If you want to 
define z as the value of (fact 10), not the expression itself. You could do 
this:

Definition z := Eval simpl in fact 10.

Or you could just print the value by running:

Eval simpl in fact 10.

Of couse, there is an alternative definition that is observationally equal to 
your "fact" function and run faster by caching the immediate previous value.

-- Duckki


On Friday, April 5, 2013 at 10:21 AM, Kenneth Roe wrote:

> 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