`simp (config := { ground := true })` で定数 Array 式を簡約する例を追加したい

概要

Lean 公式 Zulip の比較的最近の lean4 ストリームで、simp が一見単純な Array リテラルのアクセスを簡約しない一方、simp (config := { ground := true }) を使うと「自由変数を含まない定数式」の計算を進められる、という教育価値の高い話題がありました。

Lean by Example にはすでに simp、rfl、decide、Array、conv などの個別ページがありますが、simp の通常設定では止まり、ground := true を明示すると進むという挙動差を、短い Array 例で示すページはまだ見当たりませんでした。simp を「いつでも全部計算してくれるもの」と誤解しがちな読者にとって、よい補足になると思います。

投稿元

• Zulip: Simplifying Access to Array Literal

特に次の流れが要点です。

• example : #[0][0] = 0 := by simp は進まない
• rfl や decide はこの種の目標を閉じられる場合がある
• simp (config := { ground := true }) を使うと、自由変数のない定数項の計算を simp にやらせられる
• ただし計算量が増えうるので、デフォルトでは有効化されていない

重複確認

確認した既存ページ:

• booksrc/SUMMARY.md 上で関連しそうなのは以下でした
• Tactic/Simp.md
• Tactic/Rfl.md
• Tactic/Decide.md
• Tactic/Conv.md
• Type/Array.md
• Syntax/ArrayLiteral.md

ただし少なくとも目次レベルでは、simp の ground := true 設定や、定数 Array 式の簡約失敗を主題にした項目は見当たりませんでした。

確認した検索結果:

• GitHub code search in lean-ja/lean-by-example: ground := true simp ground term reduction → 0 件
• GitHub issue search in lean-ja/lean-by-example: "ground := true" → 0 件
• GitHub issue search in lean-ja/lean-by-example: "simp (config := { ground := true })" → 0 件

追加候補のコード例

example : #[0][0] = 0 := by
  -- 通常の `simp` では進まない
  simp?

example : #[0][0] = 0 := by
  -- 自由変数を含まない定数項の計算を許す
  simp (config := { ground := true })

補助的に、比較対象として次も載せられます。

example : #[0][0] = 0 := by
  rfl

example : #[0][0] = 0 := by
  decide

この例の何が面白いか

• simp は「何でも評価する」タクティクではなく、通常は ground term reduction を控えめにしている
• 同じゴールでも rfl / decide / simp (config := { ground := true }) で、それぞれ得意な理由が違う
• Array のような実装寄りのデータ構造を使うと、List では気付きにくい simp の到達範囲が見えやすい
• ground := true は便利だが、無差別に使うと計算しすぎる可能性がある、という実務的な注意点も一緒に伝えられる

コードの読み方

• #[0] は Array リテラルです
• #[0][0] は先頭要素アクセスなので、人間の感覚ではすぐ 0 になりそうに見えます
• しかし通常の simp は、この種の定数計算を常に積極的に実行する設定ではありません
• ground := true を付けると、「自由変数を含まない閉じた項」の計算を simp が進められるようになります
• 一方 rfl は definitional equality、decide は Decidable インスタンス経由で閉じるので、通る理由がそれぞれ異なります

Lean by Example に追加する価値

• simp を覚えた直後に起こりがちな「なぜこんな単純な式が簡約されないのか？」に答えられる
• rfl / decide / simp の使い分けを、極小の例で横並びに説明できる
• Array のページと simp のページをつなぐ実践的な導線になる
• 設定変更によって simp のふるまいが変わる、という一段進んだ理解につながる

前提・曖昧な点

• この issue の最小例は Zulip の投稿例をそのまま転載したものではなく、論点が一目で伝わるように再構成したものです
• simp? は「通常の simp では狙い通り進まない」ことを示す導入として書いています。実際の本文では、失敗例の見せ方を guard_msgs などに差し替える方が読みやすいかもしれません
• もし本文に載せるなら、ground := true を常用推奨するのではなく、「定数式をまとめて畳みたい時の選択肢」として位置付けるのが安全そうです

Start by reading booksrc/Tactic/Simp.md and the related Type/Array.md entry, then verify the supplied examples in Lean. Done means adding a concise explanation of the usual simp behavior, ground := true, rfl, and decide, and adding the new page to booksrc/SUMMARY.md.