coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] connecting the dots between Fixpoint definitions, Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Taral
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- RE: [Coq-Club] connecting the dots between Fixpoint definitions, Georges Gonthier
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- RE: [Coq-Club] connecting the dots between Fixpoint definitions,
Georges Gonthier
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
julien forest
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, julien forest
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, Paul Tarau
- Re: [Coq-Club] connecting the dots between Fixpoint definitions, julien forest
- Re: [Coq-Club] connecting the dots between Fixpoint definitions,
Taral
Archive powered by MhonArc 2.6.16.