Zulip Chat Archive

Stream: Is there code for X?

Topic: high scores


view this post on Zulip Patrick Massot (Apr 04 2020 at 22:02):

Sébastien, do you know whether the high scores lemma you discussed in Orsay is in mathlib ?

view this post on Zulip Sebastien Gouezel (Apr 05 2020 at 07:54):

I don't think it is, at least I never noticed it.

view this post on Zulip Sebastien Gouezel (Apr 05 2020 at 08:09):

Using nat.find, it should be pretty straightforward. The Isabelle proof I gave is very clunky as it does everything by hand, using only infs and sups.

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:06):

Do we have some form of:

class unbounded_above (α : Type*) [has_lt α] : Prop :=
(exists_gt :  a : α,  b, a < b)

This seems needed for the statement of the high scores lemma if we want a rather general sequence target.

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:07):

Of course I don't mind using a data carrying version (adding a function taking a and outputting b).

view this post on Zulip Mario Carneiro (Apr 05 2020 at 11:37):

there is order.unbounded although it is stated a bit differently

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:40):

Where is that?

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:41):

I see only def unbounded (r : α → α → Prop) (s : set α) : Prop := ∀ a, ∃ b ∈ s, ¬ r b a. Is that what you mean?

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:47):

Maybe this discussion is too abstract. I'd like to read comments about:

import order.filter

open filter

lemma exists_le_of_tendsto_at_top {α : Type*} [decidable_linear_order α]
  {β : Type*} [preorder β] {u : α  β} (h : tendsto u at_top at_top) :
 a b,  a'  a, b  u a' :=
begin
  intros a b,
  rw tendsto_at_top at h,
  haveI : nonempty α := a,
  cases mem_at_top_sets.mp (h b) with a' ha',
  exact max a a', le_max_left _ _, ha' _ $ le_max_right _ _⟩,
end

class unbounded_above (α : Type*) [has_lt α] : Prop :=
(exists_gt :  a : α,  b, a < b)

instance linear_ordered_semiring.unbounded_above {R : Type*} [linear_ordered_semiring R] :
  unbounded_above R := ⟨λ a, a+1, lt_add_one a⟩⟩

lemma exists_lt_of_tendsto_at_top {α : Type*} [decidable_linear_order α]
  {β : Type*} [preorder β] [unbounded_above β] {u : α  β} (h : tendsto u at_top at_top) :
 a b,  a'  a, b < u a' :=
begin
  intros a b,
  cases unbounded_above.exists_gt b with b' hb',
  rcases exists_le_of_tendsto_at_top h a b' with a', ha', ha'',
  exact a', ha', lt_of_lt_of_le hb' ha''
end

lemma high_scores {β : Type*} [decidable_linear_order β] [unbounded_above β] {u :   β}
  (hu : tendsto u at_top at_top) :  N,  n  N,  k < n, u k < u n :=
begin
  intros N,
  let A := finset.image u (finset.range $ N+1), -- A = {u 0, ..., u N}
  have Ane : A.nonempty,
    from u 0, finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.zero_lt_succ _),
  let M := finset.max' A Ane,
  have ex :  n  N, M < u n,
    from exists_lt_of_tendsto_at_top hu _ _,
  obtain n, hnN, hnM, hn_min :  n, N  n  M < u n   k, N  k  k < n  u k  M,
  { use nat.find ex,
    rw  and_assoc,
    split,
    { simpa using nat.find_spec ex },
    { intros k hk hk',
      simpa [hk] using nat.find_min ex hk' } },
  use [n, hnN],
  intros k hk,
  by_cases H : k  N,
  { have : u k  A,
      from finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.lt_succ_of_le H),
    have : u k  M,
      from finset.le_max' A Ane (u k) this,
    exact lt_of_le_of_lt this hnM },
  { push_neg at H,
    calc u k  M   : hn_min k (le_of_lt H) hk
         ... < u n : hnM },
end

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:48):

@Sebastien Gouezel

view this post on Zulip Sebastien Gouezel (Apr 05 2020 at 11:48):

It's called no_top_order

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:48):

Ah

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:48):

I knew it was bound to exist :wink:

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:49):

The preorder requirement in the definition of no_top_order is ridiculous.

view this post on Zulip Mario Carneiro (Apr 05 2020 at 11:50):

that's our weakest well behaved order typeclass

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:50):

But has_lt is enough here!

view this post on Zulip Mario Carneiro (Apr 05 2020 at 11:50):

if you want less than that you should go for the piecemeal is_irrefl etc typeclasses

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:50):

:stuck_out_tongue:

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:51):

Anyway, let's go back to serious stuff. no_top_order is indeed what I was looking for. Any other observation about that high scores stuff?

view this post on Zulip Mario Carneiro (Apr 05 2020 at 11:53):

it occurs to me that the statement of high_scores could be stated using order.unbounded, although I'm not sure if the result is more or less readable

view this post on Zulip Patrick Massot (Apr 05 2020 at 11:54):

In my intended use, the sequence target is either nat or real.

view this post on Zulip Sebastien Gouezel (Apr 05 2020 at 11:59):

I think your code is nice. How do you feel it compare to the Isabelle proof wrt to length and readability? For the record, here is the Isabelle code:

lemma high_scores:
  fixes u::"nat ⇒ real" and i::nat
  assumes "u ⇢ ∞"
  shows "∃n ≥ i. ∀l ≤ n. u l ≤ u n"
proof -
  define M where "M = Max {u l|l. l < i}"
  define n where "n = Inf {m. u m > M}"
  have "eventually (λm. u m > M) sequentially"
    using assms by (simp add: filterlim_at_top_dense tendsto_PInfty_eq_at_top)
  then have "{m. u m > M} ≠ {}" by fastforce
  then have "n ∈ {m. u m > M}" unfolding n_def using Inf_nat_def1 by metis
  then have "u n > M" by simp
  have "n ≥ i"
  proof (rule ccontr)
    assume " ¬ i ≤ n"
    then have *: "n < i" by simp
    have "u n ≤ M" unfolding M_def apply (rule Max_ge) using * by auto
    then show False using u n > M by auto
  qed
  moreover have "u l ≤ u n" if "l ≤ n" for l
  proof (cases "l = n")
    case True
    then show ?thesis by simp
  next
    case False
    then have "l < n" using l  n by auto
    then have "l ∉ {m. u m > M}"
      unfolding n_def by (meson bdd_below_def cInf_lower not_le zero_le)
    then show ?thesis using u n > M by auto
  qed
  ultimately show ?thesis by auto
qed

view this post on Zulip Patrick Massot (Apr 05 2020 at 12:04):

I think it's pretty comparable. The only painful part in Lean is finding the lemmas. Basically every intermediate assumption should be proved by automation. Some of it already is (by library_search).

view this post on Zulip Patrick Massot (Apr 05 2020 at 12:04):

I also wish nat.find had a less cryptic name.


Last updated: May 07 2021 at 22:14 UTC