如何从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