The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.