## Stream: Coq users

### Topic: ✔ binary logarithm on nat

#### Pierre Rousselin (Dec 05 2022 at 05:39):

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?

#### Huỳnh Trần Khanh (Dec 05 2022 at 06:16):

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

#### Guillaume Melquiond (Dec 05 2022 at 07:23):

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

#### Pierre Rousselin (Dec 05 2022 at 08:11):

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) ?

#### Notification Bot (Dec 05 2022 at 08:12):

Pierre Rousselin has marked this topic as resolved.

Last updated: Sep 25 2023 at 12:01 UTC