# Zulip Chat Archive

## Stream: new members

### Topic: Return of the monolith

#### Kevin Doran (Apr 11 2020 at 01:44):

Hey everyone,

I have some questions regarding the proof below (or in live editor).

- Are there some tactics that I can use to simplify inequalities involving absolutes?
- In the proof of the reverse part of the bi-implication, what is a better way of introducing a positive real greater than two others?

Any tips at all welcome.

import data.real.basic import data.set namespace ch9 local notation `|`x`|` := abs x def is_bounded (X : set ℝ) : Prop := ∃ M > 0, X ⊆ set.Icc (-M) M def has_finite_sup (X : set ℝ) : Prop := X.nonempty ∧ (upper_bounds X).nonempty def has_finite_inf (X : set ℝ) : Prop := X.nonempty ∧ (lower_bounds X).nonempty -- This is an trivial proof on paper, but I ended up with a mess in Lean. example (X : set ℝ) (h : X.nonempty) : is_bounded X ↔ has_finite_sup X ∧ has_finite_inf X := begin split, { -- The forward proof isn't too bad—it's the reverse that is the main issue. intro hb, rcases hb with ⟨u, hu, h₁⟩, let l := -u, have hub : u ∈ upper_bounds X, intros x hx, exact (h₁ hx).right, have hlb : l ∈ lower_bounds X, intros x hx, exact (h₁ hx).left, have hfs : has_finite_sup X, from ⟨h, set.nonempty_of_mem hub⟩, have hfi : has_finite_inf X, from ⟨h, set.nonempty_of_mem hlb⟩, exact ⟨hfs, hfi⟩, }, { -- This part is a mess, mainly becase: -- 1. I don't find a simple way of going from `u l : ℝ` to `∃ m > 0, m ≥ u ∧ m ≥ l` -- 2. I don't know of a tactic like `linarith` that will work with abs inequalities. intro h, rcases h.left.right with ⟨u, hu⟩, rcases h.right.right with ⟨l, hl⟩, -- Try create m by setting it equal to `|upper bound| + |lower bound| + 1` let m0 := |u| + |l|, have h₁ : m0 ≥ |u| ∧ m0 ≥ |l|, split; {norm_num, apply abs_nonneg}, let m1 : ℝ := m0 + 1, have h₂ : m0 ≤ m1, by norm_num, have h₄ : m1 ≥ |u| ∧ m1 ≥ |l|, -- Short but opaque alternative for h₄ proof: -- split; cases h₁; apply le_trans; assumption, split, { apply le_trans h₁.left h₂, }, { apply le_trans h₁.right h₂, }, use m1, split, { -- Can't find any automation for here. have m0_nonneg : 0 ≤ m0, from add_nonneg (abs_nonneg u) (abs_nonneg l), have h₃ : 0 < m1, from add_pos_of_nonneg_of_pos m0_nonneg (by norm_num), exact h₃, }, { intros x hx, -- Can't find any automation for here. have hxm : x ≤ m1, from le_trans (hu hx) (le_trans (le_abs_self u) h₄.left), have hml : -l ≤ m1, from le_trans (neg_le_abs_self l) h₄.right, rw neg_le at hml, have hmx := le_trans hml (hl hx), exact ⟨hmx, hxm⟩, }, }, end end ch9

It's an attempt to replicate some book material, and I understand that definitions exist in a different form in mathlib. (For reference, a previous related post).

#### Mario Carneiro (Apr 11 2020 at 03:01):

Here's a reasonably clean proof of the statement. There are probably also more automated proofs of this using `linarith`

example (X : set ℝ) (h : X.nonempty) : is_bounded X ↔ has_finite_sup X ∧ has_finite_inf X := begin simp [is_bounded, has_finite_inf, has_finite_sup, h], simp [set.nonempty, upper_bounds, lower_bounds, set.subset_def], split, { rintro ⟨M, M0, hM⟩, exact ⟨⟨M, λ x h, (hM _ h).2⟩, ⟨-M, λ x h, (hM _ h).1⟩⟩ }, { rintro ⟨⟨u, hu⟩, ⟨v, hv⟩⟩, use max 1 (max u (-v)), split, { apply lt_of_lt_of_le zero_lt_one, apply le_max_left }, { intros x hx, split, { apply neg_le.1, apply le_trans _ (le_max_right _ _), apply le_trans _ (le_max_right _ _), apply neg_le_neg, exact hv hx }, { apply le_trans _ (le_max_right _ _), apply le_trans _ (le_max_left _ _), exact hu hx } } } end

#### Reid Barton (Apr 11 2020 at 03:07):

I am really tempted to write another compactness proof

#### Mario Carneiro (Apr 11 2020 at 03:09):

these statements with maxes seem like they should follow from some filter based reasoning

#### Kevin Doran (Apr 11 2020 at 03:46):

Thanks for the example @Mario Carneiro.

Some of my takeaways:

*the use of `max`

; using `max`

, it is quick to get a positive real greater than `u`

and `l`

, and it also avoids the need for dealing with absolutes.

*I should try experiment with more `_`

, with `rintro`

, and I should consider `<some_bijection>.1`

instead of `iff.elim`

.

Is the use of simp at the beginning common? I feel that one downside is that later on in the proof, the tactic goal is less legible.

#### Mario Carneiro (Apr 11 2020 at 03:50):

The point of the simp at the beginning is to clean up the proof statement until it is just basic logic. You don't have to, because they are all defeq simplifications; I think you can just delete those lines and it will still work

#### Mario Carneiro (Apr 11 2020 at 03:54):

Actually that's not entirely true, the first `simp`

gets rid of the nonempty X assumptions. But the proof changes only very slightly if you skip the `simp`

example (X : set ℝ) (h : X.nonempty) : is_bounded X ↔ has_finite_sup X ∧ has_finite_inf X := begin split, { rintro ⟨M, M0, hM⟩, exact ⟨⟨h, M, λ x h, (hM h).2⟩, ⟨h, -M, λ x h, (hM h).1⟩⟩ }, { rintro ⟨⟨_, u, hu⟩, ⟨_, v, hv⟩⟩, use max 1 (max u (-v)), split, { apply lt_of_lt_of_le zero_lt_one, apply le_max_left }, { intros x hx, split, { apply neg_le.1, apply le_trans _ (le_max_right _ _), apply le_trans _ (le_max_right _ _), apply neg_le_neg, exact hv hx }, { apply le_trans _ (le_max_right _ _), apply le_trans _ (le_max_left _ _), exact hu hx } } } end

#### Patrick Massot (Apr 11 2020 at 09:54):

Another version that would be rather easy to automate:

example (X : set ℝ) (h : X.nonempty) : is_bounded X ↔ has_finite_sup X ∧ has_finite_inf X := begin split, { rintro ⟨M, M0, hM⟩, exact ⟨⟨h, M, λ x h, (hM h).2⟩, ⟨h, -M, λ x h, (hM h).1⟩⟩ }, { rintro ⟨⟨_, u, hu⟩, ⟨_, v, hv⟩⟩, use max 1 (max u (-v)), have := le_max_left 1 (max u (-v)), have := le_max_right 1 (max u (-v)), have := le_max_left u (-v), have := le_max_right u (-v), split, { linarith }, { intros x hx, split, { linarith [hv hx] }, { linarith [hu hx] } } }, end

The missing tactic would crawl the context and assumptions looking for `max A B`

and doing `have := le_max_left A B, have := le_max_right A B`

.

#### Patrick Massot (Apr 11 2020 at 09:55):

It should be a fun meta-programming exercise. You can also do the analogous thing handling `min`

and `abs`

.

#### Kevin Buzzard (Apr 11 2020 at 09:55):

`max_le`

is also useful, but is this too hard because it's an implication?

#### Patrick Massot (Apr 11 2020 at 09:56):

I *think* that https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md has everything you need for this exercise.

#### Kevin Buzzard (Apr 11 2020 at 09:56):

I always felt that `linarith`

could be beefed up by epsilon in this regard, but my understanding is that the correct approach is not to hack linarith but instead to write something else which uses it under the hood.

#### Patrick Massot (Apr 11 2020 at 09:57):

Yes, this is the exercise I'm proposing.

#### Kevin Buzzard (Apr 11 2020 at 09:57):

But to get `max_le`

involved one would also need something like `cc`

perhaps?

#### Patrick Massot (Apr 11 2020 at 09:58):

Note that we still manage to pity Rob from time to times. Recently he added splitting conjunctions.

#### Patrick Massot (Apr 11 2020 at 09:58):

Yes, you can add `max_le`

to the game but you'll need `tauto`

to instantiate it, and I'm not sure it would work.

#### Kevin Buzzard (Apr 11 2020 at 09:58):

Another useful fact, I *guess*, might be `max a b = a \or max a b = b`

#### Kevin Buzzard (Apr 11 2020 at 09:59):

You need more than `tauto`

to instantiate it because the proofs a<= X and b<=X which will need might be themselves proved using linarith

#### Kevin Buzzard (Apr 11 2020 at 10:00):

There is something here which always feels accessible to me, but which I don't quite understand properly.

#### Patrick Massot (Apr 11 2020 at 10:00):

Yes, that's why it's more complicated.

#### Patrick Massot (Apr 11 2020 at 10:00):

Kevin, I suggest you first do the meta-programming exercise I set above.

#### Kevin Buzzard (Apr 11 2020 at 10:01):

I did that PR with the core tactic docs but I draw the line at metaprogramming :-)

#### Kevin Buzzard (Apr 11 2020 at 10:01):

I don't know any programming, let alone metaprogramming. I think my time today would be better spent making games :-)

#### Kevin Buzzard (Apr 11 2020 at 10:02):

[although the first 2 hours of it have been spent dealing with work emails :-/ ]

Last updated: May 14 2021 at 07:19 UTC