*Induction Principles for All Variants
We've now seen induction principles for
Generalizing from what we've seen, each constructor of a variant either
generates a base case for the inductive proof, or an inductive case. And, if a
constructor itself carries values of that data type, each of those values
generates in inductive hypothesis. For example:
Leafall generated base cases.
Nodeall generated inductive cases.
::each generated one IH, because each carries one value of the data type.
Nodegenerated two IHs, because it carries two values of the data type.
Suppose we have these types to represent the AST for expressions in a simple language with integers, Booleans, unary operators, and binary operators:
type uop = | UMinus type bop = | BPlus | BMinus type expr = | Int of int | Bool of bool | Unop of uop * expr | Binop of expr * bop * expr
The induction principle for
forall properties P, if forall i, P(Int i) and forall b, P(Bool b) and forall u e, P(e) implies P(Unop (u, e)) and forall b e1 e2, (P(e1) and P(e2)) implies P(Binop (e1, b, e2)) then forall e, P(e)
There are two base cases, corresponding to the two constructors that don't carry
expr. There are two inductive cases, corresponding to the two constructors
that do carry
Unop gets one IH, whereas
Binop gets two IHs,
because of the number of
exprs that each carries.