The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

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.
>
> 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.

> 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.

"divide x y" is the proposition that x divides evenly into y.

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

Dan