Zulip Chat Archive

Stream: new members

Topic: Defining "hat games"


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 24 2021 at 18:33):

Or open_locale classical

view this post on Zulip 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