The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

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