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?