The Coq mailing list

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

Dear Wilayat,

 

I can only agree with Pierre. The point is not to do destructs as fast as possible, the point is to do as few goals / proof steps as possible. Many simple proof search strategies need time growing expeonentially with some size, like number of variables in your case. It is much more important to not let this exponential growth happen by smarter proof search strategies than to make the individual steps faster.

 

Btw.: there is a tactic to solve Boolean tautologies called btauto. It only works for the built in bools (as far as I can tell). It would be interesting how it performs compared to destructing in your example cases (although I think the strength of btauto comes if there are quantifiers).

 

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