Basic Analysis hangup in Lean

Stream: new members

[Jon Bannon]

I'm quite looking forward to LFTCM next week at ICERM!

My students (@David Talone and @Christian Kolker) are working on trying to construct a sequence using choice in order to solve a basic analysis exercise, and have hit an interesting wall that I can't seem to help them over. The code references are from the Real Number Game (I hope all of the imports are there, but the code may run with only a little modification). It seems to me as if they have been able to manufacture a sequence successfully using choice, but we aren't sure what Lean is doing...and whether it remembers the construction of the sequence. The membership claim should be easy to see from the definition of the set...but we're unable to do so. Can anyone enlighten us on what Lean is doing with this?

import game.sup_inf.level02
import data.real.basic
import tactic

namespace xena -- hide

open classical

axiom choice {α : Sort*} : nonempty α → α

definition is_limit (a : ℕ → ℝ) (α : ℝ) :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |a n - α| < ε

lemma generate_element {x : ℝ}{S : set ℝ} {h1 : S ≠ ∅} (h2 : is_lub S x) (ε : ℝ) : (0 < ε)→ ¬ (is_upper_bound S (x-ε)) :=
begin
intro h,
unfold is_lub at h2,
cases h2 with h2l h2r,
have Q := h2r(x-ε),
by_contradiction,
have R := Q(a),
linarith,
end


theorem seq_conv_to_sup {x : ℝ}{S : set ℝ} {h1 : S ≠ ∅} (h2 : is_lub S x): ∃(a : ℕ → ℝ), ((is_limit a x) ∧ (∀(n : ℕ),(a n ∈ S))) :=
begin
split,
swap,
intro n,
have Q := generate_element h2 (1/(n + 1) : ℝ),
have R : 0 < (1 / ((n : ℝ) + 1)),
      sorry,
have P := Q(R),
unfold is_upper_bound at P,
push_neg at P,
set T1 := λ s, s ∈ S ∧ x - 1 / (↑n + 1) < s,
have T2 : ∃s, T1 s, by exact P,
have s0 := classical.some T2,--here is where choice is used to get the element!
exact s0,
exact h1,
split,
simp,
swap,
simp,
end


end xena

[Ruben Van de Velde]

I'm pretty sure have s0 := classical.some T2 is not going to work - try with let?

[Patrick Massot]

Where did you find that real number game?

[Patrick Massot]

And is there any reason why you're doing that instead of the tutorial project that covers this in a more reproducible environment?

[Jon Bannon]

Ruben Van de Velde said:

I'm pretty sure have s0 := classical.some T2 is not going to work - try with let?

Good point. Made that change (also even tried set). I'm having the students play with that code and solve the levels. When we run this, they still end up with a goal ∀ (n : ℕ), some _ ∈ S as a result of the choice. I think Lean remembers that this some_ knows that the result of the choice of something from S, but I have no idea how to access this fact...

@Patrick Massot we cloned the Git repository: https://github.com/ImperialCollegeLondon/real-number-game

[Patrick Massot]

After push_neg at P you probably want to type choose s₀ s₀_in lt_s₀ using P,

[Patrick Massot]

But really, your life would be much easier in the tutorial project.

[Patrick Massot]

The only point of playing the real number game is if you wan to play it in a web browser without installing Lean.

[Patrick Massot]

There you'll find https://github.com/leanprover-community/tutorials/blob/master/src/exercises/09_limits_final.lean#L79-L81

[Patrick Massot]

Note how the outline of the proof is offered.

[Jon Bannon]

@Patrick Massot Thanks! I've had them look at the tutorial as well to learn. They are working on trying to make the web-based game work, with the eventual goal of making it available (and completely usable in an Analysis course) without installing Lean. Roughly, at many liberal arts colleges in the US, introductory Algebra and Analysis are the core courses for a math major. Rationale: if the Real Number Game (or the tutorial levels you linked to) were available to instructors without the need to install Lean, this would broaden Lean's use in the US, since one could simply aim faculty and students at the NN game, and then the Real Number Game and then Algebra (or Group) game with low barrier of entry.

[Patrick Massot]

Your proof has a weird beginning. What are you trying to do exactly?

[Patrick Massot]

I think a much more promising start is

have : ∀ n : ℕ, ∃ a ∈ S, x - 1/(n+1) < a,
{ intros n,
  have Q := generate_element h2 (1/(n + 1) : ℝ),
  have R : 0 < (1 / ((n : ℝ) + 1)),
      sorry,
  have P : ¬ ∀ a ∈ S, a ≤ x - 1 / (n + 1) := Q R,
  push_neg at P,
  simpa using P,
  exact h1 },
choose a a_in lt_a using this,

[Jon Bannon]

Patrick Massot said:

I think a much more promising start is

have : ∀ n : ℕ, ∃ a ∈ S, x - 1/(n+1) < a,
{ intros n,
  have Q := generate_element h2 (1/(n + 1) : ℝ),
  have R : 0 < (1 / ((n : ℝ) + 1)),
      sorry,
  have P : ¬ ∀ a ∈ S, a ≤ x - 1 / (n + 1) := Q R,
  push_neg at P,
  simpa using P,
  exact h1 },
choose a a_in lt_a using this,
````
They are trying to prove that given a nonempty subset of \R that is bounded above then there is a sequence that converges to the supremum...so I think what you suggest as an alternative start will help.

[Jon Bannon]

Jon Bannon said:

Patrick Massot said:

I think a much more promising start is

have : ∀ n : ℕ, ∃ a ∈ S, x - 1/(n+1) < a,
{ intros n,
  have Q := generate_element h2 (1/(n + 1) : ℝ),
  have R : 0 < (1 / ((n : ℝ) + 1)),
      sorry,
  have P : ¬ ∀ a ∈ S, a ≤ x - 1 / (n + 1) := Q R,
  push_neg at P,
  simpa using P,
  exact h1 },
choose a a_in lt_a using this,
````
They are trying to prove that given a nonempty subset of \R that is bounded above then there is a sequence that converges to the supremum...so I think what you suggest as an alternative start will help.
`````
They tried it @**Patrick Massot|110031** , and it worked. Thanks again!

[Eric Wieser]

Note that there are other paths to getting instructors (and students) an online lean installation:

• Gitpod. There should be a button on the tutorials project to launch this. The free tier is good enough for courses where students do less than 50hrs/mo.
• GitHub codespaces. We haven't set this up yet, but it's free for educational use via GitHub classroom

Both give you the full lean experience in browser rather than the limitations of the game view

[Kevin Buzzard]

The real number game is basically an abandoned project which IIRC never really found a coherent way of doing real analysis. I was supposed to be working on it with some people over summer of 2020 but then covid happened and everything fell apart. My memory is that, unlike the natural number game which went through an extensive planning stage and then a huge amount of testing on undergraduates, the real number game was just some ideas written down which never turned into anything coherent. My instinct would be that if you wanted to make a real number game then you need to start with a coherent plan on how to develop the theory, and I'm not sure we ever got that far. I thought about things like min and max, and me and the others ended up making the max minigame but I think that was the only coherent thing which happened.