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)))
->(f:forest)(P0 f)
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 PropCoq < 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).