The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here's one way to do it.  There's probably an easier way, such that the proof that the halving function does what it says it does is simpler...

Inductive even_nat :=

| O_even : even_nat

| S_even : odd_nat -> even_nat

with odd_nat :=

     | S_odd : even_nat -> odd_nat.

Fixpoint even_nat_to_nat (n : even_nat) : nat :=

  match n with

    | O_even => O

    | S_even n' => S (odd_nat_to_nat n')

  end

with odd_nat_to_nat (n : odd_nat) : nat :=

       match n with

         | S_odd n' => S (even_nat_to_nat n')

       end.

Fixpoint half_even (n : even_nat) : nat :=

  match n with

    | O_even => O

    | S_even (S_odd n') => S (half_even n')

  end.

Fixpoint is_even (n : nat) : bool :=

  match n with

    | O => true

    | S n' => negb (is_even n')

  end.

Fixpoint nat_to_even_odd_nat (n : nat) : if is_even n then even_nat else odd_nat :=

  match n as n0 return (if is_even n0 return Set then even_nat else odd_nat) with

    | 0 => O_even

    | S n' => (if is_even n' as b0

                  return

                  ((if b0 then even_nat else odd_nat) ->

                   if negb b0 then even_nat else odd_nat)

               then

                 S_odd

               else

                 S_even)

                (nat_to_even_odd_nat n')

  end.

Definition odd_pred (n : odd_nat) : even_nat :=

  match n with

    | S_odd n' => n'

  end.

Definition floor_half_nat (n : nat) : nat :=

  half_even

    ((if is_even n as b0

         return ((if b0 then even_nat else odd_nat) -> even_nat)

      then (fun x => x)

      else odd_pred) (nat_to_even_odd_nat n)).

On Wed, Dec 19, 2012 at 10:17 PM, fengsheng <fsheng1990 AT 163.com> wrote:

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.