The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

(looks like we forgot to cc the list - citations are below)

As Jean-Christophe Filliâtre suggested in a recent post, proof terms 
constructed by a script are  rechecked by the "Save" command. Still it 
seems that "Save" cleverly reuses some of the judgements that have 
already been obtained from the kernel by the script (thus obscuring the 
total checking time), as shown by this example:
  Variable P : nat -> Prop.
  Hypothesis H : P (500*100 - 500*100).

  Lemma P_0 : P 0.
  exact H. (* takes a long time *)
  Save. (* takes little time *)

What time do you want to measure? Proof search, or just checking of 
already constructed proofs?
In the latter case you could display the proof term with the "Print" 
command, then recheck its coercion to the goal:
  Check H : P 0.

Hope this helps.

> Thank you very much, Roland.
> Your trick with inconsistent assumption was helpful.
>
> Unfortunately Time Qed works only for individual proofs.
> It seems that measuring "Load" or compilations time is closer to what 
> I need.
> Ideally, I'd prefer to load compiled script and replay proofs stored 
> there (to exclude parsing and compilation time) but it seems 
> impossible in Coq.
>
>
> Roland Zumkeller wrote:
> > > 1. I have bunch of lemmas with proofs and I want to measure
> > > how much time it will take to check those proofs. May I ask Coq to
> > > measure it or I have to use external tools (like watches on my 
> > > wrist)?
> > Instead of "Qed" use "Time Qed".
> > This will give you the time coq spent checking the proof term 
> > developed by your script (not the execution time of your proof 
> > script).
> > > 2. Again I have a bunch of lemmas with proofs but some of them are 
> > > not
> > > correct (simply because some decision procedure didn't succeed).
> > > CoqIDE stops on such lemma and dos not allow to proceed to the next
> > > statement. May I force Coq to check several proofs and not to stop on
> > > the first failure?
> > Coq is made to assure correctness of proofs, so you need to use some 
> > hack ...
> > You could make an inconsistent assumption
> >   Hypothesis admit : forall A:Type, A.
> > and use it to cheat everytime your decision procedure fails
> >   Lemma l1 : 2=3.
> >   auto ||
> >   apply admit.
> >   Time Qed.
> > Replace "auto" by your decision procedure - if it succeeds, "apply 
> > admit" will not get called. If the procedure fails "apply admit" is 
> > used to cheat and have Coq process the rest of the file.
> > (The command "Admitted" doesn't work here since we would have to know 
> > a priori if the proof worked or no every time).
> > Regards,
> > Roland
> > --
> > http://www.lix.polytechnique.fr/~zumkeller/
>
>
> --
> Best regards,
> Yegor
> __________________________________________________________
> Yegor Bryukhov, PhD student at GC CUNY
> office:       4330
> office phone: +1(212)817-8653
> cell phone:   +1(917)650-2035
> e-mail:       
> ybryukhov AT gc.cuny.edu
>  
> ynb AT mail.ru
> home-page:    http://www.cs.gc.cuny.edu/~yegor/