(* Time-stamp: *) (****************************************************************************) (* hat.v *) (* *) (* Pierre Lescanne *) (* *) (* LIP (ENS-Lyon, CNRS, INRIA) *) (* *) (* *) (* Developed in V7.4 January 2001 --- March 2004 *) (****************************************************************************) Section Hat. (* ========= Requirements ======= *) Require Arith. Require classic. Require modal. (* ======== Syntax ======== *) Notation "|- p" := (theorem p) (at level 7). Infix RIGHTA 5 "=>" Imp. Infix 4 "&" AND. Infix 4 "V" OR. Infix RIGHTA 4 "|" Xor. Notation "¬ p" := (Not p) (at level 3). (* ======== Data ======== *) (* (white i) means "Agent i wears at least a white hat". (red i) means "Agent i wear only read hats". *) Variable white, red: (i:nat)proposition. (* ========== Abbreviations ======= *) Definition Alice := (0). Definition Bob := (1). Definition Carol := (2). (* Kh i means "Agent i knows she wears a white hat or not". *) Definition Kh := [i:nat] (K i (white i)) V (K i (red i)). (* ========= Basic properties ====== *) (* An agent wears at least a white hat xor only red ones. *) Axiom One_hat: (i:nat) |- (white i) | (red i). (* There are only two white hats *) Axiom Two_white_hats: |- (white Bob) & (white Carol) => (red Alice). (* Each agent knows the hat of the two other agents, in some events, namely agent 0 and 1 know the hat of the others when this hat is white. *) Axiom KA_white1: |- (white Bob) => (K Alice (white Bob)). Axiom KA_white2: |- (white Carol) => (K Alice (white Carol)). Axiom KB_white2: |- (white Carol) => (K Bob (white Carol)). (* =========== Some lemmas ============ *) (* -------------------- about One_hat -------------------- *) Lemma One_hat1: (i:nat) |- ¬(white i) => (red i). Proof. Intros. Apply MP with (white i) | (red i). Apply Xor_Imp. Apply One_hat. Qed. Lemma One_hat3: (i:nat) |- ¬(red i) => (white i). Proof. Intros. Apply MP with (red i) | (white i). Apply Xor_Imp. Apply MP with (white i) | (red i). Apply Xor_comm. Apply One_hat. Qed. Lemma One_hat4: (i:nat) |- (white i) => ¬(red i). Proof. Intros. Apply MP with (white i) | (red i). Apply Xor_Imp2. Apply One_hat. Qed. Lemma KB_nrC: |- ¬(red Carol) => (K Bob ¬(red Carol)). Proof. Apply Cut_rule with (white Carol). Apply One_hat3. Apply Cut_rule with (K Bob (white Carol)). Apply KB_white2. Apply rule_imp_K. Apply One_hat4. Qed. (* -------------------- about Kh -------------------- *) Lemma wB_wC_then_KA_rA: |- (white Bob) & (white Carol) => (K Alice (red Alice)). Proof. Apply Cut_rule with (K Alice (white Bob) & (white Carol)). Apply Cut_rule with (K Alice (white Bob)) & (K Alice (white Carol)). Apply rule_glueAND. Apply KA_white1. Apply KA_white2. Apply AND_Ki. Apply rule_imp_K. Apply Two_white_hats. Qed. (* -------------------- relations between white and red --------------------*) Lemma not_wB_wC_then_rB_or_rC: |- ¬((white Bob) & (white Carol)) => (red Bob) V (red Carol). Proof. Apply Cut_rule with ¬(white Bob) V ¬(white Carol). Apply Class_OR_Not. Apply rule_glueOR; Apply One_hat1. Qed. (* ------------ What can be inferred from "Agent i don't know her hat"? ----------- *) Lemma Not_KhA_then_rB_or_rC: |- ¬(Kh Alice) => (red Bob) V (red Carol). Proof. Apply Cut_rule with ¬(K Alice (red Alice)). Apply rule_Contrapos1. Unfold Kh. Apply OR2. Apply Cut_rule with ¬((white Bob) & (white Carol)). Apply rule_Contrapos1. Apply wB_wC_then_KA_rA. Apply not_wB_wC_then_rB_or_rC. Qed. Lemma Not_KhA_and_Not_rC_then_rB: |- ¬(Kh Alice) & ¬(red Carol) => (red Bob). Proof. Apply Cut_rule with ((red Bob) V (red Carol)) & (Not (red Carol)). Apply rule_AND_right_regular. Apply Not_KhA_then_rB_or_rC. Apply Cut_rule with ((red Bob) & ¬(red Carol)) V ((red Carol) & ¬(red Carol)). Apply dist_AND2. Apply Cut_rule with (red Bob) V FALSE. Apply rule_glueOR. Apply AND1. Apply Cut_rule with ¬(red Carol) & (red Carol). Apply AND_comm. Apply Not_p_AND_p. Apply OR_FALSE. Qed. (* ==================== The final theorem ==================== *) Theorem Final: |- (K Bob ¬(Kh Alice)) & ¬(Kh Bob) => (red Carol). Proof. Apply r_not_p_then_q. Apply Cut_rule with (K Bob ¬(Kh Alice)) & (K Bob ¬(red Carol)). Apply rule_AND_left_regular. Apply KB_nrC. Apply Cut_rule with (K Bob ¬(Kh Alice) & ¬(red Carol)). Apply AND_Ki. Apply Cut_rule with (K Bob (red Bob)). Apply rule_imp_K. Apply Not_KhA_and_Not_rC_then_rB. Unfold Kh. Apply OR2. Qed. Lemma Final1: |- (K Carol (K Bob ¬(Kh Alice)) & ¬(Kh Bob)) => (K Carol (red Carol)). Proof. Apply rule_imp_K. Apply Final. Qed. Lemma Final2: |- (K Carol (K Bob ¬(Kh Alice)) & ¬(Kh Bob)) => (Kh Carol). Proof. Apply Cut_rule with (K Carol (red Carol)). Apply Final1. Unfold Kh. Apply OR2. Qed. End Hat.