我如何在精益中证明这一点？ p ∨ ¬p答案

【问题标题】：How do I prove this in Lean? p ∨ ¬p我如何在精益中证明这一点？ p ∨ ¬p
【发布时间】：2021-05-03 14:16:35
【问题描述】：

我有一个关于精益的定理要证明，

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B)

为了证明，我想，我需要使用，

or.elim (B ∨ ¬B) (assume b: B, ...) (assume nb:¬B, ...)

为此，我必须再次证明

B v ¬B

那么，我该如何进行呢？有没有更好的方法？

【问题讨论】：

标签： logic lean

【解决方案1】：

p v ¬p 是来自名为classical.em 的核心库的引理。

【讨论】：

【解决方案2】：

import tactic

variables (A B : Prop)

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B) := by tauto!

【讨论】：