The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Thanks.  I actually thought about using "vm_compute."  The problem is that I have many goals that look like the following:

    ?86 = simplify (...)

"simplify" is a fixpoint that does some sort of simplification on a complex term such as a program AST.  What I would like to do is evaluate the rhs term and then instantiate the variable ?86 with the result.  The problem is that "vm_compute" does not work with existentials.  Is there a trick for working around this issue?

                         - Ken

> From: thomas.braibant AT gmail.com
> Date: Mon, 22 Apr 2013 21:14:43 +0200
> To: kendroe AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Slow QED
>
> I have run into this issue: some information that corresponds to
> unfold/compute seems to be lost in the generated proof term, and this
> causes trouble when type-checking the proof term at Qed. I think you
> should give vm_compute a try because it will generate more appropriate
> casts in the proof terms (or, if you want to use vm_compute with evars
> and avoid reducing some constants, you could use my evm_compute plugin
> https://github.com/braibant/evm_compute)
>
> Below is a small example where the proof takes a few seconds, and the
> proof term takes more than a hundred seconds to type check.
>
> Require Import ZArith.
>
> Section fold.
> Variable A : Type.
> Variable f : Z -> A -> A.
> Fixpoint fold n acc:= match n with
> | 0 => acc
> | S k => fold k (f (Z.of_nat k) acc)
> end.
> End fold.
>
>
> Open Scope Z_scope.
>
> Definition divide x y :=
> Z.modulo x y =? 0 .
>
> Definition try n z acc :=
> match acc with
> | None =>
> if z <? 2 then
> None
> else if divide n z then
> Some (z,Z.div n z)
> else None
> | Some x => acc
> end.
>
>
> Definition factor n :=
> match fold _ (try (Z.of_nat n)) n None with
> | Some x => x
> | None => (Z.of_nat n,1)
> end.
>
> Remark factorisable : forall x:nat, (let (a,b) := factor x in (a *
> b)%Z) = Z.of_nat x.
> Admitted.
>
> Definition k : nat := 1111%nat. Definition ka := 101. Definition kb := 11.
>
> Require Import String.
>
> Check ("cbv without witnesses")%string.
> Goal exists e1 e2, Z.of_nat k = e1 * e2.
> intros. eexists. eexists.
> rewrite <- factorisable.
> set (f :=Z.mul).
> Time cbv - [f]; unfold f; reflexivity. (* 4 s *)
> Time Qed. (* 154 s !!! *)
>
>
> Thomas
>
>
> On Mon, Apr 22, 2013 at 8:50 PM, Kenneth Roe <kendroe AT hotmail.com> wrote:
> > I have a proof of about 100 lines. The proof itself takes a few minutes to
> > process in Coq. However, it seems to hang on processing the QED at the end.
> > I waited several hours and it had not completed. The proof involves
> > frequent uses of "compute" to cause some fairly complex function evaluation.
> > Has anyone run into this problem? I can email code to anyone who is
> > interested in looking into the issue.
> >
> > - Ken