如何在Lean定理证明器中证明逻辑命题A → ¬ (¬ A ∧ B)

现有代码问题 #

你目前的假设顺序完全不符合命题的逻辑结构：你要证明的目标是A → ¬ (¬ A ∧ B)，根据否定命题的定义¬P = P → False，这个目标等价于A → (¬A ∧ B) → False，你一开始就假设了要证明的否定结论¬ (¬ A ∧ B)，属于循环假设，自然无法完成证明。

正确证明步骤 #

• 第一步：假设命题前件A成立，记为hA
• 第二步：要证明¬ (¬A ∧ B)，即假设¬A ∧ B成立，记为h
• 第三步：从合取命题h中分别提取出¬A和B两个子证明
• 第四步：此时你同时持有A和¬A的证明，二者应用即可得到矛盾False，完成证明

完整可运行代码 #

术语模式写法 #

example : A → ¬ (¬ A ∧ B) :=
assume hA : A,          -- 假设前件A成立
assume h : ¬ A ∧ B,     -- 假设否定式的前件(¬A ∧ B)成立，对应¬的展开逻辑
have h_notA : ¬ A := h.left,  -- 取出合取式左支¬A
show false, from h_notA hA    -- ¬A作用在A的证明上得到矛盾

Tactic模式写法 #

example : A → ¬ (¬ A ∧ B) :=
begin
  intro hA,
  intro h,
  cases h with h_notA hB,
  exact h_notA hA,
end

如果不需要显式标注中间步骤，直接用自动 tactic 也可以一步完成：

example : A → ¬ (¬ A ∧ B) := by tauto!

内容的提问来源于stack exchange，提问作者Lina Nguyen