grind_pattern ドキュメントに _ ワイルドカード必須の利用例を追加

[Copilot]

grind_pattern のパターン指定でワイルドカード _ を使える点に加えて、_ を使わないと書けないケースを明示する例に更新しました。
「未登録では失敗し、_ を含むパターン登録後に成功する」ことを同一文脈で示しています。

• 変更内容

  • LeanByExample/Declarative/GrindPattern.lean の _ 例を、_ が必須になるシナリオに差し替え
  • local axiom RfSucc を使い、grind_pattern 未設定時は grind が通らない例を維持
  • local grind_pattern RfSucc => R (f z) y は unknown identifier 'z' で失敗することを #guard_msgs で明示
  • local grind_pattern RfSucc => R (f _) y なら登録でき、grind が通ることを対比で提示

• 追加した例（抜粋）

  example (b : Nat) (h : R (f 0) b) : R (f 0) (b + 1) := by
    fail_if_success grind
  
  /-⋆-//--
  error: unknown identifier 'z'
  -/
  #guard_msgs in --#
  local grind_pattern RfSucc => R (f z) y
  
  -- この位置は `_` ワイルドカードでしか書けない
  local grind_pattern RfSucc => R (f _) y
  
  example (b : Nat) (h : R (f 0) b) : R (f 0) (b + 1) := by
    grind

[Seasawher]

@copilot ワイルドカードを「使わなければいけない」ようなシチュエーションを考案し、それをコード例にしてください

[Copilot]

@copilot ワイルドカードを「使わなければいけない」ようなシチュエーションを考案し、それをコード例にしてください

_ を使わないと書けないケースに差し替えました。RfSucc では f の引数位置に対応する変数が定理引数に存在しないため、R (f z) y は unknown identifier 'z' で失敗し、R (f _) y なら登録できることを #guard_msgs と後続の grind 成功例で示しています。対応コミット: df6b8bc

[Seasawher]

@copilot 存在量化されている箇所とか、引数じゃない変数が入ってるところを埋めるのに、ワイルドカードは役立つのでは？

[Copilot]

@copilot 存在量化されている箇所とか、引数じゃない変数が入ってるところを埋めるのに、ワイルドカードは役立つのでは？

はい、その理解で合っています。該当箇所の説明コメントを更新して、「定理の引数に現れない位置を埋めるときに _ が必要で、存在量化された位置を埋めたい場合も同様」という意図を明示しました。対応コミット: f30f805