The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

This question arise often on this list. Coq does not allow the
definition of mutual recursive function when they do not recurse on
inductive of the same family. If you redefine lists as a mutual
inductive together with C, your definition is accepted.

Inductive C : Set :=
   Build_C : LC -> C
with LC : Set :=
  nil: LC
| cons: C -> LC -> LC.

Infix "::" := cons.

Fixpoint h (l : LC) : LC :=
   match l with |
      nil => nil |
      c :: l' => g c :: h l'
   end
with g (c : C) : C :=
   match c with |
      Build_C x => Build_C (h x)
   end.

In the case of lists however you can use Gregory's trick, which allows
to stay with the standard list library.

Best regards,
Pierre

2012/5/2 Terrell, Jeffrey 
<jeffrey.terrell AT kcl.ac.uk>:
> Thanks Gregory. If I unfold map in your solution, I more or less get
>
> Fixpoint g (c : C) : C :=
>    match c with |
>       Build_C x => Build_C (
>          (fix h (l : list C) : list C :=
>             match l with |
>                nil => nil |
>                c' :: l' => g c' :: h l'
>          end) x)
>    end.
>
> What I'm interested to know is how this differs from
>
>> Fixpoint h (l : list C) : list C :=
>>    match l with |
>>       nil => nil |
>>       c :: l' => g c :: h l'
>>    end
>> with g (c : C) : C :=
>>    match c with |
>>       Build_C x => Build_C (h x)
>>    end.
>
>
> Is Coq being conservative in rejecting the latter definition?
>
> Regards,
> Jeff.
>
> On 1 May 2012, at 22:03, Gregory Malecha wrote:
>
> Hi, Jeffrey --
>
> Coq has some special cases for list functions, so it turns out that this
> definition works:
>
> Fixpoint h (c : C) : C :=
>   match c with
>     | Build_C x => Build_C (map h x)
>   end.
>
> Hope this helps.
>
> On Tue, May 1, 2012 at 4:37 PM, Terrell, Jeffrey 
>Â <jeffrey.terrell AT kcl.ac.uk>
> wrote:
>>
>> Hi,
>>
>> Given
>>
>> Inductive C : Set :=
>>    Build_C : list C -> C.
>>
>> how would you define a function with the same functionality as
>>
>> Definition f (c : C) : C := c
>>
>> but which constructed its return value recursively? Presumably Coq won't
>> accept
>>
>> Fixpoint h (l : list C) : list C :=
>>    match l with |
>>       nil => nil |
>>       c :: l' => g c :: h l'
>>    end
>> with g (c : C) : C :=
>>    match c with |
>>       Build_C x => Build_C (h x)
>>    end.
>>
>> because it cannot be sure that the function will terminate.
>>
>> Thanks.
>>
>> Regards,
>> Jeff.
>
>
>
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>
>