We need to port the max minigame

[kbuzzard]

In lectures I raised the question of showing that the collection of all subsets of the naturals that contained the infinite set {m,m+1,m+2,m+3,...} for some number m, was a filter.

The proof that the intersection of two sets of this form is also of this form, involves using facts about the maximum of two numbers m and n. So to do this level we need to know something about the API (the main theorems) for Lean's max function.

I once wrote down this API and made a one-world game called the Max Minigame once. The game is still online here: https://www.ma.imperial.ac.uk/~buzzard/xena/max_minigame/

And the proofs (written in Lean 3) are here. A port of this game to a world of the Filter Game would be welcome! You could call it MinMaxWorld. You should present the inequalities as axioms and offer them all to the reader in world 1. Probably you should prove everything for a general totally ordered type. You'll need to translate the proofs from Lean 3: Just do this by hand or with Copilot or whatever; cases is now cases' and split is now constructor.

[kbuzzard]

Question: how much of it works for a general lattice? This is a partially ordered set which has sups and infs for two elements. Here's some example code.

-- hunch : max min stuff works not just for total orders but for *lattices*

-- Open problem: how much of the game doesn't actually assume total order?

import Game.Levels.SetWorld

-- let L be a lattice
variable (L : Type) [Lattice L] (a b c : L)

#check a ≤ b -- a true-false statement

example (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  -- idea: make some kind of lattice tactic which does stuff like the below
  aesop (add unsafe [le_trans, inf_le_right, le_sup_left])

#check a ⊔ b -- least upper bound of a and b

example : a ≤ a ⊔ b := by exact SemilatticeSup.le_sup_left a b
example : b ≤ a ⊔ b := by exact SemilatticeSup.le_sup_right a b

example (h1 : a ≤ c) (h2 : b ≤ c) : a ⊔ b ≤ c := by exact SemilatticeSup.sup_le a b c h1 h2

-- conclusion: a ⊔ b = least uipper bound of a and b

#check a ⊓ b -- greatest lower bounds also exist

-- does max minigame work in this generality? I have no idea

[kbuzzard]

We need this stuff when we do example 2 and 3 of filters, i.e. atTop and nhds. Right now I'm putting these off!