πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Connectives.More
open import Padova2025.ProvingBasics.Termination.Ordering
open import Padova2025.Explorations.Pigeonhole

module Padova2025.Recreational.Choice.Boxes.Base (ℝ : Set) (n : β„•) where

Intro

An evil monster prepares a secret room containing infinitely many opaque boxes. The boxes are numbered by the naturals and each box contains a real number of the monster’s choosing.

One by one, the evil monster privately guides the members of a team of n mathematicians into the room, with the other members waiting outside. While in the room, each mathematician may open as many boxes as they wish, even infinitely many, inspecting their contents. They may base their decision as to which boxes to open on the contents they have seen so far. The only requirement is that they keep one box of their choosing untouched: The monster will ask them for a guess regarding the contents of that box.

The mathematicians win as a team if and only if at most one of them guesses incorrectly. As usual, communication among the team is allowed only beforehand. Between successive visits to the room, the room is reset to its original state (so all the opened boxes are closed again).

Config : Set
Config = β„• β†’ ℝ

Player : Set
Player = Fin n

βˆ… : β„• β†’ Set
βˆ… _ = βŠ₯

infixl 5 _β–·_
_β–·_ : {I : Set} β†’ (β„• β†’ Set) β†’ (I β†’ β„•) β†’ (β„• β†’ Set)
Opened β–· xs = Ξ» x β†’ Opened x ⊎ βˆƒ[ i ] xs i ≑ x

For a predicate Opened : β„• β†’ Set, the type PlayerStrategy Opened is the type of all possible strategies which are valid in the sense of not offering a guess for an already opened box.

data PlayerStrategy (Opened : β„• β†’ Set) : Set₁ where
  guess : (x : β„•) β†’ Β¬ Opened x β†’ ℝ β†’ PlayerStrategy Opened
  peek  : {I : Set} β†’ (xs : I β†’ β„•) β†’ ((I β†’ ℝ) β†’ PlayerStrategy (Opened β–· xs)) β†’ PlayerStrategy Opened

guessesCorrectly : {Opened : β„• β†’ Set} β†’ PlayerStrategy Opened β†’ Config β†’ Set
guessesCorrectly (guess x _ y) c = y ≑ c x
guessesCorrectly (peek xs k)   c = guessesCorrectly (k (Ξ» i β†’ c (xs i))) c

TeamStrategy : Set₁
TeamStrategy = Player β†’ PlayerStrategy βˆ…

isSuccessful : TeamStrategy β†’ Set
isSuccessful s
  = (c : Config)
  β†’ (q q' : Player) β†’ Β¬ guessesCorrectly (s q)  c β†’ Β¬ guessesCorrectly (s q') c
  β†’ q ≑ q'

Lane arithmetic

pack : Player β†’ β„• β†’ β„•
pack p zero     = toβ„• p
pack p (succ m) = n + pack p m

pack-β‰₯ : (p : Player) (m : β„•) β†’ pack p (succ m) β‰₯ n
pack-β‰₯ p m = +-inflationaryβ‚— n (pack p m)

pack-injective : {q q' : Player} {m m' : β„•} β†’ pack q m ≑ pack q' m' β†’ q ≑ q' Γ— m ≑ m'
pack-injective {q} {q'} {zero}   {zero}    eq = toβ„•-injective eq , refl
pack-injective {q} {q'} {zero}   {succ m'} eq = βŠ₯-elim (<-irreflexive' (≀-trans (pack-β‰₯ q' m') (≑⇒≀ (sym eq))) (toβ„•-bounded q))
pack-injective {q} {q'} {succ m} {zero}    eq = βŠ₯-elim (<-irreflexive' (≀-trans (pack-β‰₯ q m) (≑⇒≀ eq)) (toβ„•-bounded q'))
pack-injective {q} {q'} {succ m} {succ m'} eq with pack-injective (+-cancelβ‚— n _ _ eq)
... | q≑q' , m≑m' = q≑q' , cong succ m≑m'

insert : (j : β„•) β†’ (Ξ£[ i ∈ β„• ] i β‰’ j β†’ ℝ) β†’ ℝ β†’ Config
insert j c x i with eq? i j
... | left  _   = x
... | right i≒j = c (i , i≒j)

insert-β‰—* : (j : β„•) β†’ (c : Config) β†’ (x : ℝ) β†’ insert j (Ξ» (i , _) β†’ c i) x β‰—* c
insert-β‰—* j c x = j ∷ [] , go
  where
  go : (i : β„•) β†’ insert j (Ξ» (i , _) β†’ c i) x i ≑ c i ⊎ i ∈ (j ∷ [])
  go i with eq? i j
  ... | left  refl = right (here refl)
  ... | right _    = left refl

TODO cite Gabay–O’Connor and Hardin & Taylor