Choosing an inductive principle

From CS2800 wiki
Revision as of 15:21, 17 March 2020 by {{GENDER:Mdg39|[math]'"2}} [/math]'"7
(<math>1) </math>2 | <math>3 (</math>4) | <math>5 (</math>6)

Often, when proving things about an inductively defined function, it is useful to use the same inductive principle for the proof as was used for the definition. For example, we argued that the [math]\href{/cs2800/wiki/index.php/Gcd}{gcd} [/math] function is well-defined because it's second argument is decreasing (that is, while defining [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) [/math], we could assume that [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(b,r) [/math] was already defined, since [math]r \lt b [/math]. This is a form of strong induction argument on [math]b [/math]. Therefore, a good heuristic for proving things about [math]\href{/cs2800/wiki/index.php/Gcd}{gcd} [/math] is to do induction on the second argument. That is, to prove "for all [math]a, b [/math], some fact involving [math]gcd(a,b) [/math]", it makes sense to define [math]P(b) [/math] as "for all [math]a [/math], the fact involving [math]gcd(a,b) [/math]", and then use strong induction to prove for all [math]b, P(b) [/math].

The reason for this is that in the inductive step, you are likely to plug in the definition, and you would then like to apply the inductive hypothesis to reason about the expression you derive. If the inductive principle used in your proof matches the inductive principle used in your definition, you will be able to do this.