The Coq mailing list

[Casteran Pierre <pierre.casteran AT labri.fr>]

Hi,

 You should look at the Standard Library; The type N is what you think 
about, with a slight difference :
 Your proposal can represent zero in an infinite number of ways: O, 
twO, tw (tw O), etc.
which can be an harmful inductive representation of a datatype.
Coq's representation avoids this problem.


The conversion functions are N.to_nat and N.of_nat:

Require Import NArith.

Coq <   SearchAbout (nat -> N).
N.shiftl_nat: N -> nat -> N
N.shiftr_nat: N -> nat -> N
N.of_nat: nat -> N
BinNatDef.N.shiftl_nat: N -> nat -> N
BinNatDef.N.shiftr_nat: N -> nat -> N
BinNatDef.N.of_nat: nat -> N


Coq < Compute (N.of_nat 6).
     = 6%N
     : N








Le 16/07/2013 06:48, fengsheng a écrit :
> Hello everyone:
>    I was stuck when I thought about the following question:
>    Consider a different, more efficient representation of natural numbers 
> using
> a binary rather than unary system.  That is, instead of saying that each
> natural number is either zero or the successor
>   of a natural number, we can say that each binary number is either
> - zero,
> - twice a binary number, or
> - one more than twice a binary number.
>    I define the binary  as following:
>    Inductive bin : Type :=
>    | O : bin
>    | tw : bin -> bin
>    | tw_one : bin -> bin .
>    Now I want to write a function to convert natural numbers to binary
> numbers,but I have no idea.Could you give me any advice?