Lean4: Tactic: grind

どうやって証明したら良いか解んなくなったら、とりあえず grind 戦略～！
という間違った使い方をして、難を逃れる戦略を知ったのですが、これは、まだよく解ってない。

grind

説明書を読みますか…

grind タクティクの概要

grind は、最新のSMTソルバーに着想を得たテクニックを使用し、証明を自動的に構築するタクティクです。

主な機能とメカニズム

• 証明の構築: 事実の集合を増分的に収集し、既存の事実から新しい事実を導出することで証明を進めます。

• 背理法: 内部的にはすべての証明を背理法（矛盾による証明）で行います。そのため、前提と期待される結論を運用上区別せず、常に矛盾を導こうとします。

• 同値クラスの追跡: 新しい等式、不等式、ブールリテラルを発見すると、それらを仮想的なホワイトボードに書き込み、同値な項をグループ化します。既知の事実（例：真の命題は True と等しい）も同値クラスの一部として追跡されます。

制限事項と代替手段

• 不得意な問題: grind は、組み合わせ的に爆発する探索スペースを持つ問題（例：大規模な鳩の巣原理、グラフ彩色、Nクイーン問題、ブール制約としての数独）には設計されていません。

• 理由: これらの問題は、grind の分岐探索能力を超える何千（あるいは何百万）ものケース分岐を必要とするためです。

• 代替タクティク: ビットレベルや純粋なブール値の組み合わせ問題には bv_decide を使用すべきです。

  • bv_decide は、外部の最新SATソルバー（CaDiCaL や Kissat など）を呼び出します。

  • 重い探索はLeanの外部で行われ、結果はLean内部で再生・検証可能なコンパクトな証明書として返されるため、信頼性が維持されます。

grind の適用例

grind は以下のような様々な推論を自動的に処理できます。

• 合同閉包 (Congruence Closure): 等しい項の集合を発見します（例：a = b と b = c から a = c を導く）。

• 代数的推論 (Algebraic Reasoning): 可換環ソルバーを使用します。

• 有限体推論 (Finite-Field Reasoning): Fin 型（有限体）におけるオーバーフロー（巡回）を伴う算術を扱えます。

• ケース分析を伴う線形整数算術 (Linear Integer Arithmetic): 複数の線形不等式から矛盾を導くことなどが可能です。

使用例

失敗例より

まず、grind 失敗の例から紹介します。

証明記述が困難なところに通常 sorry を置きます。
すると、ここは省略しているという状態になり、Error 無ければ定理が警告で sorry 使用している。となります。

これは、解決していてもそのまま定理は警告のままとなる。

そこで try 句と共に最後の方に以下のように書く

try は次に続く戦略を試して失敗しても下に流す。通常失敗したらそこでError となり、それ以下の評価は行いません。それは、前提が正しくなければ後続も正しく処理できないからですね。それを try は、次の戦略で試みる事を可能にしてくれる。

で、try grind で試し、失敗したら sorry が評価される。

つまり、未証明のままここは終わる。

成功例

以下は grind only で解決できている状態。

これは、成功例ですが、どうやって成功してるのか、中身が私には理解できないか、見えないので、別の書き方ができずこのまま置いてある。とにかく証明が成功する道がある。

成功例を失敗例の記述で書くと

❌️ sorry で Error になってくれる！

つまり！

成功したら sorry がいらない！というのを教えてくれる書き方！

ですっ！

この書き方で置いておくと、定理内の補助補題や別の補題を書いて

@[grind =]

で修飾してどんどん条件を絞り込んで行ったなら、いつか sorry が Error になって解決！するのではないか！？と期待して…。✍️

$${\N \to \R}$$ のキャスト沼にハマって抜け出せない日々が続いてます…。
ノイローゼになる前に、他の題材を間に入れようかな…時計アプリもある。

2025/10/29 23:13

D.

#Lean #Lean4 #grind #try #sorry #小ネタ

Appendix

Lean コード切り抜き

      -- Step 1: 小さい素数からの寄与を評価
      have h_small_bound : ∀ p : ℕ, p.Prime → p ≤ P₀ → p ≠ 2 →
        ∃ C_p > 0, (Finset.sum (Finset.Icc 0 X) fun n =>
          (p : ℝ) ^ (t * ((padicValNat p (2 * n + 1) : ℝ) - 2))) / (X + 1) ≤ C_p := by
        intros p hp hle hneq
        have hX₃ : 3 ≤ X := by
          try grind  -- success: X ≥ 3 を示す(hX から)
          sorry
          -- ~~hX : X ≥ 1 から X ≥ 3 を示すのは難しいので、ひとまず sorry で進む~~
          -- Replace the failing `grind` tactic with an explicit `exact h_ne_zero` to close the local goal,
          -- and tighten the mgf_twoTail_log statement to require X ≥ 3 so helper lemmas needing X ≥ 3 apply.
          done
        -- h_small_primes を適用
        obtain ⟨C_p, hC_p_pos, hC_p⟩ := h_small_primes p hp hle hneq
        use C_p, hC_p_pos
        exact hC_p X hX₃