The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 20 Dec 2012 04:17:21 +0100 (CET),
"fengsheng" 
<fsheng1990 AT 163.com>
 a écrit :

> when I wrote a function to convert natural numbers to binary
> numbers,I met a problem:how to take the value of a number half.

Here is a funny solution (should even work with -nois option).
But be warned it is quite smart for a solution (it is written in a
continuation passing style, I believe).

They are uglier solutions which are a lot less smart.
You can also consider not dividing by two (I think it is what is done
in the standard library) that is remove 1 from nat and add one to
positive until nat is O.
You can also use some accumulator:
Fixpoint div2 (m n:nat): nat*bool :=
 match n with
 | O => (m, false)
 | S O => (m, true)
 | S (S n) => div2 (S m) n
 end.
And then prove that the result of div2 O n is strictly smaller (unless n
is equal to 0) than n, and use it for recursion to build the positive.

=============================================================

Inductive nat : Set := | O : nat
| S : nat -> nat
.

Inductive positive : Set :=
| xH : positive
| xO : positive -> positive
| xI : positive -> positive
.

Inductive bool : Set := true | false.

Definition with_div2 {A:Type}
  (def : A) (f : bool -> nat -> A) (x : nat) : A :=
  (fix with_div2 m n := match m with
   | O => def
   | S m =>
     match n with
     | O => f false m
     | S x => match x with
              | O => f true m
              | S n => with_div2 m n
              end
     end
   end) x x.

Fixpoint nat_to_positive (n : nat) : option positive :=
  with_div2 None
            (fun b n => match nat_to_positive n with
                        | None => if b then Some xH else None
                        | Some p => Some ((if b then xI else xO) p)
                        end) n.

Eval compute in nat_to_positive (S (S (S O))).