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.
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.
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 : 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.