萩原先生から出題された課題(脳トレ)を解いてみた.
import Mathlib.Tactic
section
variable (A : Prop)
example : ¬ (A ↔ ¬ A) := by
intro (h : A ↔ ¬ A)
have h1 : A → ¬ A := h.mp
have h2 : ¬ A → A := h.mpr
have h3 : (A → ¬ A) → ¬ A := by
intro (hana : A → ¬ A) (ha : A)
apply hana ha
apply ha
have ha : A := h2 (h3 h1)
have hna : ¬ A := h1 ha
exact hna ha
end
-- 以下の飛び道具(定理)を使った別解
-- imp_not_self {a : Prop} : a → ¬a ↔ ¬a
-- not_imp_self {a : Prop} : ¬a → a ↔ a
section -- 2023-10-30
variable (A : Prop)
example : ¬ (A ↔ ¬ A) := by
intro (h : A ↔ ¬ A)
have h1 : A → ¬ A := h.mp
have h2 : ¬ A → A := h.mpr
simp only [imp_not_self, not_imp_self] at h1 h2 -- (h1 : ¬ A) (h2 : A) にする.
exact h1 h2
end
Leave a Reply