I am currently reading the first volume of the softwarefoundations series. In one of the exercises I am supposed to write a function which turns a natural number (unary form) into the equivalent binary number.
This is my code/approach:
Inductive bin : Type :=
| Z
| B0 (n : bin)
| B1 (n : bin).
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Fixpoint nat_to_bin (n:nat) : bin :=
match n with
| 0 => Z
| 1 => B1 Z
| 2 => B0 (B1 Z)
| m => match evenb(m) with
| true => B0 (nat_to_bin (Nat.div m 2))
| false => B1 (nat_to_bin (Nat.modulo m 2))
end
end.
I am using https://jscoq.github.io/scratchpad.html to work on these exercises. Now I get this error message:
Recursive definition of nat_to_bin is ill-formed. In environment nat_to_bin : nat -> bin
n : nat
n0 : nat
n1 : nat
n2 : nat
Recursive call to nat_to_bin has principal argument equal to "Nat.div n 2 " instead of one of the following variables: "n0" "n1" "n2" . Recursive definition is: "fun n : nat => match n with
| 0 => Z
| 1 => B1 Z
| 2 => B0 (B1 Z )
| S (S (S _) ) =>
if evenb n then B0 (nat_to_bin (Nat.div n 2 ) )
else B1 (nat_to_bin (Nat.modulo n 2 ) )
end " .
To retain good logical properties, all functions definable in Coq are terminating. To enforce that, there is a restriction on fixpoint definitions, like the one you are trying to do, called the guard condition. This restriction is roughly that the recursive call can only be done on subterms of the argument of the function.
This is not the case in your definition, where you apply nat_to_bin
to the terms (Nat.div n 2)
and (Nat.modulo n 2)
which are functions applied to n
. Although you can mathematically prove that those are always smaller than n
, they are no subterms of n
, so your function does not respect the guard condition.
If you wanted to define nat_to_bin
in the way you are doing, you would need to resort to well-founded induction, which would use the well-foundedness of the order on nat
to allow you to call you function on any term you can prove smaller than n
. However, this solution is quite complex, because it would force you to do some proofs that are not that easy.
Instead, I would advise going another way: just above in the book, it is suggested to define a function incr : bin -> bin
that increments a binary number by one. You can use that one to define nat_to_bin
by a simple recursion on n
, like this:
Fixpoint nat_to_bin (n:nat) : bin :=
match n with
| 0 => Z
| S n' => incr (nat_to_bin n')
end.
As for incr
itself, you should also be able to write it down using a simple recursion on your binary number, as they are written with low-order bit outside.