The Coq mailing list

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

OH!

Yeah, gosh encoding the binary representation of an increment function, which acts on binary numbers from *right to left*, and carries a value over to the highest (furthermost left) available slot (or adds it) is in a *left to right* type encoding is hard. That felt unnatural...

Thanks for the pointer. I had the feeling I had something wrong. We're all here to learn hopefully, I'm just getting into Coq, but it's something that I've wanted to thoroughly learn for a long time.

(* /me: privately forwards Dan an improved edition that is hopefully correct :-) )

On Sat, May 16, 2015 at 6:50 PM, Dan Christensen <jdc AT uwo.ca> wrote:

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