问在精益生产中证明A→(-A∧B)

EN

你写的东西在我看来很奇怪，因为你的目标是证明某些东西并不意味着什么(而不是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 infoview中从一行单击到另一行，您将能够看到发生了什么。

当然，您也可以在term模式中证明这一点。您甚至可以避免所有的证明内容(assume只是函数式编程λ的语法糖)，并立即写下术语assume：

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