Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Recursive call to convert_bin has principal argument equal to "div2 n"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive call to convert_bin has principal argument equal to "div2 n"


Chronological Thread 
  • From: Ramana Kumar <Ramana.Kumar AT cl.cam.ac.uk>
  • To: AUGER Cédric <sedrikov AT gmail.com>
  • Cc: Adam Chlipala <adamc AT csail.mit.edu>, fengsheng <fsheng1990 AT 163.com>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Recursive call to convert_bin has principal argument equal to "div2 n"
  • Date: Sat, 12 Jan 2013 08:16:07 +1100

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)…




Archive powered by MHonArc 2.6.18.

Top of Page