The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Thanks everyone.  It looks like "compute. reflexivity." in place of "simpl. reflexivity." produces the intended result.

           - Ken

---

From: aspiwack AT lix.polytechnique.fr
Date: Sat, 6 Apr 2013 01:04:12 +0200
To: kendroe AT hotmail.com
CC: gmalecha AT eecs.harvard.edu; coq-club AT inria.fr
Subject: Re: [Coq-Club] Performance of simpl

compute is much faster than simpl on this example, and it supports existential variable, contrary to vm_compute. In trunk, there is also cbn which has a similar semantics as simpl and is also much faster here. simpl probably spends a lot of time in his refolding strategy.

On 6 April 2013 00:51, Kenneth Roe <kendroe AT hotmail.com> wrote:

First, if you noticed, I used (fact 7) in the second example, not (fact 10) which is still large but doable in Coq.  As an interesting exercise, add on "instantiate (1 := (fact 7)). smpl."  instead of "simpl. reflexivity." at the end of that example. Compare the time for this to compute to "instantiate (1 := (fact 7)). vm_compute."

Simply add "reflexivity." rather than "simpl. reflexivity." causes the existential variable to be instantiated with (fact 7).  My goal is to get the existential instantiated with the fully beta reduced evaluation which in this case is 5040.

                 - Ken

---

From: gmalecha AT eecs.harvard.edu
Date: Fri, 5 Apr 2013 17:46:49 -0400
To: s9joober AT gmail.com
CC: kendroe AT hotmail.com; coq-club AT inria.fr

Subject: Re: [Coq-Club] Performance of simpl

Hi, Ken --

I agree with Jonas. For this problem, the result is simply too large. If this is the actual goal that you are trying to solve and not just a representative example, then Jonas's solution is probably what you want.

If this is just an example indicative of a larger problem then perhaps you can provide some more information about the real problem. In a recent paper we've come up with some excellent ways to get around problems with unification variables for reflective proofs and it is possible that some of them can be applied to your setting.

On Fri, Apr 5, 2013 at 4:14 PM, Jonas Oberhauser <s9joober AT gmail.com> wrote:

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

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/