The Coq mailing list

["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/