7.15 Generation of induction principles with Scheme

The Scheme command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema:

Scheme ident1 := Induction for ident'1 Sort sort1
with
...
with identm := Induction for ident'm Sort sortm
ident'1 ... ident'm are different inductive type identifiers belonging to the same package of mutual inductive definitions. This command generates ident1... identm to be mutually recursive definitions. Each term identi proves a general principle of mutual induction for objects in type termi.


Variants:
  1. Scheme ident1 := Minimality for ident'1 Sort sort1
    with
    ...
    with     identm := Minimality for ident'm Sort sortm
    Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations.

See also: 8.3