Consider a state machine with tuple of numbers describing its state, i.e. $(i,j)$ such that $i \geq 0$ and $j \geq 0$.
The initial state is $q_0 =(i,j) = (15, 12)$
There are only two transitions allowed:
$(i,j) \to (i-3, j+2)$
and
$(i,j) \to (j,i)$
I was told that the invariant of this state machine is the following predicate:
$P(k)$ = " for state step k, the difference between i and j is $i -j = 5k+2$ or $i-j = 5k+3$".
I was able to verify that this is indeed true by induction, however, without knowing the answer beforehand (i.e. $i -j = 5k+2$ or $i-j = 5k+3$) I would have not been able to realize this on my own. How do you realize that this invariant holds without just knowing the answer? What are some ways people found this out? Is there a trick for realizing that the reminder of the difference mod 5 is always 2 or 3? If the starting state would have been different, would it have been a different invariant? Is there a way of finding out the invariant without making it feel it came out of thin air? How did people figure out the pattern?
Well, that is a good question. I am afraid there is no easy answer.
In this particular case, the transitions are extremely simple. For example, there are no squares or cubes. You might notice for example that $i+j$ goes down by 1 each time that the first transition happens and remains the same if the second transition happens.
Given simple transitions, any invariant has to be simple. The simplest of all is that something like $i+j$ is always the same. We have just seen that is unlikely to work here, because $i+j$ sometimes goes down and sometimes doesn't. At that point looking for something simple that remains fixed modulo something is a good bet. Why? Well, there are not many other simple things left to try.
From that point on, things are simpler. We are obviously looking for a linear relationship. So something like $ai+bj=c\mod k$ for fixed $a,b,c,k$. The first thing to try is obviously $a=b=1$, but that won't work because there would be no change for the second type and -1 for the first. There is no way of making that work.
After trying a few more things that fail to work. You pause for thought. If you repeatedly get transition 2, then the best you can hope for with a linear thing like $ai+bj$ is for it to toggle backwards and forwards. So you want $a=-b$, and you need to accept two values of $k$.
After that breakthrough, you are on the home straight.
All that sounds totally messy. It is. But that is problem solving. The old adage is that no preparation is "necessary or sufficient". You constantly think to yourself can I think of any similar or simpler case that I already know, or might be able to handle? Equally important, you have to be energetic and try lots of things.
You also have to be energetic about constantly learning new things. Most results are proved by adaptations of existing proofs, not by totally new insights.