## Stream: new members

#### 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,
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
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

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