时间戳

首页 > 解决方案 > 在精益中证明 A → ¬ (¬ A ∧ B)

proof - 在精益中证明 A → ¬ (¬ A ∧ B)

问题描述

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

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

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

标签： prooftheorem-provingnegationlean

解决方案

你写的东西在我看来很奇怪，因为你的目标是证明某事不暗示（不是 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

推荐阅读