# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: high scores

#### 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 ?

#### Sebastien Gouezel (Apr 05 2020 at 07:54):

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

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

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

#### 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`

).

#### Mario Carneiro (Apr 05 2020 at 11:37):

there is `order.unbounded`

although it is stated a bit differently

#### Patrick Massot (Apr 05 2020 at 11:40):

Where is that?

#### 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?

#### 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

#### Patrick Massot (Apr 05 2020 at 11:48):

@Sebastien Gouezel

#### Sebastien Gouezel (Apr 05 2020 at 11:48):

It's called `no_top_order`

#### Patrick Massot (Apr 05 2020 at 11:48):

Ah

#### Patrick Massot (Apr 05 2020 at 11:48):

I knew it was bound to exist :wink:

#### Patrick Massot (Apr 05 2020 at 11:49):

The `preorder`

requirement in the definition of `no_top_order`

is ridiculous.

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

that's our weakest well behaved order typeclass

#### Patrick Massot (Apr 05 2020 at 11:50):

But `has_lt`

is enough here!

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

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

etc typeclasses

#### Patrick Massot (Apr 05 2020 at 11:50):

:stuck_out_tongue:

#### 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?

#### 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

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

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

#### 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

#### 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`

).

#### 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