The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

It appeared correct to me, I did what it requested for that exercise. It said something along the lines of: an incr and bin to Nat call could correspond to a final value equal to direct Nat incrementation. Test it with incrementing from 1 to 5.

It passed for all those, 1 to 5. Is what I've done poor for lack of correctness or that it produces inefficient code?

(At the current moment I'm not by the computer where I did this work, so I can look at editing it, only interaction)

On May 16, 2015 10:32 AM, "Dan Christensen" <jdc AT uwo.ca> wrote:

[I originally sent this yesterday, but it got stuck in moderation
because I wasn't yet subscribed to the list, so I'm resending.]

Kenneth Adam Miller <kennethadammiller AT gmail.com> writes:

> So, I'm doing the basic exercises, and I encountered this issue:

It looks like you are attempting the exercise on binary numbers
from near the end of:

  http://www.cis.upenn.edu/~bcpierce/sf/current/Basics.html
  http://www.cis.upenn.edu/~bcpierce/sf/current/Basics.v

> Inductive bin : Type :=
>   | O : bin
>   | Beven : bin -> bin
>   | Bodd : bin -> bin.

In this representation of binary numbers, a term like

  Beven Bodd Bodd O

would correspond to the binary number 110.

> Fixpoint incr (b : bin) :=
>   match b with
>     | O => Bodd b
>     | Beven e => Bodd (Beven e)
>     | Bodd o => Beven (Bodd o)
>   end.

If this is supposed to add one to a binary number, it isn't doing the
right thing.  The number of bits should only sometimes increase.

> Require Import Coq.Numbers.Natural.Peano.NPeano.
>
> Fixpoint bin_to_nat (b : bin) : nat :=
>   match b with
>     | O => 0
>     | Beven e => 2 * (( divide (bin_to_nat e) 2) + 1)
>     | Bodd o => 1 + (bin_to_nat o)
>   end.

[As others have said] "divide x y" is the proposition that x divides
evenly into y.

But a correct solution here shouldn't use division at all.

Dan