search

lean-ja / lean-by-example

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

可換性や結合法則を simp に登録しても問題がない…？ #383

Open Seasawher opened 6 days ago

Seasawher commented 6 days ago

TPiLには次のように書かれている

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/tactics.html?highlight=local#using-the-simplifier-%E5%8D%98%E7%B4%94%E5%8C%96%E5%99%A8%E3%81%AE%E4%BD%BF%E7%94%A8

にも拘わらず，なぜ Mathlib では可換性や結合法則に simp が付与されていないのだろうか？