From 8097b742da6aea1850bf5cf83957f735d8f88792 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 1 Nov 2023 22:49:29 +0900 Subject: [PATCH] =?UTF-8?q?push=5Fneg=20=E3=81=AE=E3=82=B3=E3=83=BC?= =?UTF-8?q?=E3=83=89=E4=BE=8B=E3=82=92=E3=81=9D=E3=81=AE=E3=81=BE=E3=81=BE?= =?UTF-8?q?=E5=AE=9F=E8=A1=8C=E3=81=A7=E3=81=8D=E3=82=8B=E5=BD=A2=E5=BC=8F?= =?UTF-8?q?=E3=81=AB=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/PushNeg.lean | 35 ++++++++++++++++++++++++++++------- src/push_neg.md | 14 +++----------- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/Examples/PushNeg.lean b/Examples/PushNeg.lean index a501f597..16583226 100644 --- a/Examples/PushNeg.lean +++ b/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 \ No newline at end of file diff --git a/src/push_neg.md b/src/push_neg.md index 12607711..fa084e6e 100644 --- a/src/push_neg.md +++ b/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` としたりします. \ No newline at end of file