decide and log

Stream: mathlib4

[Violeta Hernández]

Is there a way to get this to work?

import Init.Data.Nat.Log2

example : Nat.log2 8 = 3 := by decide

I could make my own implementation of this function using fuel, i.e.

private def log2_with_fuel (n : ℕ) (fuel : ℕ) : ℕ :=
  if n < 2 then 0 else match fuel with
  | 0 => 0
  | fuel + 1 => log2_with_fuel (n / 2) fuel + 1

private def log2 (n : ℕ) : ℕ :=
  log2_with_fuel n n

But then I'd have to prove that it matches Nat.log2. Is there some out-of-the-box mechanism to deal with this?

[Eric Wieser]

The answer is to redefine docs#Nat.log2 to use fuel

[Violeta Hernández]

Here's a core-friendly implementation

import Init.Data.Nat.Log2

private theorem add_two_div_le (n : Nat) : (n + 2) / 2 ≤ n + 1 := by
  simpa using Nat.div_le_self n 2

private def log2_with_fuel (n fuel : Nat) : Nat :=
  if n < 2 then 0 else match fuel with
  | 0 => unreachable!
  | fuel + 1 => log2_with_fuel (n / 2) fuel + 1

private theorem log2_with_fuel_of_lt_two {n fuel : Nat} (h : n < 2) : log2_with_fuel n fuel = 0 := by
  rw [log2_with_fuel.eq_def, if_pos h]

private theorem log2_with_fuel_add_two {n fuel : Nat} :
    log2_with_fuel (n + 2) (fuel + 1) = log2_with_fuel ((n + 2) / 2) fuel + 1 := by
  rw [log2_with_fuel.eq_def, if_neg]
  exact Nat.not_lt.2 (Nat.le_add_left 2 n)

private theorem log2_with_fuel_of_le {n fuel : Nat} (h : n ≤ fuel) :
    log2_with_fuel n fuel = log2_with_fuel n n :=
  match n with
  | 0 | 1 => by rw [log2_with_fuel_of_lt_two (by decide), log2_with_fuel_of_lt_two (by decide)]
  | n + 2 => by
    match fuel with
    | 0 => contradiction
    | fuel + 1 =>
      rw [log2_with_fuel_add_two, log2_with_fuel_add_two,
        log2_with_fuel_of_le, log2_with_fuel_of_le (fuel := n + 1)]
      · exact add_two_div_le n
      · simp only [Nat.reduceLeDiff] at h
        exact Nat.le_trans (add_two_div_le n) h

/--
Base-two logarithm of natural numbers. Returns `⌊max 0 (log₂ n)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `Nat.log2 0 = 0`
 * `Nat.log2 1 = 0`
 * `Nat.log2 2 = 1`
 * `Nat.log2 4 = 2`
 * `Nat.log2 7 = 2`
 * `Nat.log2 8 = 3`
-/
@[extern "lean_nat_log2"]
def log2 (n : @& Nat) : Nat :=
  log2_with_fuel n n

theorem log2_def (n : Nat) : log2 n = if n < 2 then 0 else log2 (n / 2) + 1 :=
  match n with
  | 0 | 1 => rfl
  | n + 2 => by
    rw [log2, log2_with_fuel_add_two, if_neg, log2_with_fuel_of_le]
    · rfl
    · exact add_two_div_le n
    · exact Nat.not_lt.2 (Nat.le_add_left 2 n)

example : log2 8 = 3 := by decide

[Aaron Liu]

you should prove the 0 branch is unreachable instead of putting a panic

[Violeta Hernández]

Really I could put a 37 in there and it wouldn't matter

[Violeta Hernández]

log2_def is the public API and it works whatever you put in there

[Kim Morrison]

What Aaron said :-)

[Violeta Hernández]

Well, the branch isn't unreachable. It's unreachable when you call the function with n = fuel.

[Aaron Liu]

then make the function take an additional proof argument (h : n ≤ fuel)

[Violeta Hernández]

I feel like that just complicates things.

[Aaron Liu]

fine I'll do it

[Violeta Hernández]

Would you be happy if I wrote 0 instead of unreachable!?

[Aaron Liu]

somehow I feel like it became shorter

import Init.Data.Nat.Log2

private def log2_with_fuel (n fuel : Nat) (h : n ≤ fuel) : Nat :=
  if hn : n < 2 then 0 else match fuel, (show fuel ≠ 0 by omega) with
  | fuel + 1, _ => log2_with_fuel (n / 2) fuel
    (Nat.le_of_lt_add_one (Nat.lt_of_lt_of_le (Nat.div_lt_self (by omega) Nat.one_lt_two) h)) + 1

private theorem log2_fuel_irrel {n fuel fuel' : Nat} (h : n ≤ fuel) (h' : n ≤ fuel') :
    log2_with_fuel n fuel h = log2_with_fuel n fuel' h' := by
  fun_induction log2_with_fuel n fuel' h' generalizing fuel
  · rw [log2_with_fuel, dif_pos ‹_›]
  · rw [log2_with_fuel, dif_neg ‹_›]
    split
    simp_all

/--
Base-two logarithm of natural numbers. Returns `⌊max 0 (log₂ n)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `Nat.log2 0 = 0`
 * `Nat.log2 1 = 0`
 * `Nat.log2 2 = 1`
 * `Nat.log2 4 = 2`
 * `Nat.log2 7 = 2`
 * `Nat.log2 8 = 3`
-/
@[extern "lean_nat_log2"]
def log2 (n : @& Nat) : Nat :=
  log2_with_fuel n n (Nat.le_refl n)

theorem log2_def (n : Nat) : log2 n = if n < 2 then 0 else log2 (n / 2) + 1 := by
  rw [log2, log2, log2_with_fuel]
  split
  · rfl
  · split
    rw [log2_fuel_irrel]

example : log2 8 = 3 := by decide

[Violeta Hernández]

Well, I've been proven wrong

[Violeta Hernández]

I guess this means you now get to PR it

[Aaron Liu]

maybe tomorrow

[Violeta Hernández]

fyi the reason I need this is so that nimber multiplication on naturals can be computed using decide

[Kyle Miller]

Violeta's is actually a bit faster at reduction.

private def log2_with_fuel (n fuel : Nat) (h : n ≤ fuel) : Nat :=
  if hn : n < 2 then 0 else match fuel, (show fuel ≠ 0 by omega) with
  | fuel + 1, _ => log2_with_fuel (n / 2) fuel
    (Nat.le_of_lt_add_one (Nat.lt_of_lt_of_le (Nat.div_lt_self (by omega) Nat.one_lt_two) h)) + 1

def log2 (n : @& Nat) : Nat :=
  log2_with_fuel n n (Nat.le_refl n)

private def log2_with_fuel' (n fuel : Nat) : Nat :=
  if n < 2 then 0 else match fuel with
  | 0 => 0
  | fuel + 1 => log2_with_fuel' (n / 2) fuel + 1

def log2' (n : @& Nat) : Nat :=
  log2_with_fuel' n n

def t := (List.range 400).map (log2 <| · + 100000)
def t' := (List.range 400).map (log2' <| · + 100000)

#time #reduce t  -- 535ms
#time #reduce t' -- 455ms

The code that Aaron's generates avoids a comparison, though somehow Violeta's is still slightly faster at #eval.

For #reduce, I think the deal is that reduction involves substituting values into proofs. The proofs are abstracted out of the definitions so it's not a big deal, but it's measurable.

I'm not sure it's a big enough difference to justify using one over the other.

[Robin Arnez]

I mean if you really care, then

noncomputable def log2 (n : Nat) : Nat :=
  n.rec (fun _ => nat_lit 0) (fun _ ih n =>
    ((nat_lit 2).ble n).rec (nat_lit 0) ((ih (n.div (nat_lit 2))).succ)) n

and it's ~6 times faster

[Violeta Hernández]

Wait what how why

[Violeta Hernández]

Noncomputable? How come?

[Robin Arnez]

Missing support for recursors during compilation

[Violeta Hernández]

Does this mean decide / eval won't work?

[Robin Arnez]

#eval and native_decide but you can fix this using csimp (or extern if this were in lean core)

[Violeta Hernández]

Wait, so native_decide won't work, but decide will?

[Robin Arnez]

yeah, but:

@[csimp]
theorem log2_eq_natLog2 : log2 = Nat.log2 := by
  funext n
  let k := n
  change k.rec _ _ n = (_ : Nat)
  have h₁ : n ≤ k := Nat.le_refl _
  clear_value k
  fun_induction Nat.log2 generalizing k
  · rename_i n h ih
    rcases k with _ | k
    · simp_all
    · simp only [Nat.ble_eq_true_of_le h]
      apply congrArg Nat.succ
      apply ih; omega
  · rename_i n h
    cases k
    · rfl
    · simp only [mt Nat.le_of_ble_eq_true h]

and everything works

[Violeta Hernández]

That's awesome! Could you PR this?

[Aaron Liu]

Why are we stripping stuff down to the recursors

[Violeta Hernández]

Performance, presumably

[Aaron Liu]

Is this done anywhere else?

[Violeta Hernández]

Idk, core is the place of monsters

[Robin Arnez]

Is this done anywhere else?

Rarely but sometimes in grind verification stuff, e.g. https://github.com/leanprover/lean4/blob/6683d1eb911291fe52333cba05abae2f6578c314/src/Init/Grind/Ring/Poly.lean#L54

[Robin Arnez]

https://github.com/leanprover/lean4/blob/6683d1eb911291fe52333cba05abae2f6578c314/src/Init/Data/RArray.lean#L40 is also a notable example

[Robin Arnez]

This is rare in user-facing declarations though, yes

[Kyle Miller]

This is the Lean kernel version of programming in assembly language for speed.

It's probably a premature optimization, but if it's easy to do and we can prove it's correct, I guess why not?

[Kim Morrison]

I'm in favour of a fast Nat.log2!

[Robin Arnez]

lean4#10046

[Robin Arnez]

Goes up to

example : Nat.log2 (1 <<< 500) = 500 := rfl

now

[Yuyang Zhao]

Can we use a term elaborator to avoid writing lean assembly ourselves? I guess this is similar to what I tried in #13795.