(* Time-stamp: <modified on 28 Apr 2004 at 17:37 by Pierre Lescanne> *)

(****************************************************************************)
(*                              modal.v                                     *)
(*                                                                          *)
(*                             Pierre Lescanne                              *)
(*                                                                          *)
(*		       LIP (ENS-Lyon, CNRS, INRIA)                          *)
(*                                                                          *)
(*                                                                          *)
(* Developed in V7.4   January 2001   ---   March 2004                      *)
(****************************************************************************)
Section Modal_logic.

Require Export predicates.

(* ======== Syntax ======== *)

Notation "|- p" := (theorem p) (at level 7).
Infix RIGHTA 5 "=>" Imp.
Infix 4 "&" AND.
Infix 4 "V" OR.

(* ------------------------- Modal calculus ------------------------- *)

(* Distribution Axiom *)
Axiom K_K: (i: nat) (p,q:proposition) 
    |- (K i p) => (K i (p => q)) => (K i q).		                

(* Knowledge Axiom *)   
Axiom K_T: (i: nat) (p:proposition) |- (K i p) => p.                        

(* Knowledge rule *)
Axiom K_rule: (i: nat) (p:proposition) |- p ->  |- (K i p)          .          		


(* ------------------------- Lemmas ------------------------- *)


(* Ki(p) , Ki(p => q) |- Ki(q) *)

Lemma rule_K: (i:nat) (p,q:proposition) 
  |- (K i p) -> |- (K i (p => q)) -> |- (K i q).

Proof.
Intros.
Apply MP with p:=(K i p).
Apply MP with p:=(K i (p => q)).
Apply MP with p:=(K i p) => (K i (p => q)) => (K i q).
Apply Hilbert_C.
Apply K_K.
Trivial.
Trivial.
Qed.

(* Ki(p=>q) => Ki p => Ki q *)

Lemma K_K_rev: (i: nat) (p,q:proposition) 
    |- (K i (p => q)) => (K i p) => (K i q).     
Proof.
Intros. Apply rule_C. Apply K_K.
Qed.

Lemma rule_K_K_rev: (i: nat) (p,q:proposition) 
    |- (K i (p => q)) -> |- (K i p) => (K i q).
Proof.
Intros. Apply MP with (K i (p => q)). Apply K_K_rev. Assumption.
Qed.

Lemma rule_imp_K : (i: nat) (p,q:proposition) 
    |- (p => q) -> |- (K i p) => (K i q).
Proof.
Intros. Apply rule_K_K_rev. Apply K_rule. Trivial.
Qed.

(* Ki(p1 & p2) => Ki p1 *)

Lemma Ki_AND1: (p1,p2:proposition; i:nat) |- (K i (p1 & p2)) => (K i p1).
Proof.
Intros. Apply MP with (K i ((p1 & p2) => p1)).
Apply K_K_rev.
Apply K_rule. Apply AND1.
Qed.

(* Ki(p1 & p2) => Ki p2 *)

Lemma Ki_AND2:(p1,p2:proposition; i:nat) |- (K i (p1 & p2)) => (K i p2).
Proof.
Intros. Apply MP with (K i (p1 & p2) => p2).
Apply K_K_rev.
Apply K_rule. Apply AND2.
Qed.

(* Ki(p1 & p2) => (Ki p1  & Ki p2) *)

Lemma Ki_AND: (p1,p2:proposition; i:nat)
    |- (K i (p1 & p2)) => ((K i p1) & (K i p2)).
Proof.
Intros. Apply rule_AND_Imp. Apply Ki_AND1. Apply Ki_AND2.
Qed.

(*  Ki(p1 & p2) |- (Ki p1 & Ki p2) *)

Lemma rule_Ki_AND: (i:nat) (p1,p2: proposition) 
   |- (K i (p1 & p2)) ->  |- ((K i p1) & (K i p2)).
Proof.
Intros. Apply MP with (K i (p1 & p2)). Apply Ki_AND. Assumption.
Qed.

(*  (Ki p1 & Ki p2) => Ki(p1 & p2) *)

Lemma AND_Ki: (i:nat) (p1,p2: proposition) 
    |- ((K i p1) & (K i p2)) => (K i (p1 & p2)).
Proof.
Intros.
Apply rule_Imp_AND.
Apply Cut_rule with (K i p2 => p1 & p2).
Apply MP with (K i p1 => p2 => p1 & p2).
Apply K_K_rev.
Apply K_rule.
Apply AND0.
Apply K_K_rev.
Qed.


(*  (Ki p1 & Ki p2) |- Ki(p1 & p2) *)

Lemma rule_AND_Ki: (i:nat) (p1,p2: proposition) 
    |- ((K i p1) & (K i p2)) -> |- (K i (p1 & p2)).
Proof.
Intros.
Apply rule_K with p1. 
Apply MP with ((K i p1) & (K i p2)). Apply AND1. Assumption. 
Apply rule_K with p2. 
Apply MP with ((K i p1) & (K i p2)). Apply AND2. Assumption. 
Apply K_rule. Apply rule_C. Apply AND0.
Qed.

(* Ki Forall P  => Forall Ki P *)

Lemma KiForall: (A: Set) (i:nat) (P:A->proposition)
    |- (K i (Forall A P)) -> |- (Forall A [x:A](K i (P x))).
Proof.
Intros. Apply ForallRule. Intro a. Apply rule_K with p:=(Forall A P). 
Assumption.
Apply K_rule. Apply Forall1.
Qed.

(* Ki p V Ki q => Ki(p V q) *)

Lemma ORKi: (i:nat) (p1,p2: proposition) 
   |- ((K i p1) V (K i p2)) => (K i (p1 V p2)).
Proof.
Intros.
Apply rule_OR0. Apply MP with (K i p1 => (p1 V p2)).
Apply rule_C.
Apply K_K. Apply K_rule. Apply OR1.
Apply MP with (K i p2 => (p1 V p2)).
Apply rule_C.
Apply K_K. Apply K_rule.  Apply OR2.
Qed.

(*  WARNING: Note that their could not be a lemma Ki(p v q) => Ki p v Ki q 
    as it is not true that "if Alice knows a v b, then Alice knows a or Alice knows b" *)


(* Exist x Ki(P x) => Ki(Exist x (P x)) *)
Lemma KiExist: (A: Set) (i:nat) (P:A->proposition)
    |- (Exist A [x:A] (K i (P x))) => (K i (Exist A P)).
Proof.
Intros. 
Apply MP with (Forall A [x:A]((K i (P x)) => (K i (Exist A P)))).
Apply Exist2 with P:= [x:A](K i (P x)).
Apply ForallRule. Intros a. Apply MP with (K i (P a) => (Exist A P)).
Apply rule_C. Apply K_K. Apply K_rule. Apply Exist1.
Qed.

End Modal_logic.