# Zulip Chat Archive

## Stream: maths

### Topic: div_pos_iff_mul_pos golf

#### Kevin Buzzard (Nov 14 2018 at 21:26):

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 (Nov 14 2018 at 21:28):

I'm not, that's a weird theorem

#### Kevin Buzzard (Nov 14 2018 at 21:30):

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

?

#### Kevin Buzzard (Nov 14 2018 at 21:30):

and similarly for `0 < x / y`

#### Kenny Lau (Nov 14 2018 at 21:31):

`pos_and_pos_or_neg_and_neg_of_mul_pos`

?

#### Kevin Buzzard (Nov 14 2018 at 21:31):

Oh, you found it?

#### Kenny Lau (Nov 14 2018 at 21:32):

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

#### Mario Carneiro (Nov 14 2018 at 21:32):

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 (Nov 14 2018 at 21:32):

ha ha it's in core

#### Kevin Buzzard (Nov 14 2018 at 21:32):

I think you should use `pos_and_pos_or_neg_and_neg_of_mul_pos`

#### Kevin Buzzard (Nov 14 2018 at 21:32):

just for the name

#### Mario Carneiro (Nov 14 2018 at 21:33):

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

#### Kevin Buzzard (Nov 14 2018 at 21:33):

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

#### Kevin Buzzard (Nov 14 2018 at 21:33):

to keep them shorter

#### Mario Carneiro (Nov 14 2018 at 21:33):

have you seen metamath naming conventions? :D

#### Mario Carneiro (Nov 14 2018 at 21:34):

it would probably be called `mulanor`

or the like

#### Reid Barton (Nov 14 2018 at 21:34):

that's a cool name

#### Kevin Buzzard (Nov 14 2018 at 21:34):

the md5sum of `pos_and_pos_or_neg_and_neg_of_mul_pos`

is shorter, maybe we should use that

#### Mario Carneiro (Nov 14 2018 at 21:34):

lol that's a bad sign

#### Mario Carneiro (Nov 14 2018 at 21:35):

probably gzip can do better

#### Kevin Buzzard (Nov 14 2018 at 21:51):

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 (Nov 14 2018 at 21:52):

oh god

#### Kevin Buzzard (Nov 14 2018 at 21:53):

yes it's M1F sheet 3

#### Kevin Buzzard (Nov 14 2018 at 21:53):

you should have seen my proof last year!

#### Kevin Buzzard (Nov 14 2018 at 21:54):

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

#### Kevin Buzzard (Nov 14 2018 at 21:55):

and now the case bash is much easier

#### Kevin Buzzard (Nov 14 2018 at 21:55):

but I had to clear denominators along the way

#### Kenny Lau (Nov 14 2018 at 21:57):

how about no

#### Kevin Buzzard (Nov 14 2018 at 21:57):

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 (Nov 14 2018 at 21:58):

Someone want to implement a cylindrical algebraic decomposition tactic?

#### Kevin Buzzard (Nov 14 2018 at 21:59):

Is that what's necessary?

#### Mario Carneiro (Nov 14 2018 at 21:59):

it's a case bash

#### Kevin Buzzard (Nov 14 2018 at 21:59):

Can we make it an issue or is this unreasonable?

#### Kevin Buzzard (Nov 14 2018 at 21:59):

It's a cylindrical algebraic decomposition Mario

#### Mario Carneiro (Nov 14 2018 at 21:59):

the generalization of this to more vars is CAD

#### Reid Barton (Nov 14 2018 at 22:00):

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

#### Kevin Buzzard (Nov 14 2018 at 22:00):

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

you mean like this?

#### Kevin Buzzard (Nov 14 2018 at 22:01):

It's still a pain to prove that if `1/3 < x`

and `x < 1`

then `3 * x + 1 / x < 4`

#### Kevin Buzzard (Nov 14 2018 at 22:01):

My reworking to `⊢ 0 < (1 - x) * x * (3 * x - 1) ↔ x < 0 ∨ 1 / 3 < x ∧ x < 1`

is definitely paying dividends

#### Kenny Lau (Nov 14 2018 at 22:02):

I think you should just let the IC gang prove that

#### Mario Carneiro (Nov 14 2018 at 22:02):

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

#### Mario Carneiro (Nov 14 2018 at 22:03):

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

#### Kenny Lau (Nov 14 2018 at 22:05):

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

#### Kevin Buzzard (Nov 14 2018 at 22:24):

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 (Nov 14 2018 at 22:28):

"much better"

#### Kevin Buzzard (Nov 14 2018 at 22:28):

thanks

#### Kenny Lau (Nov 14 2018 at 23:02):

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 (Nov 14 2018 at 23:02):

@Kevin Buzzard

#### Kenny Lau (Nov 14 2018 at 23:03):

half your size

#### Kevin Buzzard (Nov 14 2018 at 23:04):

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

#### Kevin Buzzard (Nov 14 2018 at 23:06):

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 (Nov 14 2018 at 23:06):

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 (Nov 14 2018 at 23:07):

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 (Nov 14 2018 at 23:09):

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 (Nov 14 2018 at 23:10):

(98 characters!)

#### Kenny Lau (Nov 14 2018 at 23:10):

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 (Nov 14 2018 at 23:11):

Isn't that `Hy`

hypothesis actually unneeded?

#### Reid Barton (Nov 14 2018 at 23:11):

If `y = 0`

then both things are 0

#### Kenny Lau (Nov 14 2018 at 23:14):

great

#### Kenny Lau (Nov 14 2018 at 23:14):

"Lean helps me understand maths better"

#### Kenny Lau (Nov 14 2018 at 23:15):

"`y`

doesn't need to be nonzero"

#### Mario Carneiro (Nov 15 2018 at 01:40):

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 (Nov 15 2018 at 02:55):

I shall explode this proof tomorrow

#### Patrick Massot (Nov 15 2018 at 08:37):

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 (Nov 15 2018 at 08:43):

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

#### Simon Hudon (Nov 15 2018 at 16:39):

Mario is still unhappy with it.

Last updated: May 10 2021 at 07:15 UTC