Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] connecting the dots between Fixpoint definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] connecting the dots between Fixpoint definitions


chronological Thread 
  • From: julien forest <forest AT ensiie.fr>
  • To: Paul Tarau <paul.tarau AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] connecting the dots between Fixpoint definitions
  • Date: Mon, 12 Jul 2010 20:59:00 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:in-reply-to:references :x-mailer:mime-version:content-type:content-transfer-encoding; b=PM5CJfMvOKugmIwG9l+sX49Rm9kAFd/P1Trjndri1D45VSqBQFumefjF/l9oxPvhH/ g7+/5ZEms/tsJUTGzhZXNR5I0wyYnFeBJ9ZxRU9FRNhsuR/eZI8pV0+lsxrMy4SCXtLU pb/tjqzyCtpH7glWGoBZMF76lXIlh7Ir5olhI=

Hi,

On Mon, 12 Jul 2010 11:56:38 -0500
Paul Tarau 
<paul.tarau AT gmail.com>
 wrote:

> An interesting thing with this functional induction version is that
> when trying something like:
> 
> Eval compute in buggy 360.
> 
> Coq 8.1pl2 on a Mac returns
> 
> =1 (incorrectly)

No, this is correct. 

Try this command to see the unfolding of the function definition and
evaluation: 

Goal buggy 360 = 1.
rewrite buggy_equation. (* first recursion on 359 *)
simpl.
rewrite buggy_equation. (* second recursion on (half 359) -1 i.e. 178
which is even *)
simpl.

Qed.

> 
> while
> 
> Coq 8.2 (February 2009) on a Mac returns
> 
>    = let (v, _) := buggy_terminate 360 in v
>      : nat
> 
> which, I suppose needs to be further reduced or it just states
> "I do not know what the value is but I know it will terminate".
> 
My mistake, you should end the proof after the definition of buggy by
Defined and not Qed. 

> Does 8.3 beta work correctly on such functional induction examples?
yes of course. In fact, they have been defined using coq trunk. 


Best regards, 
Julien. 



Archive powered by MhonArc 2.6.16.

Top of Page