Zulip Chat Archive

Stream: new members

Topic: Understanding Contradiction


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Dev-Indra (Mar 16 2020 at 22:29):

Do I need to import anything too?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Daniel Keys (Mar 16 2020 at 22:32):

You need to open classical or use classical.by_contradiction instead of just by_contradiction.

view this post on Zulip 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 ?

view this post on Zulip Mario Carneiro (Mar 16 2020 at 22:34):

you have to type apply classical.by_contradiction

view this post on Zulip Mario Carneiro (Mar 16 2020 at 22:34):

because classical.by_contradiction is a theorem, not a tactic

view this post on Zulip Dev-Indra (Mar 16 2020 at 22:34):

So thanks, I see

view this post on Zulip Mario Carneiro (Mar 16 2020 at 22:35):

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

view this post on Zulip Mario Carneiro (Mar 16 2020 at 22:35):

but tactics and theorems live in different namespaces

view this post on Zulip 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.

view this post on Zulip 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