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: Sep 26 2023 at 13:01 UTC