## Stream: Coq users

### Topic: Coq gets killed

#### Huỳnh Trần Khanh (Nov 29 2022 at 05:50):

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

#### Guillaume Melquiond (Nov 29 2022 at 07:20):

I am no user of Equation, so I can only guess, but this part `N.to_nat a` looks like it would blow.

#### Huỳnh Trần Khanh (Nov 29 2022 at 09:24):

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

#### Huỳnh Trần Khanh (Nov 29 2022 at 09:26):

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

#### Guillaume Melquiond (Nov 29 2022 at 09:38):

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

#### Meven Lennon-Bertrand (Nov 29 2022 at 10:07):

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…

#### Paolo Giarrusso (Nov 29 2022 at 13:06):

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` :-| ?

#### Paolo Giarrusso (Nov 29 2022 at 13:07):

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

#### Paolo Giarrusso (Nov 29 2022 at 13:08):

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

Last updated: Jan 29 2023 at 01:02 UTC