Defining "hat games"

Stream: new members

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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]

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]

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]

Or open_locale classical

[Eric Rodriguez]

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