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.

[Sorrachai Yingchareonthawornchai]

Is there a short proof for this lemma? My proof is embarrassingly long.

lemma solve_quadratic_ineq  {x n:ℕ } [NeZero n] (h:  x ^ 2 ≤ n * (n * (n - 1) + x)) : x ≤ 4 * n * Nat.sqrt n  := by

[Ilmārs Cīrulis]

Maybe this is enough for your purposes?
(I was too lazy to prove your theorem with Nat.sqrt. :sweat_smile:)

import Mathlib

lemma aux {x n: ℕ} (h: x ^ 2 ≤ n ^ 3 - n ^ 2 + n * x): x ^ 2 ≤ 2 * n ^ 3 := by
  have H1: n ^ 2 ≤ n ^ 3 := by
    have H2: n = 0 ∨ 1 ≤ n := by omega
    obtain H2 | H2 := H2 <;> nlinarith
  obtain H2 | H2 := le_or_lt x (2 * n)
  . have H3: n * x ≤ 2 * n ^ 2 := by nlinarith
    have H4: 0 ≤ n ^ 3 := by nlinarith
    omega
  . have H3: 2 * n * x ≤ x ^ 2 := by rw [Nat.pow_two]; nlinarith
    have H4: 0 ≤ n ^ 2 := by nlinarith
    have H5: n ^ 2 ≤ n ^ 3 := by nlinarith
    have H6: 2 * x ^ 2 ≤ 2 * (n ^ 3 - n ^ 2) + 2 * n * x := by nlinarith
    omega

[Ilmārs Cīrulis]

Out of curiosity - what do you need your theorem for?

[Moritz Firsching]

you could leave out a few haves here:

lemma aux {x n: ℕ} (h: x ^ 2 ≤ n ^ 3 - n ^ 2 + n * x): x ^ 2 ≤ 2 * n ^ 3 := by
  have H1: n ^ 2 ≤ n ^ 3 := by
    have H2: n = 0 ∨ 1 ≤ n := by omega
    obtain H2 | H2 := H2 <;> nlinarith
  obtain H2 | H2 := le_or_lt x (2 * n)
  · have H3: n * x ≤ 2 * n ^ 2 := by nlinarith
    omega
  · have H3: 2 * n * x ≤ x ^ 2 := by nlinarith
    have H6: 2 * x ^ 2 ≤ 2 * (n ^ 3 - n ^ 2) + 2 * n * x := by nlinarith
    omega

[Ilmārs Cīrulis]

Thank you!