The Coq mailing list

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

I did it in 15 minutes now that I had more time to sit down at home. Should I give my new implementation to the mailing list? I don't want to mess up the learning experience for anybody else.

Thanks to all who helped.

On Thu, May 21, 2015 at 11:23 AM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

Dan,

Sorry for the slow turn around. I appreciate you assisting me. I've been really busy lately and I do still want to do it. I'll try and attempt it tonight.

On Mon, May 18, 2015 at 11:39 AM, Dan Christensen <jdc AT uwo.ca> wrote:

Kenneth,

Your incr function is not correct:  it doesn't handle 8 increments of O
correctly.  I didn't carefully check your bin_to_nat.  Also, both incr
and bin_to_nat are overly complicated.  I've put some templates below,
where there are just three cases for each function, corresponding to the
three constructors of bin.  Can you replace the ... with appropriate
terms to make it all work?  Remember to use recursion!

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

Eval compute in (incr (incr (incr (incr (incr (incr (incr (incr O)))))))).

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

Dan

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

> Dan,
>
> I was just hoping that you would be so kind as to review the below and tell
> me if it's correct. It appears so, I was able to increment even beyond 5,
> types are no longer always appended.
>
> Fixpoint incr (b : bin) :=
>   match b with
>     | O => Bodd O
>     | Bodd O => Beven (Bodd O)
>     | Beven (Bodd e) => Bodd (Bodd e)
>     | Bodd (Beven e) => Beven (Bodd e)
>     | Bodd (Bodd o) => Beven (Beven (Bodd o))
>     | Beven e => Bodd e
>   end.
>
> Require Import Coq.Numbers.Natural.Peano.NPeano.
>
> Fixpoint bin_to_nat (b : bin) : nat :=
>   let conv := (fix f b accum :=
>       (match b with
>         | O => 0
>         | Beven e => f e (accum+1)
>         | Bodd o => f o (accum+1) + 2^accum
>       end ))
>   in conv b 0.
>
>
>
> Eval compute in (bin_to_nat (incr (O))).
> Eval compute in bin_to_nat (incr (incr O)).
> Eval compute in bin_to_nat (incr (incr (incr O))).
> Eval compute in bin_to_nat (incr (incr (incr (incr O)))).
> Eval compute in bin_to_nat (incr (incr (incr (incr (incr O))))).
>
>
> 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