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

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

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

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