After running this code, Coq gets killed. Why? I'm using binary numbers here.

```
From Equations Require Import Equations.
From stdpp Require Import numbers base option options.
Equations? log2 (a : N) : N by wf (N.to_nat a) lt :=
| a := if decide (a = 0%N) then 0 else log2 (a / 2) + 1.
Proof.
rewrite N2Nat.inj_div.
apply Nat.div_lt; lia.
Qed.
Compute (log2 (231234423%N)).
```

I am no user of Equation, so I can only guess, but this part `N.to_nat a`

looks like it would blow.

Oh dear, wut? I thought it would only be used to prove the recursion is well founded. This gets executed?

So I guess the only way to write this function without exponential blowup would be adding a fuel parameter.

In this specific case, you do not need any fuel. You can directly write your `log2`

over the binary representation of your number. Said otherwise, `log2`

is structurally decreasing over the number. (Obviously, you would not use Equations for this purpose.)

I don't know if it is in the library, but you can also use the equivalent of `lt`

directly on `N`

rather than on `nat`

? All lemmas you need on the `N`

side should follow from their `nat`

equivalent + the fact that `N.to_nat`

preserves and reflects order, but that way you might keep you proof tidier. Although you might encounter a similar blowup by doing this, and might have to prove your lemmas in a smarter way…

Ouch, this doesn't quite compute:

```
#[global] Instance: WellFounded N.lt.
Proof. apply N.lt_wf_0. Defined.
Equations? log2 (a : N) : N by wf a N.lt :=
| a := if decide (a = 0%N) then 0 else log2 (a / 2) + 1.
Proof.
apply N.div_lt; lia.
Qed.
```

the problem _might_ be that, while `N.lt_wf_0`

is correctly `Defined`

, `N.lt_wf`

is `Qed`

:-| ?

I assume Guillaume's solution is best, but this is unfortunate :-|

this matters because well-founded is just structural recursion on `Acc`

Last updated: Jun 18 2024 at 09:02 UTC