The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

If you apply your incr function n times to O, you get an alternating bit
string of n bits.  And then bin_to_nat is computing (in an awkward way)
the length of the bit string.  But the question asks you to encode
numbers in binary, so, for example, the number 255 should be encoded
with 8 bits, not 255 bits.

Dan

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

> 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