Induction-schemes
A variety of basic, widely applicable induction schemes.
The definitions here are meant to be used in induct hints or
as the :scheme for induction rules. You would typically include
them only locally, e.g., with:
(local (include-book "std/basic/inductions" :dir :system))
For general background on induction schemes, see logic-knowledge-taken-for-granted-inductive-proof and example-inductions.
Subtopics
- Dec-dec-induct
- (dec-dec-induct n m) inducts by simultaneously subtracting
1 each from n and m, until either one reaches 0.
- Cdr-dec-induct
- (cdr-dec-induct x n) inducts by simultaneously cdr'ing
x and subtracting 1 from n, until we reach the end of x or
n reaches 0.
- Cdr-cdr-induct
- (cdr-cdr-induct x y) inducts by simultaneously cdr'ing
x and y until we reach the end of either.
- Dec-induct
- (dec-induct n) is classic natural-number induction on n;
we just subtract 1 until reaching 0.
- Cdr-induct
- (cdr-induct x) is classic list induction, i.e., cdr
until you reach the end of the list.
