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: Dec 20 2023 at 11:08 UTC