7.15 Generation of induction principles with Scheme

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 term1 Sort sort1
with
  ...
with identm := Induction for termm Sort sortm


term1 ...termm are different inductive types 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 term1 Sort sort1
    with
      ...
    with     identm := Minimality for termm Sort sortm
    Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations.



See also: 8.3

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.14.html at 8/10/98