search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
39 stars 7 forks source link

simproc 機能について紹介する #109

Open Seasawher opened 6 months ago

Seasawher commented 6 months ago

v4.6.0 から導入された機能

https://github.com/leanprover/lean4/releases/tag/v4.6.0

Seasawher commented 5 months ago

simproc の利点について

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/what.20is.20advantage.20of.20simprocs

Seasawher commented 4 months ago

良いコード例が思いつかないので，紹介は保留

Seasawher commented 3 months ago

最も単純な simproc の実装例 必ず Lean.Expr を扱わなければならないので，説明するためには Expr のことを説明する必要がある

import Lean.Meta.Tactic.Simp

open Lean Meta

def foo : Nat := 10

simproc reduceFoo (foo) := fun e => do
  dbg_trace "hello, simproc!"
  return .done { expr := Lean.mkNatLit 10 }

example (x : Nat) : x + foo = 10 + x := by
  simp
  ac_rfl