The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT lri.fr>]

On Thu, 18 Nov 1999, Dimitri Hendriks wrote:

> In the file changes.html it is said that the condition for guarded fixpoints
> has been extended and that it is now possible to define structural fixpoints
> for positive inductive definitions with nested recursion.
> 
> But when I try the given example (after Require PolyList.):
> 
>       Inductive term : Set := fun : (list term)->term.
> 
> I get:
> 
>       Warning: Ignoring recursive call
> 
> 
> What's wrong?

Nothing !

That means that the recursor generated for this type is not the good one:

Coq < Check term_ind.
term_ind
     : (P:(term->Prop))((l:(list term))(P (fun l)))->(t:term)(P t)

The one you would like, you need to define it yourself !

Lemma good_term_ind
     : (P:(term->Prop))
        (P (fun (nil term)))
        ->((t:term; l:(list term))(P (fun l))->(P (fun (cons t l))))
        ->(t:term)(P t).

Induction t. Induction l. Assumption. Assumption.

It's like mutual inductive types with which you need to define the "good"
induction principle with Scheme. Your type term is like the following one:

Mutual Inductive term2: Set :=
  fun2: list_term2->term2
with list_term2: Set :=
  nil2: list_term2
  | cons2: term2->list_term2->list_term2.

Coq < Check term2_ind.
term2_ind
     : (P:(term2->Prop))((l:list_term2)(P (fun2 l)))->(t:term2)(P t)

Scheme good_term2_ind := Induction for term2 Sort Prop      
with good_list_term2_ind := Induction for list_term2 Sort Prop.

Coq < Check good_term2_ind.
good_term2_ind
     : (P:(term2->Prop); P0:(list_term2->Prop))
        ((l:list_term2)(P0 l)->(P (fun2 l)))
        ->(P0 nil2)
        ->((t:term2)(P t)->(l:list_term2)(P0 l)->(P0 (cons2 t l)))
        ->(t:term2)(P t)

Then, you can define something like good_term_ind.

Lemma good_term2_ind2
     : (P:(term2->Prop))
        (P (fun2 nil2))
        ->((t:term2; l:list_term2)(P (fun2 l))->(P (fun2 (cons2 t l))))
        ->(t:term2)(P t).

I wonder if it can be automatically generated also. If so, does the Coq
team expect to extend the generation mechanism also ?

Frederic Blanqui.

------------------------------------------------------------------------------
Laboratoire de Recherche en Informatique (LRI) - Equipe DEMONS
batiment 490, bureau 153, Universite Paris-Sud 91405 ORSAY (FRANCE)
tel:33.1.69.15.42.35 - fax:33.1.69.15.65.86 - web:http://www.lri.fr/~blanqui