Recursive definition of nat_to_bin is ill-formed

Question

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 " .

Meven Lennon-Bertrand Meven Lennon-Bertrand · Accepted Answer · 2021-03-11T10:05:48

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.

Recursive definition of nat_to_bin is ill-formed

1 Answers