The Coq mailing list

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

Dear Jim,

 

Logs meaning the console output from Set Debug Auto/Set Debug Eauto?  By the branching factor, you just mean paying attention to the output (e.g. 1.2.3.1 is depth 4) and each digit counts the branches at it's level?

 

Yes, I do regular profiling runs with coqc running on the command line and output redirected to a file. I tend to generate statistics over the number of applictions/tactics tried vs. the final proof depth (I can provide a python script for this, if you are interested). Usually I can manage to keep this between 2 and 3 on average by proper hint database engineering, so that overall I have linear search time. This means the branching factor is in most cases one and only in some cases a small number. To make the log analysis easier I have in my eauto wrappers also a tactic which first prints the current goal.

 

How helpful would it be if auto/eauto detected and avoided looping?  Either by a) detecting that the proof state has already been seen in the current search (e.g. there is a tactic for a commutative property) and/or b) using a queue that ranks various proof states by a size metric and processing the smaller proof states first.  This might give better performance and allow for a higher depth limit.

 

I think you would in many cases still have exponential search time, because it usually takes 2..3 steps for a loop. So you would detect the loop only after 3 steps and it is not unlikely that in each step of the loop you can also do something else. But yes, it would be helpful to hash the proof state and detect that you have been here before for complicated cases. I have some tactics which do this manually to a certain extent (record the set of seen goals in a proof state variable). But I would first try to eliminate the loop by managing my hint databases and especially proper gating tactics and resort to hashing only in cases where it gets complicated otherwise.

 

I think what would really help is to build up some pattern matching based database which learns by “trial and error eauto proofs” which things make sense in which context. Best would likely be to couple eauto with a neural network. I have some idea on how to approach this, but didn’t have time to try it as yet. It might also be that something in the back of my mind is slightly scared about this. But I have some of our (Intel) neuromorphic chips in my drawer …

 

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