push_neg のコード例をそのまま実行できる形式に修正

Examples/PushNeg.lean

@@ -3,21 +3,43 @@ import Mathlib.Tactic.Linarith
 
 variable (P Q : Prop)
 
--- ANCHOR: first
+/-! ## push_neg -/
+
 example (h: P → Q) : ¬ (P ∧ ¬ Q) := by
   -- ドモルガン則を適用して，`¬` を内側に押し込む
   push_neg
 
-  -- `¬` を内側に押し込んだ結果，`¬ P ∨ Q` が得られる
-  -- これは `P → Q` と同値
+  -- デフォルトの設定だと `P → Q` に変形される
   show P → Q
 
   exact h
--- ANCHOR_END: first
 
+/-!
+  ## use_distrib
+
+  option で `push_neg.use_distrib` を `true` にすると，
+  `¬ (p ∧ q)` を `¬ p ∨ ¬ q` に変形する．
+-/
+
+set_option push_neg.use_distrib true
+
+example (h: P → Q) : ¬ (P ∧ ¬ Q) := by
+  -- ドモルガン則を適用して，`¬` を内側に押し込む
+  push_neg
+
+  -- goal が論理和の形になる
+  show ¬ P ∨ Q
+
+  -- 場合分けで示す
+  by_cases hP : P
+  · right
+    exact h hP
+  · left
+    assumption
+
+/-! ## 量化子に対して使った場合 -/
 
--- ANCHOR: all_exists
-example : ¬ ∃ x : Int , ∀ y : Int, (x + y = 0) := by
+example : ¬ ∃ (x : ℤ), ∀ (y : ℤ), (x + y = 0) := by
   -- ドモルガン則を適用して，`¬` を内側に押し込む
   push_neg
 
@@ -27,4 +49,3 @@ example : ¬ ∃ x : Int , ∀ y : Int, (x + y = 0) := by
   intro x
   exists (- x + 1)
   linarith
--- ANCHOR_END: all_exists

src/push_neg.md

@@ -1,23 +1,15 @@
 # push_neg
 
-needs: `import Mathlib.Tactic.PushNeg`
-
 named after: 押し込む(push) 否定(negation)
 
-`push_neg` はドモルガン則を使って，否定を式の中に押し込みます．たとえば
+`push_neg` はドモルガン則を使って，否定を式の中に押し込みます．デフォルトの設定だと, たとえば
 
 * `¬ (P ∧ Q)` は `P → ¬ Q` に，
 
 * `¬ ∀ x, P x` は `∃ x, ¬ P x` に
 
-という調子で変形します．[^impl]
+という調子で変形します．
 
 ```lean
-{{#include ../Examples/PushNeg.lean:first}}
+{{#include ../Examples/PushNeg.lean}}
 ```
-
-```lean
-{{#include ../Examples/PushNeg.lean:all_exists}}
-```
-
-[^impl] モードによって `¬ (P ∧ Q)` を `P → ¬ Q` としたり，`¬ P ∨ ¬ Q` としたりします．