theorem-proving - 如何从 LEAN 中的第一原理证明 (¬∀ x, p x) → (∃ x, ¬ p x)？

Question

第一性原理的这种基本含义的证明，“精益定理证明”4.4 中的一个练习，击败了我迄今为止的所有尝试:

open classical
variables (α : Type) (p q : α → Prop)
variable a : α

local attribute [instance] classical.prop_decidable
theorem T08R : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    intro nAxpx, 
    --by_contradiction nExnpx,
    --apply nAxpx,
end

后 intro不知道怎么用 nAxpx走得更远。我想到了 by_contradiction ，但这只会引入否定存在 nExnpx ，不能与 cases 一起使用，所以我无法生成 x : α .排除的中间似乎也没有帮助。我可以用 mathlib 得到证明策略，

theorem T08R : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    push_neg,
    tauto
end

但没有足够的知识将其转换回战术模式，所以这无助于我的理解。

Answer 1

我想你必须做by_contradiction两次。后 apply naXpx试试 intro a然后 by_contradiction .然后你会有一个 a ¬p a的证明，也证明了¬∃ (x : α), ¬p x这是一个矛盾。

一个完整的证明是

theorem T08R : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    intro nAxpx, 
    by_contradiction nExnpx,
    apply nAxpx,
    assume a,
    by_contradiction hnpa,
    apply nExnpx,
    existsi a,
    exact hnpa,
end