The Coq mailing list

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

Tout make my answer more complete, you can often use the same trick
(nested fixpoints), not only for lists.

P.

2012/5/2 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/
>>
>>