tauto のページの校正

Author: Seasawher

LeanByExample/Tactic/Tauto.lean

@@ -4,7 +4,7 @@
 import Aesop -- `aesop` を使うため --#
 import Mathlib.Tactic.Tauto -- `tauto` を使うのに必要
 
-namespace Tauto --#
+section --#
 
 variable (P Q R : Prop)
 
@@ -20,23 +20,28 @@ example : (P → (Q → R)) → ((P → Q) → (P → R)) := by
 example : (P ↔ ¬ P) → False := by
   tauto
 
-/- `tauto` が扱えるのは命題論理の範囲で記述できる命題だけです。述語論理における恒真な式は、ごく簡単なものであっても `tauto` で示せないことがあります。-/
+end --#
+/- `tauto` が扱う対象の「トートロジー」は、命題論理の範囲で記述できるものに限ります。述語論理における恒真な式は、`tauto` で示せないことがあります。-/
 
-variable (α : Type) (S : α → Prop)
-
-example : ¬(∀ x, S x) → (∃ x, ¬ S x) := by
+example (α : Type) (S : α → Prop) : ¬(∀ x, S x) → (∃ x, ¬ S x) := by
   -- `tauto` では示せない
   fail_if_success tauto
 
   aesop
 
-/- また、排中律を使わずに示せる命題であっても、`tauto` は排中律を使って示してしまうことがあります。直観主義論理の枠内で命題を示すには、代わりに[`itauto`](./Itauto.md)を使用してください。-/
+example (Q : Prop) : ∀ (P : Prop), P → (Q → P) := by
+  -- これは量化子を含むが、`tauto` でも示すことができる。
+  tauto
+
+/- ## 排中律
+
+排中律を使わずに示せる命題であっても、`tauto` は排中律を使って示してしまうことがあります。直観主義論理の枠内で命題を示すには、代わりに [`itauto`](./Itauto.md) タクティクを使用してください。-/
 
 /-- 命題とその否定は同値ではない -/
 theorem not_neg_iff {P : Prop} : ¬ (P ↔ ¬ P) := by tauto
 
 -- 選択原理を使っているが、これは排中律を使っているため
-/-- info: 'Tauto.not_neg_iff' depends on axioms: [propext, Classical.choice, Quot.sound] -/
+/-- info: 'not_neg_iff' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms not_neg_iff
 
 -- 実際には排中律は必要ない
@@ -49,7 +54,5 @@ theorem not_neg_iff' {P : Prop} : ¬ (P ↔ ¬ P) := by
   have hp : P := by rwa [← h] at hnp
   contradiction
 
-/-- info: 'Tauto.not_neg_iff'' depends on axioms: [propext] -/
+/-- info: 'not_neg_iff'' depends on axioms: [propext] -/
 #guard_msgs in #print axioms not_neg_iff'
-
-end Tauto --#