diff --git a/404.html b/404.html index ffbb103b..9d59737c 100644 --- a/404.html +++ b/404.html @@ -89,7 +89,7 @@ diff --git a/aesop.html b/aesop.html index 2d11e650..ad5a080d 100644 --- a/aesop.html +++ b/aesop.html @@ -88,7 +88,7 @@ @@ -175,21 +175,42 @@

Lean4 タクティク逆引きリスト

aesop

-

needs: import Aesop

-

aesop は，intro や simp を使用してルーチンな証明を自動で行おうとします．

-
-- 合成 `g ∘ f` が単射なら，`f` も単射
+
aesop は，intro や simp を使用してルーチンな証明を自動で行う，強力なタクティクです． aesop? を使うことにより，中身を見ることも可能です．

+
import Aesop -- `aesop` を使用するため
+import Mathlib.Init.Function -- `Injective` を使用するため
+import Mathlib.Tactic.Says -- `says` を使用するため
+
+-- CI 環境で `says` のチェックをしない
+set_option says.no_verify_in_CI true
+
+-- 以下 `X` `Y` `Z`を集合とする
+variable {X Y Z : Type}
+
+open Function
+
+/-! ## aesop -/
+
+-- 合成 `g ∘ f` が単射なら，`f` も単射
 example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
   rw [Injective]
+  show ∀ ⦃a₁ a₂ : X⦄, f a₁ = f a₂ → a₁ = a₂
+
+  -- 示すべきことがまだまだあるように見えるが，一発で証明が終わる
   aesop
-

-
aesop?

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

-
example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
+
+/-!
+  ## aesop?
+  aesop が成功するとき，aesop? に置き換えると，
+  ゴールを達成するのにどんなタクティクを使用したか教えてくれる．
+-/
+
+example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
   rw [Injective]
-  -- `aesop?` は以下を返す
-  intro a₁ a₂ a
-  apply hgfinj
-  simp_all only [comp_apply]
+  -- `aesop?` は `says` 以下に続く一連のタクティクを示す
+  aesop? says
+    intro a₁ a₂ a
+    apply hgfinj
+    simp_all only [comp_apply]
diff --git a/apply.html b/apply.html index e834f685..523e8415 100644 --- a/apply.html +++ b/apply.html @@ -88,7 +88,7 @@ @@ -220,7 +220,7 @@

- @@ -234,7 +234,7 @@

- diff --git a/apply_assumption.html b/apply_assumption.html index 652f734e..8e110ccf 100644 --- a/apply_assumption.html +++ b/apply_assumption.html @@ -88,7 +88,7 @@ @@ -177,7 +177,13 @@

Lean4 タクティク逆引きリスト

apply_assumption

needs: import Mathlib.Tactic.SolveByElim

apply_assumption は，ゴールが ⊢ head であるときに，... → ∀ _, ... → head という形の命題をローカルコンテキストから探し，それを用いてゴールを書き換えます．

-
example (hPQ : P → Q) : ¬ Q → ¬ P := by
+
import Mathlib.Tactic.SolveByElim
+
+variable (P Q R : Prop)
+
+/-! ## apply_assumption -/
+
+example (hPQ : P → Q) : ¬ Q → ¬ P := by
   intro hQn hP
 
   -- 矛盾を示したい
@@ -193,10 +199,19 @@ 
apply_assum
 
   -- 自動で `hP` を適用
   apply_assumption
+
+  -- 証明終わり
   done
-

-
タクティクを繰り返すことを指示するタクティク repeat と組み合わせると，「ローカルコンテキストにある仮定を適切に選んで apply, exact することを繰り返し，ゴールを閉じる」ことができます．

-
example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
+
+/-!
+  ## repeat apply_assumption
+
+  タクティクを繰り返すことを指示するタクティク `repeat` と組み合わせると，
+  「ローカルコンテキストにある仮定を適切に選んで apply, exact することを繰り返し，
+  ゴールを閉じる」ことができます．
+-/
+
+example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
   repeat apply_assumption
 

 
diff --git a/apply_question.html b/apply_search.html
similarity index 66%
rename from apply_question.html
rename to apply_search.html
index c5710711..6fa249b1 100644
--- a/apply_question.html
+++ b/apply_search.html
@@ -3,7 +3,7 @@
     
         
         
-        apply?: ライブラリ検索で後方推論 - Lean4 タクティク逆引きリスト
+        apply?: apply できるか検索 - Lean4 タクティク逆引きリスト
 
 
         
@@ -88,7 +88,7 @@
 
         
@@ -175,36 +175,37 @@ 
Lean4 タクティク逆引きリスト

                 

                     

                         
apply?

-
needs: import Mathlib.Tactic.LibrarySearch

-
apply? は，ゴールを閉じるのに必要な命題をライブラリから検索してきて，提案してくれるタクティクです．

-
-- 群準同型は積を保つ
+
apply? は，カレントゴールを apply や refine で変形することができないか，ライブラリから検索して提案してくれるタクティクです．

+
複数の候補が提案されたときは，どれを選ぶとゴールが何に変わるのか表示されるので，その中から好ましいものを選ぶと良いでしょう．

+
import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Hom.Group.Defs
+import Mathlib.Tactic.LibrarySearch -- apply? を使うのに必要
+
+/-- 群準同型は積を保つ -/
 example [Group G] [Group H] (f : G →* H) (a b : G) :
     f (a * b) = f a * f b := by
-    -- `exact MonoidHom.map_mul f a b` を提案してくれる
-    apply?
-

-
複数の候補が提案されたときは，どれを選ぶとゴールが何に変わるのか表示されるので，その中から好ましいものを選ぶと良いでしょう．

-
補足

-
apply? はあくまで証明を書くときに補助として使うものです．sorry と同じように，清書した証明に残してはいけません．

-
sorry と同じと言いましたが，実際 apply? は sorryAx 1 を裏で使用します．これは，#explode で証明の中身を出力させれば分かります．sorry を使っているという旨の警告も出ます．

-
theorem T (x y : Nat) (_: x ≤ y) : 2 ^ x ≤ 2 ^ y := by
-    apply?
-
-    -- `apply?` しただけで `done` が通り，示せているように見える
-    done
-
-/-
-T : ∀ (x y : ℕ), x ≤ y → 2 ^ x ≤ 2 ^ y
-
-0│       │ x       ├ ℕ
-1│       │ y       ├ ℕ
-2│       │ h       ├ x ≤ y
-3│       │ sorryAx │ 2 ^ x ≤ 2 ^ y
-4│0,1,2,3│ ∀I      │ ∀ (x y : ℕ), x ≤ y → 2 ^ x ≤ 2 ^ y
+  -- `exact MonoidHom.map_mul f a b` を提案してくれる
+  apply?
+
+/-!
+  ## 補足
+
+  `apply?` はあくまで証明を書くときに補助として使うものです．
+  `sorry` と同じように，清書した証明に残してはいけません．
+  `sorry` と同じと言いましたが，実際 `apply?` は `sorryAx` を裏で使用します．
 -/
-#explode T
+
+theorem T (x y : Nat) (_: x ≤ y) : 2 ^ x ≤ 2 ^ y := by
+  apply?
+
+  -- `apply?` しただけで `done` が通り，示せているように見える
+  done
+
+-- 以下に示すように，裏で `sorryAx` が使われている
+
+/-- info: 'T' depends on axioms: [sorryAx] -/
+#guard_msgs in #print axioms T
 

-
1 sorry が裏で使用している公理のこと

 
                     

 
diff --git a/assumption.html b/assumption.html
index c4530bf7..458fee0b 100644
--- a/assumption.html
+++ b/assumption.html
@@ -88,7 +88,7 @@
 
         
@@ -186,7 +186,7 @@ 
exact 
 
                     

 
             
diff --git a/exact_question.html b/exact_search.html
similarity index 70%
rename from exact_question.html
rename to exact_search.html
index da453c3f..85b3145f 100644
--- a/exact_question.html
+++ b/exact_search.html
@@ -3,7 +3,7 @@
     
         
         
-        exact?: ゴールをライブラリ検索 - Lean4 タクティク逆引きリスト
+        exact?: exact できるか検索 - Lean4 タクティク逆引きリスト
 
 
         
@@ -88,7 +88,7 @@
 
         
@@ -175,15 +175,17 @@ 
Lean4 タクティク逆引きリスト

                 

                     

                         
exact?

-
needs: import Mathlib.Tactic.LibrarySearch

-
exact? は，ライブラリとローカルコンテキストにある命題を使って，ゴールを閉じることができないか探索します．

-
-- `exact?` はライブラリ検索を行う
+
exact? は，カレントゴールを exact で閉じることができないか，ライブラリから検索して提案してくれるタクティクです．閉じることができなければ，エラーになります．

+
import Mathlib.Tactic.LibrarySearch -- `exact?` を使うのに必要
+
+variable (P Q : Prop)
+
+-- `exact?` はライブラリ検索を行う
 example : x < x + 1 := by
   -- `Try this: exact Nat.lt.base x` と出力される
   exact?
-

-
apply? と似ていますが，apply? とは異なりゴールを変形するのではなくて exact で直接閉じようとします．

-
-- ローカルコンテキストにある仮定を自動で使ってゴールを導いてくれる
+
+-- ローカルコンテキストにある仮定を自動で使ってゴールを導いてくれる
 example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
   -- `Try this: exact hQR (hPQ hQ)` と出力される
   exact?
diff --git a/exists.html b/exists.html
index 99f683fd..378b7bce 100644
--- a/exists.html
+++ b/exists.html
@@ -88,7 +88,7 @@
 
         
@@ -185,7 +185,7 @@ 
exists

 
                     

 
             
diff --git a/induction.html b/induction.html
index ce0bced2..1331c666 100644
--- a/induction.html
+++ b/induction.html
@@ -88,7 +88,7 @@
 
         
diff --git a/intro.html b/intro.html
index 7d8a84b3..9e9ce4bc 100644
--- a/intro.html
+++ b/intro.html
@@ -88,7 +88,7 @@
 
         
diff --git a/left_right.html b/left_right.html
index b3876af8..4958651b 100644
--- a/left_right.html
+++ b/left_right.html
@@ -88,7 +88,7 @@
 
         
diff --git a/linarith.html b/linarith.html
index 73807c99..3ed83170 100644
--- a/linarith.html
+++ b/linarith.html
@@ -88,7 +88,7 @@
 
         
diff --git a/nlinarith.html b/nlinarith.html
index 7ca29c12..1f4bb945 100644
--- a/nlinarith.html
+++ b/nlinarith.html
@@ -88,7 +88,7 @@
 
         
diff --git a/print.html b/print.html
index 159a2bc6..3a82446a 100644
--- a/print.html
+++ b/print.html
@@ -89,7 +89,7 @@
 
         
@@ -197,26 +197,53 @@ 
リンク集
 
 
aesop

-
needs: import Aesop

-
aesop は，intro や simp を使用してルーチンな証明を自動で行おうとします．

-
-- 合成 `g ∘ f` が単射なら，`f` も単射
+
aesop は，intro や simp を使用してルーチンな証明を自動で行う，強力なタクティクです． aesop? を使うことにより，中身を見ることも可能です．

+
import Aesop -- `aesop` を使用するため
+import Mathlib.Init.Function -- `Injective` を使用するため
+import Mathlib.Tactic.Says -- `says` を使用するため
+
+-- CI 環境で `says` のチェックをしない
+set_option says.no_verify_in_CI true
+
+-- 以下 `X` `Y` `Z`を集合とする
+variable {X Y Z : Type}
+
+open Function
+
+/-! ## aesop -/
+
+-- 合成 `g ∘ f` が単射なら，`f` も単射
 example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
   rw [Injective]
+  show ∀ ⦃a₁ a₂ : X⦄, f a₁ = f a₂ → a₁ = a₂
+
+  -- 示すべきことがまだまだあるように見えるが，一発で証明が終わる
   aesop
-

-
aesop?

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

-
example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
+
+/-!
+  ## aesop?
+  aesop が成功するとき，aesop? に置き換えると，
+  ゴールを達成するのにどんなタクティクを使用したか教えてくれる．
+-/
+
+example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
   rw [Injective]
-  -- `aesop?` は以下を返す
-  intro a₁ a₂ a
-  apply hgfinj
-  simp_all only [comp_apply]
+  -- `aesop?` は `says` 以下に続く一連のタクティクを示す
+  aesop? says
+    intro a₁ a₂ a
+    apply hgfinj
+    simp_all only [comp_apply]
 

 
apply_assumption

 
needs: import Mathlib.Tactic.SolveByElim

 
apply_assumption は，ゴールが ⊢ head であるときに，... → ∀ _, ... → head という形の命題をローカルコンテキストから探し，それを用いてゴールを書き換えます．

-
example (hPQ : P → Q) : ¬ Q → ¬ P := by
+
import Mathlib.Tactic.SolveByElim
+
+variable (P Q R : Prop)
+
+/-! ## apply_assumption -/
+
+example (hPQ : P → Q) : ¬ Q → ¬ P := by
   intro hQn hP
 
   -- 矛盾を示したい
@@ -232,10 +259,19 @@ 
aesop?

 
   -- 自動で `hP` を適用
   apply_assumption
+
+  -- 証明終わり
   done
-

-
タクティクを繰り返すことを指示するタクティク repeat と組み合わせると，「ローカルコンテキストにある仮定を適切に選んで apply, exact することを繰り返し，ゴールを閉じる」ことができます．

-
example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
+
+/-!
+  ## repeat apply_assumption
+
+  タクティクを繰り返すことを指示するタクティク `repeat` と組み合わせると，
+  「ローカルコンテキストにある仮定を適切に選んで apply, exact することを繰り返し，
+  ゴールを閉じる」ことができます．
+-/
+
+example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
   repeat apply_assumption
 

 
apply

@@ -276,36 +312,37 @@ 
exact 
 
apply_assumption との関連

 
apply は常にどの命題を使うか明示する必要がありますが，「ゴールに apply が適用できるような命題をローカルコンテキストから自動で探す」 apply_assumption というタクティクもあります．

 
apply?

-
needs: import Mathlib.Tactic.LibrarySearch

-
apply? は，ゴールを閉じるのに必要な命題をライブラリから検索してきて，提案してくれるタクティクです．

-
-- 群準同型は積を保つ
+
apply? は，カレントゴールを apply や refine で変形することができないか，ライブラリから検索して提案してくれるタクティクです．

+
複数の候補が提案されたときは，どれを選ぶとゴールが何に変わるのか表示されるので，その中から好ましいものを選ぶと良いでしょう．

+
import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Hom.Group.Defs
+import Mathlib.Tactic.LibrarySearch -- apply? を使うのに必要
+
+/-- 群準同型は積を保つ -/
 example [Group G] [Group H] (f : G →* H) (a b : G) :
     f (a * b) = f a * f b := by
-    -- `exact MonoidHom.map_mul f a b` を提案してくれる
-    apply?
-

-
複数の候補が提案されたときは，どれを選ぶとゴールが何に変わるのか表示されるので，その中から好ましいものを選ぶと良いでしょう．

-
補足

-
apply? はあくまで証明を書くときに補助として使うものです．sorry と同じように，清書した証明に残してはいけません．

-
sorry と同じと言いましたが，実際 apply? は sorryAx 1 を裏で使用します．これは，#explode で証明の中身を出力させれば分かります．sorry を使っているという旨の警告も出ます．

-
theorem T (x y : Nat) (_: x ≤ y) : 2 ^ x ≤ 2 ^ y := by
-    apply?
-
-    -- `apply?` しただけで `done` が通り，示せているように見える
-    done
-
-/-
-T : ∀ (x y : ℕ), x ≤ y → 2 ^ x ≤ 2 ^ y
-
-0│       │ x       ├ ℕ
-1│       │ y       ├ ℕ
-2│       │ h       ├ x ≤ y
-3│       │ sorryAx │ 2 ^ x ≤ 2 ^ y
-4│0,1,2,3│ ∀I      │ ∀ (x y : ℕ), x ≤ y → 2 ^ x ≤ 2 ^ y
+  -- `exact MonoidHom.map_mul f a b` を提案してくれる
+  apply?
+
+/-!
+  ## 補足
+
+  `apply?` はあくまで証明を書くときに補助として使うものです．
+  `sorry` と同じように，清書した証明に残してはいけません．
+  `sorry` と同じと言いましたが，実際 `apply?` は `sorryAx` を裏で使用します．
 -/
-#explode T
+
+theorem T (x y : Nat) (_: x ≤ y) : 2 ^ x ≤ 2 ^ y := by
+  apply?
+
+  -- `apply?` しただけで `done` が通り，示せているように見える
+  done
+
+-- 以下に示すように，裏で `sorryAx` が使われている
+
+/-- info: 'T' depends on axioms: [sorryAx] -/
+#guard_msgs in #print axioms T
 

-
1 sorry が裏で使用している公理のこと

 
assumption

 
assumption は，現在のゴール ⊢ P がローカルコンテキストにあるとき，ゴールを閉じます．

 
example (hP: P) (_: Q) : P := by
@@ -453,7 +490,7 @@ 
rcases

 
   exact ⟨g, hg⟩
 

-
補足

+
補足

 
choose が自動で示してくれることは選択原理 Classical.choice を使って手動で示すことができます．たとえば次のようになります．

 
variable (P : X → Y → Prop)
 
@@ -565,15 +602,17 @@ 
同値を示
 
assumption との関連

 
exact は常にどの命題を使うか明示する必要がありますが，「ゴールを exact で閉じることができるような命題をローカルコンテキストから自動で探す」 assumption というタクティクもあります．

 
exact?

-
needs: import Mathlib.Tactic.LibrarySearch

-
exact? は，ライブラリとローカルコンテキストにある命題を使って，ゴールを閉じることができないか探索します．

-
-- `exact?` はライブラリ検索を行う
+
exact? は，カレントゴールを exact で閉じることができないか，ライブラリから検索して提案してくれるタクティクです．閉じることができなければ，エラーになります．

+
import Mathlib.Tactic.LibrarySearch -- `exact?` を使うのに必要
+
+variable (P Q : Prop)
+
+-- `exact?` はライブラリ検索を行う
 example : x < x + 1 := by
   -- `Try this: exact Nat.lt.base x` と出力される
   exact?
-

-
apply? と似ていますが，apply? とは異なりゴールを変形するのではなくて exact で直接閉じようとします．

-
-- ローカルコンテキストにある仮定を自動で使ってゴールを導いてくれる
+
+-- ローカルコンテキストにある仮定を自動で使ってゴールを導いてくれる
 example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
   -- `Try this: exact hQR (hPQ hQ)` と出力される
   exact?
@@ -845,7 +884,7 @@ 

-
補足

+
補足

 
もう少し詳細に書くと，linarith は「ロールコンテキストにある線形な(不)等式系に矛盾があるか調べる」タクティクなので，次のような使い方もできます．

 
example (h1: x = 2 * y) (h2 : - x + 2 * y = 1) : False := by
   linarith
@@ -983,7 +1022,7 @@

rfl

@@ -1001,7 +1040,7 @@

-- `import Mathlib.Data.Nat.Basic` が必要 example (n : Nat) : n ≤ n := by rfl -

補足

+

補足

実は Mathlib.Tactic.Relation.Rfl を import するかどうかにより，内部で呼び出されるタクティクが変わります．