Stream: Coq users

Topic: Using hypotheses in automation

Patrick Nicodemus (Apr 23 2023 at 17:07):

If you have a proof search tool like auto, it generally only focuses on the goal and works backward from there. Sometimes it seems like forward reasoning is preferable though. For example suppose I have the known theorem ~ n < m -> n >= m and I have a goal where this can be applied, i.e.

H : ~ n < m
--------------
n >= m

I already have the theorem n >= m -> ~n < m in a hint database because this seems like a more convenient way to work with the information.

So what are my options here?

1. Add the hint ~ n < m -> n >= m to the hint database
2. Add a loop which searches through the hypotheses at each stage in proof search for something matching ~ n < m and rewrite it to n >= m

The first one will add lots of wasted time in depth first search.
The second seems better but I am worried about the performance of adding a loop to search over hypotheses all the time.

Patrick Nicodemus (Apr 23 2023 at 17:07):

Maybe I am overly obsessing over performance and it is not a big deal. How do you handle this situation to simplify hypotheses into a convenient form?

Patrick Nicodemus (Apr 23 2023 at 17:09):

I have also considered adding autorewrite with arith_rewrite in * as a (very low priority) hint in auto but this also seems to be not very fast.

Michael Soegtrop (Apr 24 2023 at 07:45):

A few points on this:

• If you have a given lemma the branching factor in applying the lemma forward (doing the "closure" of the hypothesis) and backward is not the same. There are lemmas which have complicated hypothesis and a simple goal (say an equality) and lemmas which have simple hypothesis and complex goals. The first kind has a small branching factor in forward mode and a large branching factor in backward mode - the second kind is the other way around. Of course there are lemmas in between.
• One can specifically design lemmas for forward or backward application (I can look up a few examples in the standard library)
• If you assume a fixed average branching factor B in both directions and have a proof that requires N steps if you approach it from either end you need B^N proof steps. If you approach it from both ends and manage to meet in the middle you have 2*B^(N/2) steps, which is much less if N is large.
• Combining both effects, different branching factor in forward / backward mode and halving the exponent is usually worth even substantial linear effects you have in proof search - but you have to be smart about it.
• It does make sense to do statistics - do branching statistics using auto debug and measuring forwarding effort.
• Try to get the branching factor down below 1.5 in both directions - if some lemma is worse either try to reformulate it or introduce some gating tactics

Paolo Giarrusso (Apr 24 2023 at 08:34):

Michael: have you implemented custom automation, or gotten auto to help?

Michael Soegtrop (Apr 24 2023 at 16:00):

@Paolo Giarrusso : I get along with auto, eauto or typeclass eauto and some dedicated forwarding tactics which I run as extern hint at a certain cost level between likely cheap backward tactics and likely expensive backward tactics. For certain goal types I use reflexive tactics.

Last updated: Oct 04 2023 at 18:01 UTC