Explanation of the following proof

Stream: new members

[Andrew Lubrino]

Hi everyone. I'm working through the below proof:

variable  U : Type
variables A B C : U → Prop

example : (¬ ∃ x, A x) → ∀ x, ¬ A x :=
assume h₁ : ¬ ∃ x, A x,
assume x,
assume h₂ : A x,
have h₃ : ∃ x, A x, from exists.intro x h₂,
show false, from h₁ h₃

I typed this out, but don't understand it. I've managed to pull together enough examples and pushed around enough variables to eventually get to a proof that the computer accepted. Why are we allowed to assume and x : U and then assume A x? Are we always allowed to assume x and A x for "free" in predicate logic proofs?

Also, why does showing false prove this theorem? This is another piece that is very confusing to me.

[Eric Wieser]

¬A x (docs#not) is defined as A x → false - does that resolve the last confusion?

[Henrik Böving]

Your confusion seems to be not about this entire statement but rather about the ∀ x, ¬ A x part. What this means is that for an arbitrary x the predicate A does not hold, so in order to proof this we assume that x is some arbitrary value and then have to show that ¬ A x holds for this specific x. As Eric pointed out the definition of negation in Lean is that assuming the statement leads to false so if we want to prove the negation we do exactly that, assume it and base on this information prove false.

[Andrew Lubrino]

Okay. I think that makes a lot more sense now. Are there any general heuristics for proving universals (so the universal is in the goal) with Lean? Should they always be in the form "assume x, assume A x, prove whatever else there is..."

Thanks for the responses here.

[Henrik Böving]

I could think of three ways to prove a universal:

1. Use some other lemma that gives you the statement
2. As you said, assume an arbitrary x and then prove the inner statement
3. using docs#false.elim which will change your goal from whatever it is right now to proving falsebased on your current assumptions.

But in the beginning stages you will most likely be perfectly fine with just using 2.

[Andrew Lubrino]

Got it. Thank you!