Thinking of using hammer/automation to guide the order of proving lemmas

Using Coq
1

I’m thinking of ways in which I could use proof automation (currently I’ve tried coq-hammer) in a wider way than merely to help me prove a lemma and then move to a next one. I have a few thoughts here, but especially since I’m rather new to Coq, I’d like to hear if you think my thoughts make any sense.

Background: I’ve been working on an implementation of integer log3 and log3_up (that is, ceiling of base-3 logarithm) since I need those for a proof I’m working on. There’s a large bunch of lemmas to prove, and I think it might be possible to reduce the work by using hammer more cleverly. Many of those I could just adapt from the already proven log2 lemmas, but this is also a Coq-learning exercise for me, so I’ve done that only occasionally.

I’ve been going through the log2 lemmas picking the ones which I believe have a corresponding log3 property.

Rather obviously, there are good orders and bad orders in which to prove lemmas; many simple lemmas are useful for more complex ones. So, essentially starting from the propositions modified from log2 lemmas, I have a large number of candidate lemmas to prove and want to come up with an efficient order to do so.

I think of two possible and probably complementary strategies here:

  1. For each candidate lemma not yet proven, try to prove it using hammer, with all of the lemmas proven so far in the context. Stop when no candidate lemma can be proven within a time limit. Conversely, do sanity checks by trying to prove the falsity of each unproven candidate lemma.

This is essentially “free”; it only takes CPU time, no human effort once set up.

  1. Try to answer the question of how useful a proof of a candidate lemma would be for the total effort by admitting that lemma as an axiom and checking how many other candidates can be proven automatically with the help of it.

Do these ideas make at all sense to you? If so, I could try to hack together some kind of a prototype implementation (I’m a software developer/theoretical computer scientist/data scientist with a passing familiarity with ocaml, much more familiarity of other programming languages, but little knowledge of Coq internals).