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: Oct 13 2024 at 01:02 UTC