The Coq mailing list

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

Dear Théo, Armaël,

 

yes, I sticked with the current Ltac implementation waiting for Ltac-2. As I said, it is kind of a dirty hack and also looks a bit ugly in the code, but it works and for the time being I can live with it.

 

But let me put some more words on the search strategy I use – and for which I think it makes sense to have some sort of native support in Coq.

 

The reasoning behind splitting proof search in forward (hypothesis based) and backward (goal based) search is as follows:

 

1.) Assume that the total search depth is N and you have an average branching factor (number of possibilities tried at each step) of B. If you do just forward or backward search, you need B^N apply tries. If you do half of the steps forward and half of the steps backwards, the number of things to try is just 2*B^(N/2), which is 2x the square root of the former.

 

An example: it is quite feasible (not really efficient but doable) to solve a Rubic’s cube by brute force search from both ends. Usually it can be solved in 14 steps where each steps has 27 possibilities (3 rotation axes x 3 slices x 3 possible angles). If you search from one end (from where you are towards the goal or from the goal to where you are), there are 27^14 steps, which is 10^20. If you search from both ends, there 2x27^7 steps which is 2*10^10. But in practice point 2 below gives a much better improvement, and both can be combined.

 

2.) For most lemmas the branching factor B is different for forward and backward search. If you have some lemmas with very specific conclusion, but very generic hypothesis, the backward branching factor might be 1 (only one lemma applies to any given goal) while the forward branching factor would be much larger (many lemmas can be instantiated in the given context, but the conclusions are useless). For lemmas with very specific hypothesis but very general goal, the opposite is true. So you end up with BF^NF + BB^NB as number of applies. Here BF and BB are the forward and backward branching factors, which are both much smaller than B.  NF and NB are the forward and backward depth, which add up to N. BF^NF + BB^NB is usually orders of magnitude smaller than B^N, especially if lemmas are upfront designed such that they have a very small forward or backward branching factor. I sometimes use additional gating to ensure this. It is definitely much easier to get a lemma working efficiently in a hint database in one or the other direction than it is when one sticks to one search direction only. I use tracing and scripts to ensure that hint databases are well designed and lead on average to branching factors close to 1.

 

3.) Some lemmas don’t work at all in backward mode, e.g. if you can prove an equality from hypothesis using forward search and simplify the goal with a substitution, there is no way to see that this would be possible with backward search.

 

What would help for this strategy is native support for forward search and some hint database management/analysis tools, which give some estimates on branch factors or warn about cyclic applicability of lemmas.

 

Best regards,

 

Michael

 

Michael Soegtrop

 

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