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。在应用 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