The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

After reading the Chlipala paper, I think I am pretty close to a solution for "simpl".  I would like to replace it with "vm_compute".  However, I usually end up with goals of the form "?25 = expr" where "expr" is the thing I want to simplify.  Consider the following contrived piece of code:

Definition funnyProp n x := (x=n+1).

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

Theorem propagate : forall z n n',
    n = n' ->
    funnyProp n z ->
    funnyProp n' z.
Proof. admit. Qed.

Theorem q: forall z,
    funnyProp (fact 7) z ->
    funnyProp (fact 7) z.
Proof.
    intros. eapply propagate.

The proof could be completed with " simpl. reflexivity. simpl in H. apply H. Qed."  However, I would like to replace the first "simpl" with "vm_compute" for performance.  Is there a way to chop out the rhs of the equality and just apply vm_compute there?

                             - Ken

> Date: Fri, 5 Apr 2013 10:35:00 -0400
> From: duckki AT mit.edu
> To: kendroe AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Performance of simpl
>
> 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
>
>