Library chapeau

Require Import ssreflect ssrfun ssrbool eqtype seq fintype ssrnat ssralg zmodp.

Import GRing.Theory.

Section Chapeau.

(* Les personnes                                                              *)

Definition person := 'I_3.
Definition albert : person := 0%R.
Definition marie : person := 1%R.
Definition sophie : person := 2%:R%R.

(* Les couleurs                                                               *)

Definition colour := bool.
Definition white : colour := true.
Definition black : colour := false.

Lemma WNB (c : colour) : (c == white) = (c != black).

(* Une configuration associe à une personne une couleur de chapeau            *)

Definition config := person -> colour.

(* Un maximum de 2 chapeaux blancs                                            *)

Hypothesis max_white : forall (c : config),
  (c albert == white) + (c marie == white) + (c sophie == white) <= 2.

Lemma max_whileP (c : config) :
  [|| c albert == black, c marie == black | c sophie == black].

(* Albert sait si il voit deux chapeaux blancs                                *)

Definition Aknows (c : config) := (c marie == white) && (c sophie == white).

(* Si albert sait, il a un chapeau noir                                       *)

Lemma AknowsB c : Aknows c -> c albert = black.

(* Marie sait si elle voit que sophie a un chapeau blanc                      *)

Definition Mknows (c : config) := (c sophie == white).

(* Si albert ne sait pas et marie sait alors marie a un chapeau noir          *)

Lemma MknowsB c : ~ Aknows c -> Mknows c -> c marie = black.

(* Si ni albert ni marie ne savent, alors sophie a un chapeau noir            *)

Fact result c : ~ Aknows c -> ~ Mknows c -> c sophie = black.

End Chapeau.