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

Answer 1

by_cases「真理値表による証明」にアクセスできます。¬(p → q) → p ∧ ¬qつまり、 4 つのケース (pおよびqtrue、ptrue but qfalse、...)で true であることを確認するだけで証明できます。

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, _)
  )

ここでは 4 つの_引数を入力しませんでしたが、それぞれにカーソルを置くと、ローカル コンテキストが表示されます。この非常に冗長な用語モードが私を夢中にさせるので、それらを記入したくありません。

戦術モード (第 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 をインストールしなくても、これらすべてをオンラインで試すことができます。