The Coq mailing list

[Ramana Kumar <Ramana.Kumar AT cl.cam.ac.uk>]

You may be interested in what the HOL community calls "Norrish numerals".

They are like binary numerals but with unique representations.
The constructors are
zero,

n |-> 2n+1, and

n |-> 2n+2.

On Sat, Jan 12, 2013 at 3:50 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:

Le Fri, 11 Jan 2013 09:36:40 -0500,
Adam Chlipala <adamc AT csail.mit.edu> a écrit :

> Your message doesn't ask a question, but I will be nice and infer
> what it is. ;)
>
> On 01/11/2013 09:33 AM, fengsheng wrote:
> > When I define the convert_bin,Coq give a message : Recursive call to
> > convert_bin has principal argument equal to "div2 n" instead of "n".
> >
> > Fixpoint convert_bin (m : nat){struct m}: bin :=
> >    match m with
> >    | 0 =>  O
> >    | S n =>  match evenb n with
> >             | true =>  tw_one (convert_bin (div2 n))
> >             | false =>  tw (convert_bin (div2 n))
> >             end
> >    end.
>
> Yup.  Your function is not terminating for the reason that you give
> with the [struct m] annotation, which is redundant anyway.  See
> Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/> to learn how to
> write Coq functions with more complex recursion patterns than
> primitive recursion.
>
> > 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.
> >
>
> This representation is already part of the standard library: see the
> [NArith] library.

I do not think there is this representation.
There is the positive type which does not allow for zero and replace
this constructor with one. Then you can define binary representation of
even 0 by considering "option positive" and extend the operation.

Note that the proposed represatation has an infinite number of
representants for each number.

That is:

zero ~ tw zero ~ tw (tw zero)…