(* Time-stamp: *) (****************************************************************************) (* epistemic.v *) (* *) (* Pierre Lescanne *) (* *) (* LIP (ENS-Lyon, CNRS, INRIA) *) (* *) (* *) (* Developed in V7.4 January 2001 -- March 2004 *) (****************************************************************************) Section Epistemic_Logic. Require PolyList. Require Export modal. (* ======== Syntax ======== *) Notation "|- p" := (theorem p) (at level 7). Infix RIGHTA 5 "=>" Imp. Infix 4 "&" AND. (* The modality E for "shared knowledge" *) Fixpoint E [g: (list nat)]: proposition -> proposition := [p:proposition] Cases g of nil => TRUE | (cons i g1) => (K i p) & (E g1 p) end. (* ==================== Lemmas on E ======================= *) Lemma E_nil_nat: (p:proposition) |- (E (nil nat) p). Proof. Intros. Simpl. Apply theorem_True. Qed. (* E(p) => p *) Lemma E_T: (g:(list nat); p:proposition; i:nat) |- (E (cons i g) p) => p. Proof. Intros. Unfold E. Apply rule_Imp_AND. Apply rule_Drop. Apply K_T. Qed. (* E(p) => E(p => q) => E(q) *) Lemma E_K: (g:(list nat); p,q:proposition) |- (E g p) => (E g (p => q)) => (E g q). Proof. Intros. Elim g. Unfold E. Apply Hilbert_K. Intros. Unfold E. Apply rule_glueAND2. Apply K_K. Apply H. Qed. (* E(p => q) |- E(p) => E(q) *) Lemma rule_E_K : (g:(list nat); p,q:proposition) |- (E g (p => q)) -> |- (E g p) => (E g q). Proof. Intros. Apply MP with (E g (p => q)). Apply rule_C. Apply E_K. Assumption. Qed. (* p |- E(p) *) Lemma E_rule: (g:(list nat); p:proposition) |- p -> |- (E g p). Proof. Intros. Elim g. Unfold E. Apply theorem_True. Intros. Unfold E. Apply rule_split_AND. Apply K_rule. Assumption. Assumption. Qed. (* p => q |- E(p) => E(q) *) Lemma rule_E_imp : (g:(list nat); p,q:proposition) |- p => q -> |- (E g p) => (E g q). Proof. Intros. Apply rule_E_K. Apply E_rule. Assumption. Qed. (* i in g |- E(p) => Ki(p) *) Lemma E_Ki: (g:(list nat); p:proposition; i:nat) (In i g) -> |- (E g p) => (K i p). Proof. Intros g p i. Elim g. Intro. Elim H. Intros. Elim H0. Intro. Elim H1. Unfold E. Apply AND1. Intros. Unfold E. Apply Cut_rule with (E l p). Apply AND2. Apply H. Assumption. Qed. (* E(p1 & p2) => E(p1) *) Lemma E_AND1: (g:(list nat); p1,p2:proposition) |- (E g (p1 & p2)) => (E g p1). Proof. Intros. Elim g. Unfold E. Apply I. Intros. Unfold E. Apply rule_glueAND. Apply Ki_AND1. Apply H. Qed. (* E(p1 & p2) => E(p2) *) Lemma E_AND2: (g:(list nat); p1,p2:proposition) |- (E g (p1 & p2)) => (E g p2). Proof. Intros. Elim g. Unfold E. Apply I. Intros. Unfold E. Apply rule_glueAND. Apply Ki_AND2. Apply H. Qed. (* E(p1 & p2) => E(p1) & E(p2) *) Lemma E_AND: (g:(list nat); p1,p2:proposition) |- (E g (p1 & p2)) => (E g p1) & (E g p2). Proof. Intros. Apply rule_AND_Imp. Apply E_AND1. Apply E_AND2. Qed. (* E(p1) & E(p2) => E(p1 & p2) *) Lemma ANDE: (g:(list nat); p1,p2:proposition) |- (E g p1) & (E g p2) => (E g (p1 & p2)). Proof. Intros. Apply rule_Imp_AND. Apply Cut_rule with (E g (p2 => (p1 & p2))). Apply MP with (E g p1 => p2 => (p1 & p2)). Apply rule_C. Apply E_K. Apply E_rule. Apply AND0. Apply rule_C. Apply E_K. Qed. (* E(p1 & p2) => E(p2 & p1) *) Lemma E_AND_comm: (g:(list nat); p1,p2:proposition) |- (E g p1 & p2) => (E g p2 & p1). Proof. Intros. Apply Cut_rule with (E g p1) & (E g p2). Apply E_AND. Apply Cut_rule with (E g p2) & (E g p1). Apply AND_comm. Apply ANDE. Qed. (* ------------------------- Knowledge calculus ------------------------- *) (* Axiom for C *) Axiom Knowledge: (g:(list nat)) (p:proposition) |- (C g p) => p & (E g (C g p)). (* Rule for C *) (* q => p & E(q) |- q => C(p) *) Axiom Rule_for_C: (g:(list nat)) (p,q:proposition) |- q => (p & (E g q)) -> |- q => (C g p). (* ==================== Lemmas on C ======================= *) (* C(p) => p *) Lemma C_T: (g:(list nat); p:proposition) |- (C g p) => p. Proof. Intros. Apply Cut_rule with p & (E g (C g p)). Apply Knowledge. Apply AND1. Qed. (* C(p) => E(p) *) Lemma C_E : (g:(list nat); p:proposition) |- (C g p) => (E g p). Proof. Intros. Apply Cut_rule with p & (E g (C g p)). Apply Knowledge. Apply rule_Imp_AND_right. Apply MP with (E g ((C g p)) => p). Apply rule_C. Apply E_K. Apply E_rule. Apply C_T. Qed. (* C(p) => E(C(p)) *) Lemma C_EC: (g:(list nat); p:proposition) |- (C g p) => (E g (C g p)). Proof. Intros. Apply Cut_rule with p & (E g (C g p)). Apply Knowledge. Apply AND2. Qed. (* C(p) => C(E(p)) *) Lemma C_CE: (g:(list nat); p:proposition) |- (C g p) => (C g (E g p)). Proof. Intros. Apply Rule_for_C. Apply rule_AND_Imp; [Apply C_E | Apply C_EC]. Qed. (* C(p) => C(p=>q) => C(q) *) Lemma C_K: (g:(list nat); p, q:proposition) |- (C g p) => (C g (p => q)) => (C g q). Proof. Intros. Apply rule_rev_AND_Imp. Apply Rule_for_C. Apply rule_AND_Imp. Apply Cut_rule with p & (p => q). Apply rule_glueAND; Apply C_T. Apply rule_Imp_AND. Apply CI. Apply Cut_rule with (E g (C g p)) & (E g (C g (p => q))). Apply rule_glueAND; Apply C_EC. Apply ANDE. Qed. (* C(p) => C(C(p)) *) (* This does not require K_4 *) Lemma C_4: (g: (list nat); p:proposition) |- (C g p) => (C g (C g p)). Proof. Intros. Apply Rule_for_C. Apply rule_AND_Imp. Apply I. Apply C_EC. Qed. (* p |- C(p) *) Lemma C_rule: (g:(list nat); p:proposition) |- p -> |- (C g p). Proof. Intros. Apply MP with p. Apply Rule_for_C. Apply Drop_hyp. Apply rule_split_AND. Assumption. Apply E_rule. Assumption. Assumption. Qed. (* i in g |- C(p) => Ki(p) , if "i is in g" and "p is a common knowledge", then "agent i knows p" *) Lemma C_Ki : (g:(list nat); i:nat; p:proposition) (In i g) -> |- (C g p) => (K i p). Proof. Intros. Apply Cut_rule with p & (E g (C g p)). Apply Knowledge. Apply rule_Imp_AND_right. Apply Cut_rule with (E g p). Apply rule_E_imp. Apply C_T. Apply E_Ki. Assumption. Qed. (* i in g |- C(p) => Ki(C(p)) *) Lemma C_KiC: (g:(list nat); p:proposition; i:nat) (In i g) -> |- (C g p) => (K i (C g p)). Proof. Intros. Apply Cut_rule with p & (E g (C g p)). Apply Knowledge. Apply Cut_rule with (E g (C g p)). Apply AND2. Apply E_Ki. Assumption. Qed. (* ==== Other fixed points ==== *) Lemma p_and_ECp_is_fxp: (g:(list nat); p:proposition) |- p & (E g (C g p)) => (C g p). Proof. Intros. Apply Rule_for_C. Apply rule_AND_left_regular. Apply MP with (E g ((C g p) => (p & (E g (C g p))))). Apply rule_C. Apply E_K. Apply E_rule. Apply Knowledge. Qed. Lemma p_and_CEp_is_fxp1: (g:(list nat); p:proposition) |- p & (C g (E g p)) => (C g p). Proof. Intros. Apply Rule_for_C. Apply rule_AND_left_regular. Apply Cut_rule with (E g p) & (E g (C g (E g p))). Apply rule_AND_Imp. Apply C_T. Apply C_EC. Apply ANDE. Qed. Lemma p_and_CEp_is_fxp2: (g:(list nat); p:proposition) |- (C g p) => (p & (C g (E g p))). Proof. Intros. Apply rule_AND_Imp. Apply C_T. Apply Rule_for_C. Apply rule_AND_Imp. Apply C_E. Apply C_EC. Qed. Lemma p_and_CEp_is_fxp: (g:(list nat); p:proposition) |- (p & (C g (E g p)) => (C g p)) & ((C g p) => p & (C g (E g p))). Proof. Intros. Apply rule_split_AND; [Apply p_and_CEp_is_fxp1 | Apply p_and_CEp_is_fxp2]. Qed. (* The same properties as for Ki with the same proofs *) Lemma rule_KC: (g:(list nat); p,q:proposition) |- (C g p) -> |- (C g (p => q)) -> |- (C g q). Proof. Intros. Apply MP with p:=(C g p). Apply MP with p:=(C g (p => q)). Apply MP with p:=(C g p) => (C g (p => q)) => (C g q). Apply Hilbert_C. Apply C_K. Trivial. Trivial. Qed. (* C(p=>q) => C(p) => C(q) *) Lemma C_K_rev: (g:(list nat); p,q:proposition) |- (C g (p => q)) => (C g p) => (C g q). Proof. Intros. Apply rule_C. Apply C_K. Qed. (* C(p => q) |- C(p) => C(q) *) Lemma rule_C_K_rev : (g:(list nat); p,q:proposition) |- (C g (p => q)) -> |- (C g p) => (C g q). Proof. Intros. Apply MP with (C g (p => q)). Apply C_K_rev. Assumption. Qed. (* C(p & p2) => C(p) *) Lemma C_AND1: (g:(list nat); p1, p2:proposition) |- (C g (p1 & p2)) => (C g p1). Proof. Intros. Apply MP with (C g (p1 & p2) => p1). Apply C_K_rev. Apply C_rule. Apply AND1. Qed. (* C(p1 & p2) => C p2 *) Lemma C_AND2:(g:(list nat); p1,p2:proposition)|- (C g (p1 & p2)) => (C g p2). Proof. Intros. Apply MP with (C g (p1 & p2) => p2). Apply C_K_rev. Apply C_rule. Apply AND2. Qed. (* C(p1 & p2) => C p1 & C p2 *) Lemma C_AND: (g:(list nat); p1,p2:proposition) |- (C g (p1 & p2)) => (C g p1) & (C g p2). Proof. Intros. Apply rule_AND_Imp. Apply C_AND1. Apply C_AND2. Qed. (* C(p1 & p2) |- (C p1 & C p2) *) Lemma rule_C_AND: (g:(list nat); p1,p2: proposition) |- (C g (p1 & p2)) -> |- ((C g p1) & (C g p2)). Proof. Intros. Apply MP with (C g (p1 & p2)). Apply C_AND. Assumption. Qed. (* C p1 & C p2 => C(p1 & p2) *) Lemma AND_C: (g:(list nat); p1,p2: proposition) |- (C g p1) & (C g p2) => (C g (p1 & p2)). Proof. Intros. Apply rule_Imp_AND. Apply Cut_rule with (C g p2 => (p1 & p2)). Apply MP with (C g p1 => p2 => (p1 & p2)). Apply C_K_rev. Apply C_rule. Apply AND0. Apply C_K_rev. Qed. (* (C p1 & C p2) |- C(p1 & p2) *) Lemma rule_AND_C: (g:(list nat); p1,p2: proposition) |- ((C g p1) & (C g p2)) -> |- (C g (p1 & p2)). Proof. Intros. Apply rule_KC with p1. Apply MP with ((C g p1) & (C g p2)). Apply AND1. Assumption. Apply rule_KC with p2. Apply MP with ((C g p1) & (C g p2)). Apply AND2. Assumption. Apply C_rule. Apply rule_C. Apply AND0. Qed. End Epistemic_Logic.