`rw` がラムダ内部で効かないときの `simp_rw` 例を追加したい

概要

Lean の rw は、式の表面ではなくラムダ抽象の内部に現れる項を書き換えたいときに、そのままでは失敗することがあります。最近の Lean 公式 Zulip で、この挙動と simp_rw / conv が実用上の回避策になる、という短くて教育価値の高い例が議論されていました。

Lean by Example にはすでに rw、conv、Monad、do 構文のページがありますが、「束縛変数の内側にある書き換え対象」という rw のつまずきどころを正面から説明するページはまだ見当たりませんでした。rw! が解決する問題と、simp_rw が解決する問題が違うことも一緒に説明できるので、追加価値があると思います。

投稿元

• Zulip: Rewrite rule not being applied inside lambda

Zulip 上では、List.count_cons を rw したいが、ラムダの内部ではうまく当たらない、という相談があり、simp_rw や conv が候補として挙がっていました。さらに rw! は「binder の下の書き換え」ではなく、motive 周りの型整合性を助けるためのものだという補足も入っています。

重複確認

確認した既存ページ:

• booksrc/SUMMARY.md の目次上、関連しそうなのは Tactic/Rw.md, Tactic/Conv.md, Type/Monad.md, DoSyntax/README.md
• ただし少なくとも目次レベルでは、「ラムダ内部・binder 下での書き換え失敗」を扱う独立項目は見当たりませんでした

確認した検索:

• GitHub code search: simp_rw conv rw lambda binder bound variables → 0件
• GitHub code search: rewrite under binder lambda count_cons → 0件
• GitHub issue search: simp_rw conv rw lambda binder bound variable → 0件

追加候補のコード例

import Mathlib
open List

variable {α : Type*} [DecidableEq α]
variable (h : α) (tl : List α)

-- `rw [List.count_cons]` は、ラムダ抽象の内部にある `count` にはそのまま当たらない。
example :
    map (fun x => count x (h :: tl)) tl =
      map (fun x => count x tl + if h == x then 1 else 0) tl := by
  simp_rw [List.count_cons]

この例の何が面白いか

• rw は万能な「どこでも書き換え」ではなく、binder の下ではそのまま失敗することがある
• simp_rw は単なる simp の別名ではなく、rewrite rule を式の内側まで反復的に適用したいときに使い分ける価値がある
• rw! も似た場面で名前が挙がりやすいが、解決する問題は別であることを説明できる

コードの読み方

• 左辺の map (fun x => count x (h :: tl)) tl は、「各 x について h :: tl の中での出現回数を数える関数」を tl に写しています
• List.count_cons は、count x (h :: tl) を count x tl + if h == x then 1 else 0 に展開する定理です
• 問題は、その count x (h :: tl) がラムダ fun x => ... の中にあることです
• ここで simp_rw を使うと、ラムダの内部に入ってこの書き換えを実行できます

Lean by Example に追加する価値

• rw を覚えた直後の読者がかなり高い確率で遭遇する「なぜここでは書き換わらないのか？」に答えられる
• rw / simp_rw / conv / rw! の役割分担を、短い例ひとつで説明できる
• Monad や do 構文よりも、まずは戦術の到達範囲の違いとして整理した方が読み手に伝わりやすい

前提・曖昧な点

• この issue の最小例は Zulip の相談文をそのまま再掲したものではなく、論点を保ったまま単独で読める形に簡約したものです
• ローカルで Lean を実行しての検証環境が今回の自動化では用意できなかったため、必要なら実装時に最終確認をお願いします
• conv を併記するなら、rw と対比した補助例として別ブロックに分けるのが読みやすそうです

Start with booksrc/SUMMARY.md and the existing Tactic/Rw.md and Tactic/Conv.md pages, then verify the proposed example in a Lean environment. Add a focused explanation of rewriting inside a lambda and the roles of simp_rw, conv, and rw!, with the example compiling as the done condition.