The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Hello all,

I don't use Coq except for my personal hobbyist time, and I would just like to explain that I'm working through the manual problems from the Software Foundations book. Here's my current problem:

First, write a function to convert natural numbers to binary

        numbers.  Then prove that starting with any natural number,

        converting to binary, then converting back yields the same

        natural number you started with.

I'm having an awful time getting this:

Require Import Coq.Arith.Arith_base.

Require Import Coq.ZArith.ZArith.

Require Import Coq.Init.Datatypes.

Local Open Scope Z_scope.

Fixpoint nat_to_bin n := 

  let f :=fun f index =>

  (if (Zeq_bool index 0) then Terminus

   else if (Zeq_bool index (log_inf n)) then

          Biton (nat_to_bin (Z.to_pos (Zminus (Z.pos n) (log_inf n))) (index-1))

        else

          Bitoff (nat_to_bin n (index-1))

  ) in f (log_inf n).

To go through the coq interpreter, the error being. Here are my thoughts of what is going on:

Match statements allow the "magic" that the Coq interpreter executes with to see according to the type what the direction is in terms of a fixpoint in the knaster-tarski understanding, and so therefore can see when a particular variable is on a strictly descending nature. Therefore, at times it may see when a function will terminate. I need to use if statements because I want to look for a certain value of Z, and I didn't want to use peano integers for index. I tried to make the internal anonymous fixpoint because I wanted the system to recognize that index is the parameter that is being iterated over.

Does anybody have any advice how to move forward so that I can get the Coq interpreter to accept my definition?