Zulip Chat Archive

Stream: new members

Topic: Return of the monolith


view this post on Zulip Kevin Doran (Apr 11 2020 at 01:44):

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).

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 11 2020 at 03:07):

I am really tempted to write another compactness proof

view this post on Zulip Mario Carneiro (Apr 11 2020 at 03:09):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 09:55):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 11 2020 at 09:57):

Yes, this is the exercise I'm proposing.

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 09:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 09:58):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 11 2020 at 10:00):

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

view this post on Zulip Patrick Massot (Apr 11 2020 at 10:00):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 10:01):

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

view this post on Zulip 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 :-)

view this post on Zulip 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