How to write a proof by contradiction?

Stream: new members

[Philip B.]

Hi. In Natural numbers game: Advanced multiplication world level 2 my goal is

a b : mynat,
h : a * b = 0
⊢ a = 0 ∨ b = 0

I would like to assume ¬(a = 0 ∨ b = 0) and show that both cases (a = 0 and b = 0) lead to a contradiction. But I can't figure out how to assume ¬(a = 0 ∨ b = 0).

In Proposition world level 8 I had to prove lemma contrapositive (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) which seems related, but I don't know how to use it here.

Just in case, I know that instead of doing such a proof by contradiction, I could consider 4 cases and solve them all. But instead I want to just do a proof by contradiction because 1. that seems the most natural way to me; 2. I want to know how it's done in Lean.

[Kevin Buzzard]

I don't understand what you want to do. If you're trying to prove a=0 or b=0, you can't assume it.

[Philip B.]

@Kevin Buzzard I want to assume ¬(a=0∨b=0), a*b=0 and derive a contradiction. (Sorry, I forgot the negation symbol in my message)

[Kevin Buzzard]

Oh sorry, I misread. You could try by_contra h, I guess. Is that in NNG?

[Philip B.]

I haven't encountered by_contra yet.

[Kevin Buzzard]

There are many many tactics

[Kevin Buzzard]

I only explain an extremely small number of them in NNG

[Kevin Buzzard]

(about ten)

[Kevin Buzzard]

v https://leanprover-community.github.io/mathlib_docs/tactics.html

[Philip B.]

Alright. Then I guess I'll finish NNG without extra tactics and will learn about them later.

[Kevin Buzzard]

Mathematicians have a very classical idea about proof by contradiction; in constructive mathematics about 50% of the things we think of as "proof by contradiction" are not really proofs by contradiction. For example we say "sqrt(2) is irrational -- proof by contradiction. Assume it's rational...". But the definition of rational is "not rational", and in constructive maths the definition of "not X" is "X implies false", so you can see that actually this isn't a proof by contradiction at all.

[Kevin Buzzard]

It is a proof which at some point involves trying to prove something false -- but constructively this doesn't mean a proof by contradiction. In the proof of P->Q -> (not Q -> not P) the goal can be false in the middle and then something else later.

[Chris Wong]

The cases and exfalso tactics will come in handy here.

[Kenny Lau]

you don't need any of those. this theorem can be constructively proved

[Chris Wong]

I assume you mean by_contra? cases and exfalso are constructive last time I checked... :laughing:

[Kenny Lau]

nvm