evalNatLog

Mathlib.Tactic.NormNum.NatLog

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.evalNatLog

Lean4

/-- Evaluates the `Nat.log` function.
-/
@[norm_num Nat.log _ _]
def evalNatLog : NormNumExt where
  eval {u α}
    e := do
    let mkApp2 _ (b : Q(ℕ)) (n : Q(ℕ)) ← Meta.whnfR e |
      failure
    let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
    let ⟨eb, pb⟩ ← deriveNat b sℕ
    let ⟨en, pn⟩ ← deriveNat n sℕ
    let ⟨ek, pf⟩ := proveNatLog eb en
    let pf' : Q(IsNat (Nat.log $b $n) $ek) := q(isNat_log $pb $pn $pf)
    return .isNat sℕ ek pf'

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru