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

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