I am trying to define an integer binary logarithm on `nat`

in the following way:

```
Fixpoint half (n : nat) : nat :=
match n with
0 => 0
| S 0 => 0
| S (S n') => S (half n')
end.
Fixpoint lb (n : nat) : nat :=
match n with
0 => 0 (* arbitrary *)
| S 0 => 0
| S (S n') => S (lb (S (half n')))
end.
```

It is rejected with the following error message:

```
Recursive definition of lb is ill-formed.
In environment
lb : nat → nat
n : nat
n0 : nat
n' : nat
Recursive call to lb has principal argument equal to
"S (half n')" instead of one of the following variables:
"n0" "n'".
Recursive definition is:
"λ n : nat, match n with
| S (S n') => S (lb (S (half n')))
| _ => 0
end".
```

- What is the
`"n0"`

variable in the error message? - If I understand correctly, it is rejected because coq is not sure it terminates. Is there a not too complicated workaround?

There is a workaround. I guess it is a standard workaround in the Coq community, but I'm not a researcher. This should not be construed as expert advice. The workaround is to add an additional parameter, called "fuel", which is the upper bound on the number of iterations the `lb`

fixpoint has to go through. You can then prove that if enough fuel is supplied, the fixpoint has the recursion formulas that you expect.

```
Fixpoint half (n : nat) : nat :=
match n with
0 => 0
| S 0 => 0
| S (S n') => S (half n')
end.
Fixpoint lb_aux (n : nat) (fuel : nat) : nat :=
match n, fuel with
| _, 0 => 0 (* also very arbitrary! *)
| 0, (S fuel) => 0 (* arbitrary *)
| (S 0), (S fuel) => 0
| (S (S n')), (S fuel) => S (lb_aux (S (half n')) fuel)
end.
Definition lb (n : nat) := lb_aux n n.
Compute lb 1024.
```

As for your first question, `n0`

denotes the pattern of the first match. Indeed, `match n with S (S n') => ... end`

is actually syntactic sugar for `match n with S n0 => match n0 with S n' => ... end end`

. It would be clearer if the error message was mentioning `S n'`

instead of `n0`

, except that it would be just as wrong. (`S n'`

is semantically a subterm, but not syntactically.)

Thank you @Huỳnh Trần Khanh for the nice trick (and the cool interpretation of the second variable as *fuel*).

Thank you @Guillaume Melquiond for the explanation. Maybe it could be possible to let `n0`

appear in the definition, as printed by coq (it's already different from what I wrote) ?

Pierre Rousselin has marked this topic as resolved.

Last updated: Jun 24 2024 at 13:02 UTC