Subject: Re: dealing with mutually-inductive definitions
Newsgroups: gmane.science.mathematics.logic.coq.club
Date: 2007-08-09 16:27:19 GMT (4 years, 40 weeks, 6 days, 20 hours and 9 minutes ago)
<snip/>
> Of course, all this footwork to define adequate induction principles
> would be unnecessary if "Scheme" were extended to generate principles
> of the "even_odd_mutual_ind" kind. (Hint, hint.)
The "Combined Scheme" command is available in the trunk and 8.1pl1
versions and does exactly this. Sadly it does not appear in the coq
documentation on the website which stayed at version 8.1 (Hint, hint.).
So here's the relevant documentation:
10.3.1 Combined Scheme
We can define the induction principles for trees and forests using:
Coq < Scheme tree_forest_ind := Induction for tree Sort Prop
Coq < with forest_tree_ind := Induction for forest Sort Prop.
tree_forest_ind, forest_tree_ind are recursively defined
Then we can build the combined induction principle:
Coq < Combined Scheme tree_forest_mutind from tree_forest_ind,
forest_tree_ind.
tree_forest_mutind is recursively defined
The type of tree_forest_mutrec will be:
Coq < Check tree_forest_mutind.
tree_forest_mutind
: forall (P : tree -> Prop) (P0 : forest -> Prop),
(forall (a : A) (f : forest), P0 f -> P (node a f)) ->
(forall b : B, P0 (leaf b)) ->
(forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t
f1)) ->
(forall t : tree, P t) /\ (forall f2 : forest, P0 f2)
Hope this helps.
-- Matthieu Sozeau