From ae99e296cff3ba8f97ecaa6625a9578b95edfe77 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Fri, 25 Oct 2024 05:08:11 +0900 Subject: [PATCH] =?UTF-8?q?tauto=20=E3=82=BF=E3=82=AF=E3=83=86=E3=82=A3?= =?UTF-8?q?=E3=82=AF=E3=81=AE=E8=AA=AC=E6=98=8E=E3=81=A7=E3=80=81=E5=91=BD?= =?UTF-8?q?=E9=A1=8C=E8=AB=96=E7=90=86=E3=82=92=E5=BC=B7=E8=AA=BF=E3=81=99?= =?UTF-8?q?=E3=82=8B=20Fixes=20#964?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Tactic/Tauto.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Reference/Tactic/Tauto.lean b/LeanByExample/Reference/Tactic/Tauto.lean index 4049089c..0d9b2b0c 100644 --- a/LeanByExample/Reference/Tactic/Tauto.lean +++ b/LeanByExample/Reference/Tactic/Tauto.lean @@ -17,10 +17,10 @@ example : (P → (Q → R)) → ((P → Q) → (P → R)) := by tauto -- 否定と同値なら矛盾 -example : (P ↔ ¬ P) → false := by +example : (P ↔ ¬ P) → False := by tauto -/- `tauto` はすべてのトートロジーを示せるわけではありません。ごく簡単なトートロジーの中にも `tauto` で示せないものがあります。-/ +/- `tauto` が扱えるのは命題論理の範囲で記述できる命題だけです。述語論理における恒真な式は、ごく簡単なものであっても `tauto` で示せないことがあります。-/ variable (α : Type) (S : α → Prop)