The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Gregory, Matthieu,

 

indeed it's

pretty bad to have an axiom be part of the initial auto with *

database.

 

another bad thing about the standard library hint databases is that they contain quite a few lemmas and lemma combinations which can loop indefinitely, like symmetry or transitivity laws or both directions of a P<->Q lemma. This results in bad proof search performance in many - maybe almost all except trivial - cases. After removing 20 or so looping lemmas, I stopped using the standard library hint databases. With a non-looping hint databases it is quite efficient to use eauto with search depth of 100. With the standard library hint databases a search depth of 10 can easily take a very long time.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928