From 93dc45fd6af25fc8bb822cae97a9142a5c197197 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 13 Oct 2024 20:21:02 +0900
Subject: [PATCH 1/3] =?UTF-8?q?aesop=20=E3=81=AE=20destruct=E3=83=93?=
 =?UTF-8?q?=E3=83=AB=E3=83=80=E3=83=BC=E3=81=AB=E3=81=A4=E3=81=84=E3=81=A6?=
 =?UTF-8?q?=E8=AA=AC=E6=98=8E=E3=81=99=E3=82=8B=20Fixes=20#795?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Reference/Declarative/AddAesopRules.lean  | 44 ++++++++++++++++++-
 1 file changed, 42 insertions(+), 2 deletions(-)

diff --git a/LeanByExample/Reference/Declarative/AddAesopRules.lean b/LeanByExample/Reference/Declarative/AddAesopRules.lean
index eca3db1c..f647746b 100644
--- a/LeanByExample/Reference/Declarative/AddAesopRules.lean
+++ b/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 で証明できない
@@ -190,3 +229,4 @@ add_aesop_rules safe tactic [(by omega)]
 example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
   -- aesop で証明できるようになった!
   aesop
+end --#

From 32ceb38a2e91329e76b0a64081baacf98a97daa8 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 13 Oct 2024 20:33:14 +0900
Subject: [PATCH 2/3] =?UTF-8?q?=E3=83=AA=E3=83=B3=E3=82=AF=E3=81=AE?=
 =?UTF-8?q?=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 booksrc/links.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/booksrc/links.md b/booksrc/links.md
index 8a858a95..3d44521e 100644
--- a/booksrc/links.md
+++ b/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 公式のパッケージレジストリ。
 

From 9c64b2e60746b2a2d8ada6f81317e11dbd4bf8bf Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 13 Oct 2024 20:33:28 +0900
Subject: [PATCH 3/3] =?UTF-8?q?local=20=E3=81=AE=E8=BF=BD=E5=8A=A0?=
 =?UTF-8?q?=E6=BC=8F=E3=82=8C=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Declarative/AddAesopRules.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanByExample/Reference/Declarative/AddAesopRules.lean b/LeanByExample/Reference/Declarative/AddAesopRules.lean
index f647746b..45af7722 100644
--- a/LeanByExample/Reference/Declarative/AddAesopRules.lean
+++ b/LeanByExample/Reference/Declarative/AddAesopRules.lean
@@ -224,7 +224,7 @@ 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 で証明できるようになった!