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.

Sign up for GitHub

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

Jump to bottom

aesop タクティクの説明方法 #1044

Merged
merged 1 commit into from
Nov 3, 2024
Merged

aesop タクティクの説明方法 #1044

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 7 additions & 3 deletions LeanByExample/Reference/Tactic/Aesop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,7 @@

`aesop` は汎用的かつ強力な自動証明のためのタクティクです。

Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があります。様々なタクティクやルールを使用しながら最良優先探索を行い、ルーチンな証明を自動で終わらせます。

Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があります。様々なタクティクやルールを使用しながら最良優先探索を行い、証明を自動で終わらせようとします。
-/
import Aesop -- `aesop` を使用するため
import Mathlib.Tactic.Says
Expand All @@ -22,6 +21,9 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
rw [Injective]
show ∀ ⦃a₁ a₂ : X⦄, f a₁ = f a₂ → a₁ = a₂

-- `simp_all` では示せない
fail_if_success simp_all

-- 示すべきことがまだまだあるように見えるが、一発で証明が終わる
aesop

Expand All @@ -38,7 +40,9 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
apply hgfinj
simp_all only [comp_apply]

/- なお上記の例により、`aesop` が組み込みのルールとして `simp` 補題や `intro` タクティク等を使用することがわかります。-/
/- なお上記の例により、`aesop` が実行の過程で `simp_all` タクティクや `intro` タクティク等を使用することがわかります。
特に、`aesop` は `simp_all` の強化版であるということができます。
実際には `aesop` は `simp_all` よりずっと多くの機能を持ちますが、固有の機能については [`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) のページを参照してください。-/

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