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 の destructビルダーについて説明する #985

Merged
merged 3 commits into from
Oct 13, 2024
Merged
Changes from all commits
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
46 changes: 43 additions & 3 deletions LeanByExample/Reference/Declarative/AddAesopRules.lean
Original file line number Diff line number Diff line change
@@ -112,6 +112,7 @@ end --#
`apply` タクティクと同様にはたらくルールを登録します。
-/
section --#

example (a b c d e : Nat)
(h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
-- 最初は aesop で示せない
@@ -129,10 +130,12 @@ example (a b c d e : Nat)
(h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
-- aesop で証明できるようになった
aesop

end --#
/- ### constructors
`constructors` ビルダーは、[帰納型](../Declarative/Inductive.md) `T` の形をしたゴールに遭遇した際に、コンストラクタを適用するように指示します。
-/
section --#

/-- 自前で定義した偶数を表す命題 -/
inductive Even : Nat → Prop where
@@ -148,15 +151,17 @@ example : Even 2 := by
apply Even.zero

-- aesop にルールを登録する
add_aesop_rules safe constructors [Even]
local add_aesop_rules safe constructors [Even]

example : Even 2 := by
-- aesop で証明できるようになった
aesop

end --#
/- ### cases
`cases` ビルダーは、帰納型 `T` の形をした仮定がローカルコンテキストにある場合に、それに対して再帰的に `cases` タクティクを使用して分解するように指示します。
-/
section --#

example (n : Nat) (h : Even (n + 2)) : Even n := by
-- 最初は aesop で証明できない
@@ -167,15 +172,49 @@ example (n : Nat) (h : Even (n + 2)) : Even n := by
assumption

-- aesop にルールを登録する
add_aesop_rules safe cases [Even]
local add_aesop_rules safe cases [Even]

example (n : Nat) (h : Even (n + 2)) : Even n := by
-- aesop で証明できるようになった
aesop

end --#
/- ### destruct
`destruct` ビルダーは、`A₁ → ⋯ → Aₙ → B` という形の命題を登録することで、仮定に `A₁, ..., Aₙ` が含まれている場合に、元の仮定を消去して `B` を仮定に追加します。
-/
section --#

/-- 任意の数 n について、n か n + 1 のどちらかは偶数 -/
theorem even_or_even_succ (n : Nat) : Even n ∨ Even (n + 1) := by
induction n with
| zero => left; apply Even.zero
| succ n ih =>
rcases ih with ih | ih
· right
apply Even.succ
assumption
· left
assumption

example {n : Nat} : Even n ∨ Even (n + 1) := by
-- 最初は aesop で証明できない
fail_if_success aesop

-- 手動で補題を示すことで証明する
have := even_or_even_succ n
assumption

local add_aesop_rules unsafe 30% destruct [even_or_even_succ]

example {n : Nat} : Even n ∨ Even (n + 1) := by
-- aesop で示せるようになった!
aesop

end --#
/- ### tactic
`tactic` ビルダーは、タクティクを追加のルールとして直接利用できるようにします。
-/
section --#

example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
-- aesop で証明できない
@@ -185,8 +224,9 @@ example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
omega

-- aesop にルールを登録する
add_aesop_rules safe tactic [(by omega)]
local add_aesop_rules safe tactic [(by omega)]

example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
-- aesop で証明できるようになった!
aesop
end --#
2 changes: 1 addition & 1 deletion booksrc/links.md
Original file line number Diff line number Diff line change
@@ -20,7 +20,7 @@
* [Lean4 VSCode 拡張機能](https://github.com/leanprover/vscode-lean4) Lean4 のための VSCode 拡張機能。
* [Loogle](https://loogle.lean-lang.org/) Mathlib の検索ツール。型の情報や定数名から検索ができます。vscode-lean4 から実行することもできます。
* [Moogle](https://www.moogle.ai/) 自然言語で Mathlib から定理や定義が検索できるサイト。VSCode 拡張機能もあります。
* [Lean Search](https://leansearch.net/) 自然言語で Mathlib から定理や定義が検索できるサイト。これに関連して[「A Semantic Search Engine for Mathlib4」](https://arxiv.org/abs/2403.13310)という論文があります。
* [Lean Search](https://leansearch.net/) 自然言語で Mathlib から定理や定義が検索できるサイト。これに関連して[「A Semantic Search Engine for Mathlib4」](https://www.semanticscholar.org/paper/A-Semantic-Search-Engine-for-Mathlib4-Gao-Ju/da6bf364987a605843d56b19f9d0b1546b192c5f?utm_source=direct_link)という論文があります。
* [Lean4 Web](https://live.lean-lang.org/) ブラウザ上で Lean が実行できるプレイグラウンド。
* [Reservoir](https://reservoir.lean-lang.org/) Lean 公式のパッケージレジストリ。