CODEWITHSUNDEEP
theorem-provinglean
Vox
Vox

Reputation: 323

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

The proof of this basic implication from first principles, an exercise in "Theorem proving in Lean" 4.4, beats all my attempts so far:

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

After the intro I don't know how to use nAxpx to go further. I thought of by_contradiction, but that only introduces the negated existence nExnpx, which can't be used with cases, so I can't produce an x : α. Excluded middle doesn't seem to help either. I can get a proof with mathlib tactics,

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

but don't have enough knowledge to translate that back into tactics mode, so this doesn't help my understanding.

Upvotes: 2

Views: 476

Answers (1)

Christopher Hughes
Christopher Hughes

Reputation: 1129

I think you have to do by_contradiction twice. After apply naXpx try intro a and then by_contradiction. Then you'll have an a a proof of ¬p a, but also a proof that ¬∃ (x : α), ¬p x which is a contradiction.

A full proof is

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

Upvotes: 2

Related Questions