İnduction/inversion and others in coq

Question

I'm trying to learn Coq using the software foundations. I somehow made it to the 2nd volume but I'm struggling writing proofs on my own. Especially whether I should be using inversion or induction. I usually try inversion first and if it's not strong enough or I feel like I need additional hypotheses, I go back and try induction. Half the time I am not even sure what to induct on either. I try to first think and reason about it myself, but that doesn't always prove to be useful.

Are there tips/tricks to it, should I just keep practicing and going through what others came up with to get some sort of muscle memory, or something else entirely?

Thanks in advance!

Answer 1

Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.

For instance if you have a hypothesis of type:

H: S n <= m

And you want to deduce that « m has necessarily shape S m’ for some m’» then inversion (on H itself) is enough. Because just matching the possible constructors for H gives that immediately.

On the other hand if you want to deduce from the same fact that n <= m then you need induction (on H itself) because it does not only follow from the shape of constructors but from the fact that unfolding constructors will eventually end up with a base case (which is the raison d’être of induction/recursion)

Hope I gave the intuition but anyways it is not always clear that a property is of one kind or another. And anyways sometimes using an already established lemma avoids induction or inversion completely.

EDIT: note that if you want to prove the inductive property above you may have to first manipulate H to be of the form n’ <= m.