在精益中证明 A → ¬ (¬ A ∧ B)答案

【问题标题】：Proving A → ¬ (¬ A ∧ B) in Lean在精益中证明 A → ¬ (¬ A ∧ B)
【发布时间】：2021-11-13 17:57:50
【问题描述】：

我很难用精益定理证明器证明 A → ¬ (¬ A ∧ B)。我是这样设置的：

example : A → ¬ (¬ A ∧ B) :=
assume h1: ¬ (¬ A ∧ B),
assume h2: A,
assume h3: B,
show false, from sorry

我无法找到证明这种否定的例子。任何解决此问题的帮助将不胜感激。

【问题讨论】：

标签： proof theorem-proving negation lean

【解决方案1】：

你写的东西在我看来很奇怪，因为你的目标是证明某事不暗示（不是 A 和 B），而你的第一行似乎假设正是这个。我猜你的代码的第一行甚至没有编译。请注意，最好发布完整的工作代码（现在如果我剪切并粘贴此代码块，那么我会收到 Lean 不知道 A 或 B 是什么的错误）。

如果您正在学习如何使用精益中的定理证明来做这些事情，而您还没有读到第 5 章，我建议您直接跳过那里并了解战术模式。战术模式可以帮助您准确地了解您的假设以及您要证明的内容。这是您在战术模式下的示例的证明：

example (A B : Prop) : A → ¬ (¬ A ∧ B) :=
begin
  intro hA, -- proof of A
  intro h1, -- proof of (not A and B)
  cases h1 with hnA hB, -- take h1 apart
  apply hnA, -- recall that "not A" is defined to mean "A implies false"
  exact hA,
end

如果您在 VS Code 信息视图中逐行单击，您将能够看到发生了什么。

当然，您也可以在术语模式下证明这一点。你甚至可以避免所有assume 的东西（assume 只是函数式编程λ 的语法糖）并立即写下术语证明：

example (A B : Prop) : A → ¬ (¬ A ∧ B) :=
λ hA ⟨hnA, hB⟩, hnA hA

【讨论】：