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".
"n0"variable in the error message?
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: Sep 25 2023 at 12:01 UTC