5
$\begingroup$

There are many kinds of induction (induction over the natural numbers ⊂ structural induction ⊂ Noetherian induction), when do I use which flavour? And what should I keep in mind when doing proofs by induction?

Simple example: I have an inductively defined predicate EVEN and a function even. Now I want to show completeness and soundness, ie. EVEN x ⟹ even x and even x ⟹ EVEN x. What kind of induction do I use for each?


Are there some general guidelines I can follow? Sometimes, we need to strengthen induction hypothesis or generalize variables (Coq's generalize or Isabelle's arbitrary). When and how do I use simultaneous induction on different well-founded partial orders?

I understand that there is no general principle that always applies, but are there some heuristics I can follow to develop an intuition?

When transferring a pen-and-paper proof to a specific proof assistant, are there any quirks or things to keep in mind?

$\endgroup$

1 Answer 1

3
$\begingroup$

The best guideline is: If you don't know how to do the proof on pen-and-paper, you probably will get lost doing it in a proof assistant. If you don't know what your induction hypothesis is supposed to be, you will probably struggle to find the right one when working in a proof assistant.

That said, the next best guideline, I've found, is that (almost) everything is fundamentally structural induction. If you want to use a different form of induction (such as well-founded recursion), I've found it useful to be aware that it's using structural recursion under the hood.

To address your concrete examples:

Simple example: I have an inductively defined predicate EVEN and a function even. Now I want to show completeness and soundness, ie. EVEN x ⟹ even x and even x ⟹ EVEN x. What kind of induction do I use for each?

When proving EVEN x ⟹ even x, you can either induct on EVEN x, or you can induct on x and then invert your proof of EVEN x; both will work equally well. When proving even x ⟹ EVEN x, the only thing you can do is induct on x.

When and how do I use simultaneous induction on different well-founded partial orders?

I'm not sure what you're asking here. You do simultaneous induction on different well-founded partial orders if that's what the pen-and-paper proof needs to go through. As for how, my impulse is that you want to combine the two partial orders into a single partial-order on the cartesian product of the types, and prove this single partial order well-founded. You could do a nested induction/fixpoint, which is powerful and convenient, but almost never needed.

$\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.