8.3 Scheme

8.3 `Scheme`

Example 1: Induction scheme for tree and forest

The definition of principle of mutual induction for tree and forest over the sort Set is defined by the command:

Coq < Scheme tree_forest_rec := Induction for tree Sort Set
Coq < with forest_tree_rec := Induction for forest Sort Set.

You may now look at the type of tree_forest_rec:

Coq < Check tree_forest_rec.
tree_forest_rec
     : (P:(tree->Set); P0:(forest->Set))
        ((a:A; f:forest)(P0 f)->(P (node a f)))
        ->((b:B)(P0 (leaf b)))
        ->((t:tree)(P t)->(f:forest)(P0 f)->(P0 (cons t f)))
        ->(t:tree)(P t)

This principle involves two different predicates for trees and forests; it also has three premises each one corresponding to a constructor of one of the inductive definitions.

The principle tree_forest_rec shares exactly the same premises, only the conclusion now refers to the property of forests.

Coq < Check forest_tree_rec.
forest_tree_rec
     : (P:(tree->Set); P0:(forest->Set))
        ((a:A; f:forest)(P0 f)->(P (node a f)))
        ->((b:B)(P0 (leaf b)))
        ->((t:tree)(P t)->(f:forest)(P0 f)->(P0 (cons t f)))
        ->(f2:forest)(P0 f2)

Example 2: Predicates odd and even on naturals

Let odd and even be inductively defined as:

Coq < Mutual Inductive odd : nat->Prop :=
Coq <     oddS : (n:nat)(even n)->(odd (S n))
Coq < with even : nat -> Prop :=
Coq <     evenO : (even O)
Coq <   | evenS : (n:nat)(odd n)->(even (S n)).

The following command generates a powerful elimination principle:

Coq < Scheme odd_even := Minimality for odd Sort Prop
Coq < with even_odd := Minimality for even Sort Prop.

The type of odd_even for instance will be:

Coq < Check odd_even.
odd_even
     : (P,P0:(nat->Prop))
        ((n:nat)(even n)->(P0 n)->(P (S n)))
        ->(P0 O)
        ->((n:nat)(odd n)->(P n)->(P0 (S n)))
        ->(n:nat)(odd n)->(P n)

The type of even_odd shares the same premises but the conclusion is (n:nat)(even n)->(Q n).