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?

- Add the hint
`~ n < m -> n >= m`

to the hint database - 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.

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?

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.

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

Michael: have you implemented custom automation, or gotten `auto`

to help?

@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