Repo zawiera rozwiązanie i dowód formalny poprawności rozwiązania zagadki logicznej o więźniach
W więzieniu było N więźniów. Naczelnik ogłosił więźniom, że mają szansę odzyskać wolność, jeśli sprostają wyzwaniu. Naczelnik przedstawił więźniom następujące zasady wyzwania:
- Naczelnik da więźniom kilka dni do namysłu i ustalenia strategii
- Gdy czas do namysłu się skończy, więźniowie dostaną zakaz jakiejkolwiek komunikacji między sobą
- Naczelnik napisze na czole każdego z więźniów liczbę od 0 do N-1, liczby mogą się powtarzać
- Każdy z więźniów będzie widział liczby na czołach pozostałych współwięźniów, ale nie będzie widział swojej
- Więźniowie będą po kolei szeptali na ucho naczelnikowi domniemaną odpowiedź na pytanie: "Jaką liczbę masz na czole?"
- Jeśli co najmniej jeden z więźniów zgadnie, wszyscy odzyskują wolność
Jaka jest optymalna strategia dla więźniów? W jakich przypadkach zadziała, a w jakich nie?
Źródło zagadki: nie wiem, znalazłem tą zagadkę na zkserowanym fragmencie kartki w formie bajki o Pawle i Gawle. Jeśli ktoś zna źródło to proszę o podanie.
Tutaj jest opis słowno-muzyczny, a dowód formalny w pliku Wiezniowie.v.
Wymagane zależności (w nawiasie podano wersje, które na pewno działają):
- Coq (8.13.2)
- Mathematical Components: ssreflect, algebra (1.12.0)
Kompilacja: make