(********************************************************************************)
(*                           epistemic_logic.v                                 	*)
(*                                                                          	*)
(*                             Pierre Lescanne                              	*)
(*                                                                          	*)
(*		       LIP (ENS-Lyon, CNRS, INRIA) 				*)
(*                                                                          	*)
(*                                                                          	*)
(* Developed in V8.0                 September 2004 (mod. March-June-Sept 2005  *)
(*                                                        August 2006)     	*)
(********************************************************************************)

(* 
    This file contains a development of higher order epistemic logic
    with common knowledge in COQ.  It is made of 11 Sections

    - The definition of "proposition" is based on a non predicative
    notion of Set.  It requires to be run in COQ V8.0 with the
    -impredicative-set option.

    - Section Connector_quantifier_modality gives the axioms for
    epistemic logic with common knowledge and introduces the other
    connectors as abbreviations namely TRUE, FALSE, &, V and ¬. It
    also introduces the quantifier "Exist" and the modality E for
    shared knowledge.

    - Section Minimal_logic gives lemmas in minimal logic, i. e., the
    proposition logic involving only ==>.

    - Section Propositional_logic gives lemmas about intuitionistic
    propositional logic.

    - Section Classic gives lemmas that are consequence of the classic
    axiom: ¬¬p ==> p.

    - Section Predicates_logic gives lemmas about \-/ and Exist.

    - Section Modal_logic gives the consequences of the axioms about
    K, i. e., modal logic lemmas.

    - Section Common_Knowledge gives axioms on epistemic logic with
    common knowledge.

    - The very small Section Barcan sets the Barcan axiom and proves a
    lemma about it.

    - Section Sato proves the equivalence between Masahiko Sato and my
    axioms for common knowledge.

    - Section Hat and Section Muddy_Children treats two examples
    namely the "the king, the three wise men and the hats" and the
    "muddy children".

*)

Section Connector_quantifier_modality.

Require Import List.

(* The connectives *)

Inductive proposition : Set :=
  | Imp : proposition -> proposition -> proposition
  | Forall : forall A : Set, (A -> proposition) -> proposition
  | K : nat -> proposition -> proposition
  | C : list nat -> proposition -> proposition. 

Infix "==>" := Imp (right associativity, at level 85).
Notation "\-/ p" := (Forall _ p) (at level 70, right associativity).

Definition Exist (A : Set) (P : A -> proposition) :=
  \-/ (fun p : proposition => \-/ (fun a : A => P a ==> p) ==> p).
Definition FALSE := \-/ (fun p : proposition => p).
Definition TRUE := Exist proposition (fun p : proposition => p).
Definition NOT (p : proposition) := p ==> FALSE.
    Notation "¬ p" := (NOT p) (at level 45, right associativity).

(* AND noted & *)
Definition AND (p q : proposition) :=
  \-/ (fun r : proposition => (p ==> q ==> r) ==> r).
(* status *)   Infix "&" := AND (left associativity, at level 50).

(* OR noted V *)
Definition OR (p q : proposition) :=
  \-/ (fun r : proposition => (p ==> r) ==> (q ==> r) ==> r).
(* status *)   Infix "V" := OR (left associativity, at level 50).


(* The modality E for "shared knowledge" *)

Fixpoint E (g : list nat) (p : proposition) {struct g} : proposition :=
  match g with
  | nil => TRUE
  | i :: g' => K i p & E g' p
  end.
                           
Inductive theorem : proposition -> Prop :=
 
 (* ------------------------- Propositional calculus ------------------------- *)
 
 (* Hilbert axioms for intuitionistic propositional logic *)
  | Hilbert_K : forall p q : proposition, theorem (p ==> q ==> p)
  | Hilbert_S : forall p q r : proposition,
      theorem ((p ==> q ==> r) ==> (p ==> q) ==> p ==> r)
  | (* Classic *)
    Classic_NOTNOT : forall p : proposition, theorem (¬¬p ==> p)
  | (* Modus Ponens *) (* p ==> q , p |- q *)
     MP : forall p q : proposition, theorem (p ==> q) -> theorem p -> theorem q

      (* --------------------------- Predicate   calculus --------------------------- *)
      
  | Forall1 : forall (A : Set) (P : A -> proposition) (a : A), theorem (\-/ P ==> P a)
  | (* x not in FV(q)  (\-/x (q ==> (P x))) ==> q ==> (\-/x(P x)) *)
      Forall2 : forall (A : Set) (P : A -> proposition) (q : proposition),
      theorem (\-/ (fun x : A => (q ==> P x)) ==> q ==> \-/ P)

  | ForallRule : forall (A : Set) (P : A -> proposition),
      (forall x : A, theorem (P x)) -> theorem (\-/ P)
      
      (* ------------------------- Modal calculus ------------------------- *)
      
  | (* Distribution Axiom *)
      K_K : forall (i : nat) (p q : proposition), theorem (K i p ==> K i (p ==> q) ==> K i q)
  | (* Knowledge Axiom *) 
      K_T : forall (i : nat) (p : proposition), theorem (K i p ==> p)
  | (* Knowledge rule *)
      K_rule : forall (i : nat) (p : proposition), theorem p -> theorem (K i p)
  | (* Positive introspection *)
      K_4 : forall (i : nat) (p : proposition), theorem (K i p ==> K i (K i p))
  | (* Negative introspection *)
      K_5 : forall (i : nat) (p : proposition), theorem (¬K i p ==> K i (¬K i p))
       
      (* ------------------------- Common knowledge logic ------------------------- *)
      
  | Fixpoint_C : forall (g : list nat) (p : proposition), theorem (C g p ==> p & E g (C g p))
  | Greatest_Fixpoint_C : forall (g : list nat) (p q : proposition),
      theorem (q ==> p & E g q) -> theorem (q ==> C g p).

End Connector_quantifier_modality.

Section Minimal_logic.

Notation "|- p" := (theorem p) (at level 80).
Infix "==>" := Imp (right associativity, at level 70).

(* ==================== Implicative Lemmas ======================= *)

Lemma I : forall p : proposition, |- p ==> p.
Proof.
intros. 
apply MP with (p ==> p ==> p). 
apply MP with (p ==> (p ==> p) ==> p).
apply Hilbert_S. apply Hilbert_K. apply Hilbert_K.
Qed.

Lemma KI : forall p q : proposition, |- q ==> p ==> p.                    
Proof.
intros.
apply MP with (p ==> p).
apply Hilbert_K.
apply I.
Qed.

Lemma KS :
 forall p q r t : proposition,
 |- t ==> (p ==> q ==> r) ==> (p ==> q) ==> p ==> r.
Proof.
intros. 
apply MP with ((p ==> q ==> r) ==> (p ==> q) ==> p ==> r).
apply Hilbert_K. 
apply Hilbert_S.
Qed.

Lemma SKS :
 forall p q r t : proposition,
 |-(t ==> p ==> q ==> r) ==> t ==> (p ==> q) ==> p ==> r.
Proof.
intros. 
apply MP with (t ==> (p ==> q ==> r) ==> (p ==> q) ==> p ==> r).
apply Hilbert_S.
apply KS.
Qed.

Lemma B : forall p q r : proposition, |-(p ==> q) ==> (r ==> p) ==> r ==> q.
Proof.
intros.
apply MP with (p := (p ==> q) ==> r ==> p ==> q).
apply SKS.
apply Hilbert_K. 
Qed.

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

Lemma Transitivity_of_Imp :
 forall p q r : proposition, |- p ==> q -> |- q ==> r -> |- p ==> r.
Proof.
intros.
apply MP with (p ==> q).
apply MP with (q ==> r).
apply B.
trivial.
trivial.
Qed.

Lemma BB :
 forall p q r t : proposition,
 |-(p ==> q ==> r) ==> p ==> (t ==> q) ==> t ==> r.
Proof.
intros.
apply MP with ((q ==> r) ==> (t ==> q) ==> t ==> r).
apply B.
apply B.
Qed.

Lemma BBS :
 forall p q r s : proposition,
 |-(p ==> q ==> r) ==> (s ==> p ==> q) ==> s ==> p ==> r.
Proof.
intros.
apply MP with ((p ==> q ==> r) ==> (p ==> q) ==> p ==> r).
apply BB.
apply Hilbert_S.
Qed.

Lemma SBBS :
 forall p q r t : proposition,
 |-((p ==> q ==> r) ==> t ==> p ==> q) ==> (p ==> q ==> r) ==> t ==> p ==> r.
Proof.
intros.
apply MP with ((p ==> q ==> r) ==> (t ==> p ==> q) ==> t ==> p ==> r).
apply Hilbert_S.
apply BBS.
Qed.

Lemma KK : forall p q r : proposition, |- p ==> q ==> r ==> q.
Proof.
intros.
apply MP with (q ==> r ==> q).
apply Hilbert_K.   
apply Hilbert_K.   
Qed.

Lemma Hilbert_C :
 forall p q r : proposition, |-(p ==> q ==> r) ==> q ==> p ==> r.
Proof.
intros.
apply MP with ((p ==> q ==> r) ==> q ==> p ==> q).
apply SBBS.
apply KK.
Qed.

(* p ==> q ==> r |- q ==> p ==> r *)

Lemma rule_C : forall p q r : proposition, |- p ==> q ==> r -> |- q ==> p ==> r. 
Proof.
intros.
apply MP with (p ==> q ==> r).
apply Hilbert_C.
apply H.
Qed.

Lemma CI : forall p q : proposition, |- p ==> (p ==> q) ==> q.
Proof.
intros.
apply MP with ((p ==> q) ==> p ==> q).
apply Hilbert_C.
apply I.
Qed.

Lemma C2 :
 forall p q r s : proposition,
 |-(p ==> q ==> r ==> s) ==> p ==> r ==> q ==> s.
Proof.
intros.
apply MP with ((q ==> r ==> s) ==> r ==> q ==> s).
apply B.
apply Hilbert_C.
Qed.

Lemma rule_C2 :
 forall p q r s : proposition, |- p ==> q ==> r ==> s -> |- p ==> r ==> q ==> s.
Proof.
intros.
apply MP with (p ==> q ==> r ==> s).
apply C2.
trivial.
Qed.

Lemma Transitivity_of_Imp2 :
 forall p q r s : proposition,
 |- p ==> q -> |- s ==> r ==> p -> |- s ==> r ==> q.
Proof.
intros. 
apply Transitivity_of_Imp with (r ==> p).
apply H0. 
apply MP with (p ==> q). apply B. apply H.
Qed.

Lemma CB : forall p q r : proposition, |-(r ==> p) ==> (p ==> q) ==> r ==> q.
Proof.
intros.
apply MP with ((p ==> q) ==> (r ==> p) ==> r ==> q).
apply Hilbert_C.
apply B.
Qed.

Lemma Drop_hyp : forall p q : proposition, |- p -> |- q ==> p.
Proof.
intros. apply MP with p.
apply Hilbert_K. assumption.
Qed.

Lemma Drop_2nd_hyp :
 forall p q r : proposition, |-(p ==> q) ==> p ==> r ==> q.
Proof.
intros. apply Transitivity_of_Imp with (r ==> p ==> q). apply Hilbert_K. apply Hilbert_C.
Qed.

Lemma rule_Drop : forall p q r : proposition, |- p ==> q -> |- p ==> r ==> q.
Proof.
intros. apply MP with (p ==> q). apply Drop_2nd_hyp. assumption.
Qed.

Lemma Cut2 :
 forall p1 p2 q r : proposition,
 |-(p1 ==> p2 ==> q) ==> (q ==> r) ==> p1 ==> p2 ==> r.
Proof.
intros.
apply MP with ((q ==> r) ==> (p1 ==> p2 ==> q) ==> p1 ==> p2 ==> r).
apply Hilbert_C.
apply Transitivity_of_Imp with ((p2 ==> q) ==> p2 ==> r).
apply B.
apply B.
Qed.

Lemma CSI : forall p q : proposition, |-(p ==> p ==> q) ==> p ==> q.
Proof.
intros.
apply MP with (p ==> p).
apply MP with ((p ==> p ==> q) ==> (p ==> p) ==> p ==> q).
apply Hilbert_C.
apply Hilbert_S.
apply I.
Qed.

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

Lemma rule_CSI : forall p q : proposition, |- p ==> p ==> q -> |- p ==> q.
Proof.
intros.
apply MP with (p ==> p ==> q).
apply CSI.
assumption.
Qed.


End Minimal_logic.

Section Propositional_logic.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Infix "V" := OR (left associativity, at level 50).
Notation "¬ p" := (NOT p) (at level 45).

(* a notation for Forall *)

Notation "\-/ p" := (Forall _ p) (at level 80, right associativity).

(* -------------------- Two handy lemmas -------------------- *)

Lemma rule_Forall2 :
 forall (A : Set) (P : A -> proposition) (q : proposition),
 |- \-/ (fun x : A => q ==> P x) -> |- q ==> (\-/ P).
intros. 
apply MP with (Forall A (fun x : A => q ==> P x)).
apply Forall2. 
trivial.
Qed.

Lemma Forall_Imp :
 forall (A : Set) (P Q : A -> proposition) (a : A),
 |- P a ==> (\-/ (fun b : A => P b ==> Q b)) ==> Q a.
Proof.
intros. 
apply rule_C.
apply Forall1 with (P := fun a : A => P a ==> Q a).
Qed.

(* ==================== Proof of the basic properties of OR ==================== *)

Lemma OR0 :
 forall p q r : proposition, |-(p ==> r) ==> (q ==> r) ==> p V q ==> r.
Proof.
intros. 
apply rule_C2.
unfold OR in |- *.
apply
 Forall_Imp
  with
    (P := fun r : proposition => p ==> r)
    (Q := fun r : proposition => (q ==> r) ==> r).
Qed.

Lemma OR1 : forall p q : proposition, |- p ==> p V q.
Proof.
intros. 
unfold OR in |- *.
apply
 MP with (\-/ (fun r : proposition => p ==> (p ==> r) ==> (q ==> r) ==> r)).
apply
 Forall2 with (P := fun r : proposition => (p ==> r) ==> (q ==> r) ==> r).
apply ForallRule. intros. 
apply rule_C.
apply MP with (x ==> (q ==> x) ==> x).
apply B.
apply Hilbert_K.
Qed.

Lemma OR2 : forall p q : proposition, |- q ==> p V q.
Proof.
intros. 
unfold OR in |- *.
apply
 MP with (\-/ (fun r : proposition => q ==> (p ==> r) ==> (q ==> r) ==> r)).
apply
 Forall2 with (P := fun r : proposition => (p ==> r) ==> (q ==> r) ==> r).
apply ForallRule. intros.
apply rule_Drop.
apply rule_C. 
apply I.
Qed.

(* ==================== Proof of the basic properties of AND ==================== *)

Lemma AND0 : forall p q : proposition, |- p ==> q ==> p & q.
Proof.
intros.
unfold AND in |- *.
apply
 Transitivity_of_Imp with (\-/ (fun r : proposition => q ==> (p ==> q ==> r) ==> r)).
apply
 MP with (\-/ (fun r : proposition => p ==> q ==> (p ==> q ==> r) ==> r)).
apply Forall2 with (P := fun r : proposition => q ==> (p ==> q ==> r) ==> r).
apply ForallRule. intros.
apply rule_C2. apply rule_C.
apply I.
apply Forall2 with (P := fun r : proposition => (p ==> q ==> r) ==> r).
Qed.

Lemma AND1 : forall p q : proposition, |- p & q ==> p.
Proof.
intros. 
unfold AND in |- *.
apply Transitivity_of_Imp with ((p ==> q ==> p) ==> p).
apply
 Forall1 with (a := p) (P := fun r : proposition => (p ==> q ==> r) ==> r).
apply MP with (p ==> q ==> p).
apply CI.
apply Hilbert_K.
Qed.

Lemma AND2 : forall p q : proposition, |- p & q ==> q.
Proof.
intros. 
unfold AND in |- *.
apply Transitivity_of_Imp with ((p ==> q ==> q) ==> q).
apply Forall1 with (P := fun r : proposition => (p ==> q ==> r) ==> r).
apply MP with (p ==> q ==> q).
apply CI.
apply KI.
Qed.

(* ==================== Proof of the basic properties for Exist ==================== *)

Lemma Exist1 :
 forall (A : Set) (P : A -> proposition) (a : A), |- P a ==> Exist A P.
Proof.
intros. 
unfold Exist in |- *.
apply
 rule_Forall2
  with (P := fun p : proposition => (\-/ (fun a0 : A => P a0 ==> p)) ==> p).
apply ForallRule. intro q. 
apply Forall_Imp with (Q := fun a : A => q).
Qed.

Lemma Exist2 :
 forall (A : Set) (P : A -> proposition) (q : proposition),
 |-(\-/ (fun x : A => P x ==> q)) ==> Exist A P ==> q.
Proof.
intros. 
unfold Exist in |- *.
apply
 Forall_Imp
  with
    (P := fun p : proposition => \-/ (fun a : A => P a ==> p))
    (Q := fun p : proposition => p).
Qed.

(* ==================== Lemmas about FALSE ================= *)


Definition FF := forall p : proposition, |- p.
Definition NEG (P : Prop) := P -> FF.

Lemma False_Imp_everything : forall p : proposition, |- FALSE ==> p.
Proof.
intros. unfold FALSE in |- *. apply Forall1 with (P := fun p : proposition => p).
Qed.

Lemma Everything_Imp_True : forall p : proposition, |- p ==> TRUE.
Proof.
intros. unfold TRUE in |- *. apply Exist1 with (P := fun p : proposition => p).
Qed.

Lemma True_is_False_imp_False : |- TRUE ==> FALSE ==> FALSE.
Proof.
apply KI.
Qed.

Lemma False_imp_False_is_True : |- (FALSE ==> FALSE) ==> TRUE. 
Proof.
apply 
Everything_Imp_True.
Qed.

Lemma NEGFalse : NEG (|- FALSE).
Proof.
unfold FALSE, NEG in |- *. unfold FF in |- *. intros. apply MP with FALSE. apply False_Imp_everything. assumption.
Qed.

Lemma FalseFF : |- FALSE -> FF.
Proof.
unfold FF, FALSE in |- *.
intros.
apply MP with (Forall proposition (fun p : proposition => p)).
apply Forall1 with (P := fun p : proposition => p).
assumption.
Qed.

Lemma FFFalse : FF -> |- FALSE.
Proof.
unfold FF, FALSE in |- *.
intros.
apply ForallRule with (P := fun p : proposition => p). 
assumption.
Qed.


Lemma NEGNOT : forall p : proposition, |-¬p -> NEG (|- p).
unfold NEG in |- *.
intros. 
apply FalseFF.
apply MP with p; assumption.
Qed.

Lemma theorem_True : |- TRUE.
Proof.
unfold TRUE in |- *. apply MP with (TRUE ==> TRUE).
apply Exist1 with (P := fun p : proposition => p). apply I.
Qed.

Lemma NOTNOT : forall p : proposition, |- p ==> ¬(¬p).
Proof.
intros. unfold NOT in |- *. apply rule_C. apply I.
Qed.

Lemma Contraposition : forall p q : proposition, |-(p ==> q) ==> ¬q ==> ¬p.
Proof.
intros.
unfold NOT in |- *.
apply CB. 
Qed.

Lemma rule_Contrapos1 : forall p q : proposition, |- p ==> q -> |-¬q ==> ¬p.
Proof.
intros. 
apply MP with (p ==> q). apply Contraposition. assumption.
Qed.

Lemma rule_Contrapos2 : forall p q : proposition, |- p ==> q -> |-¬q -> |-¬p.
Proof.
intros.
apply MP with (¬q).
apply MP with (p ==> q).
apply Contraposition.
trivial.
trivial.
Qed.

(* ==================== OR Lemmas ======================= *)

(* This lemma shows the connection between \/ (meta or) and V (object or) *)

Lemma rule_OR : forall p q : proposition, (|- p) \/ |- q -> |- p V q.
Proof.
intros. elim H. intros. apply MP with p. apply OR1. assumption.
intros. apply MP with q. apply OR2. assumption.
Qed.


Lemma rule_OR0 :
 forall p q r : proposition, |- p ==> r -> |- q ==> r -> |- p V q ==> r.
Proof.
intros.
apply MP with (q ==> r).
apply MP with (p ==> r).
apply OR0.
assumption.
assumption.
Qed.

Lemma Imp_OR1 : forall p q r : proposition, |- p ==> q -> |- p ==> q V r.
Proof.
intros. 
apply Transitivity_of_Imp with q; auto. apply OR1.
Qed.

Lemma Imp_OR2 : forall p q r : proposition, |- p ==> r -> |- p ==> q V r.
Proof.
intros. 
apply Transitivity_of_Imp with r; auto. apply OR2.
Qed.



Lemma OR_comm : forall p q : proposition, |- p V q ==> q V p.
Proof.
intros.
apply rule_OR0.
apply OR2.
apply OR1.
Qed.

Lemma rule_OR_comm : forall p q : proposition, |- p V q -> |- q V p.
Proof.
intros.
apply MP with (p V q). apply OR_comm. assumption.
Qed.

Lemma OR_ass1 : forall p q r : proposition, |- p V (q V r) ==> p V q V r.
Proof.
intros.
apply rule_OR0.
apply Transitivity_of_Imp with (p V q).
apply OR1.
apply OR1.
apply rule_OR0.
apply Transitivity_of_Imp with (p V q).
apply OR2.
apply OR1.
apply OR2.
Qed.


Lemma OR_ass2 : forall p q r : proposition, |- p V q V r ==> p V (q V r).
Proof.
intros.
apply rule_OR0.
apply rule_OR0.
apply OR1.
apply Transitivity_of_Imp with (q V r).
apply OR1.
apply OR2.
apply Transitivity_of_Imp with (q V r).
apply OR2.
apply OR2.
Qed.


Lemma OR_idempotence : forall p : proposition, |- p V p ==> p.
intro.
apply rule_OR0.
apply I.
apply I.
Qed.

Lemma OR_left_regular :
 forall p q r : proposition, |-(p ==> q) ==> r V p ==> r V q.
Proof.
intros.
apply rule_C.
apply rule_OR0.
apply Transitivity_of_Imp with (r V q).
apply OR1.
apply Hilbert_K.
apply rule_C.
apply MP with (q ==> r V q).
apply B.
apply OR2.
Qed.

Lemma rule_OR_left_regular :
 forall p q r : proposition, |- p ==> q -> |- r V p ==> r V q.
Proof.
intros. 
apply MP with (p ==> q).
apply OR_left_regular.
assumption.
Qed.


Lemma OR_right_regular :
 forall p q r : proposition, |-(p ==> q) ==> p V r ==> q V r.
Proof.
intros.
apply rule_C.
apply rule_OR0.
apply rule_C.
apply MP with (q ==> q V r).
apply B.
apply OR1.
apply Transitivity_of_Imp with (q V r).
apply OR2.
apply Hilbert_K.
Qed.


Lemma rule_OR_right_regular :
 forall p q r : proposition, |- p ==> q -> |- p V r ==> q V r.
Proof.
intros.
apply MP with (p ==> q).
apply OR_right_regular.
trivial.
Qed.


Lemma rule_glueOR :
 forall p1 p2 q1 q2 : proposition,
 |- p1 ==> q1 -> |- p2 ==> q2 -> |- p1 V p2 ==> q1 V q2.
Proof.
intros. 
apply rule_OR0.
apply Transitivity_of_Imp with q1. assumption. apply OR1.
apply Transitivity_of_Imp with q2. assumption. apply OR2.
Qed.

(* ==================== AND Lemmas ======================= *)


Lemma rule_split_AND : forall p1 p2 : proposition, |- p1 -> |- p2 -> |- p1 & p2.
Proof.
intros. 
apply MP with p2. 
apply MP with p1. 
apply AND0. 
assumption. assumption.
Qed.

(* These lemmas shows the connection between /\ (meta and) and & (object and) *)

Lemma rule_AND : forall p1 p2 : proposition, (|- p1) /\ (|- p2) -> |- p1 & p2.
Proof.
intros. elim H. intros. 
apply MP with p2. apply MP with p1. 
apply AND0. assumption. assumption.
Qed.

Lemma rule_AND_alt :
 forall p1 p2 : proposition, |- p1 & p2 -> (|- p1) /\ (|- p2).
Proof.
intros.
apply conj.
apply MP with (p1 & p2). apply AND1. assumption.
apply MP with (p1 & p2). apply AND2. assumption.
Qed.


Lemma Imp_AND : forall p q r : proposition, |-(p ==> q ==> r) ==> p & q ==> r.
Proof.
intros.
apply rule_C.
apply rule_CSI.
apply rule_C2.
apply Transitivity_of_Imp with p.
apply AND1.
apply rule_C.
apply MP with ((q ==> r) ==> p & q ==> r).
apply B.
apply MP with (p & q ==> q).
apply CB.
apply AND2.
Qed.


Lemma rule_Imp_AND :
 forall p q r : proposition, |- p ==> q ==> r -> |- p & q ==> r.
Proof.
intros.
apply MP with (p ==> q ==> r).
apply Imp_AND. assumption.
Qed.


Lemma rule_Imp_AND_left :
 forall p q r : proposition, |- p ==> r -> |- p & q ==> r.
Proof.
intros.
apply rule_Imp_AND.
apply rule_Drop.
assumption.
Qed.


Lemma rule_Imp_AND_right :
 forall p q r : proposition, |- q ==> r -> |- p & q ==> r.
Proof.
intros.
apply rule_Imp_AND.
apply rule_C.
apply rule_Drop.
assumption.
Qed.


Lemma rule_AND_Imp :
 forall p q r : proposition, |- p ==> q -> |- p ==> r -> |- p ==> q & r.
Proof.
intros. 
apply rule_CSI. 
apply MP with (p ==> r). 
apply MP with (r ==> p ==> q & r).
apply B.
apply rule_C. 
apply Transitivity_of_Imp with q. 
assumption. apply AND0.
assumption.
Qed.


Lemma rule_rev_AND_Imp :
 forall p q r : proposition, |- p & q ==> r -> |- p ==> q ==> r.
Proof.
intros. 
apply Transitivity_of_Imp2 with (p & q).  
assumption. apply AND0. 
Qed.


Lemma rule_glueAND :
 forall p1 p2 q1 q2 : proposition,
 |- p1 ==> q1 -> |- p2 ==> q2 -> |- p1 & p2 ==> q1 & q2.
Proof.
intros. 
apply rule_CSI.
apply Transitivity_of_Imp with q1. 
apply Transitivity_of_Imp with p1. 
apply AND1. assumption.
apply rule_C. 
apply Transitivity_of_Imp with p2. 
apply AND2.
apply Transitivity_of_Imp with q2. 
assumption. 
apply rule_C. apply AND0.
Qed.


Lemma rule_glueAND2 :
 forall p1 p2 q1 q2 r1 r2 : proposition,
 |- p1 ==> q1 ==> r1 ->
 |- p2 ==> q2 ==> r2 -> |- p1 & p2 ==> q1 & q2 ==> r1 & r2.
Proof.
intros. 
apply rule_rev_AND_Imp. apply rule_AND_Imp.
apply rule_Imp_AND. 
apply Transitivity_of_Imp with p1. apply AND1. 
apply rule_C. 
apply Transitivity_of_Imp with q1. apply AND1.
apply rule_C. assumption.
apply rule_Imp_AND. 
apply Transitivity_of_Imp with p2. apply AND2. apply rule_C. 
apply Transitivity_of_Imp with q2. apply AND2.
apply rule_C. assumption.
Qed.


Lemma AND_drop1 : forall p1 p2 : proposition, |- p1 & p2 -> |- p1.
Proof.
intros. 
apply MP with (p1 & p2). apply AND1. assumption.
Qed.

Lemma AND_drop2 : forall p1 p2 : proposition, |- p1 & p2 -> |- p2.
Proof.
intros. 
apply MP with (p1 & p2). apply AND2. assumption.
Qed.


Lemma AND_comm : forall p q : proposition, |- p & q ==> q & p.
Proof.
intros.
apply rule_CSI.
apply Transitivity_of_Imp with p.
apply AND1.
apply rule_C.
apply Transitivity_of_Imp with q.
apply AND2.
apply AND0.
Qed.


Lemma rule_AND_comm : forall p q : proposition, |- p & q -> |- q & p.
Proof.
intros. 
apply MP with (p & q).
 apply AND_comm. assumption.
Qed.

Lemma AND_ass : forall p q r : proposition, |- p & q & r ==> p & (q & r).
Proof.
intros.
apply Transitivity_of_Imp with (q & r & p).
apply rule_CSI.
apply Transitivity_of_Imp with p.
apply Transitivity_of_Imp with (p & q).
apply AND1.
apply AND1.
apply rule_C.
apply rule_CSI.
apply Transitivity_of_Imp with r.
apply AND2.
apply rule_C.
apply Transitivity_of_Imp with q.
apply Transitivity_of_Imp with (p & q).
apply AND1.
apply AND2.
apply MP with (q ==> r ==> q & r).
apply MP with (q & r ==> p ==> q & r & p).
apply rule_C.
apply Cut2.
apply AND0.
apply AND0.
apply AND_comm.
Qed.

Lemma AND_ass1 : forall p q r : proposition, |- p & (q & r) ==> p & q & r.
Proof.
intros. apply Transitivity_of_Imp with (r & (p & q)).
apply Transitivity_of_Imp with (r & p & q).
apply Transitivity_of_Imp with (q & (r & p)).
apply Transitivity_of_Imp with (q & r & p).
apply AND_comm. apply AND_ass. apply AND_comm. apply AND_ass. apply AND_comm.
Qed.


Lemma rule_AND_ass : forall p q r : proposition, |- p & q & r -> |- p & (q & r).
Proof. 
intros. 
apply MP with (p & q & r). 
apply AND_ass.
assumption.
Qed.


Lemma rule_AND_ass1 :
 forall p q r : proposition, |- p & (q & r) -> |- p & q & r.
Proof. 
intros. 
apply MP with (p & (q & r)). 
apply AND_ass1.
assumption.
Qed.

Lemma AND_right_regular :
 forall p q r : proposition, |-(p ==> q) ==> p & r ==> q & r.
Proof.
intros.
apply rule_C.
apply rule_CSI.
apply Transitivity_of_Imp with r.
apply AND2.
apply rule_C.
apply MP with (p & r ==> (p ==> q) ==> r ==> q & r).
apply MP with (((p ==> q) ==> r ==> q & r) ==> r ==> (p ==> q) ==> q & r).
apply rule_C.
apply CB.
apply Hilbert_C.
apply Transitivity_of_Imp with p.
apply AND1.
apply rule_C.
apply MP with (q ==> r ==> q & r).
apply rule_C.
apply CB.
apply AND0.
Qed.


Lemma rule_AND_right_regular :
 forall p q r : proposition, |- p ==> q -> |- p & r ==> q & r.
Proof.
intros.
apply MP with (p ==> q).
apply AND_right_regular.
assumption.
Qed.

Lemma AND_left_regular :
 forall p q r : proposition, |-(p ==> q) ==> r & p ==> r & q.
Proof.
intros.
apply rule_C.
apply Transitivity_of_Imp with (p & r).
apply AND_comm.
apply Transitivity_of_Imp2 with (q & r).
apply AND_comm.
apply rule_C.
apply AND_right_regular.
Qed.


Lemma rule_AND_left_regular :
 forall p q r : proposition, |- p ==> q -> |- r & p ==> r & q.
Proof.
intros.
apply MP with (p ==> q).
apply AND_left_regular.
assumption.
Qed.

Lemma AND_idempotence : forall p : proposition, |- p ==> p & p.
Proof.
intros. 
apply rule_CSI. 
apply AND0.
Qed.


Lemma ANDAND : forall p q : proposition, |- p & p ==> q -> |- p ==> q.
Proof.
intros. 
apply Transitivity_of_Imp with (p & p). 
apply AND_idempotence. assumption.
Qed.

Lemma AND_perm : forall p q r : proposition, |- p & (q & r) ==> r & (p & q).
Proof.
intros. 
apply Transitivity_of_Imp with (p & q & r). 
apply AND_ass1.
apply AND_comm.
Qed.

Lemma rule_AND_perm :
 forall p q r : proposition, |- p & (q & r) -> |- r & (p & q).
Proof. 
intros.
apply rule_AND_comm. 
apply rule_AND_ass1. 
assumption.
Qed.

Lemma AND_swap : forall p q r : proposition, |- p & (q & r) ==> q & (p & r).
Proof.
intros. 
apply Transitivity_of_Imp with (p & q & r). 
apply AND_ass1. 
apply Transitivity_of_Imp with (q & p & r). 
apply rule_AND_right_regular.
apply AND_comm. apply AND_ass.
Qed.


(* ==================== Distributivity Lemmas ======================= *)

Lemma undist_AND :
 forall p q r : proposition, |- p & q V (p & r) ==> p & (q V r).
Proof.
intros.
apply rule_OR0.
apply rule_AND_left_regular.
apply OR1.
apply rule_AND_left_regular.
apply OR2.
Qed.

Lemma undist_AND2 :
 forall p q r : proposition, |- p & r V (q & r) ==> p V q & r.
Proof.
intros.
apply Transitivity_of_Imp with (r & (p V q)).
apply Transitivity_of_Imp with (r & p V (r & q)).
apply rule_glueOR; apply AND_comm.
apply undist_AND.
apply AND_comm.
Qed.


Lemma dist_AND :
 forall p q r : proposition, |- p & (q V r) ==> p & q V (p & r).
Proof.
intros.
apply rule_Imp_AND.
apply rule_C.
apply rule_OR0.
apply rule_C.
apply Transitivity_of_Imp2 with (p & q).
apply OR1.
apply AND0.
apply rule_C.
apply Transitivity_of_Imp2 with (p & r).
apply OR2.
apply AND0.
Qed.

Lemma dist_AND2 : forall p q r : proposition, |- p V q & r ==> p & r V (q & r).
Proof.
intros.
apply Transitivity_of_Imp with (r & (p V q)).
apply AND_comm.
apply Transitivity_of_Imp with (r & p V (r & q)).
apply dist_AND.
apply rule_glueOR; apply AND_comm.
Qed.


Lemma undist_OR :
 forall p q r : proposition, |- p V q & (p V r) ==> p V (q & r).
Proof.
intros.
apply rule_Imp_AND.
apply rule_OR0.
apply rule_C.
apply MP with (p ==> p V (q & r)).
apply Hilbert_K.
apply OR1.
apply rule_C.
apply rule_OR0.
apply rule_C.
apply MP with (p ==> p V (q & r)).
apply Hilbert_K.
apply OR1.
apply Transitivity_of_Imp2 with (q & r).
apply OR2.
apply rule_C.
apply AND0.
Qed.

Lemma undist_OR2 :
 forall p q r : proposition, |- q V p & (r V p) ==> q & r V p.
Proof.
intros.
apply Transitivity_of_Imp with (p V (q & r)).
apply Transitivity_of_Imp with (p V q & (p V r)).
apply rule_glueAND; apply OR_comm.
apply undist_OR.
apply OR_comm.
Qed.

Lemma dist_OR : forall p q r : proposition, |- p V (q & r) ==> p V q & (p V r).
Proof.
intros.
apply rule_OR0.
apply rule_CSI.
apply Transitivity_of_Imp with (p V q).
apply OR1.
apply rule_C.
apply Transitivity_of_Imp with (p V r).
apply OR1.
apply rule_C.
apply AND0.
apply rule_Imp_AND.
apply Transitivity_of_Imp with (p V q).
apply OR2.
apply rule_C.
apply Transitivity_of_Imp with (p V r).
apply OR2.
apply rule_C.
apply AND0.
Qed.

Lemma p_or_r_and_q_or_r :
 forall p q r : proposition, |- p V r & (q V r) ==> p & q V r.
Proof.
intros.
apply Transitivity_of_Imp with (p & (q V r) V (r & (q V r))).
apply dist_AND2.
apply Transitivity_of_Imp with (p & (q V r) V r).
apply rule_OR_left_regular.
apply AND1.
apply Transitivity_of_Imp with (p & q V (p & r V r)).
apply Transitivity_of_Imp with (p & q V (p & r) V r).
apply rule_OR_right_regular.
apply dist_AND.
apply OR_ass2.
apply rule_OR_left_regular.
apply rule_OR0.
apply AND2.
apply I.
Qed.


(* ==================== Lemmas about NOT  ======================= *)

Lemma AND_NOT : forall p q : proposition, |-¬(p V q) ==> ¬p & ¬q.
Proof.
intros. 
unfold NOT in |- *. apply rule_AND_Imp.
apply MP with (p ==> p V q). apply Contraposition with (q := p V q) (p := p). apply OR1.
apply MP with (q ==> p V q). apply Contraposition with (q := p V q) (p := q). apply OR2.
Qed.

Lemma AND_NOT_rule : forall p q : proposition, |-¬(p V q) -> |-¬p & ¬q.
Proof.
intros. apply MP with (¬(p V q)). apply AND_NOT. assumption.
Qed.

Lemma Not_OR : forall p q : proposition, |-¬p & ¬q ==> ¬(p V q).
Proof.
intros. unfold NOT in |- *.  apply rule_Imp_AND. apply OR0.
Qed.

Lemma rule_Not_OR : forall p q : proposition, |-¬p & ¬q -> |-¬(p V q).
Proof.
intros. apply MP with (¬p & ¬q). apply Not_OR. assumption.
Qed.

Lemma Not_AND : forall p q : proposition, |-¬p V ¬q ==> ¬(p & q).
Proof.
unfold NOT in |- *.
intros. 
apply rule_OR0.
apply rule_C.
apply Transitivity_of_Imp with p.
apply AND1.
apply rule_C. apply I.
apply rule_C.
apply Transitivity_of_Imp with q.
apply AND2.
apply rule_C. apply I.
Qed.

Lemma rule_Not_AND : forall p q : proposition, |-¬p V ¬q -> |-¬(p & q).
Proof.
intros. 
apply MP with (¬p V ¬q).
apply Not_AND.
assumption.
Qed.

Lemma Not_p_AND_p : forall p : proposition, |-¬p & p ==> FALSE.
Proof.
intros.
unfold NOT in |- *. 
apply rule_Imp_AND.
apply I.
Qed.

Lemma OR_FALSE : forall p : proposition, |- p V FALSE ==> p.
Proof.
intros. 
apply rule_OR0.
apply I.
apply False_Imp_everything.
Qed.

Lemma AND_FALSE : forall p : proposition, |- p & FALSE ==> FALSE.
Proof.
intros.
apply rule_Imp_AND.
apply KI.
Qed.

Lemma AND_TRUE : forall p : proposition, |- p ==> p & TRUE.
Proof.
intros.
apply rule_AND_Imp. apply I. apply Everything_Imp_True.
Qed.


(* ==================== Xor  ======================= *)

Definition Xor (p q : proposition) := p V q & ¬(p & q). 
    Infix "|" := Xor (right associativity, at level 55).

Lemma Xor_Imp : forall p q : proposition, |- p | q ==> ¬p ==> q.
Proof.
intros. unfold Xor in |- *.
apply rule_Imp_AND. apply rule_Drop.
apply rule_OR0.
unfold NOT in |- *. apply rule_C. apply MP with (FALSE ==> q).
apply B. apply False_Imp_everything. apply Hilbert_K.
Qed.

Lemma Xor_comm : forall p q : proposition, |- p | q ==> q | p.
intros p q.
unfold Xor in |- *.
apply rule_glueAND.
apply OR_comm.
apply rule_Contrapos1.
apply AND_comm.
Qed.

End Propositional_logic. 

Section Classic.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Infix "V" := OR (left associativity, at level 50).
Infix "|" := Xor (right associativity, at level 55).
Notation "¬ p" := (NOT p) (at level 45).


Lemma Class_OR_NOT : forall p q : proposition, |-¬(p & q) ==> ¬p V ¬q.
Proof.
intros.
apply Transitivity_of_Imp with (¬(¬(¬p V ¬q))).
apply rule_Contrapos1.
apply Transitivity_of_Imp with (¬(¬p) & ¬(¬q)). apply AND_NOT.
apply rule_glueAND; apply Classic_NOTNOT.
apply Classic_NOTNOT.
Qed.

Lemma rule_Class_OR_NOT : forall p q : proposition, |-¬(p & q) -> |-¬p V ¬q.
Proof.
intros.
apply MP with (¬(p & q)).
apply Class_OR_NOT.
assumption.
Qed.

Lemma not_p_then_q : forall p q : proposition, |-(¬p ==> q) ==> ¬q ==> p.
Proof.
intros. 
apply Transitivity_of_Imp with (¬q ==> ¬(¬p)).
apply Contraposition.
apply MP with (¬(¬p) ==> p).
apply B.
apply Classic_NOTNOT.
Qed.

Lemma r_not_p_then_q :
 forall p q r : proposition, |- r & ¬p ==> q -> |- r & ¬q ==> p.
Proof.
intros.
apply rule_Imp_AND. 
apply Transitivity_of_Imp with (¬p ==> q).
apply rule_rev_AND_Imp.
assumption.
apply not_p_then_q.
Qed.

Lemma Class_OR : forall p q : proposition, |-¬(¬p & ¬q) ==> p V q.
Proof.
intros. apply Transitivity_of_Imp with (¬(¬p) V ¬(¬q)).
apply Class_OR_NOT.
apply rule_glueOR; apply Classic_NOTNOT.
Qed.

Lemma rule_Class_OR : forall p q : proposition, |-¬(¬p & ¬q) -> |- p V q.
Proof.
intros. apply MP with (¬(¬p & ¬q)).
apply Class_OR.
assumption.
Qed.

Lemma Excluded_middle : forall p : proposition, |- p V ¬p.
Proof.
intros. 
apply rule_Class_OR. apply MP with (¬FALSE).
apply rule_Contrapos1.
apply rule_Imp_AND.
apply rule_C.
apply rule_rev_AND_Imp.
apply Not_p_AND_p.
unfold NOT in |- *. apply I.
Qed.

Lemma Class_OR_with_disjunction :
 forall p q : proposition, |- p V q ==> p & ¬q V q.
Proof.
intros. 
apply Transitivity_of_Imp with (p V q & (¬q V q)).
apply rule_AND_Imp.
apply I.
apply Transitivity_of_Imp with TRUE.
apply Everything_Imp_True.
apply Transitivity_of_Imp with (¬(q & ¬q)).
apply Transitivity_of_Imp with (¬FALSE). unfold NOT in |- *. apply KI.
apply rule_Contrapos1. unfold NOT in |- *.
apply rule_Imp_AND. apply CI.
apply Transitivity_of_Imp with (¬(¬(¬q) & ¬q)).
apply rule_Contrapos1.
apply rule_AND_right_regular.
apply Classic_NOTNOT.
apply Class_OR.
apply undist_OR2.
Qed.


(* About Xor *)

Lemma Xor_Imp2 : forall p q : proposition, |- p | q ==> p ==> ¬q.
Proof.
intros. unfold Xor in |- *.
apply rule_Imp_AND.
apply rule_C.
apply Transitivity_of_Imp with (¬p V ¬q).
apply Class_OR_NOT.
apply rule_OR0.
apply rule_C.
apply rule_OR0.
apply Transitivity_of_Imp2 with FALSE.
apply False_Imp_everything.
unfold NOT in |- *. apply CI.
apply rule_C. apply rule_Drop.
apply Transitivity_of_Imp2 with FALSE.
apply False_Imp_everything.
unfold NOT in |- *. apply I.
apply rule_Drop. apply rule_Drop.
apply I.
Qed.

End Classic.

Section Predicates_logic.


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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Notation "\-/ p" := (Forall _ p) (at level 70, right associativity).

(* =====================  Forall Lemmas ======================= *)

(* (\-/x,y) Q(x,y) ==> Q(a,b)  *)

Lemma Forallx_Forally :
 forall (A : Set) (Q : A -> A -> proposition) (a b : A),
 |-(\-/ (fun x : A => \-/ Q x)) ==> Q a b.
Proof.
intros. apply Transitivity_of_Imp with (\-/ Q a). 
apply Forall1 with (a := a) (P := fun x1 : A => \-/ Q x1). 
apply Forall1.
Qed.

(* (\-/x(\-/y Q(x,y))) ==> (\-/y(\-/x Q(x,y))) *)

Lemma ForallForall :
 forall (A : Set) (Q : A -> A -> proposition),
 |-(\-/ (fun x : A => \-/ Q x)) ==>
   \-/ (fun y : A => \-/ (fun x : A => Q x y)).
Proof.
intros.
apply
 MP
  with
    (\-/
     (fun y : A =>
      (\-/ (fun x : A => \-/ Q x)) ==>
      (fun y : A => \-/ (fun x : A => Q x y)) y)).
apply
 Forall2
  with
    (q := \-/ (fun x : A => \-/ Q x))
    (P := fun y : A => \-/ (fun x : A => Q x y)).
apply ForallRule.  intro.
apply MP with (\-/ (fun x1 : A => (\-/ (fun x0 : A => \-/ Q x0)) ==> Q x1 x)).
apply
 Forall2 with (q := \-/ (fun x0 : A => \-/ Q x0)) (P := fun x0 : A => Q x0 x).
apply ForallRule. intro.
apply Forallx_Forally.
Qed.

(* Q(a,b)  ==>  (Exist x,y) Q(x,y) *)

Lemma Existy_Existx :
 forall (A : Set) (Q : A -> A -> proposition) (a b : A),
 |- Q a b ==> Exist A (fun y1 : A => Exist A (fun x1 : A => Q x1 y1)).
Proof.
intros. apply Transitivity_of_Imp with (Exist A (fun x1 : A => Q x1 b)). apply Exist1 with (P := fun x1 : A => Q x1 b).
apply
 Exist1 with (P := fun y1 : A => Exist A (fun x1 : A => Q x1 y1)) (a := b).
Qed.

(* (Exist x (Exist y Q(x,y))) ==> (Exist y (Exist x Q(x,y))) *)

Lemma ExistExist :
 forall (A : Set) (Q : A -> A -> proposition),
 |- Exist A (fun x : A => Exist A (Q x)) ==>
   Exist A (fun y : A => Exist A (fun x : A => Q x y)).
Proof.
intros. apply
  MP
   with
     (\-/
      (fun x : A =>
       Exist A (Q x) ==> Exist A (fun y : A => Exist A (fun x : A => Q x y)))).
apply
 Exist2
  with
    (P := fun x : A => Exist A (Q x))
    (q := Exist A (fun y : A => Exist A (fun x : A => Q x y))).
apply ForallRule. intro.
apply
 MP
  with
    (\-/
     (fun y0 : A =>
      Q x y0 ==> Exist A (fun y : A => Exist A (fun x0 : A => Q x0 y)))).
apply
 Exist2
  with
    (P := Q x)
    (q := Exist A (fun y : A => Exist A (fun x0 : A => Q x0 y))).
apply ForallRule. intro. apply Existy_Existx.
Qed.

(* (Exist x (\-/y Q(x,y))) ==> (\-/y (Exist x Q(x,y))) *)

Lemma ExistForall :
 forall (A : Set) (Q : A -> A -> proposition),
 |- Exist A (fun x : A => \-/ Q x) ==>
   \-/ (fun y : A => Exist A (fun x : A => Q x y)).
Proof.
intros. apply
  MP
   with
     (\-/
      (fun x : A =>
       (\-/ Q x) ==> \-/ (fun y : A => Exist A (fun x : A => Q x y)))).
apply
 Exist2
  with
    (P := fun x : A => \-/ Q x)
    (q := \-/ (fun y : A => Exist A (fun x : A => Q x y))).
apply ForallRule. intro a. apply
  MP with (\-/ (fun y : A => (\-/ Q a) ==> Exist A (fun x : A => Q x y))).
apply
 Forall2 with (q := \-/ Q a) (P := fun y : A => Exist A (fun x : A => Q x y)).
apply ForallRule. intro b. apply Transitivity_of_Imp with (Q a b). apply Forall1. 
apply Exist1 with (P := fun x : A => Q x b). 
Qed.


End Predicates_logic.

Section Modal_logic.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Infix "V" := OR (left associativity, at level 50).
Notation "\-/ p" := (Forall _ p) (at level 70, right associativity).
Notation "¬ p" := (NOT p) (at level 45).

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


Lemma rule_K :
 forall (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.


Lemma K_K_rev :
 forall (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 :
 forall (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 :
 forall (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.


Lemma Ki_AND1 :
 forall (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.


Lemma Ki_AND2 :
 forall (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.


Lemma Ki_AND :
 forall (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.


Lemma rule_Ki_AND :
 forall (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.


Lemma AND_Ki :
 forall (i : nat) (p1 p2 : proposition), |- K i p1 & K i p2 ==> K i (p1 & p2).
Proof.
intros.
apply rule_Imp_AND.
apply Transitivity_of_Imp 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.


Lemma rule_AND_Ki :
 forall (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.


Lemma KiForall :
 forall (A : Set) (i : nat) (P : A -> proposition),
 |- K i (\-/ P) -> |- \-/ (fun x : A => K i (P x)).
Proof.
intros. apply ForallRule. intro a. apply rule_K with (p := \-/ P). 
assumption.
apply K_rule. apply Forall1.
Qed.


Lemma ORKi :
 forall (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" *)


Lemma KiExist :
 forall (A : Set) (i : nat) (P : A -> proposition),
 |- Exist A (fun x : A => K i (P x)) ==> K i (Exist A P).
Proof.
intros. 
apply MP with (Forall A (fun x : A => K i (P x) ==> K i (Exist A P))).
apply Exist2 with (P := fun 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.


Theorem Rumsfeld1 :
 forall i : nat,
 |- K i (Exist proposition (fun p : proposition => K i (K i p))).
 Proof.
intros. 
apply K_rule.
apply MP with (K i (K i TRUE)).
apply Exist1 with (P := fun p : proposition => K i (K i p)).
apply MP with (K i TRUE).
apply K_4.
apply K_rule.
apply theorem_True.
Qed.


(* Secretary of Defense Donald Rumsfeld has declared that "we know
   there are known unknowns" *)

Theorem Rumsfeld2 :
 forall i : nat,
 |- K i (Exist proposition (fun p : proposition => K i (¬K i p))).
Proof.
intros.
apply K_rule.
apply MP with (K i (¬K i FALSE)).
apply Exist1 with (P := fun p : proposition => K i (¬K i p)).
apply MP with (¬K i FALSE).
apply K_5.
unfold NOT in |- *.
apply K_T.
Qed.

End Modal_logic.

Section Common_Knowledge.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Notation "\-/ p" := (Forall _ p) (at level 70, right associativity).

(* ==================== Lemmas on E ======================= *)

Lemma E_nil_nat : forall p : proposition, |- E nil p.
Proof.
intros.
simpl in |- *.
apply theorem_True.
Qed.


Lemma E_T :
 forall (g : list nat) (p : proposition) (i : nat), |- E (i :: g) p ==> p.
Proof.
intros. unfold E in |- *. apply rule_Imp_AND. apply rule_Drop. apply K_T.
Qed.


Lemma E_K :
 forall (g : list nat) (p q : proposition),
 |- E g p ==> E g (p ==> q) ==> E g q. 
Proof.
intros. elim g. unfold E in |- *. apply Hilbert_K.
intros. unfold E in |- *. apply rule_glueAND2. apply K_K. apply H.
Qed.


Lemma rule_E_K :
 forall (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.


Lemma E_rule : forall (g : list nat) (p : proposition), |- p -> |- E g p.
Proof.
intros. elim g. unfold E in |- *. apply theorem_True.
intros. unfold E in |- *. apply rule_split_AND. apply K_rule. assumption. assumption.
Qed.


Lemma rule_E_imp :
 forall (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.


Lemma E_Ki :
 forall (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 in |- *. apply AND1.
intros. unfold E in |- *. apply Transitivity_of_Imp with (E l p). apply AND2. apply H. assumption.
Qed.


Lemma E_AND1 :
 forall (g : list nat) (p q : proposition), |- E g (p & q) ==> E g p.
Proof.
intros. elim g. unfold E in |- *. apply I.
intros. unfold E in |- *. apply rule_glueAND. apply Ki_AND1. apply H.
Qed.


Lemma E_AND2 :
 forall (g : list nat) (p q : proposition), |- E g (p & q) ==> E g q.
Proof.
intros.  elim g. unfold E in |- *. apply I. 
intros. unfold E in |- *. apply rule_glueAND. apply Ki_AND2. apply H.
Qed.


Lemma E_AND :
 forall (g : list nat) (p q : proposition), |- E g (p & q) ==> E g p & E g q.
Proof.
intros. apply rule_AND_Imp. apply E_AND1. apply E_AND2.
Qed.


Lemma ANDE :
 forall (g : list nat) (p q : proposition), |- E g p & E g q ==> E g (p & q).
Proof.
intros. apply rule_Imp_AND. apply Transitivity_of_Imp with (E g (q ==> p & q)). 
apply MP with (E g (p ==> q ==> p & q)). apply rule_C. apply E_K.
apply E_rule. apply AND0. apply rule_C. apply E_K.
Qed.


Lemma E_AND_comm :
 forall (g : list nat) (p q : proposition), |- E g (p & q) ==> E g (q & p).
Proof.
intros. apply Transitivity_of_Imp with (E g p & E g q). apply E_AND.
apply Transitivity_of_Imp with (E g q & E g p). apply AND_comm. apply ANDE.
Qed.


(* ==================== Lemmas on C ======================= *)


Lemma C_T : forall (g : list nat) (p : proposition), |- C g p ==> p.
Proof.
intros. apply Transitivity_of_Imp with (p & E g (C g p)). 
apply Fixpoint_C. apply AND1.
Qed.

Lemma C_E : forall (g : list nat) (p : proposition), |- C g p ==> E g p.
Proof.
intros. 
apply Transitivity_of_Imp with (p & E g (C g p)).
apply Fixpoint_C.
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.


Lemma C_EC : forall (g : list nat) (p : proposition), |- C g p ==> E g (C g p).
Proof.
intros. apply Transitivity_of_Imp with (p & E g (C g p)). apply Fixpoint_C. apply AND2.
Qed.

Lemma C_K :
 forall (g : list nat) (p q : proposition),
 |- C g p ==> C g (p ==> q) ==> C g q.
Proof.
intros. apply rule_rev_AND_Imp. apply Greatest_Fixpoint_C. apply rule_AND_Imp. apply Transitivity_of_Imp with (p & (p ==> q)).
apply rule_glueAND; apply C_T. 
apply rule_Imp_AND. apply CI. 
apply Transitivity_of_Imp with (E g (C g p) & E g (C g (p ==> q))). 
apply rule_glueAND; apply C_EC.
apply ANDE.
Qed.

Lemma C_K_rev: 
 forall (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.

Lemma rule_C_K_rev:
 forall (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.

Lemma C_CE : forall (g : list nat) (p : proposition), |- C g p ==> C g (E g p).
Proof.
intros.
apply Greatest_Fixpoint_C.
apply rule_AND_Imp; [ apply C_E | apply C_EC ].
Qed.

(* This does not require K_4 *)

Lemma C_4 : forall (g : list nat) (p : proposition), |- C g p ==> C g (C g p).
Proof.
intros. apply Greatest_Fixpoint_C. apply rule_AND_Imp. apply I. apply C_EC.
Qed.


Lemma C_rule : forall (g : list nat) (p : proposition), |- p -> |- C g p.
Proof.
intros. apply MP with p.
apply Greatest_Fixpoint_C.
apply Drop_hyp. apply rule_split_AND. assumption. apply E_rule. assumption. assumption.
Qed.

Lemma C_CKi : forall (i : nat) (g : list nat) (p : proposition), (In i g) -> |- C g p ==> C g (K i p).
Proof.
intros.
apply Transitivity_of_Imp with (C g (E g p)).
apply C_CE.
apply rule_C_K_rev.
apply C_rule.
apply E_Ki.
auto.
Qed.

(* If "i is in g" and "p is a common knowledge", then "agent i knows p" *)

Lemma C_Ki :
 forall (g : list nat) (i : nat) (p : proposition),
 In i g -> |- C g p ==> K i p.

Proof.
intros. apply Transitivity_of_Imp with (p & E g (C g p)). apply Fixpoint_C. 
apply rule_Imp_AND_right.
apply Transitivity_of_Imp with (E g p). 
apply rule_E_imp.
apply C_T.
apply E_Ki. assumption.
Qed.


Lemma C_KiC :
 forall (g : list nat) (p : proposition) (i : nat),
 In i g -> |- C g p ==> K i (C g p).
Proof.
intros. apply Transitivity_of_Imp with (p & E g (C g p)). apply Fixpoint_C. apply Transitivity_of_Imp with (E g (C g p)).
apply AND2. apply E_Ki. assumption.
Qed.


(* ==== Other fixed points ==== *)

Lemma p_and_ECp_is_fxp :
 forall (g : list nat) (p : proposition), |- p & E g (C g p) ==> C g p.
Proof.
intros.
apply Greatest_Fixpoint_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 Fixpoint_C.
Qed.

Lemma p_and_CEp_is_fxp1 :
 forall (g : list nat) (p : proposition), |- p & C g (E g p) ==> C g p.
Proof.
intros.
apply Greatest_Fixpoint_C.
apply rule_AND_left_regular.
apply Transitivity_of_Imp 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 :
 forall (g : list nat) (p : proposition), |- C g p ==> p & C g (E g p).
Proof.
intros. 
apply rule_AND_Imp.
apply C_T. 
apply Greatest_Fixpoint_C.
apply rule_AND_Imp.
apply C_E.
apply C_EC.
Qed.

Lemma p_and_CEp_is_fxp :
 forall (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 :
 forall (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.

Lemma C_AND1 :
 forall (g : list nat) (p q : proposition), |- C g (p & q) ==> C g p.

Proof.
intros. apply MP with (C g (p & q ==> p)).
apply C_K_rev.
apply C_rule. apply AND1.
Qed.


Lemma C_AND2 :
 forall (g : list nat) (p q : proposition), |- C g (p & q) ==> C g q.
Proof.
intros. apply MP with (C g (p & q ==> q)).
apply C_K_rev.
apply C_rule. apply AND2.
Qed.


Lemma C_AND :
 forall (g : list nat) (p q : proposition), |- C g (p & q) ==> C g p & C g q.
Proof.
intros. apply rule_AND_Imp. apply C_AND1. apply C_AND2.
Qed.


Lemma rule_C_AND :
 forall (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_AND. assumption.
Qed.


Lemma AND_C :
 forall (g : list nat) (p q : proposition), |- C g p & C g q ==> C g (p & q).
Proof.
intros.
apply rule_Imp_AND.
apply Transitivity_of_Imp with (C g (q ==> p & q)).
apply MP with (C g (p ==> q ==> p & q)).
apply C_K_rev.
apply C_rule.
apply AND0.
apply C_K_rev.
Qed.


Lemma rule_AND_C :
 forall (g : list nat) (p q : proposition), |- C g p & C g q -> |- C g (p & q).
Proof.
intros.
apply rule_KC with p. 
apply MP with (C g p & C g q). apply AND1. assumption. 
apply rule_KC with q. 
apply MP with (C g p & C g q). apply AND2. assumption. 
apply C_rule.  apply rule_C. apply AND0.
Qed.

Lemma C_nil: forall p:proposition, |- p ==> C nil p.
Proof.
intros p.
apply Greatest_Fixpoint_C.
simpl.
apply AND_TRUE.
Qed.

(* ==== Meyer and van der Hoek.axiom A10 ==== *)

(* Here is the proof of axiom (A10) page 46 in the book 
   John-Jules Ch. Meyer and Wiebe van der Hoek.
   "Epistemic Logic for Computer Science and Artificial
   Intelligence", volume 41 of Cambridge Tracts in Theoretical Computer
   Science, Cambridge University Press, 1995. *)

Lemma A10 :
  forall (g : list nat) (p : proposition), 
    |-  C g (p ==> E g p) ==> p ==> C g p.
Proof.
intros.
apply rule_rev_AND_Imp.
apply Greatest_Fixpoint_C.
apply rule_AND_Imp.
apply AND2.
apply Transitivity_of_Imp with  (E g (C g (p ==> E g p)) & E g p).
apply rule_AND_Imp.
apply rule_Imp_AND_left.
apply C_EC.
apply Transitivity_of_Imp with ((p ==> E g p) & p).
apply rule_AND_right_regular.
apply C_T.
apply rule_Imp_AND.
apply I.
apply ANDE.
Qed.

(* ==== Deduction rule ====*)

(* Those rules are a step for proving the Deduction for knowledge logic,
   namely (|- p -> |- q) -> |- C g p ==> C g q.  

  Actually one has to  prove that property for each basic rule.

    - for MP this is C_K.

    - for rule_K this is C_Ki.

   - The following lemma is for rule Leas_Fixpoint_C.
*)

Theorem Deduction_Greatest_Fixpoint_C:
 forall (g: list nat) (p q r: proposition), 
    |-C g (q ==> p & E g q) ==> C g (q ==> C g p).
Proof.
intros.
apply Greatest_Fixpoint_C.
apply rule_AND_Imp.
apply rule_C.
apply rule_rev_AND_Imp.
apply Greatest_Fixpoint_C.
apply rule_AND_Imp.
apply Transitivity_of_Imp with (q & (q ==> p & E g q)).
apply rule_AND_left_regular.
apply C_T.
apply rule_Imp_AND.
apply rule_C.
apply MP with (p & E g q ==> p).
apply B.
apply AND1.
apply Transitivity_of_Imp with (E g (q) & E g (C g (q ==> p & E g q))).
apply rule_AND_Imp.
apply rule_Imp_AND.
apply rule_C.
apply Transitivity_of_Imp with (q ==> p & E g q).
apply C_T.
apply MP with (p & E g q ==> E g q).
apply B.
apply AND2.
apply rule_Imp_AND.
apply Drop_hyp.
apply C_EC.
apply ANDE.
apply C_EC.
Qed.

End Common_Knowledge.

Section Barcan.

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Notation "\-/ p" := (Forall _ p) (at level 70, right associativity).

Axiom Barcan :
    forall (i : nat) (A : Set) (P : A -> proposition),
        |-(\-/ fun a : A => K i (P a)) ==> K i (\-/ P).

Theorem Barcan1 :
 forall (A : Set) (i : nat) (P : A -> proposition),
 (forall a : A, |- K i (P a)) -> |- K i (\-/ P).
Proof.
intros.
apply MP with (\-/ (fun a : A => K i (P a))).
apply Barcan.
apply ForallRule.
apply H.
Qed.

(* This axiom should be proven easily. *)

Lemma ForallAND:
    forall (A: Set) (P Q: A -> proposition),
    |- (\-/fun a:A => P a & Q a) ==>  (\-/ P) & \-/ Q.
Proof.
intros.
apply rule_AND_Imp.
apply rule_Forall2.
apply ForallRule.
intros.
apply Transitivity_of_Imp with (P x & Q x).
apply Forall1 with (P := (fun a : A => P a & Q a)).
apply AND1.
apply rule_Forall2.
apply ForallRule.
intros.
apply Transitivity_of_Imp with (P x & Q x).
apply Forall1 with (P := (fun a : A => P a & Q a)).
apply AND2.
Qed.


Lemma Barcan_E:
    forall (g : list nat) (A : Set) (P : A -> proposition),
        |-(\-/ fun a : A => E g (P a)) ==> E g (\-/ P).
Proof.
intros.
elim g.
simpl.
apply Everything_Imp_True.
intros.
simpl.
apply rule_AND_Imp.
apply Transitivity_of_Imp with ((\-/ (fun x:A => (K a (P x)))) &  (\-/ (fun x:A => (E l (P x))))).
apply ForallAND with (P := (fun x : A => K a (P x))) (Q :=  (fun x:A => E l (P x))).
apply rule_Imp_AND_left.
apply Barcan.
apply Transitivity_of_Imp with ((\-/ (fun x:A => (K a (P x)))) &  (\-/ (fun x:A => (E l (P x))))).
apply ForallAND with (P := (fun x : A => K a (P x))) (Q :=  (fun x:A => E l (P x))).
apply rule_Imp_AND_right.
apply H.
Qed.

Theorem Barcan_C:
    forall (g : list nat) (A : Set) (P : A -> proposition),
        |-(\-/ fun a : A => C g (P a)) ==> C g (\-/ P).
Proof.
intros.
apply Greatest_Fixpoint_C.
apply rule_AND_Imp.
apply rule_Forall2.
apply ForallRule.
intros.
apply Transitivity_of_Imp with (C g (P x)).
apply Forall1 with (P := (fun a : A => C g (P a))).
apply C_T.
apply Transitivity_of_Imp with (\-/ fun a : A => E g (C g (P a))). 
apply rule_Forall2.
apply ForallRule.
intros.
apply Transitivity_of_Imp with (C g (P x)).
apply Forall1 with (P := (fun a : A => C g (P a))).
apply C_EC.
apply Barcan_E  with (P := (fun a : A => C g (P a))).
Qed.


End Barcan.

Section Sato.

(* In this section I prove that the formalization of common knowledge by the unique axiom 
        |- (K O p) ==> (K i (K O p)).  
   presented by Mutsuhicho Sato is equivalent to the presentdation by fixpoint usually presented.
*)

(* ========= Requirements ======= *)

Require Import Arith.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Notation "¬ p" := (NOT p) (at level 45).

(* ======= Sato implies C as fixpoint ======= *)

Lemma Sato_imp_Rule_For_C :
 forall (g : list nat) (i : nat) (p q : proposition),
 In i g -> |- q ==> p & E g q -> |- q ==> K i p.
Proof.
intros. 
apply Transitivity_of_Imp with (E g p).
apply Transitivity_of_Imp with (p & E g (p & E g q)).
apply Transitivity_of_Imp with (p & E g q).
trivial.
apply rule_AND_left_regular.
apply rule_E_K.
apply E_rule.
trivial.
apply Transitivity_of_Imp with (E g (p & E g q)).
apply AND2.
apply rule_E_imp.
apply AND1.
apply E_Ki.
trivial.
Qed.


Lemma Sato_imp_Knowledge :
 forall (g : list nat) (p : proposition),
 (forall i : nat, In i g -> |- K 0 p ==> K i (K 0 p)) ->
       |- K 0 p ==> p & E g (K 0 p).
Proof.
intro g.
elim g.
intros.
apply rule_AND_Imp.
apply K_T.
unfold E in |- *. 
apply Everything_Imp_True.
intros.
apply rule_AND_Imp.
apply K_T.
unfold E in |- *. 
apply rule_AND_Imp.
apply H0.
apply in_eq.
apply Transitivity_of_Imp with (p & E l (K 0 p)).
apply H.
intros.
apply H0.
apply in_cons.
apply H1.
apply AND2.
Qed.

(* ======= C as fixpoint implies Sato ======= *)

Lemma C_imp_Sato :
 forall (i : nat) (g : list nat) (p : proposition),
 |- K 0 p ==> C g p -> In i g -> In 0 g -> |- K 0 p ==> K i (K 0 p).
Proof.
intros. 
apply Transitivity_of_Imp with (C g p).
trivial.
apply Transitivity_of_Imp with (K i (C g p)).
apply C_KiC.
trivial.
apply rule_K_K_rev.
apply K_rule.
apply C_Ki.
trivial.
Qed.
End Sato.

Section Hat.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Infix "V" := OR (left associativity, at level 50).
Infix "|" := Xor (right associativity, at level 55).
Notation "¬ p" := (NOT p) (at level 45).

(* ======== Data ======== *)

(* (white i) means "Agent i wears at least a white hat". 
   (red i) means "Agent i wear only read hats". *)

Variable white red : nat -> proposition.

(* ========== Abbreviations ======= *)

Definition Alice := 0.
Definition Bob := 1.
Definition Carol := 2.

(* Kh i means "Agent i knows he (she) wears a white hat or not". 
   in other words "Agent i knows the color ofhis (her) hats" if we assume
   he (she) wears only one hat.  
*)

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 : forall 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 : forall 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 : forall 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 : forall 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 Transitivity_of_Imp with (white Carol).
apply One_hat3.
apply Transitivity_of_Imp 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 Transitivity_of_Imp with (K Alice (white Bob & white Carol)).
apply Transitivity_of_Imp 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 Transitivity_of_Imp 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 Transitivity_of_Imp with (¬K Alice (red Alice)).
apply rule_Contrapos1. unfold Kh.
apply OR2.
apply Transitivity_of_Imp 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 Transitivity_of_Imp with (red Bob V red Carol & ¬red Carol).
apply rule_AND_right_regular.
apply Not_KhA_then_rB_or_rC.
apply Transitivity_of_Imp with (red Bob & ¬red Carol V (red Carol & ¬red Carol)).
apply dist_AND2.
apply Transitivity_of_Imp with (red Bob V FALSE).
apply rule_glueOR.
apply AND1.
apply Transitivity_of_Imp 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 Transitivity_of_Imp with (K Bob (¬Kh Alice) & K Bob (¬red Carol)).
apply rule_AND_left_regular.
apply KB_nrC.
apply Transitivity_of_Imp with (K Bob (¬Kh Alice & ¬red Carol)).
apply AND_Ki.
apply Transitivity_of_Imp with (K Bob (red Bob)).
apply rule_imp_K.
apply Not_KhA_and_Not_rC_then_rB.
unfold Kh in |- *.
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 Transitivity_of_Imp with (K Carol (red Carol)).
apply Final1.
unfold Kh in |- *.
apply OR2.
Qed.


End Hat.


Section Muddy_Children.

Require Import Arith.

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

Notation "|- p" := (theorem p) (at level 85).
Infix "==>" := Imp (right associativity, at level 70).
Infix "&" := AND (left associativity, at level 50).
Infix "V" := OR (left associativity, at level 50).
Notation "¬ p" := (NOT p) (at level 45).
Notation "n +1" := (S n) (at level 30).
Notation "\-/ p" := (Forall _ p) (at level 70, right associativity).


(* ======== Operators ======== *)

(* a list of n children 1 ... n *)

Fixpoint list_of (n : nat) : list nat :=
  match n with
  | O => nil (A:=nat)
  | m+1 => m :: list_of m
  end.

Notation "[: n :]" := (list_of n) (at level 40).


(* ========== Exactly ========== *)

Variable At_least : nat -> nat -> proposition.
Definition Exactly (n p : nat) := At_least n p & ¬At_least n (p+1).

Lemma At_least_p_and_not_Exactly_p :
 forall n p : nat, |- At_least n p & ¬Exactly n p ==> At_least n (p+1).
Proof.
intros. 
unfold Exactly in |- *.
apply
 Transitivity_of_Imp
  with (At_least n p & ¬At_least n p V (At_least n p & At_least n (p+1))).
apply Transitivity_of_Imp with (At_least n p & (¬At_least n p V At_least n (p+1))).
apply rule_AND_left_regular.
apply Transitivity_of_Imp with (¬At_least n p V ¬(¬At_least n (p+1))).
apply Class_OR_NOT.
apply rule_OR_left_regular.
apply Classic_NOTNOT.
apply dist_AND.
apply rule_OR0.
apply Transitivity_of_Imp with FALSE.
unfold NOT in |- *.
apply rule_Imp_AND.
apply rule_C.
apply I.
apply False_Imp_everything.
apply AND2.
Qed.




(* ================ The axiom ================ *)

Axiom
  Knowledge_Diffusion :
    forall n p i : nat,
    |- E ([:n:]) (At_least n p) ==>
       E ([:n:]) (¬Exactly n p) ==> K i (E ([:n:]) (¬Exactly n p)).

(* ========== The lemmas ========== *)

Lemma Pre_E_Awareness :
 forall n p k : nat,
 k <= n ->
 |- E ([:n:]) (At_least n p) ==>
   E ([:n:]) (¬Exactly n p) ==> E ([:k:]) (E ([:n:]) (¬Exactly n p)).
Proof.
intros n p k. 
elim k.
intro.
simpl in |- *. apply Drop_hyp. apply Drop_hyp. apply theorem_True.

intros. 
simpl in |- *.
apply rule_rev_AND_Imp.
apply rule_AND_Imp.
apply rule_Imp_AND.
apply Knowledge_Diffusion.
apply rule_Imp_AND.
apply H.
apply le_Sn_le. assumption.
Qed.

Lemma E_Awareness :
 forall n p : nat,
 |- E ([:n:]) (At_least n p) ==>
   E ([:n:]) (¬Exactly n p) ==> E ([:n:]) (E ([:n:]) (¬Exactly n p)).
Proof.
intros.
apply Pre_E_Awareness. 
auto.
Qed.

Lemma C_Awareness :
 forall n p : nat,
 |- C ([:n+1:]) (At_least (n+1) p) ==>
   E ([:n+1:]) (¬Exactly (n+1) p) ==> C ([:n+1:]) (¬Exactly (n+1) p).
Proof.
intros. 
apply rule_rev_AND_Imp.
apply Greatest_Fixpoint_C.
apply rule_AND_Imp.
apply rule_Imp_AND_right.
unfold list_of in |-  *.
apply E_T.
apply
 Transitivity_of_Imp
  with
    (E ([:n+1:]) (C ([:n+1:]) (At_least (n+1) p)) &
     E ([:n+1:]) (E ([:n+1:]) (¬Exactly (n+1) p))).
apply rule_AND_Imp.
apply rule_Imp_AND_left.
apply C_EC.
apply
 Transitivity_of_Imp
  with (E ([:n+1:]) (At_least (n+1) p) & E ([:n+1:]) (¬Exactly (n+1) p)).
apply rule_AND_right_regular.
apply C_E.
apply rule_Imp_AND.
apply E_Awareness.
auto.
apply ANDE.
Qed.

Lemma Progress :
 forall n p : nat,
 |- C ([:n+1:]) (At_least (n+1) p) & E ([:n+1:]) (¬Exactly (n+1) p) ==>
    C ([:n+1:]) (At_least (n+1) (p+1)). 
Proof.
intros. apply
  Transitivity_of_Imp
   with (C ([:n+1:]) (At_least (n+1) p) & C ([:n+1:]) (¬Exactly (n+1) p)).
apply rule_AND_Imp.
apply AND1.
apply rule_Imp_AND.
apply C_Awareness.
apply rule_Imp_AND.
apply
 Transitivity_of_Imp with (C ([:n+1:]) (¬Exactly (n+1) p ==> At_least (n+1) (p+1))).
apply rule_C_K_rev.
apply C_rule.
apply rule_rev_AND_Imp.
apply At_least_p_and_not_Exactly_p.
apply C_K_rev.
Qed.

Lemma Progress2 :
 forall n p : nat,
 1 <= n ->
 |- C ([:n:]) (At_least n p) & E ([:n:]) (¬Exactly n p) ==>
   C ([:n:]) (At_least n (p+1)).
Proof.
intros. 
induction n as [| n Hrecn].
absurd (1 <= 0).
apply gt_not_le.
auto.
trivial.
apply Progress.
Qed.

Variable nb_children : nat.
Axiom At_least_1 : 1 <= nb_children.
Axiom First_Father_Statement : |- C ([:nb_children:]) (At_least nb_children 1).

Variable nb_muddy : nat.
Variable muddy_child : nat.
Axiom Muddy_child_is_a_child : In muddy_child ([:nb_children:]).
Axiom
  What_they_saw :
    forall q : nat,
    q < nb_muddy -> |- E ([:nb_children:]) (¬Exactly nb_children q).
Axiom
  What_the_muddy_child_sees :
    |- K muddy_child (¬At_least nb_children (nb_muddy+1)).

Lemma Induction_on_C :
 forall p : nat,
 p < nb_muddy ->
 |- C ([:nb_children:]) (At_least nb_children p) ->
 |- C ([:nb_children:]) (At_least nb_children (p+1)).
Proof.
intros.
apply MP with (E ([:nb_children:]) (¬Exactly nb_children p)).
apply MP with (C ([:nb_children:]) (At_least nb_children p)).
apply rule_rev_AND_Imp.
apply Progress2.
apply At_least_1.
trivial.
apply What_they_saw.
trivial.
Qed.

Lemma C_at_least :
 forall p : nat,
 p < nb_muddy -> |- C ([:nb_children:]) (At_least nb_children (p+1)).
Proof.
simple induction p.
intros. 
apply First_Father_Statement.
intros. 
apply Induction_on_C.
trivial.
apply H.
unfold lt in |- *.
apply lt_le_weak.
trivial.
Qed.

Lemma C_at_least_nb_muddy :
 0 < nb_muddy -> |- C ([:nb_children:]) (At_least nb_children nb_muddy).
Proof.
intros. 
replace nb_muddy with (pred nb_muddy+1).
apply C_at_least.
apply lt_pred_n_n.
trivial.
symmetry  in |- *.
apply S_pred with 0.
trivial.
Qed.

Lemma E_childern_Exactly :
 0 < nb_muddy -> |- K muddy_child (Exactly nb_children nb_muddy).
Proof.
intros. 
unfold Exactly in |- *.
apply rule_AND_Ki.
apply rule_split_AND.
apply MP with (C ([:nb_children:]) (At_least nb_children nb_muddy)).
apply C_Ki.
apply Muddy_child_is_a_child.
apply C_at_least_nb_muddy.
trivial.
apply What_the_muddy_child_sees.
Qed.

End Muddy_Children.