Slow rfl / Nat.log

Stream: mathlib4

[Gareth Ma]

Hi, does anyone mind explaining why the following behaviour? In particular, how should I resolve the last case? norm_num also does nothing to the goal.

import Mathlib.Data.Nat.Log
open Nat
set_option profiler true

/-
tactic execution of Lean.Parser.Tactic.refl took 28.8s
type checking took 20.8s
-/
example : log 10 1003 = 3 := by
  rfl
  done

/- 200ms -/
example : log 10 1003 = 3 := by
  unfold log
  simp
  done

/- both hangs - at least I don't have the patience -/
/- example : log 10 10300 = 4 := by -/
/-   rfl -/
/-   done -/

example : log 10 10300 = 4 := by
  unfold log
  simp
  done

[Gareth Ma]

This does solve the final case, but takes 10 seconds (9s on type checking):

example : log 10 10300 = 4 := by
  unfold log
  beta_reduce
  simp only [dite_true]
  rfl

[Gareth Ma]

example : log 10 1019835301 = 9 := by
  iterate 9 rw [log_of_one_lt_of_le]
  all_goals trivial

This takes no time - is it the "recommended" way?

[Thomas Murrills]

(Btw, you can even golf it to by simp only [log_of_one_lt_of_le])

[Damiano Testa]

If you are going to use it frequently, this quick macro may be useful:

macro "norm_log" : tactic => `(tactic| focus
  repeat
    apply (log_of_one_lt_of_le ?_ ?_).trans <| (add_left_inj _).mpr ?_
    pick_goal 3
  )

macro "norm_log!" : tactic => `(tactic| focus (norm_log; all_goals try trivial))

example : log 10 10198353000 = 10 := by
  norm_log!

[Thomas Murrills]

Ultimately, there should simply be a norm_num extension for Nat.log, though!

But the slow rfl is still worth investigating in its own right...I wonder if it's anything like the issue with gcd from a while back, where, iirc, it was building a huge termination proof?

[Damiano Testa]

Of course a norm_num extension would be great!

I was simply suggesting a quick workaround: Gareth is working on a project for which the unprincipled macro above could be useful. (The project is for a module that I am teaching :smile: )