goal contradicts hypothesis - `contradiction` doesn't work

Stream: new members

[rzeta0]

Working through the exercises in MoP from the "law of the excluded middle" section, I have several times come to a goal state that looks like the following:

P : Prop
h : ¬P
⊢ P

How do I resolve this? Using contradiction doesn't work.

This issue came up as an aside from a different discussion and the reply was that this situation should never arise if I'm designing lean proofs properly.

Is that correct - should I backtrack whenever this happens?

[Kyle Miller]

This state isn't a contradiction. In words "given that P is false, prove that P is true". This is not possible to prove in a sound logical system.

Yes, if you get into such a state, you should backtrack.

[rzeta0]

Thanks Kyle

Below is an example of a work-in-progress where this arises. I can't see what I'm doing that is so naughty that it leads to that unresolvable goal-state.

example (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by
  constructor
  · intro g
    by_cases h: P
    · constructor
      · exact h
      · intro f
        have x: P → Q := by rel [h, f]
        contradiction
    · constructor
      · sorry -- < --  problem happens here
      · sorry

  · sorry

[Kyle Miller]

There seems to be more in your context there:

P Q : Prop
g : ¬(P → Q)
h : ¬P
⊢ P

Here's a more refined rule: if you see ¬P as a hypothesis and P as a goal, then there is redundant information. Next step: either clear h or do exfalso to remove the redundancy.

[Kyle Miller]

(exfalso is a good choice)

[rzeta0]

clear and exfalso aren't part of the MoP course (at least up to chapter 4) so I guess backtracking and trying a different path is probably best.

[Kyle Miller]

Why is this redundant? Try doing by_contra in this state. You will get two hypotheses that are ¬P.

[Kyle Miller]

I guess backtracking and trying a different path is probably best.

No, definitely not! There's nothing wrong with a state with redundant information.

[Kyle Miller]

I thought you were talking about literally the state in your original message, which definitely is not possible.

[rzeta0]

I had shorted the goal state in my original question as I thought the additional hypothis g wasn't relevant. my apologies

[Kyle Miller]

Are you opposed to learning clear or exfalso at this point because it's not in the book? They're straightforward: clear deletes a hypothesis, and exfalso replaces the goal with False

[Kyle Miller]

Both clear and exfalso can bring you into an unprovable state, so you need to be prepared to backtrack if necessary. At least it's worth trying them out to see what they do.

[rzeta0]

My preference is to try to complete the exercises using only the tactics we've been taught.

I think doing additional tactics may take our train of thought away from what the teacher is trying to train us to do.

In fact the MoP course disables or weakens certain tactics. eg linarith is completely disabled.

[Daniel Weber]

You can do what you did above, of using have to get P → Q, and then contradiction works

[Mario Carneiro]

I think this is not the first time you have asked this question

[rzeta0]

Thanks Mario - your memory is better than mine.

[rzeta0]

Daniel Weber said:

You can do what you did above, of using have to get P → Q, and then contradiction works

I'm not seeing how to get P → Q from the current goal state - I'll keep trying.

P Q : Prop
g : ¬(P → Q)
h : ¬P
⊢ P ∧ ¬Q

[Daniel Weber]

Try intro and see the new state

[Edward van de Meent]

have : P -> Q := hp => h hp |>.elim

[rzeta0]

Daniel Weber said:

Try intro and see the new state

intro k at the following goal state fails

P Q : Prop
g : ¬(P → Q)
h : ¬P
⊢ P ∧ ¬Q

If I use constructor as we usually when the goal is a conjunction, intro has no effect on the following goal state:

P Q : Prop
g : ¬(P → Q)
h : ¬P
⊢ P

[rzeta0]

Edward van de Meent said:

have : P -> Q := hp => h hp |>.elim

Thank Edward but these are too advanced for the course we're doing.

[Mario Carneiro]

start by exfalso, then apply g

[rzeta0]

Thanks Mario - but as mentioned above, I'd like to only use the tactics the course has introduced.

The main reason is that I think the author of MoP is trying to train our brains to think in a specific way and more advanced tactics may circumvent that. For example linarith is disabled in MoP.

[Mario Carneiro]

why are we playing games with the tactics list here? You need to define the problem better

[Mario Carneiro]

what tactics do you want to use?

[Daniel Weber]

rzeta0 said:

Daniel Weber said:

Try intro and see the new state

intro k at the following goal state fails

P Q : Prop
g : ¬(P → Q)
h : ¬P
⊢ P ∧ ¬Q

If I use constructor as we usually when the goal is a conjunction, intro has no effect on the following goal state:

P Q : Prop
g : ¬(P → Q)
h : ¬P
⊢ P

I meant inside have : P → Q := by intro; -- here

[Mario Carneiro]

exfalso and apply are not advanced tactics

[Mario Carneiro]

in fact, I suggested those because they are typical of tactics in the shortlist of an introductory course

[Mario Carneiro]

I'm not taking your course so you have to be more specific

[rzeta0]

I think I've taken lots of advice, kindly given.

I'll gp away and ponder on this myself for a while, maybe do the later exercises and come back to this one.

Thanks again everyone for trying to help.

[Dan Velleman]

A few comments:

The contradiction tactic looks for a contradiction among the hypotheses. A hypothesis that contradicts the goal doesn't count. Yes, it's a little unusual to have a hypothesis that contradicts the goal, but there's nothing wrong with it, and there's no need to do anything about it. It can even happen that a hypothesis h : ¬P can be useful for proving the goal P -- I'll give a short example below.

I think MoP introduces proof by contradiction as a method of proving a goal of the form ¬P: you assume P and derive a contradiction. That is a common use of proof by contradiction, but it's not the only one. You can also use proof by contradiction to prove a positive statement: you can prove P by assuming ¬P and deriving a contradiction. To do that, I would suggest a tactic that, as far as I can tell, is not covered in MoP. If your goal is P, then the tactic by_contra h adds the hypothesis h : ¬P and sets the goal to be False. By the way, if your goal is ¬P, then by_contra h will add the hypothesis h : P and set the goal to be False. So by_contra works for both kinds of proof by contradiction (proving a negative statement or a positive statement), whereas the approach used in MoP works only for one kind (proving a negative statement). I'm not sure why Heather chose to teach the more limited approach to proof by contradiction in MoP. I prefer to use by_contra for both kinds.

Why would you use proof by contradiction for a positive goal? Well, one reason is that it gives you a way to use a negative hypothesis. In your proof, after intro g you have g  : ¬(P → Q). Remember that in Lean that means (P → Q) → False. So if your goal is False (as it is if you're doing a proof by contradiction), then apply g will change the goal to P → Q. I have rewritten your proof a bit, using this idea:

import Mathlib.Tactic

example (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by
  constructor
  · intro g
    by_cases h: P
    · constructor
      · exact h
      · by_contra f    --(1)
        apply g
        intro x
        exact f
    · by_contra f      --(2)
      apply g
      sorry
  · sorry

Starting at the line labeled (1), I have changed your proof. I replaced intro f with by_contra f, which has exactly the same effect. I followed that with apply g, as described above.

Starting at the line labeled (2), I have completely changed your approach. Again, I have done by_contra f followed by apply g -- even though the goal at this point is not a negative statement. I'll leave it to you to see how to finish it off.

Finally, here is my example of a proof in which a hypothesis ¬P is useful for proving the goal P.

import Mathlib.Tactic

example (P : Prop) (h : ¬P → P) : P := by
  by_cases g : P
  · exact g
  · exact h g

[Dan Velleman]

By the way, in my rewrite of your proof, there are some redundant hypotheses. There's nothing wrong with that. If you want to learn how to eliminate or avoid those redundancies by using clear or exfalso, you can, but for a beginner, I wouldn't put that high on my list of things to learn.

[rzeta0]

@Dan Velleman .. having read and t thought about your explanation of by_contra I too can't see why that isn't used as the first tactic introduced for proof by contradiction. It has the benefit of negating any goal, as you say, and it also means you don't need to lean about using intro which is introduced with quantifiers....

I also want to check my thinking on positive goals. A positive goal P is ¬¬P and so we can think of it as a negation of ¬P and so assume ¬P and aim to show a contradiction. Is that correct? I'm asking as in my mind there's nothing special about a positive goal, it is just the negation of the negation.

Anyway I will try a little longer to see if I can find a solution using only MoP's tactics - then give up, in the light the very string case you made for by_contra.

[rzeta0]

(and thank you for taking the time to write all that - it was extremely helpful)

[rzeta0]

(( in fact I'm considering changing the educational example I wrote a blog for and did a YouTube video for - from intro to by_contra ))

[Dan Velleman]

rzeta0 said:

A positive goal P is ¬¬P and so we can think of it as a negation of ¬P and so assume ¬P and aim to show a contradiction. Is that correct?

Yes, you could look at it that way. My distinction between positive and negative statements was somewhat informal. I just meant "it doesn't start with ¬." But as you say, a positive statement can be rewritten as an equivalent negative statement by using a double negative. And sometimes a negative statement can be rewritten as an equivalent positive statement by using push_neg.

Here's an application of your idea: If your goal is P, then you can get the effect of by_contra h by doing apply not_not.mp, which will change the goal to ¬¬P, followed by intro h. So you can do proof by contradiction with a positive goal using only tactics introduced in MoP. But it seems easier to use by_contra.

[rzeta0]

I have now solved this using by_contra, but I think I will revisit it to see if there was a clever way that the MoP author intended us to do it.

From this thread I have learned that I can apply a hypothesis ¬P to a False goal to get a goal P which can be useful.