Seasawher/issue895

LeanByExample/Declarative/Abbrev.lean

@@ -18,7 +18,8 @@ numerals are polymorphic in Lean, but the numeral `42` cannot be used in a conte
 due to the absence of the instance above
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
-#guard_msgs in #check (42 : NaturalNumber)
+#guard_msgs in
+  #check (42 : NaturalNumber)
 
 end Abbrev0 --#
 /- ここでエラーを修正する方法の一つが、`def` の代わりに `abbrev` を使用することです。-/

LeanByExample/Declarative/Attribute.lean

@@ -56,7 +56,8 @@ example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by simp
 @[irreducible] def greet := "Hello"
 
 /-- error: attribute cannot be erased -/
-#guard_msgs in attribute [-irreducible] greet
+#guard_msgs in
+  attribute [-irreducible] greet
 
 /- ## タグ
 `attribute` コマンドを使用すると定義の後から属性を付与することができますが、定義した直後に属性を付与する場合はタグと呼ばれる `@[..]` という書き方が使えます。-/

LeanByExample/Diagnostic/Time.lean

@@ -76,6 +76,7 @@ elab "#in_second " stx:command : command => do
 #in_second #eval fib 32
 
 /-- error: It took more than one second for the command to run. -/
-#guard_msgs (error) in #in_second #eval fibonacci 32
+#guard_msgs (error) in
+  #in_second #eval fibonacci 32
 
 end Time --#

LeanByExample/Tactic/Calc.lean

@@ -7,7 +7,7 @@ import Mathlib.Tactic -- 大雑把に import する
 variable (a b : ℝ)
 
 example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
-  -- a ^ 2 - 2 * a * b + b ^ 2 ≥ 0 を示せばよい
+  -- `a ^ 2 - 2 * a * b + b ^ 2 ≥ 0` を示せばよい
   suffices a ^ 2 - 2 * a * b + b ^ 2 ≥ 0 from by
     linarith
 

LeanByExample/Tactic/Refine.lean

@@ -1,9 +1,9 @@
 /- # refine
 
-`refine` は `exact` と同様に機能しますが、プレースホルダを受け入れて新しいゴールを生成するという違いがあります。 -/
+`refine` は [`exact`](./Exact.md) タクティクと同様に機能しますが、プレースホルダを受け入れて新しいゴールを生成するという違いがあります。 -/
 variable (P Q R : Prop)
 
-example (hP: P) (hQ: Q) : P ∧ Q := by
+example (hP : P) (hQ : Q) : P ∧ Q := by
   -- 穴埋め形式で証明を作ることができる
   refine ⟨?_, hQ⟩
 
@@ -12,35 +12,32 @@ example (hP: P) (hQ: Q) : P ∧ Q := by
 
   exact hP
 
-/- ## constructor との関連
+/- ## 用途
+
+`refine` はかなり一般的なタクティクなので、様々な場面で使うことができます。
+
+### constructor の一般化として
 
 `refine` は [`constructor`](./Constructor.md) の代わりに使うこともできます。実際 `refine` は `constructor` よりも柔軟で、`⊢ P ∧ Q ∧ R` のような形のゴールは `constructor` よりも簡潔に分割できます。-/
 
-example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
+example (hP : P) (hQ : Q) (hR : R) : P ∧ Q ∧ R := by
   -- ゴールを３つに分割する
   refine ⟨?_, ?_, ?_⟩
 
-  · show P
-    exact hP
-  · show Q
-    exact hQ
-  · show R
-    exact hR
+  · exact hP
+  · exact hQ
+  · exact hR
 
 /- `constructor` を使った場合、一度に２つのゴールに分割することしかできません。 -/
 
-example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
+example (hP : P) (hQ : Q) (hR : R) : P ∧ Q ∧ R := by
   constructor
-  · show P
-    exact hP
-  · show Q ∧ R
-    constructor
-    · show Q
-      exact hQ
-    · show R
-      exact hR
+  · exact hP
+  · constructor
+    · exact hQ
+    · exact hR
 
-/- ## apply との関連
+/- ### apply の一般化として
 
 `h : P → Q` という命題があって、ゴールが `⊢ Q` であるとき `refine h ?_` は `apply h` と同様に機能するので、`refine` で [`apply`](./Apply.md) を代用することができます。 -/
 
@@ -53,3 +50,17 @@ example (hPQ : P → Q) (hP : P) : Q := by
   show P
 
   refine hP
+
+/- ### 自明なケースを示す
+
+ゴールが `⊢ P ∧ Q` であり、`P` が成り立つことが自明であった場合、いちいち `⊢ P` と `⊢ Q` の２つのサブゴールを作って示すのは面倒に思えます。こうしたとき、`refine` を使うとサブゴールを生成せずにゴールを単に `⊢ Q` に変えることができます。
+-/
+
+example (hP : P) (hQ : ¬ P ∨ Q) : P ∧ Q := by
+  -- `P` が成り立つのは自明なので、`Q` だけ示せばよい
+  refine ⟨by assumption, ?_⟩
+
+  -- ゴールが `⊢ Q` になる
+  guard_target =ₛ Q
+
+  simp_all