1
$\begingroup$

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!

$\endgroup$
1
  • 2
    $\begingroup$ I think this question can be improved by giving an actual example that you struggle with, so that answerers can refer to something concrete. $\endgroup$
    – Trebor
    Aug 17, 2023 at 12:38

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.