example : ¬(p → q) → p ∧ ¬q

Stream: new members

[Eduardo Cavazos]

Question posted to stackoverflow:

https://stackoverflow.com/q/58577206/268581

Thanks for any suggestions!

[Kevin Buzzard]

I posted a suggested answer.

[Eduardo Cavazos]

Based on Kevin's suggestion, here's what I have so far:

example : ((p → q) → false) → p ∧ (q → false) :=

    (assume hpqf : (p → q) → false,

        by_cases

            (assume hp : p,

                by_cases

                    (assume hq : q, and.intro hp (λ hq' : q, hpqf (λ hp' : p, hq)))

                    (assume hqf : q → false, and.intro hp hqf))

            (assume hpf : p → false,

                by_cases

                    (assume hq : q, false.elim (hpqf (λ hp : p, hq)))

                    (assume hqf : q → false, _

                        -- and.intro hp hqf                         But we don't have hp.

                        -- false.elim (hpqf (λ hp : p, hq))         But we don't have hq.

                    )))

The first three cases appear to be complete.

In the last case, we have the following:

hpqf : (p → q) → false,
hpf : p → false,
hqf : q → false

As the inline comments above say, one option is:

and.intro hp hqf -- But we don't have hp.

Another option is:

false.elim (hpqf (λ hp : p, hq)) -- But we don't have hq.

Should I aim for the and.intro ... approach? Or the false.elim ... approach? Or something entirely different? :-)

Thanks for your help so far!

Hang on... I think I see it...

[Eduardo Cavazos]

OK, this seems to work:

example : ((p → q) → false) → p ∧ (q → false) :=

    (assume hpqf : (p → q) → false,

        by_cases

            (assume hp : p,

                by_cases

                    (assume hq : q, and.intro hp (λ hq' : q, hpqf (λ hp' : p, hq)))

                    (assume hqf : q → false, and.intro hp hqf))

            (assume hpf : p → false,

                by_cases

                    (assume hq : q, false.elim (hpqf (λ hp : p, hq)))

                    (assume hqf : q → false,

                        false.elim (hpqf (λ hp : p, false.elim (hpf hp))))))

[Eduardo Cavazos]

Thanks for your help @Kevin Buzzard !!!

[Kevin Buzzard]

import tactic.tauto
variables (p q : Prop)
open classical
def XYZ : ¬(p → q) → p ∧ ¬q := by tauto!

#print XYZ
/-
  def XYZ : ∀ (p q : Prop), ¬(p → q) → p ∧ ¬q :=
  λ (p q : Prop) (a : ¬(p → q)),
  and.dcases_on (not_imp.mp a) (λ (a_left : p) (a_right : ¬q), ⟨eq.mpr rfl a_left, eq.mpr rfl a_right⟩)
  -/

[Kevin Buzzard]

There's a super-short term mode proof, using stuff in the mathlib library which is not covered by Theorem Proving In Lean.

[Kevin Buzzard]

I do understand that you're learning this stuff so in some sense these answers are not useful, but I thought it was worth emphasizing how many ways there are to solve this problem, and what is available to you in Lean's maths library. In fact looking at the proof which tauto! finds I see that we can just do this:

import logic.basic
variables (p q : Prop)
local attribute [instance, priority 10] classical.prop_decidable
example : ¬(p → q) → p ∧ ¬q := not_imp.mp

[Eduardo Cavazos]

@Kevin Buzzard ,

These more advanced answers are very useful! Indeed, I'm interested in the various approaches. Yes, it's true that I'm currently focused on the "finger exercises" approach, but it's nice to know that exotic islands await.

[Kenny Lau]

import logic.basic
variables (p q : Prop)
example : ¬(p → q) → p ∧ ¬q := _
-- OK let's intro everything
example : ¬(p → q) → p ∧ ¬q := λ hnpq, _
-- The goal is ∧ so let's use and.intro
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨_, _⟩
-- I can't prove p directly, so let's try contradiction
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, _, _⟩
-- The only non-trivial step is to apply hnpq
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq _, _⟩
-- The goal is → so let's intro everything
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, _, _⟩
-- Oh I see a contradiction already: ¬p and p. I remember that's either hnp.elim hp or (hnp hp).elim
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, hnp.elim hp, _⟩
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, (hnp hp).elim, _⟩
-- I'll just use the first one. Now the goal is ¬, so let's intro.
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, hnp.elim hp, λ hq, _⟩
-- The only non-trivial step is to apply hnpq
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, hnp.elim hp, λ hq, hnpq _⟩
-- The goal is → so I intro.
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, hnp.elim hp, λ hq, hnpq $ λ hp, _⟩
-- The goal is in the assumptions.
example : ¬(p → q) → p ∧ ¬q := λ hnpq, ⟨classical.by_contradiction $ λ hnp, hnpq $ λ hp, hnp.elim hp, λ hq, hnpq $ λ hp, hq⟩

[Kenny Lau]

I commentate my thoughts as I fill in the solution @Eduardo Cavazos

[Kenny Lau]

I'm sure @Kevin Buzzard thinks the same way

[Scott Morrison]

I would probably do the same steps as Kenny, but in tactic mode. Perhaps at the end I'd then have an extra step golfing it back into term mode, if I care enough.

[Scott Morrison]

I find tactic mode much more pleasant. :-)

[Kevin Buzzard]

For basic logic stuff like this I can see the appeal of term mode.

[Kevin Buzzard]

One thing I've only learned relatively recently is that for these goals which are not provable constructively, one powerful trick is just to apply classical.by_contradiction whenever you're stuck.

[Kevin Buzzard]

variables (p q : Prop)
example : (¬ q → ¬ p) → (p → q) := λ hnqnp hp, _ -- stuck
example : (¬ q → ¬ p) → (p → q) := λ hnqnp hp, classical.by_contradiction _ -- I can do the rest in my head now

[Kenny Lau]

I see that you've internalized constructivism :P

[Kevin Buzzard]

I've internalised precisely how to avoid the problems it gives you.

[Eduardo Cavazos]

Thanks for that illustration @Kenny Lau! I hadn't used logic.basic yet. It caused me to see that I didn't even have mathlib installed yet. I do now, and I've worked through your example. Thanks!