General Guidelines and Tips for using Induction

Question

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?

Answer 1

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.