Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Recursive identify function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive identify function


chronological Thread 
  • From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
  • To: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Recursive identify function
  • Date: Tue, 1 May 2012 17:03:40 -0400

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/




Archive powered by MhonArc 2.6.16.

Top of Page