Merge pull request #985 from lean-ja/Seasawher/issue795

aesop の destructビルダーについて説明する

LeanByExample/Reference/Declarative/AddAesopRules.lean

@@ -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 --#

booksrc/links.md

@@ -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 公式のパッケージレジストリ。