# Zulip Chat Archive

## 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?

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 (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