## Stream: new members

### Topic: Defining "hat games"

#### Eric Rodriguez (Mar 24 2021 at 01:42):

Hey all, I'm trying to formalize some theorems about hat games in Lean, and I'm not sure how best to define it. Essentially, in a hat game, you can see your neighbouring vertices and "guess" the colour of your own hat based on that. This is modeled as a function "neighbour vertices → colour," but I'm wondering whether in Lean it's better to instead have a function "all vertices → colour" but make sure it's invariant under changes of non-neighbouring vertices. My code, for reference: (and a couple noobie questions...)

import data.set.finite
import data.set.function
import logic.function.basic
import combinatorics.simple_graph.basic

variable {α : Type*}
variable (G : simple_graph α)

-- an assignment of colours to vertices
def hat_arr (α : Type*) (n : ℕ) := α → fin n

-- ATTEMPT 1: NEIGHBOUR VERTICES → COLOUR

-- I can't figure out this type; if i ctrl+c what #check says, I get "type expected"
-- which makes some sense, as membership of a set is not expressed through types
def visible_hats {n : ℕ} (v : α) (f : hat_arr α n) : magical_type
:= (G.neighbor_set v).restrict f

structure hat_guesser (n : ℕ) (f : ∀ a : α, magical_type → ℕ) :=
(hat_guessing_cond: ∀ arr : hat_arr α n, ∃ a : α, f a (visible_hats a arr) = arr a)
-- definition looks nicer IF magical_type isn't too annoying to use

-- ATTEMPT 2: ALL VERTICES → COLOUR, check stuff is nice

structure hat_guesser (n : ℕ) (f : α → hat_arr α n → fin n) :=
(well_founded: ∀ a b : α, ¬G.adj a b → ∀ arr : hat_arr α n, ∀ k : fin n,
f a arr = f a (function.update arr b k)) -- for some reason, this fails to typecheck.
-- I want to change arr at b to k, but clearly function.update isn't right for this job
(hat_guessing_cond: ∀ arr : hat_arr α n, ∃ a : α, f a arr = arr a)


Would either of these definitions be annoying to use? Also, I'm sticking with finite stuff for now; would it make my life easier to use fintype α instead of just any α? Thanks very much!

#### Thomas Browning (Mar 24 2021 at 03:53):

This hidden information stuff might be related to this talk?
slides: https://leanprover-community.github.io/lt2021/slides/paula-LeanTogether2021.pdf
repo: https://github.com/paulaneeley/modal

#### Eric Rodriguez (Mar 24 2021 at 09:47):

thanks - that's interesting! another possible way to formalize it... been trying to use "neighbour vertices → colour" now and it's feeling okay but not amazing

#### Eric Rodriguez (Mar 24 2021 at 18:25):

i'd appreciate one more bit of advice; here's a #mwe:

import logic.function.basic

structure something {α : Type*} (n : ℕ) (f : α → (α → fin n) → fin n) :=
(well_founded: ∀ a b : α, ∀ k : fin n, ∀ arr : α → fin n,
f a arr = f a (function.update arr b k))


For some reason, function.update doesn't typecheck; what's wrong here?

#### Eric Wieser (Mar 24 2021 at 18:31):

The error message says

failed to synthesize type class instance for
α : Type ?,
n : ℕ,
f : α → (α → fin n) → fin n,
a b : α,
k : fin n,
arr : α → fin n
⊢ decidable_eq α


You need to add [decidable_eq α] to your assumptions

#### Eric Wieser (Mar 24 2021 at 18:33):

Or open_locale classical

#### Eric Rodriguez (Mar 24 2021 at 18:36):

ahh I see it's got to be able to decide whether the input is equal to b. thanks!

Last updated: May 11 2021 at 00:31 UTC