use タクティクを紹介する

LeanByExample/Tactic/Exists.lean

@@ -2,12 +2,14 @@
 
 `exists` タクティクは、「～を満たす `x` が存在する」という命題を示すために、証拠になる `x` を具体的に示します。
 
-ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`exists x` によりゴールが `P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
+ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`exists x` によりゴールが `⊢ P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
 import Lean --#
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
+/- 上位互換にあたるタクティクに [`use`](./Use.md) タクティクがあります。 -/
+
 /- ## 舞台裏
 なお Lean での存在量化の定義は次のようになっています。-/
 --#--

LeanByExample/Tactic/Use.lean

@@ -0,0 +1,64 @@
+/- # use
+
+`use` タクティクは、「～を満たす `x` が存在する」という命題を示すために、証拠になる `x` を具体的に示します。
+
+ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`use x` によりゴールが `⊢ P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。
+-/
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Linarith
+
+#guard_msgs (drop warning) in --#
+example {α : Type} (P : α → Prop) (x : α) : ∃ y, P y := by
+  use x
+  -- ゴールが `P x` に変わる
+  guard_target =ₛ P x
+
+  sorry
+
+/- ## exists との違い
+これだけの説明だと [`exists`](./Exists.md) タクティクと同じに見えますが、`use` タクティクには `exists` より優れている点があります。
+
+### discharger が指定できる
+`use` は、証拠を与えた後にゴールを閉じるために使うタクティク（`discharger` と呼ばれます）を指定することができます。
+-/
+
+example (x : Rat) (h : 3 * x + 6 > 6) : ∃ (y : Rat), y > 0 := by
+  exists x
+  linarith
+
+example (x : Rat) (h : 3 * x + 6 > 6) : ∃ (y : Rat), y > 0 := by
+  -- `discharger` として `linarith` を指定することができる
+  use (discharger := linarith) x
+
+/- ### Exists 以外の構造体にも使用できる
+`exists` は、ゴールの型が `Exists` であるという想定をしているため、フィールドの数が３以上であるような構造体に対して使うとエラーになります。
+-/
+
+/-- 例示のための構造体。フィールドの数が `Exists` より多い -/
+structure Foo where
+  x : Int
+  pos : x > 0
+  sq : x ^ 2 = 9
+
+/-- `Foo` の項を具体的に与える例 -/
+example : Foo := ⟨3, by simp, by simp⟩
+
+/--
+error: invalid constructor ⟨...⟩, insufficient number of arguments, constructs 'Foo.mk' has #3 explicit fields, but only #2 provided
+-/
+#guard_msgs in
+  example : Foo := by
+    exists 3
+
+/- しかし、`use` タクティクであれば対応することができます。 -/
+
+example : Foo := by
+  -- 最初のフィールドを `3` で埋めるように指示する
+  use 3
+
+  -- 残りのフィールドは `simp` で証明することができる
+  all_goals simp
+
+example : Foo := by
+  -- `discharger` を指定するバージョン
+  use (discharger := simp) 3

booksrc/SUMMARY.md

@@ -196,6 +196,7 @@
   - [trivial: 基本的なタクティクを試す](./Tactic/Trivial.md)
   - [try: 失敗をエラーにしない](./Tactic/Try.md)
   - [unfold: 定義に展開](./Tactic/Unfold.md)
+  - [use: 存在∃を示す](./Tactic/Use.md)
   - [with_reducible: 透過度指定](./Tactic/WithReducible.md)
   - [wlog: 一般性を失わずに特殊化](./Tactic/Wlog.md)
   - [zify: 整数にキャストする](./Tactic/Zify.md)