lean - TPIL 3.6：示例：¬(p → q) → p ∧ ¬q

Answer 1

by_cases使您可以访问“真值表证明”。换句话说，我们可以¬(p → q) → p ∧ ¬q通过在四种情况下检查它的真实性来证明（p和q真，p真但q假，......）。

variables (p q : Prop)
open classical
example : ¬(p → q) → p ∧ ¬q :=
λ h, by_cases
  (assume hp : p, 
    by_cases
    (assume hq : q, _)
    (assume hnq : ¬ q, _) 
  )
  (assume hnp : ¬ p, 
    by_cases
    ( assume hq : q, _)
    (assume hnq : ¬ q, _)
  )

这里我没有填写四个_参数，但是将光标放在每个参数上都会显示本地上下文。我不想填写它们，因为这种超级冗长的术语模式让我发疯。

在战术模式中（在第 5 章中介绍），你可以像这样完整地拼出它：

import tactic.interactive

variables (p q : Prop)
open classical
example : ¬(p → q) → p ∧ ¬q :=
begin
  intro hnpq,
  classical,
  by_cases hp : p; by_cases hq : q; split;
  -- 8 goals (replace previous semicolon by a comma to see this)
  try {assumption}, -- four left
  { intro h, apply hnpq, intro h', assumption},
  { exfalso, apply hnpq, intro h, assumption},
  { intro h, apply hnpq, intro h', assumption},
  { exfalso, apply hnpq, intro h', exfalso, apply hp, assumption}
end

但实际上我会这样做：

import tactic.tauto
variables (p q : Prop)
example : ¬(p → q) → p ∧ ¬q := by tauto!

您可以在线尝试所有这些，甚至无需安装 Lean。