Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

aesop に追加の補題を渡す方法を説明する #781

Merged
merged 5 commits into from
Sep 11, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
aesop のカスタマイズ方法を説明する
see #120
Seasawher committed Sep 10, 2024
commit 003000b3d9b06ed267146110ce758fbcceec9835
67 changes: 50 additions & 17 deletions Examples/Tactic/Aesop.lean
Original file line number Diff line number Diff line change
@@ -1,14 +1,20 @@
/-
# aesop
`aesop` は、Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があるタクティクです。`aesop` は `intro` や `simp` を使用してルーチンな証明を自動で行ってくれます。
`aesop` は汎用的かつ強力な自動証明のためのタクティクです。
Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があります。`intro` や `simp` を使用しながら最良優先探索を行い、ルーチンな証明を自動で終わらせます。
-/
import Aesop -- `aesop` を使用するため
import Mathlib.Logic.Function.Defs -- `Injective` を使用するため
import Mathlib.Tactic.Says

-- 以下 `X` `Y` `Z`を集合とする
variable {X Y Z : Type}

/-- 関数の単射性 -/
def Function.Injective (f : X → Y) : Prop := ∀ ⦃a₁ a₂ : X⦄, f a₁ = f a₂ → a₁ = a₂

open Function

-- 合成 `g ∘ f` が単射なら、`f` も単射
@@ -19,30 +25,57 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
-- 示すべきことがまだまだあるように見えるが、一発で証明が終わる
aesop

/-!
/-
## aesop?
`aesop` が成功するとき、`aesop?` に置き換えるとゴールを達成するのにどんなタクティクを使用したか教えてくれます。
-/

example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
rw [Injective]
aesop? says
intro a₁ a₂ a
apply hgfinj
simp_all only [comp_apply]

/- ## カスタマイズ
`aesop` はユーザがカスタマイズ可能です。補題やタクティクを登録することで、証明可能な命題を増やすことができます。
-/

/-- 自然数 n が正の数であることを表す命題 -/
inductive Pos : Nat → Prop
| succ n : Pos (n + 1)

example : Pos 1 := by
-- ルールが登録されていないので、`aesop` で示すことはできない
fail_if_success aesop

/-
Try this:
intro a₁ a₂ a
apply hgfinj
simp_all only [comp_apply]
-/
aesop?
-- 手動でコンストラクタを `apply` することで証明できる
apply Pos.succ

/-! ## 補足
より詳細には `aesop` は下記のような性質を持ちます:
-- `Pos` 関連のルールを `aesop` に憶えさせる
attribute [aesop safe constructors] Pos

* `simp` と同様に、`@[aesop]` という属性(attribute)を付けることで補題や定義を登録し、`aesop` に使用させることができます。
* `aesop` は登録されたルールを最初のゴールに適用しようとします。成功してサブゴールが生成されたら、`aesop` はサブゴールにも再帰的にルールを適用し、探索ツリーを構築します。
* 探索ツリーは最良優先探索(best-first search)により探索されます。ルールには有用である可能性が高いか低いかもマークすることができ、`aesop` は探索ツリー内のより有望そうなゴールを先に調べます。
* `aesop` はまず `simp_all` を用いてゴールを正規化するため、`simp` が使用する補題は `aesop` にも使用されます。
-- `aesop` で証明できるようになった!
example : Pos 1 := by aesop

もっと詳しいことが知りたい方は、[aesopのリポジトリ](https://github.com/leanprover-community/aesop)をご参照ください。
/- 上記の例のように `[aesop]` 属性によってルールを追加することもできますし、`add_aesop_rules` というコマンドでルールを追加することもできます。-/

example (n : Nat) (h : Pos n) : 0 < n := by
-- ルールが足りないので、`aesop` で示すことはできない
fail_if_success aesop

-- 手動で `h : Pos n` を分解して証明する
rcases h with ⟨h⟩
simp

-- `Pos` 関連のルールを `aesop` に追加
add_aesop_rules safe [cases Pos]

-- `aesop` で証明できるようになった!
example (n : Nat) (h : Pos n) : 0 < n := by
aesop

/-
カスタマイズ方法の詳細を知りたい方は[aesopのリポジトリ](https://github.com/leanprover-community/aesop)をご参照ください。また、内部のロジックの詳細については論文 [Aesop: White-Box Best-First Proof Search for Lean](https://dl.acm.org/doi/pdf/10.1145/3573105.3575671) で説明されています。
-/