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

Question

"Theorem proving in Lean" 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

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

How can one prove (¬ ∀ x, p x) → (∃ x, ¬ p x) from first principles in LEAN?

theorem-proving

lean