# Zulip Chat Archive

## Stream: new members

### Topic: Understanding Contradiction

#### Dev-Indra (Mar 16 2020 at 22:21):

I have read ch.3 of Theorem Proving in Lean and I am currently in ch. 4. I have tried some direct proof tactics in the examples provided and in the Natural Number Game. I am curious how to do the contradiction proofs. Can anyone tell me how contradiction works in lean to get me going?

#### Mario Carneiro (Mar 16 2020 at 22:23):

There is a constant called `classical.by_contradiction`

which has the type `(\not p -> false) -> p`

. That is, if you apply it when your goal is `p`

, then your new goal is `\not p -> false`

, and you can then `assume hnp : \not p`

and proceed to prove `false`

#### Dev-Indra (Mar 16 2020 at 22:28):

I applied `classical.by_contradiction`

within my proof but Lean is giving me an error?! Do I apply it outside of my proof or within?

#### Dev-Indra (Mar 16 2020 at 22:29):

Do I need to import anything too?

#### Daniel Keys (Mar 16 2020 at 22:29):

Here's an example:

lemma andNeg : (¬ P) ∧ (¬ Q) → ¬ ( P ∨ Q ) := begin intro nPnQ, by_contradiction pORq, cases pORq with hp hq, exact nPnQ.left hp, exact nPnQ.right hq end

#### Mario Carneiro (Mar 16 2020 at 22:30):

Note that `by_contradiction`

is also the name of a tactic, that combines the application of the theorem `classical.by_contradiction`

and the `assume`

step into one

#### Mario Carneiro (Mar 16 2020 at 22:31):

@Dev-Indra your comment is too vague to guess what the error is. You should post code

#### Daniel Keys (Mar 16 2020 at 22:32):

You need to `open classical`

or use `classical.by_contradiction`

instead of just `by_contradiction`

.

#### Dev-Indra (Mar 16 2020 at 22:33):

@ **Daniel Keys** Ok I see. I will give it a shot.

@Mario Carneiro . Here was my error message when I just typed `classical.by_contradiction`

within my proof.

type mismatch at application tactic.istep 130 2 130 2 classical.by_contradiction term classical.by_contradiction has type (¬?m_1 → false) → ?m_1 : Prop but is expected to have type tactic ?m_1 : Type ?

#### Mario Carneiro (Mar 16 2020 at 22:34):

you have to type `apply classical.by_contradiction`

#### Mario Carneiro (Mar 16 2020 at 22:34):

because `classical.by_contradiction`

is a theorem, not a tactic

#### Dev-Indra (Mar 16 2020 at 22:34):

So thanks, I see

#### Mario Carneiro (Mar 16 2020 at 22:35):

`by_contradiction`

is a tactic with a similar name, used in Daniel's proof above

#### Mario Carneiro (Mar 16 2020 at 22:35):

but tactics and theorems live in different namespaces

#### Daniel Keys (Mar 16 2020 at 22:37):

I just noticed you're in chapter 4. Tactics are introduced in chapter 5. Sorry I jumped too far ahead.

#### Mario Carneiro (Mar 16 2020 at 22:39):

if you do the NNG then tactics are there from day 1

Last updated: May 14 2021 at 22:15 UTC