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
Qed :-| ?
I assume Guillaume's solution is best, but this is unfortunate :-|
this matters because well-founded is just structural recursion on
Last updated: Jan 29 2023 at 01:02 UTC