div_pos_iff_mul_pos golf

Stream: maths

[Kevin Buzzard]

import analysis.real

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
begin
  have H : 0 < y * y := mul_self_pos Hy,
  split,
    intro H1,
    have H2 : (x * y) / (y * y) = x / y,
      rw div_eq_div_iff (ne_of_gt H) Hy,
      rw mul_assoc,
    rw ←H2,
    apply div_pos H1 H,
  intro H1,
  have H2 : (x / y) * (y * y) = x * y,
    rw div_mul_eq_mul_div_comm,
    rw mul_div_cancel _ Hy,
  rw ←H2,
  exact mul_pos H1 H,
end

I was surprised this wasn't already in, for preordered semimonoids with bot or whatever

[Mario Carneiro]

I'm not, that's a weird theorem

[Kevin Buzzard]

what about 0 < x * y iff (x < 0 and y < 0) or (x > 0 and y > 0)?

[Kevin Buzzard]

and similarly for 0 < x / y

[Kenny Lau]

pos_and_pos_or_neg_and_neg_of_mul_pos?

[Kevin Buzzard]

Oh, you found it?

[Kenny Lau]

I found x*y>0 implies x,y>0 or x,y<0

[Mario Carneiro]

I guess the best decomposition of it is something like

0 < x * y
    ↔ (0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0)
... ↔ (0 < x ∧ 0 < y⁻¹ ∨ x < 0 ∧ y⁻¹ < 0)
... ↔ 0 < x * y⁻¹
... ↔ 0 < x / y

[Kevin Buzzard]

ha ha it's in core

[Kevin Buzzard]

I think you should use pos_and_pos_or_neg_and_neg_of_mul_pos

[Kevin Buzzard]

just for the name

[Mario Carneiro]

whenever the name gets that long my eyes cross trying to read it

[Kevin Buzzard]

we should think of a more rigorous encrypted way to name lemmas

[Kevin Buzzard]

to keep them shorter

[Mario Carneiro]

have you seen metamath naming conventions? :D

[Mario Carneiro]

it would probably be called mulanor or the like

[Reid Barton]

that's a cool name

[Kevin Buzzard]

the md5sum of pos_and_pos_or_neg_and_neg_of_mul_pos is shorter, maybe we should use that

[Mario Carneiro]

lol that's a bad sign

[Mario Carneiro]

probably gzip can do better

[Kevin Buzzard]

I'm not, that's a weird theorem

How would you do

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } =
  {x : ℝ | x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1)} :=

? I used this along the way to clear denominators but it was still an annoying case bash

[Kenny Lau]

oh god

[Kevin Buzzard]

yes it's M1F sheet 3

[Kevin Buzzard]

you should have seen my proof last year!

[Kevin Buzzard]

It took me 25 lines to get to ⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1

[Kevin Buzzard]

and now the case bash is much easier

[Kevin Buzzard]

but I had to clear denominators along the way

[Kenny Lau]

how about no

[Kevin Buzzard]

If it's a reasonable M1F question and if you want formal proof verification systems to be taken seriously by mathematicians, this has to be relatively straightforward

[Reid Barton]

Someone want to implement a cylindrical algebraic decomposition tactic?

[Kevin Buzzard]

Is that what's necessary?

[Mario Carneiro]

it's a case bash

[Kevin Buzzard]

Can we make it an issue or is this unreasonable?

[Kevin Buzzard]

It's a cylindrical algebraic decomposition Mario

[Mario Carneiro]

the generalization of this to more vars is CAD

[Reid Barton]

Yeah you don't really need it for one variable & rational roots.

[Kevin Buzzard]

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } = {y : ℝ | y < 0 ∨ ((1 : ℝ) / 3 < y ∧ y < 1)} you mean like this?

[Kevin Buzzard]

It's still a pain to prove that if 1/3 < x and x < 1 then 3 * x + 1 / x < 4

[Kevin Buzzard]

My reworking to ⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1 is definitely paying dividends

[Kenny Lau]

I think you should just let the IC gang prove that

[Mario Carneiro]

in general you have to figure out ordering of real algebraic numbers which is a pain

[Mario Carneiro]

and the best known algorithm is double exponential, a great improvement over the previous algorithm

[Kenny Lau]

what a pity, I was going to use it in my next gce exam

[Kevin Buzzard]

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } =
  {x : ℝ | x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1)} :=
begin
  ext x,
  show x ≠ 0 ∧ 3 * x + 1 / x < 4 ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1,
  cases classical.em (x = 0) with H0 Hn0,
  { -- junk case x = 0
    rw H0,
    norm_num,
  },
  rw (show x ≠ 0 ↔ true, by simp [Hn0]),
  rw true_and,
  show (3 : ℝ) * x + 1 / x < 4 ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1,
  have this : (3 : ℝ) * x + 1 / x < 4 ↔ 0 < 4 - (3 * x + 1 / x)
    := (@sub_pos ℝ (by apply_instance) (4 : ℝ) ((3 : ℝ) * x + 1 / x)).symm,
  rw this,
  rw ←sub_sub,
  rw ←mul_one (4 - 3 * x),
  -- annoying rewrite
  have H : 0 < (4 - 3 * x) * 1 - 1 / x ↔ 0 < (4 - 3 * x) * (x / x) - 1 / x,
    rw div_self Hn0,
  rw H,
  rw ←mul_div_assoc,
  rw ←sub_div,
  rw ←mul_pos_iff_div_pos Hn0,
  replace H : x * x > 0 := mul_self_pos Hn0,
  rw (show ((4 - 3 * x) * x - 1) * x = (1 - x) * x * (3 * x - 1), by ring),
  -- goal now
  -- ⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1
  cases lt_or_ge x 0 with h h1,
  -- x < 0
    rw (show x < 0 ↔ true, by simp [h]),
    rw true_or,
    rw iff_true,
    apply mul_pos_of_neg_of_neg,
      refine mul_neg_of_pos_of_neg _ h,
      apply sub_pos_of_lt,
      apply lt_trans h zero_lt_one,
    apply sub_neg_of_lt,
    refine lt_trans _ zero_lt_one,
    apply mul_neg_of_pos_of_neg _ h,
    norm_num,
  rw (show x < 0 ↔ false, by rw iff_false; exact not_lt_of_ge h1),
  rw false_or,
  cases le_or_gt x ((1 : ℝ) / 3) with h2 h2,
    rw (show (1 : ℝ) / 3 < x ↔ false, by rw iff_false; exact not_lt_of_ge h2),
    rw false_and,
    rw iff_false,
    apply not_lt_of_ge,
    refine mul_nonpos_of_nonneg_of_nonpos _ _,
      refine mul_nonneg _ h1,
      show 0 ≤ 1 - x,
      rw sub_nonneg,
      exact le_trans h2 (by norm_num),
    rw sub_nonpos,
    rw mul_comm,
    apply mul_le_of_le_div (by norm_num) h2,
  cases lt_or_ge x 1,
    rw (iff_true ((1 : ℝ) / 3 < x)).2 h2,
    rw (iff_true (x < 1)).2 h,
    rw true_and,
    rw iff_true,
    refine mul_pos _ _,
      refine mul_pos _ _,
        show 0 < (1 - x),
        rwa sub_pos,
      refine lt_trans (by norm_num) h2,
    show 0 < 3 * x - 1,
    rw sub_pos,
    rwa ←div_lt_iff',
    norm_num,
  rw (show x < 1 ↔ false, by rw iff_false; exact not_lt_of_ge h),
  rw and_false,
  rw iff_false,
  apply not_lt_of_ge,
  refine mul_nonpos_of_nonpos_of_nonneg _ _,
    refine mul_nonpos_of_nonpos_of_nonneg _ h1,
    simp [h], exact h,
  show 0 ≤ 3 * x - 1,
  rw sub_nonneg,
  rw mul_comm,
  apply le_mul_of_div_le,
    norm_num,
  apply le_trans _ h,
  norm_num,
end

Much better than last year's effort

[Kenny Lau]

"much better"

[Kevin Buzzard]

thanks

[Kenny Lau]

import analysis.real

theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } =
  {x : ℝ | x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1)} :=
begin
  ext x,
  rcases lt_trichotomy x 0 with hxneg | hx0 | hxpos,
  { refine iff_of_true ⟨ne_of_lt hxneg, _⟩ (or.inl hxneg),
    refine lt_trans (add_neg (mul_neg_of_pos_of_neg _ hxneg) (one_div_neg_of_neg hxneg)) _;
    norm_num },
  { subst x, norm_num },
  show x ≠ 0 ∧ 3 * x + 1 / x < 4 ↔ x < 0 ∨ ((1 : ℝ) / 3 < x ∧ x < 1),
  rw [eq_true_intro (ne_of_gt hxpos)],
  rw [true_and],
  rw [eq_false_intro (not_lt_of_gt hxpos)],
  rw [false_or],
  rw [← mul_lt_mul_right hxpos],
  rw [add_mul],
  rw [one_div_mul_cancel (ne_of_gt hxpos)],
  rw [div_lt_iff (show (0:ℝ) < 3, by norm_num)],
  split,
  { assume h : 3 * x * x + 1 < 4 * x,
    replace h := sub_neg_of_lt h,
    rw [show 3 * x * x + 1 - 4 * x = (1 - x * 3) * (1 - x), by ring] at h,
    have : 1 < x * 3,
    { apply lt_of_not_ge,
      assume h2 : x * 3 ≤ 1,
      replace h := neg_of_mul_neg_left h (sub_nonneg_of_le h2),
      refine not_lt_of_le h2 _,
      refine lt_trans (show (1:ℝ) < 3, by norm_num) _,
      replace h := lt_of_sub_neg h,
      rw [← mul_lt_mul_right (show (0:ℝ) < 3, by norm_num)] at h,
      rwa [one_mul] at h },
    refine ⟨this, lt_of_sub_pos _⟩,
    apply lt_of_not_ge,
    assume h3 : 1 - x ≤ 0,
    apply not_le_of_lt h,
    exact mul_nonneg_of_nonpos_of_nonpos (le_of_lt (sub_neg_of_lt this)) h3 },
  { assume h : 1 < x * 3 ∧ x < 1,
    cases h with h1 h2,
    apply lt_of_sub_neg,
    rw [show 3 * x * x + 1 - 4 * x = (1 - x * 3) * (1 - x), by ring],
    exact mul_neg_of_neg_of_pos (sub_neg_of_lt h1) (sub_pos_of_lt h2) }
end

[Kenny Lau]

@Kevin Buzzard

[Kenny Lau]

half your size

[Kevin Buzzard]

It's still a lot longer than what most of the first years produce with pen and paper though isn't it :-/

[Kevin Buzzard]

you did the case split at the start. I worked on the goal first. Is your way better or would you have written half as much as me if you'd used my strategy too?

[Kenny Lau]

btw:

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
begin
  have := mul_self_pos Hy,
  rw ← @mul_lt_mul_right _ _ _ (x/y) _ this,
  rw zero_mul,
  rw ← mul_assoc,
  rw div_mul_cancel _ Hy
end

[Kenny Lau]

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
by rw [← @mul_lt_mul_right _ _ _ (x/y) _ (mul_self_pos Hy)];
  rw [zero_mul, ← mul_assoc, div_mul_cancel _ Hy]

[Kenny Lau]

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
by rw [← div_lt_div_right (mul_self_pos Hy), zero_div, ← div_div_eq_div_mul, mul_div_cancel _ Hy]

[Kenny Lau]

(98 characters!)

[Kenny Lau]

you did the case split at the start. I worked on the goal first. Is your way better or would you have written half as much as me if you'd used my strategy too?

I mean, you also did case split at the start

[Reid Barton]

Isn't that Hy hypothesis actually unneeded?

[Reid Barton]

If y = 0 then both things are 0

[Kenny Lau]

great

[Kenny Lau]

"Lean helps me understand maths better"

[Kenny Lau]

"y doesn't need to be nonzero"

[Mario Carneiro]

import data.real.basic tactic.ring data.set.intervals

theorem mul_pos_iff {α} [linear_ordered_ring α] {a b : α} :
  0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
⟨pos_and_pos_or_neg_and_neg_of_mul_pos,
  or.rec (and.rec mul_pos) (and.rec $ by exact mul_pos_of_neg_of_neg)⟩

theorem or_iff_left {a b : Prop} (h : ¬ b) : a ∨ b ↔ a :=
or_iff_left_of_imp h.elim

theorem or_iff_right {a b : Prop} (h : ¬ a) : a ∨ b ↔ b :=
or_iff_right_of_imp h.elim

open set
theorem Q4 : { x : ℝ | x ≠ 0 ∧ 3 * x + 1 / x < 4 } = Iio 0 ∪ Ioo (1 / 3) 1 :=
begin
  ext x,
  rcases lt_trichotomy x 0 with x0|x0|x0,
  { refine iff_of_true ⟨ne_of_lt x0,
      lt_trans (add_neg
        (mul_neg_of_pos_of_neg _ x0)
        (one_div_neg_of_neg x0)) _⟩ (or.inl x0);
    norm_num },
  { subst x, norm_num },
  { dsimp [Iio, Ioo],
    rw [and_iff_right (ne_of_gt x0), or_iff_right (not_lt_of_gt x0),
      add_div_eq_mul_add_div _ _ (ne_of_gt x0),
      div_lt_iff x0, div_lt_iff' (by norm_num : 0 < (3:ℝ)), ← sub_pos,
      (by ring : 4*x - (3*x*x + 1) = (3*x - 1)*(1 - x)),
      mul_pos_iff, sub_pos, sub_pos, sub_lt_zero, sub_lt_zero,
      or_iff_left],
    rintro ⟨h₁, h₂⟩,
    refine absurd (lt_trans h₂ ((lt_div_iff' _).2 h₁)) _; norm_num }
end

[Kevin Buzzard]

I shall explode this proof tomorrow

[Patrick Massot]

Mario, why do you need to explicitly invoke all those and_iff_right, or_iff_right, or_iff_left? Isn't it something that the simplifier should do (using hypothesis x0)?

[Patrick Massot]

Makes me think: @Simon Hudon what happened to your monotonicity tactic?

[Simon Hudon]

Mario is still unhappy with it.