Shorter proof?

Stream: new members

[Martin C. Martin]

The following simple tautology seems like it should have a short proof, but the best I could come up with is quite long. Is there a shorter or more readable, more direct way to prove it?

variables p q : Prop
open classical
example : ¬(p → q) → p ∧ ¬q := assume hnotpimpliesq,
  or.elim (em p)
    (assume hp,
      have hnotq: ¬ q, from (assume hq, hnotpimpliesq (assume hpp: p, hq)),
      ⟨hp, hnotq⟩)
    (assume hnotp,
      have hpimpliesq: p → q, from (assume hp, absurd hp hnotp),
      absurd hpimpliesq hnotpimpliesq)

[Patrick Johnson]

example (p q : Prop) : ¬(p → q) → p ∧ ¬q := by tauto

[Patrick Johnson]

͏

[Filippo A. E. Nuccio]

This is just not_imp.mp I believe. Have you tried with library_search?

[Kevin Buzzard]

import tactic

example (p q : Prop) : ¬(p → q) → p ∧ ¬q := by library_search -- Filippo is right

[Kyle Miller]

Just to compare, this is the not_imp.mp proof expanded out to have a similar style (and from replacing some things using classical decidability instances along the way):

example : ¬(p → q) → p ∧ ¬q :=
  assume hnpq : ¬(p → q),
    and.intro
      (classical.by_contradiction
        (assume hnp : ¬p,
          hnpq (assume hp : p, absurd hp hnp)))
      (assume hq : q,
        hnpq (assume _ : p, hq))

[Martin C. Martin]

Thanks! @Kyle Miller that's interesting. I didn't think of using and.intro at the root, but that does simplify things. I have the same proof of ¬q, but didn't notice that it didn't use the assumption of p. And with and.intro at root, the by_contradiction is cleaner than my or.elim (em p).

[Kevin Buzzard]

Re your question about a shorter or more readable proof -- are you reading #tpil but haven't got to chapter 5 yet? Once you know some tactics then things become much more readable and typically shorter too.

[Kyle Miller]

@Martin C. Martin I'm not sure it's actually simpler, once you inline your haves and shorten variable names:

example : ¬(p → q) → p ∧ ¬q :=
  assume hnpq : ¬(p → q),
  or.elim (em p)
    (assume hp : p,
      ⟨hp, assume hq, hnpq (assume _ : p, hq)⟩)
    (assume hnp : ¬p,
      absurd (assume hp : p, absurd hp hnp) hnpq)

But comparing these term proofs is more for the fun of it. I've usually only written them after having written a tactic proof and realized somehow the term proof would be shorter/clearer after simplification.

[Kyle Miller]

Just as an example of a non- tactic#tauto proof, there's tactic#push_neg, which knows about standard manipulations involving logically negating propositions, pushing the negation inward (it applies things like double negation elimination for you).

example : ¬(p → q) → p ∧ ¬q :=
begin
  push_neg,
  exact id,
end

[Martin C. Martin]

@Kevin Buzzard yes, this is a question from chapter 3. Thanks for the tip, looking forward to chapter 5.

@Kyle Miller good point. I haven't gotten into tactics yet. Still, I find it useful to know of other ways of looking at it, even if they become moot after learning tactics.