Stream: Coq users

Topic: ✔ binary logarithm on nat


view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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) ?

view this post on Zulip Notification Bot (Dec 05 2022 at 08:12):

Pierre Rousselin has marked this topic as resolved.


Last updated: Jun 24 2024 at 13:02 UTC