how to prove false

Stream: general

[Formally Verified Waffle Maker]

What does it mean in Lean to prove

⊢ false

I am guessing that it means showing that two hypotheses contradict, but I have no idea how to do this in Lean.

[Kevin Buzzard]

There's not one golden rule which says how to prove something. Blame Gödel.

[Kenny Lau]

#mwe

[Kenny Lau]

I mean, at least include the whole context ("context" means all the hypotheses and the goals in the error message)

[Damiano Testa]

Often, you can apply a "negative statement" to convert the false to the corresponding "positive statement". If one of your hypotheses is h : 0 ≠ 0, then apply h will convert the false into a 0 = 0. Hope that this helps!

[Rémy Degenne]

to cite section 3.3.3 of Theorem Proving in Lean: "Negation, ¬p, is actually defined to be p → false, so we obtain ¬p by deriving a contradiction from p. Similarly, the expression hnp hp produces a proof of false from hp : p and hnp : ¬p. "

[Ruben Van de Velde]

Or if you have hp and hnp as hypotheses, contradiction should find them.

[Filippo A. E. Nuccio]

You can have a look at the file logic.lean where many of the "basic" logical implications are coded. For instance, you have
lemma elim (h : a ≠ b) : a = b → false := h
showing that if you have proven h : a ≠ b and you have somewhere in your proof h1 : a = b, then elim h h1 (or rather ne.elim h h1) produces false.

Similarly, you have

lemma iff_false_intro (h : ¬a) : a ↔ false :=
iff.intro h (false.rec a)

which allows you to deduce false by applying the (modus ponens) of this lemma iff_false_intro to two hypotheses h : ¬a and h2 : a namely by writing (iff_false_intro h).mp h2 (or apply (iff_false_intro h).mp h2 if you're in tactic mode).

Finally (but there might be more examples) there is also

/-- We can't have `a` and `¬a`, that would be absurd!-/
@[inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
false.rec b (h₂ h₁)

(with the nice description above): it says that from a and ¬a everything can be deduced, including false. So, you can also prove false from h and h2 : ¬h by apply absurd h h2.

[Yakov Pechersky]

In this case of apply absurd h h2 I would rather say exact absurd h h2 because there is not an application there, but rather the complete statement.

[Filippo A. E. Nuccio]

Right!

[Mario Carneiro]

golfer protip: cases h2 h

[Kevin Buzzard]

This way your one goal is replaced by a goal for each case. But there are no cases :-)

[Ruben Van de Velde]

cases h h2?

[Kevin Buzzard]

Filippo's post seems to contain both conventions.