The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 22 Apr 2013 12:56:59 -0700,
Kenneth Roe 
<kendroe AT hotmail.com>
 a écrit :

> 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?

Wouldn't "reflexivity" (or split/esplit) work for that?
Why do you want to evaluate the rhs in this condition?

> 
>                          - 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
>