The Coq mailing list

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

Hey, I've worked it and produced an alternative solution, but I wasn't sure that it was good to send it out over the whole mailing list, so I sent it just to Dan. Do you want me to send what I just sent to Dan?

The way I redid it I saw that I didn't need to used even/odd decision, so the Bodd and Beven just represents Bit on/off, it might even be termed that way, but I'm learning coq in my free time so I didn't really completely refactor.

On Mon, May 18, 2015 at 9:07 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

2015-05-15 17:54 GMT+02:00 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.

​Well, "bin​" is misleading here.

In fact, they are natural numbers with an extra bit telling oddity.

If you consider the subset of "bin" reachable by incr, you get:

O               = 0

(Bodd O)        = S 0 (and is odd)

(Beven (Bodd O))= S (S 0) (and is even)

​and so on.

You can consider the following conversion to natural numbers:

Fixpoint bin_to_nat (b : bin) : nat :=

  match b with

  | O => 0

  | Bodd x => S (bin_to_nat x)

  | Beven x => S (bin_to_nat x)

  end.

Definition nat_to_bin := nat_rec (fun _ => bin) O (fun _ x => incr x).

There is still some annoying part: given a "bin​", nothing guarantees that it will have an "alternate" form.

Thus, bin_to_nat∘nat_to_bin is the identity, but not necessarily nat_to_bin∘bin_to_nat.

And by the way, I always consider bad taste to use the "Fixpoint" keyword, when there is no recursive call.

 

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

​Indeed, the version I provided does not use division at all, and should produce the same output, assuming that the "bin" in argument has an "alternate" form.

If you really need to carry oddity information, you can consider the following types as well:

Inductive even_nat : Type :=

| O : even_nat

| Beven : odd_nat -> even_nat

with odd_nat : Type :=

| Bodd : event_nat -> odd_nat.

Definition nat_with_eveness := even_nat + odd_nat.

Or

Inductive even : bool -> Type :=

| O : even true

| Succ : forall b (n : even b), even (notb n).

Definition nat_with_eveness := {b & even b}.

Both of these types will certainly painful to use, so I would rather recommend use of already defined natural numbers with manual calls to oddity deciders (ie. a function of type "∀ n, {is_even n}+{is_odd n}").

​

 

Dan