Return of the monolith

Stream: new members

[Kevin Doran]

Hey everyone,

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

1. Are there some tactics that I can use to simplify inequalities involving absolutes?
2. 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]

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]

I am really tempted to write another compactness proof

[Mario Carneiro]

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

[Kevin Doran]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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]

Yes, this is the exercise I'm proposing.

[Kevin Buzzard]

But to get max_le involved one would also need something like cc perhaps?

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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