(********************************************************************************)
(*                       Epistemic_and_Dynamic_Logic.v                    	*)
(*                                                                          	*)
(*                             Jérôme Puisségur                              	*)
(*                                 L.3 I.F.                                  	*)
(*		                    LIP   ENS-Lyon   	      			*)
(*                                                                          	*)
(*                                                                          	*)
(* Developed in V8.0                                           June-July 2005   *)
(* Last changes                                       March-September 06 (P.L.) *)
(********************************************************************************)

(* Based on previous Pierre Lescanne's work : *)

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


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
(*********** Added by Jérôme PUISSEGUR, June and July 2005 ********)
  | Star : proposition -> proposition
  | Point : proposition -> proposition.
(******************************************************************)


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

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_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

 (* ------------------------- Epistemic and dynamic calculus ------------------------- *)
  | K_K : forall (i : nat) (p q : proposition), theorem (K i p ==> K i (p ==> q) ==> K i q)
  | K_T : forall (i : nat) (p : proposition), theorem (K i p ==> p)
  | K_rule : forall (i : nat) (p : proposition), theorem p -> theorem (K i p)

(*************** Added by Jérôme PUISSEGUR, June and July 2005 **********************)
  | Star_K : forall (p q : proposition), theorem ([*] p ==> [*] (p ==> q) ==> [*] q)
  | Star_T : forall (p : proposition), theorem ([*] p ==> p)
  | Star_rule : forall (p : proposition), theorem p -> theorem ([*] p)

  | KT1 : forall (i : nat) (p : proposition), theorem (K i ([*] p) ==> [*] (K i p))
(************************************************************************************)

  | Fixpoint_C : forall (G : list nat) (p : proposition), theorem (C G p ==> p & E G (C G p))
  | Least_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 ======================= *)

Axiom I : forall p : proposition, |- p ==> p.
Axiom KI : forall p q : proposition, |- q ==> p ==> p.
Axiom KS :
 forall p q r t : proposition,
 |- t ==> (p ==> q ==> r) ==> (p ==> q) ==> p ==> r.
Axiom SKS :
 forall p q r t : proposition,
 |-(t ==> p ==> q ==> r) ==> t ==> (p ==> q) ==> p ==> r.
Axiom B : forall p q r : proposition, |-(p ==> q) ==> (r ==> p) ==> r ==> q.
(* p ==> q , q ==> r |- p ==> r *)
Axiom Transitivity_of_Imp :
 forall p q r : proposition, |- p ==> q -> |- q ==> r -> |- p ==> r.
Axiom BB :
 forall p q r t : proposition,
 |-(p ==> q ==> r) ==> p ==> (t ==> q) ==> t ==> r.
Axiom BBS :
 forall p q r s : proposition,
 |-(p ==> q ==> r) ==> (s ==> p ==> q) ==> s ==> p ==> r.
Axiom SBBS :
 forall p q r t : proposition,
 |-((p ==> q ==> r) ==> t ==> p ==> q) ==> (p ==> q ==> r) ==> t ==> p ==> r.
Axiom KK : forall p q r : proposition, |- p ==> q ==> r ==> q.
Axiom Hilbert_C :
 forall p q r : proposition, |-(p ==> q ==> r) ==> q ==> p ==> r.
(* p ==> q ==> r |- q ==> p ==> r *)
Axiom rule_C : forall p q r : proposition, |- p ==> q ==> r -> |- q ==> p ==> r.
Axiom CI : forall p q : proposition, |- p ==> (p ==> q) ==> q.
Axiom C2 :
 forall p q r s : proposition,
 |-(p ==> q ==> r ==> s) ==> p ==> r ==> q ==> s.
Axiom rule_C2 :
 forall p q r s : proposition, |- p ==> q ==> r ==> s -> |- p ==> r ==> q ==> s.
Axiom Transitivity_of_Imp2 :
 forall p q r s : proposition,
 |- p ==> q -> |- s ==> r ==> p -> |- s ==> r ==> q.
Axiom CB : forall p q r : proposition, |-(r ==> p) ==> (p ==> q) ==> r ==> q.
Axiom Drop_hyp : forall p q : proposition, |- p -> |- q ==> p.
Axiom Drop_2nd_hyp :
 forall p q r : proposition, |-(p ==> q) ==> p ==> r ==> q.
Axiom rule_Drop : forall p q r : proposition, |- p ==> q -> |- p ==> r ==> q.
Axiom Cut2 :
 forall p1 p2 q r : proposition,
 |-(p1 ==> p2 ==> q) ==> (q ==> r) ==> p1 ==> p2 ==> r.
Axiom CSI : forall p q : proposition, |-(p ==> p ==> q) ==> p ==> q.
(* p ==> p ==> q |- p ==> q *)
Axiom rule_CSI : forall p q : proposition, |- p ==> p ==> q -> |- p ==> q.
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).

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

Axiom OR0 :
 forall p q r : proposition, |-(p ==> r) ==> (q ==> r) ==> p V q ==> r.
Axiom OR1 : forall p q : proposition, |- p ==> p V q.
Axiom OR2 : forall p q : proposition, |- q ==> p V q.

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

Axiom AND0 : forall p q : proposition, |- p ==> q ==> p & q.
Axiom AND1 : forall p q : proposition, |- p & q ==> p.
Axiom AND2 : forall p q : proposition, |- p & q ==> q.


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


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

Axiom False_Imp_everything : forall p : proposition, |- FALSE ==> p.
Axiom Everything_Imp_True : forall p : proposition, |- p ==> TRUE.
Axiom NEGFalse : NEG (|- FALSE).
Axiom FalseFF : |- FALSE -> FF.
Axiom FFFalse : FF -> |- FALSE.
Axiom NEGNOT : forall p : proposition, |-¬p -> NEG (|- p).
Axiom theorem_True : |- TRUE.
Axiom NOTNOT : forall p : proposition, |- p ==> ¬(¬p).
Axiom Contraposition : forall p q : proposition, |-(p ==> q) ==> ¬q ==> ¬p.
Axiom rule_Contrapos1 : forall p q : proposition, |- p ==> q -> |-¬q ==> ¬p.
Axiom rule_Contrapos2 : forall p q : proposition, |- p ==> q -> |-¬q -> |-¬p.

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

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

Axiom rule_OR : forall p q : proposition, (|- p) \/ |- q -> |- p V q.
Axiom rule_OR0 :
 forall p q r : proposition, |- p ==> r -> |- q ==> r -> |- p V q ==> r.
Axiom Imp_OR1 : forall p q r : proposition, |- p ==> q -> |- p ==> q V r.
Axiom Imp_OR2 : forall p q r : proposition, |- p ==> r -> |- p ==> q V r.
Axiom OR_comm : forall p q : proposition, |- p V q ==> q V p.
Axiom rule_OR_comm : forall p q : proposition, |- p V q -> |- q V p.
Axiom OR_ass1 : forall p q r : proposition, |- p V (q V r) ==> p V q V r.
Axiom OR_ass2 : forall p q r : proposition, |- p V q V r ==> p V (q V r).
Axiom OR_idempotence : forall p : proposition, |- p V p ==> p.
Axiom OR_left_regular :
 forall p q r : proposition, |-(p ==> q) ==> r V p ==> r V q.
Axiom rule_OR_left_regular :
 forall p q r : proposition, |- p ==> q -> |- r V p ==> r V q.
Axiom OR_right_regular :
 forall p q r : proposition, |-(p ==> q) ==> p V r ==> q V r.


Axiom rule_OR_right_regular :
 forall p q r : proposition, |- p ==> q -> |- p V r ==> q V r.
Axiom rule_glueOR :
 forall p1 p2 q1 q2 : proposition,
 |- p1 ==> q1 -> |- p2 ==> q2 -> |- p1 V p2 ==> q1 V q2.

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

Axiom rule_split_AND : forall p1 p2 : proposition, |- p1 -> |- p2 -> |- p1 & p2.
(* These lemmas shows the connection between /\ (meta and) and & (object and) *)

Axiom rule_AND : forall p1 p2 : proposition, (|- p1) /\ (|- p2) -> |- p1 & p2.
Axiom rule_AND_alt :
 forall p1 p2 : proposition, |- p1 & p2 -> (|- p1) /\ (|- p2).
Axiom Imp_AND : forall p q r : proposition, |-(p ==> q ==> r) ==> p & q ==> r.
Axiom rule_Imp_AND :
 forall p q r : proposition, |- p ==> q ==> r -> |- p & q ==> r.
Axiom rule_Imp_AND_left :
 forall p q r : proposition, |- p ==> r -> |- p & q ==> r.
Axiom rule_Imp_AND_right :
 forall p q r : proposition, |- q ==> r -> |- p & q ==> r.
Axiom rule_AND_Imp :
 forall p q r : proposition, |- p ==> q -> |- p ==> r -> |- p ==> q & r.
Axiom rule_rev_AND_Imp :
 forall p q r : proposition, |- p & q ==> r -> |- p ==> q ==> r.
Axiom rule_glueAND :
 forall p1 p2 q1 q2 : proposition,
 |- p1 ==> q1 -> |- p2 ==> q2 -> |- p1 & p2 ==> q1 & q2.
Axiom rule_glueAND2 :
 forall p1 p2 q1 q2 r1 r2 : proposition,
 |- p1 ==> q1 ==> r1 ->
 |- p2 ==> q2 ==> r2 -> |- p1 & p2 ==> q1 & q2 ==> r1 & r2.
Axiom AND_drop1 : forall p1 p2 : proposition, |- p1 & p2 -> |- p1.
Axiom AND_drop2 : forall p1 p2 : proposition, |- p1 & p2 -> |- p2.
Axiom AND_comm : forall p q : proposition, |- p & q ==> q & p.
Axiom rule_AND_comm : forall p q : proposition, |- p & q -> |- q & p.
Axiom AND_ass : forall p q r : proposition, |- p & q & r ==> p & (q & r).
Axiom AND_ass1 : forall p q r : proposition, |- p & (q & r) ==> p & q & r.
Axiom rule_AND_ass : forall p q r : proposition, |- p & q & r -> |- p & (q & r).
Axiom rule_AND_ass1 :
 forall p q r : proposition, |- p & (q & r) -> |- p & q & r.
Axiom AND_right_regular :
 forall p q r : proposition, |-(p ==> q) ==> p & r ==> q & r.
Axiom rule_AND_right_regular :
 forall p q r : proposition, |- p ==> q -> |- p & r ==> q & r.
Axiom AND_left_regular :
 forall p q r : proposition, |-(p ==> q) ==> r & p ==> r & q.
Axiom rule_AND_left_regular :
 forall p q r : proposition, |- p ==> q -> |- r & p ==> r & q.
Axiom AND_idempotence : forall p : proposition, |- p ==> p & p.
Axiom ANDAND : forall p q : proposition, |- p & p ==> q -> |- p ==> q.
Axiom AND_perm : forall p q r : proposition, |- p & (q & r) ==> r & (p & q).
Axiom rule_AND_perm :
 forall p q r : proposition, |- p & (q & r) -> |- r & (p & q).
Axiom AND_swap : forall p q r : proposition, |- p & (q & r) ==> q & (p & r).

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

Axiom undist_AND :
 forall p q r : proposition, |- p & q V (p & r) ==> p & (q V r).
Axiom undist_AND2 :
 forall p q r : proposition, |- p & r V (q & r) ==> p V q & r.
Axiom dist_AND :
 forall p q r : proposition, |- p & (q V r) ==> p & q V (p & r).
Axiom dist_AND2 : forall p q r : proposition, |- p V q & r ==> p & r V (q & r).
Axiom undist_OR :
 forall p q r : proposition, |- p V q & (p V r) ==> p V (q & r).
Axiom undist_OR2 :
 forall p q r : proposition, |- q V p & (r V p) ==> q & r V p.
Axiom dist_OR : forall p q r : proposition, |- p V (q & r) ==> p V q & (p V r).
Axiom p_or_r_and_q_or_r :
 forall p q r : proposition, |- p V r & (q V r) ==> p & q V r.

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

Axiom AND_NOT : forall p q : proposition, |-¬(p V q) ==> ¬p & ¬q.
Axiom AND_NOT_rule : forall p q : proposition, |-¬(p V q) -> |-¬p & ¬q.
Axiom Not_OR : forall p q : proposition, |-¬p & ¬q ==> ¬(p V q).
Axiom rule_Not_OR : forall p q : proposition, |-¬p & ¬q -> |-¬(p V q).
Axiom Not_AND : forall p q : proposition, |-¬p V ¬q ==> ¬(p & q).
Axiom rule_Not_AND : forall p q : proposition, |-¬p V ¬q -> |-¬(p & q).
Axiom Not_p_AND_p : forall p : proposition, |-¬p & p ==> FALSE.
Axiom OR_FALSE : forall p : proposition, |- p V FALSE ==> p.
Axiom AND_FALSE : forall p : proposition, |- p & FALSE ==> FALSE.
Axiom AND_TRUE : forall p : proposition, |- p ==> p & TRUE.

(* ==================== Lemmas about Xor  ======================= *)

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

Axiom Xor_Imp : forall p q : proposition, |- p | q ==> ¬p ==> q.
Axiom Xor_comm : forall p q : proposition, |- p | q ==> q | p.
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).


Axiom Class_OR_NOT : forall p q : proposition, |-¬(p & q) ==> ¬p V ¬q.
Axiom rule_Class_OR_NOT : forall p q : proposition, |-¬(p & q) -> |-¬p V ¬q.
Axiom not_p_then_q : forall p q : proposition, |-(¬p ==> q) ==> ¬q ==> p.
Axiom r_not_p_then_q :
 forall p q r : proposition, |- r & ¬p ==> q -> |- r & ¬q ==> p.
Axiom Class_OR : forall p q : proposition, |-¬(¬p & ¬q) ==> p V q.
Axiom rule_Class_OR : forall p q : proposition, |-¬(¬p & ¬q) -> |- p V q.
Axiom Excluded_middle : forall p : proposition, |- p V ¬p.
Axiom Class_OR_with_disjunction :
 forall p q : proposition, |- p V q ==> p & ¬q V q.
(* About Xor *)

Axiom Xor_Imp2 : forall p q : proposition, |- p | q ==> p ==> ¬q.
End Classic.


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" := (NOT p) (at level 45).

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

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

Axiom K_K_rev :
 forall (i : nat) (p q : proposition), |- K i (p ==> q) ==> K i p ==> K i q.
Axiom rule_K_K_rev :
 forall (i : nat) (p q : proposition), |- K i (p ==> q) -> |- K i p ==> K i q.
Axiom rule_Imp_K :
 forall (i : nat) (p q : proposition), |- p ==> q -> |- K i p ==> K i q.


Axiom Ki_AND1 :
 forall (p1 p2 : proposition) (i : nat), |- K i (p1 & p2) ==> K i p1.
Axiom Ki_AND2 :
 forall (p1 p2 : proposition) (i : nat), |- K i (p1 & p2) ==> K i p2.
Axiom Ki_AND :
 forall (p1 p2 : proposition) (i : nat), |- K i (p1 & p2) ==> K i p1 & K i p2.
Axiom rule_Ki_AND :
 forall (i : nat) (p1 p2 : proposition), |- K i (p1 & p2) -> |- K i p1 & K i p2.

Axiom AND_Ki :
 forall (i : nat) (p1 p2 : proposition), |- K i p1 & K i p2 ==> K i (p1 & p2).
Axiom rule_AND_Ki :
 forall (i : nat) (p1 p2 : proposition), |- K i p1 & K i p2 -> |- K i (p1 & p2).
Axiom ORKi :
 forall (i : nat) (p1 p2 : proposition), |- K i p1 V K i p2 ==> K i (p1 V p2).

(*  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" *)


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).
Infix "V" := OR (left associativity, at level 50).
Notation "[*] p":= (Star p) (at level 48).


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

Axiom E_nil_nat : forall p : proposition, |- E nil p.
Axiom E_T :
 forall (G: list nat) (p : proposition) (i : nat), |- E (i :: G) p ==> p.
Axiom E_K :
 forall (G: list nat) (p q : proposition),
 |- E G p ==> E G (p ==> q) ==> E G q.
Axiom rule_E_K :
 forall (G: list nat) (p q : proposition),
 |- E G (p ==> q) -> |- E G p ==> E G q.
Axiom E_rule : forall (G: list nat) (p : proposition), |- p -> |- E G p.
Axiom rule_E_Imp :
 forall (G: list nat) (p q : proposition), |- p ==> q -> |- E G p ==> E G q.
Axiom E_Ki :
 forall (G: list nat) (p : proposition) (i : nat),
 In i G -> |- E G p ==> K i p.
Axiom E_AND1 :
 forall (G: list nat) (p q : proposition), |- E G (p & q) ==> E G p.
Axiom E_AND2 :
 forall (G: list nat) (p q : proposition), |- E G (p & q) ==> E G q.
Axiom E_AND :
 forall (G: list nat) (p q : proposition), |- E G (p & q) ==> E G p & E G q.
Axiom ANDE :
 forall (G: list nat) (p q : proposition), |- E G p & E G q ==> E G (p & q).
Axiom E_AND_comm :
 forall (G: list nat) (p q : proposition), |- E G (p & q) ==> E G (q & p).

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

Axiom C_T : forall (G: list nat) (p : proposition), |- C G p ==> p.
Axiom C_E : forall (G: list nat) (p : proposition), |- C G p ==> E G p.
Axiom C_EC : forall (G: list nat) (p : proposition), |- C G p ==> E G (C G p).
Axiom C_CE : forall (G: list nat) (p : proposition), |- C G p ==> C G (E G p).
Axiom C_K :
 forall (G: list nat) (p q : proposition),
 |- C G p ==> C G (p ==> q) ==> C G q.
(* This does not require K_4 *)

Axiom C_4 : forall (G: list nat) (p : proposition), |- C G p ==> C G (C G p).
Axiom C_rule : forall (G: list nat) (p : proposition), |- p -> |- C G p.
(* If "i is in g" and "p is a common knowledge", then "agent i knows p" *)

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

Axiom C_KiC :
 forall (G: list nat) (p : proposition) (i : nat),
 In i G -> |- C G p ==> K i (C G p).

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

Axiom p_and_ECp_is_fxp :
 forall (G: list nat) (p : proposition), |- p & E G (C G p) ==> C G p.
Axiom p_and_CEp_is_fxp1 :
 forall (G: list nat) (p : proposition), |- p & C G (E G p) ==> C G p.
Axiom p_and_CEp_is_fxp2 :
 forall (G: list nat) (p : proposition), |- C G p ==> p & C G (E G p).
Axiom 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)).

(* The same properties as for Ki with the same proofs *)

Axiom rule_KC :
 forall (G: list nat) (p q : proposition),
 |- C G p -> |- C G (p ==> q) -> |- C G q.
Axiom C_K_rev :
 forall (G: list nat) (p q : proposition),
 |- C G (p ==> q) ==> C G p ==> C G q.
Axiom rule_C_K_rev :
 forall (G: list nat) (p q : proposition),
 |- C G (p ==> q) -> |- C G p ==> C G q.
Axiom C_AND1 :
 forall (G: list nat) (p q : proposition), |- C G (p & q) ==> C G p.
Axiom C_AND2 :
 forall (G: list nat) (p q : proposition), |- C G (p & q) ==> C G q.
Axiom C_AND :
 forall (G: list nat) (p q : proposition), |- C G (p & q) ==> C G p & C G q.
Axiom rule_C_AND :
 forall (G: list nat) (p q : proposition), |- C G (p & q) -> |- C G p & C G q.

Axiom AND_C :
 forall (G: list nat) (p q : proposition), |- C G p & C G q ==> C G (p & q).

Axiom rule_AND_C :
 forall (G: list nat) (p q : proposition), |- C G p & C G q -> |- C G (p & q).

Axiom C_nil: forall p:proposition, |- p ==> C nil p.

(* 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. *)

Axiom A10 :
  forall (G: list nat) (p : proposition),
    |-  C G (p ==> E G p) ==> p ==> C G p.

End Common_Knowledge.

(***************************************************************)
(***************************************************************)
(*************** Added by Jérôme PUISSEGUR *********************)
(***************************************************************)
(******************* June and July 2005 ************************)
(***************************************************************)
(***************************************************************)

Section Temporal_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":= (Star p) (at level 48).

(* ==================== Lemmas on Star ======================= *)

Lemma rule_Star_K :
 forall (p q : proposition),
 |- [*] (p ==> q) -> |- [*] p ==> [*] q.
Proof.
intros.
apply MP with ([*] (p ==> q)).
apply rule_C.
apply Star_K.
trivial.
Qed.

Lemma rule_Star_Imp :
 forall (p q : proposition), |- p ==> q -> |- [*] p ==> [*] q.
Proof.
intros.
apply rule_Star_K.
apply Star_rule.
assumption.
Qed.

Lemma Star_AND1 :
 forall (p q : proposition), |- [*] (p & q) ==> [*] p.
Proof.
intros.
apply rule_Star_Imp.
apply AND1.
Qed.

Lemma Star_AND2 :
 forall (p q : proposition), |- [*](p & q) ==> [*] q.
Proof.
intros.
apply rule_Star_Imp.
apply AND2.
Qed.

Lemma Star_AND :
 forall (p q : proposition), |- [*] (p & q) ==> [*] p & [*] q.
Proof.
intros.
apply rule_AND_Imp.
apply rule_Star_Imp.
apply AND1.
apply rule_Star_Imp.
apply AND2.
Qed.

Lemma ANDStar :
 forall (p q : proposition), |- [*] p & [*] q ==> [*] (p & q).
Proof.
intros.
apply rule_Imp_AND.
apply Transitivity_of_Imp with ([*](q ==> p&q)).
apply MP with ([*] (p ==> q ==> p & q)).
apply rule_C.
apply Star_K.
apply Star_rule.
apply AND0.
apply rule_C.
apply Star_K.
Qed.

Lemma Star_AND_comm :
 forall (p q : proposition), |- [*] (p & q) ==> [*] (q & p).
Proof.
intros.
apply Transitivity_of_Imp with ([*] p & [*] q).
apply Star_AND.
apply Transitivity_of_Imp with ([*] q & [*] p).
apply AND_comm.
apply ANDStar.
Qed.

Lemma MP_Star :
 forall (p q : proposition), |- [*] p -> |- [*] (p ==> q) -> |- [*] q.
Proof.
intros.
apply MP with (p := [*] p).
apply MP with (p := [*] (p ==> q)).
apply MP with (p := [*] p ==> [*] (p ==> q) ==> [*] q).
apply Hilbert_C.
apply Star_K.
trivial.
trivial.
Qed.

Lemma Star_K_rev :
 forall (p q : proposition), |- [*] (p ==> q) ==> [*] p ==> [*] q.
Proof.
intros. apply rule_C.
apply Star_K.
Qed.

Lemma rule_Star_K_rev :
 forall (p q : proposition), |- [*] (p ==> q) -> |- [*] p ==> [*] q.
Proof.
intros.
apply MP with ([*] (p ==> q)).
apply Star_K_rev.
assumption.
Qed.

Lemma Star_elim :
 forall (p q : proposition),
   |- p ==> [*] p -> |- (p ==> q) -> |- ([*] p ==> [*] q) ==> [*] (p==>q).
Proof.
intros.
apply Transitivity_of_Imp with (p ==> [*] q).
apply MP with (p ==> [*] p).
apply rule_C.
apply B.
apply H.
apply Transitivity_of_Imp with (p ==> q).
apply MP with ([*] q ==> q).
apply B.
apply Star_T.
apply MP with ([*] (p ==> q)).
apply Hilbert_K.
apply Star_rule.
apply H0.
Qed.

Lemma rule_Star_AND :
 forall (p1 p2 : proposition), |- [*] (p1 & p2) -> |- [*] p1 & [*] p2.
Proof.
intros. apply MP with ([*] (p1 & p2)). apply Star_AND. assumption.
Qed.

Lemma rule_AND_Star :
 forall (p1 p2 : proposition), |- [*] p1 & [*] p2 -> |- [*] (p1 & p2).
Proof.
intros.
apply MP_Star with p1.
apply MP with ([*] p1 & [*] p2). apply AND1. assumption.
apply MP_Star with p2.
apply MP with ([*] p1 & [*] p2). apply AND2. assumption.
apply Star_rule. apply rule_C. apply AND0.
Qed.

Lemma ORStar :
 forall (p1 p2 : proposition), |- [*] p1 V [*] p2 ==> [*] (p1 V p2).
Proof.
intros.
apply rule_OR0. apply MP with ([*] (p1 ==> p1 V p2)).
apply rule_C.
apply Star_K. apply Star_rule. apply OR1.
apply MP with ([*] (p2 ==> p1 V p2)).
apply rule_C.
apply Star_K. apply Star_rule.  apply OR2.
Qed.

End Temporal_Logic.

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":= (Star  p) (at level 48).

(* ======== Lemmas about F, iteration of E ======== *)

Fixpoint F (n : nat) (G: list nat) (p : proposition) {struct n} : proposition :=
  match n with
  | 0 => p
  | S m => E G ( F m G p )
  end.

Lemma F_nil_nat : forall (p : proposition) (n : nat), |- F (n+1) nil p.
Proof.
intros.
elim n.
unfold F.
apply E_nil_nat.
intros.
unfold F; fold F.
apply E_nil_nat.
Qed.

Lemma F_T :
 forall (G: list nat) (p : proposition) (n i : nat), |- F (n) (i :: G) p ==> p.
Proof.
intros.
elim n.
unfold F.
apply I.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E (i :: G) p).
apply rule_E_K.
apply E_rule.
trivial.
apply E_T.
Qed.

Lemma F_T_Sn_n :
 forall (G: list nat) (p : proposition) (n i : nat), |- F (n+1) (i :: G) p ==> F (n) (i :: G) p.
Proof.
intros.
elim n.
unfold F.
apply E_T.
intros.
unfold F; fold F.
apply rule_E_K.
apply E_rule.
unfold F in H; fold F in H.
trivial.
Qed.

Lemma F_E_T :
 forall (G: list nat) (p : proposition) (n i : nat), |- F (n+1) (i :: G) p ==> E (i :: G) p.
Proof.
intros.
elim n.
unfold F.
apply I.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E (i :: G) (E (i :: G) p)).
apply rule_E_Imp.
unfold F in H; fold F in H.
trivial.
apply E_T.
Qed.

Lemma F_K :
 forall (G: list nat) (p q : proposition) (n i:nat),
 |- F n (i::G) p ==> F n (i::G) (p ==> q) ==> F n (i::G) q.
Proof.
intros.
elim n.
unfold F.
apply CI.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E (i::G) ((F n0 (i::G) (p ==> q)) ==> (F n0 (i::G) q))).
apply rule_E_K.
apply E_rule.
trivial.
apply rule_C.
apply E_K.
Qed.

Lemma rule_F_K :
 forall (G: list nat) (p q : proposition) (i n:nat),
 |- F (n+1) (i :: G) (p ==> q) -> |- F (n+1) (i::G) p ==> F (n+1) (i :: G) q.
Proof.
intros.
elim n.
apply MP with (F 1 (i :: G) (p ==> q)).
apply rule_C.
apply F_K.
unfold F.
apply MP with (F (n+1) (i::G) (p ==> q)).
apply F_E_T.
trivial.
intros.
unfold F in H0; fold F in H0.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma F_rule : forall (G: list nat) (p : proposition) (i n:nat), |- p -> |- F n G p.
Proof.
intros.
elim n.
unfold F.
trivial.
intros.
unfold F; fold F.
apply E_rule.
trivial.
Qed.

Lemma rule_F_Imp :
 forall (G: list nat) (p q : proposition) (n:nat), |- p ==> q -> |- F n G p ==> F n G q.
Proof.
intros.
elim n.
unfold F.
trivial.
intros.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma F_Ki :
 forall (G: list nat) (p : proposition) (n i j : nat),
 In i (j::G) -> |- F (n+1) (j::G) p ==> K i p.
Proof.
intros.
elim n.
unfold F.
apply E_Ki.
trivial.
intros.
unfold F; fold F.
unfold F in H0; fold F in H0.
apply Transitivity_of_Imp with (E (j::G) (F n0 (j::G) p)).
apply E_T.
trivial.
Qed.

Lemma F_AND1 :
 forall (G: list nat) (p q : proposition) (n:nat), |- F n G (p & q) ==> F n G p.
Proof.
intros.
elim n.
unfold F.
apply AND1.
intros.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma F_AND2 :
 forall (G: list nat) (p q : proposition) (n:nat), |- F n G (p & q) ==> F n G q.
Proof.
intros.
elim n.
unfold F.
apply AND2.
intros.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma F_AND :
 forall (G: list nat) (p q : proposition) (n:nat), |- F n G (p & q) ==> F n G p & F n G q.
Proof.
intros.
elim n.
unfold F.
apply I.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E G ((F n0 G p) & (F n0 G q))).
apply rule_E_Imp.
trivial.
apply E_AND.
Qed.

Lemma ANDF :
 forall (G: list nat) (p q : proposition) (n:nat), |- F n G p & F n G q ==> F n G (p & q).
Proof.
intros.
elim n.
unfold F.
apply I.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E G ((F n0 G p) & (F n0 G q))).
apply ANDE.
apply rule_E_Imp.
trivial.
Qed.

Lemma F_AND_comm :
 forall (G: list nat) (p q : proposition) (n:nat), |- F n G (p & q) ==> F n G (q & p).
Proof.
intros.
elim n.
unfold F.
apply AND_comm.
intros.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma C_F : forall (G:list nat) (p:proposition) (n:nat), |- C G p ==> F n G p.
Proof.
intros.
elim n.
unfold F.
apply C_T.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E G (C G p)).
apply C_EC.
apply rule_E_Imp.
trivial.
Qed.

(* =================== Lemmas on STAR, iteration of Star =============== *)

Fixpoint STAR (n:nat) (p:proposition) {struct n} : proposition :=
  match n with
  | 0 => p
  | S m => [*] (STAR m p)
  end.

Notation "[*]<: n :> p":= (STAR n p) (at level 65).

Lemma STAR_T :
 forall (p : proposition) (n : nat), |- [*]<:n:> p ==> p.
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] p).
apply rule_Star_K.
apply Star_rule.
trivial.
apply Star_T.
Qed.

Lemma STAR_T_Sn_n :
 forall (p : proposition) (n : nat), |- [*]<:n+1:> p ==> [*]<:n:> p.
Proof.
intros.
elim n.
unfold STAR.
apply Star_T.
intros.
unfold STAR; fold STAR.
apply rule_Star_K.
apply Star_rule.
unfold STAR in H; fold STAR in H.
trivial.
Qed.

Lemma STAR_Star_T :
 forall (p : proposition) (n : nat), |- [*]<:n+1:> p ==> [*] p.
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] ([*] p)).
apply rule_Star_Imp.
unfold STAR in H; fold STAR in H.
trivial.
apply Star_T.
Qed.

Lemma STAR_K :
  forall (p q : proposition) (n :nat),
    |- [*]<:n:> p ==> [*]<:n:> (p ==> q) ==> [*]<:n:> q.
Proof.
intros.
elim n.
unfold STAR.
apply CI.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (([*]<:n0:> (p ==> q)) ==> ([*]<:n0:> q))).
apply rule_Star_K.
apply Star_rule.
trivial.
apply rule_C.
apply Star_K.
Qed.

Lemma rule_STAR_K :
  forall (p q : proposition) (n:nat),
    |- [*]<:n+1:> (p ==> q) -> |- [*]<:n+1:> p ==> [*]<:n+1:> q.
Proof.
intros.
elim n.
apply MP with ([*]<:1:> (p ==> q)).
apply rule_C.
apply STAR_K.
unfold STAR.
apply MP with ([*]<:n+1:> (p ==> q)).
apply STAR_Star_T.
trivial.
intros.
unfold STAR in H0; fold STAR in H0.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_rule : forall (p : proposition) (n:nat), |- p -> |- [*]<:n:> p.
Proof.
intros.
elim n.
unfold STAR.
trivial.
intros.
unfold STAR; fold STAR.
apply Star_rule.
trivial.
Qed.

Lemma rule_STAR_Imp :
 forall (p q : proposition) (n:nat), |- p ==> q -> |- [*]<:n:> p ==> [*]<:n:> q.
Proof.
intros.
elim n.
unfold STAR.
trivial.
intros.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_AND1 :
 forall (p q : proposition) (n:nat), |- [*]<:n:> (p & q) ==> [*]<:n:> p.
Proof.
intros.
elim n.
unfold STAR.
apply AND1.
intros.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_AND2 :
 forall (p q : proposition) (n:nat), |- [*]<:n:> (p & q) ==> [*]<:n:> q.
Proof.
intros.
elim n.
unfold STAR.
apply AND2.
intros.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_AND :
 forall (p q : proposition) (n:nat), |- [*]<:n:> (p & q) ==> ([*]<:n:> p) & [*]<:n:> q.
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (([*]<:n0:> p) & ([*]<:n0:> q))).
apply rule_Star_Imp.
trivial.
apply Star_AND.
Qed.

Lemma ANDSTAR :
 forall (p q : proposition) (n:nat), |- ([*]<:n:> p) & ([*]<:n:> q) ==> [*]<:n:> (p & q).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (([*]<:n0:> p) & ([*]<:n0:> q))).
apply ANDStar.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_AND_comm :
 forall (p q : proposition) (n:nat), |- [*]<:n:> (p & q) ==> [*]<:n:> (q & p).
Proof.
intros.
elim n.
unfold STAR.
apply AND_comm.
intros.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_Star_comm :
  forall (p:proposition) (n:nat), |- [*]<:n:> ([*] p) ==> [*] ([*]<:n:> p).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma Star_STAR_comm :
  forall (p:proposition) (n:nat), |- [*] ([*]<:n:> p) ==> [*]<:n:> ([*] p).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply rule_Star_Imp.
trivial.
Qed.

Lemma STAR_elim :
 forall (p q : proposition) (n :nat),
   |- p ==> [*] p -> |- (p ==> q) -> |- ([*] p ==> [*] q) ==> [*]<:n:> (p==>q).
Proof.
intros.
apply Transitivity_of_Imp with (p ==> [*] q).
apply MP with (p ==> [*] p).
apply rule_C.
apply B.
apply H.
apply Transitivity_of_Imp with (p ==> q).
apply MP with ([*] q ==> q).
apply B.
apply Star_T.
apply MP with ([*]<:n:> (p ==> q)).
apply Hilbert_K.
apply STAR_rule.
apply H0.
Qed.

(* ============================ Lambda/Epsi ======================== *)

Variable lambda : nat -> proposition.
Definition epsi (j : nat) := lambda j & ¬lambda (j+1).

Variable muddy : nat -> proposition.

Lemma lambda_epsi_Imp:
 forall j : nat, |- lambda j & ¬epsi j ==> lambda (j+1).
Proof.
intros.
unfold epsi.
apply
 Transitivity_of_Imp
  with ((lambda j & ¬lambda j) V (lambda j & lambda (j+1))).
apply Transitivity_of_Imp with (lambda j & (¬lambda j V lambda (j+1))).
apply rule_AND_left_regular.
apply Transitivity_of_Imp with (¬lambda j V ¬(¬lambda (j+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.
apply rule_Imp_AND.
apply rule_C.
apply I.
apply False_Imp_everything.
apply AND2.
Qed.

Lemma lambda_epsi_Exclu : forall (k:nat), |-lambda (k +1) & epsi k ==> FALSE.
Proof.
intros.
unfold epsi.
apply Transitivity_of_Imp with (lambda (k +1)  & ¬lambda (k +1)).
apply rule_glueAND.
apply I.
apply AND2.
apply Transitivity_of_Imp with (¬lambda (k +1)& lambda (k +1)).
apply AND_comm.
apply Not_p_AND_p.
Qed.

(* ========================================================================== *)
(* ================ The axioms of the Muddy Children Problem ================ *)
(* ========================================================================== *)

Notation "[¤] p":= (Point  p) (at level 30).

Axiom MC1_1 : forall (G: list nat),
  |- [¤] TRUE ==> C G (lambda 1).

Axiom MC1_2 : forall (k i : nat),
  |- [¤] TRUE ==>  (muddy i) ==> K i (epsi k V epsi (k+1) ).

Axiom PERS_MC1_2 : forall (i k: nat), 
  |-(muddy i ==> K i (epsi k V epsi (k +1))) ==> [*] (muddy i ==> K i (epsi k V epsi (k+1))).

Lemma MC1 : forall (G: list nat) (k i : nat),
  |- [¤] TRUE ==>  ( C G (lambda 1) & ((muddy i) ==> K i (epsi k V epsi (k+1) ) ) ).
Proof.
intros.
apply Transitivity_of_Imp with ([¤] TRUE & [¤] TRUE).
apply AND_idempotence.
apply rule_glueAND.
apply MC1_1.
apply MC1_2.
Qed.

Axiom MC2 : forall (G: list nat) (j : nat),
  |- E G (E G (lambda j)) ==> [*] (E G (¬epsi j)).

Axiom MC3 : forall (i k : nat), |- muddy i ==> K i (epsi k) ==> K i (muddy i).

Axiom PERS_lambda : forall (i:nat), |- lambda i ==> [*] (lambda i).

Axiom PERS_muddy : forall (i:nat), |- muddy i ==> [*] (muddy i).

Axiom PERS_TRUE : |- TRUE ==> [*] TRUE.

Axiom PERS_epsi : forall (i:nat), |- epsi i ==> [*] (epsi i).

Lemma rule_STAR_PERS_p : forall (p:proposition) (n:nat), |- p ==> [*] p -> |- p ==> [*]<:n:> (p).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] p).
apply H.
apply rule_Star_Imp.
apply H0.
Qed.

Lemma rule_KT1 : forall (p : proposition) (i : nat), |- p ==> [*] p -> |- K i p ==> [*] (K i p).
Proof.
intros.
apply Transitivity_of_Imp with (K i ([*] p)).
apply rule_K_K_rev.
apply K_rule.
trivial.
apply KT1.
Qed.

Lemma rule_STAR_KT1 : forall (p : proposition) (i n: nat),
  |- p ==> [*] p -> |- K i p ==> [*]<:n:> (K i p).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (K i p)).
apply rule_KT1.
apply H.
apply rule_Star_Imp.
apply H0.
Qed.

Lemma ET1 : forall (G: list nat) (p : proposition), |- E G ([*] p) ==> [*] (E G p).
Proof.
intros.
elim G.
unfold E.
apply PERS_TRUE.
intros.
unfold E; fold E.
apply Transitivity_of_Imp with ([*] (K a p) & [*] (E l p)).
apply rule_glueAND.
apply KT1.
trivial.
apply ANDStar.
Qed.

Lemma rule_ET1 : forall (p : proposition) (G: list nat), |- p ==> [*] p -> |- E G p ==> [*] (E G p).
Proof.
intros.
apply Transitivity_of_Imp with (E G ([*] p)).
apply rule_E_Imp.
trivial.
apply ET1.
Qed.

Lemma rule_STAR_ET1 : forall (p : proposition) (n: nat) (G:list nat),
  |- p ==> [*] p -> |- E G p ==> [*]<:n:> (E G p).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (E G p)).
apply rule_ET1.
apply H.
apply rule_Star_Imp.
apply H0.
Qed.

Lemma FT1 : forall (G: list nat) (p : proposition) (n: nat), |- F n G ([*] p) ==> [*] (F n G p).
Proof.
intros.
elim n.
unfold F.
apply I.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E G ([*] (F n0 G p))).
apply rule_E_Imp.
trivial.
apply ET1.
Qed.

Lemma rule_FT1 : forall (p : proposition) (G: list nat) (n: nat), |- p ==> [*] p -> |- F n G p ==> [*] (F n G p).
Proof.
intros.
apply Transitivity_of_Imp with (F n G ([*] p)).
apply rule_F_Imp.
trivial.
apply FT1.
Qed.

Lemma rule_STAR_FT1 : forall (p : proposition) (m n: nat) (G:list nat),
  |- p ==> [*] p -> |- F m G p ==> [*]<:n:> (F m G p).
Proof.
intros.
elim n.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (F m G p)).
apply rule_FT1.
apply H.
apply rule_Star_Imp.
apply H0.
Qed.

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

Lemma GainConn :
  forall  (G: list nat) (i j : nat), |- E (i::G) (E (i::G) (lambda j)) ==> [*] (E (i::G) (lambda (j+1))).
Proof.
intros.
apply Transitivity_of_Imp with ([*] (E (i::G) (lambda j & ¬epsi j))).
apply Transitivity_of_Imp with ([*] (E (i::G) (lambda j) & E (i::G) (¬epsi j))).
apply Transitivity_of_Imp with (E (i::G) (E (i::G) (lambda j)) & E (i::G) (E (i::G) (lambda j))).
apply AND_idempotence.
apply Transitivity_of_Imp with ([*] (E (i::G) (lambda j)) & [*] (E (i::G) (¬epsi j))).
apply rule_glueAND.
apply Transitivity_of_Imp with (E (i::G) (lambda j)).
apply E_T.
apply rule_ET1.
apply PERS_lambda.
apply MC2.
apply ANDStar.
apply rule_Star_Imp.
apply Transitivity_of_Imp with (E (i::G) (lambda j & ¬epsi j)).
apply ANDE.
apply rule_E_Imp.
apply I.
apply rule_Star_Imp.
apply rule_E_Imp.
apply lambda_epsi_Imp.
Qed.

Lemma MultGainConn :
  forall (G: list nat) (m i j : nat), |- F ((m+1)+1) (i::G) (lambda j) ==> [*] (F (m+1) (i::G) (lambda (j+1))).
Proof.
intros.
elim m.
unfold F.
apply GainConn.
intros.
unfold F in H; fold F in H.
unfold F; fold F.
apply Transitivity_of_Imp with ( E (i::G) ( [*] (E (i::G) (F n (i::G) (lambda (j +1))))) ).
apply rule_E_Imp.
trivial.
apply ET1.
Qed.

Lemma MultGainConn' :
  forall (G: list nat) (m i j : nat),
    |- (F ((m+1)+1) (i::G) (lambda j)) ==> [*] (E (i::G) (F (m) (i::G) (lambda (j+1)))).
Proof.
intros.
elim m.
unfold F.
apply GainConn.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E (i :: G) ( [*] (E (i::G) (F (n) (i :: G) (lambda (j +1)))))).
apply rule_E_Imp.
unfold F in H; fold F in H.
trivial.
apply ET1.
Qed.

Lemma ComImpPartIt : forall (p:proposition) (n:nat) (G: list nat), |- C G p ==> F n G p.
Proof.
intros.
elim n.
unfold F.
apply C_T.
intros.
unfold F; fold F.
apply Transitivity_of_Imp with (E G (C G p)).
apply C_EC.
apply rule_E_Imp.
trivial.
Qed.

Lemma PointImpPartIt : forall (G:list nat) (m:nat), |- [¤] TRUE ==> F m G (lambda 1).
Proof.
intros.
apply Transitivity_of_Imp with (C G (lambda 1)).
apply MC1_1.
apply ComImpPartIt.
Qed.

Lemma F_EF : forall (G:list nat) (p:proposition) (m n:nat), |- F (m+1) G p ==> E G (F (m) G p).
Proof.
intros.
elim m.
unfold F.
apply I.
intros.
unfold F in H; fold F in H.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma EF_F : forall (G:list nat) (p:proposition) (m c:nat), |- E G (F (m) G p) ==> F (m+1) G p.
Proof.
intros.
elim m.
unfold F.
apply I.
intros.
unfold F; fold F.
apply rule_E_Imp.
trivial.
Qed.

Lemma PointImpProgr : forall (G:list nat) (i j n:nat), |- [¤] TRUE ==> [*]<:j:> (F (n+1) (i::G) (lambda (j+1) ) ).
Proof.
intro G. intro i. intro j. 
elim j.
unfold STAR.
intro c.
apply Transitivity_of_Imp with (C (i::G) (lambda 1) ).
apply MC1_1.
apply C_F.
intro n.
intro H.
intro n1.
apply Transitivity_of_Imp with ( [*]<:n:> (F ((n1 +1) +1) (i::G) (lambda (n +1))) ).
apply H.
elim n.
unfold STAR.
apply MultGainConn.
intros.
unfold STAR; fold STAR; unfold STAR in H; fold STAR in H.
apply Transitivity_of_Imp with ( [*]<:n0:> ([*] (F ((n1 +1) +1) (i::G) (lambda ((n0 +1) +1)))) ).
apply Star_STAR_comm.
apply Transitivity_of_Imp with ( [*]<:n0:> ([*] ([*] (F (n1 +1) (i::G) (lambda (((n0 +1) +1) +1))))) ).
apply rule_STAR_Imp.
apply rule_Star_Imp.
apply MultGainConn.
apply Transitivity_of_Imp with ( [*] ([*]<:n0:> ([*] (F (n1 +1) (i :: G) (lambda (((n0 +1) +1) +1)))))).
apply STAR_Star_comm.
apply rule_Star_Imp.
apply STAR_Star_comm.
Qed.

Lemma PERS_STAR_MC1_2 : forall (i k c: nat), 
  |-(muddy i ==> K i (epsi k V epsi (k +1))) ==> [*]<:c:> (muddy i ==> K i (epsi k V epsi (k+1))).
Proof.
intros.
elim c.
unfold STAR.
apply I.
intros.
unfold STAR; fold STAR.
apply Transitivity_of_Imp with ([*] (muddy i ==> K i (epsi k V epsi (k +1)))).
apply PERS_MC1_2.
apply rule_Star_Imp.
apply H.
Qed.

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

Lemma TOOL2 : forall (p q r: proposition), |- p & (q ==> r) ==> (q ==> p & r).
Proof.
intros.
apply Transitivity_of_Imp with (q & q ==> p & r).
apply rule_glueAND2.
apply Hilbert_K.
apply I.
apply TOOL1.
apply AND_idempotence.
Qed.

Lemma Concl : forall (G:list nat) (i j m : nat), In i (j::G) -> |- [¤] TRUE ==> [*]<:m:> (muddy i ==> (K i (muddy i) ) ).
Proof.
intros.
apply Transitivity_of_Imp with ( [*]<:m:> ( muddy i ==> (K i (epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( [*]<:m:> ( muddy i ==> (K i (FALSE V epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( [*]<:m:> ( muddy i ==> (K i ((lambda (m+1) & epsi (m)) V epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( [*]<:m:> ( muddy i ==> (K i ((lambda (m+1) & epsi (m)) V (lambda (m+1) & epsi (m+1)) ) ) ) ).
apply Transitivity_of_Imp with ( [*]<:m:> ( muddy i ==> (K i (lambda (m+1) & (epsi (m) V epsi (m+1)) ) ) ) ).
apply Transitivity_of_Imp with ( [*]<:m:> ( muddy i ==> (K i (lambda (m+1)) & K i (epsi (m) V epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( [*]<:m:> ( K i (lambda (m+1)) & (muddy i ==> (K i (epsi (m) V epsi (m+1)) ) ) ) ).
apply Transitivity_of_Imp with ( ([*]<:m:> ( E (j::G) (lambda (m+1))) & (muddy i ==> (K i (epsi (m) V epsi (m+1)) ) ) ) ).
apply Transitivity_of_Imp with ( ([*]<:m:> ( E (j::G) (lambda (m+1)) )) & [*]<:m:> (muddy i ==> (K i (epsi (m) V epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( ([*]<:m:> ( E (j::G) (lambda (m+1)) )) & (muddy i ==> (K i (epsi (m) V epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( ([*]<:m:> ( E (j::G) (lambda (m+1)) )) & (muddy i ==> (K i (epsi (m) V epsi (m+1)) ) ) ).
apply Transitivity_of_Imp with ( [¤] TRUE & [¤] TRUE ).
apply AND_idempotence.
apply rule_glueAND.
apply Transitivity_of_Imp with ( [*]<:m:> (F 1 (j::G) (lambda (m+1))) ).
apply PointImpProgr.
apply rule_STAR_Imp.
unfold F.
apply I.
apply MC1_2.
apply I.
apply rule_glueAND.
apply I.
apply PERS_STAR_MC1_2.
apply ANDSTAR.
apply rule_STAR_Imp.
apply Transitivity_of_Imp with ( (E (j::G) (lambda (m +1))) & (muddy i ==> K i (epsi m V epsi (m +1) ) ) ).
apply I.
apply rule_AND_right_regular.
apply E_Ki.
trivial.
apply rule_STAR_Imp.
apply TOOL2.
apply rule_STAR_Imp.
apply MP with ( K i (lambda (m +1)) & K i (epsi m V epsi (m +1)) ==> K i (lambda (m +1) & (epsi m V epsi (m +1)) ) ).
apply B.
apply AND_Ki.
apply rule_STAR_Imp.
apply MP with ( (K i (lambda (m +1) & (epsi m V epsi (m +1)))) ==> (K i ((lambda (m +1) & epsi m) V (lambda (m +1) & epsi (m +1))) ) ).
apply B.
apply rule_K_K_rev.
apply K_rule.
apply dist_AND.
apply rule_STAR_Imp.
apply MP with ( K i (lambda (m +1) & epsi m V (lambda (m +1) & epsi (m +1))) ==> K i (lambda (m +1) & epsi m V epsi (m +1) ) ).
apply B.
apply rule_K_K_rev.
apply K_rule.
apply rule_OR_left_regular.
apply AND2.
apply rule_STAR_Imp.
apply MP with ( K i (lambda (m +1) & epsi m V epsi (m +1)) ==> K i (FALSE V epsi (m +1)) ).
apply B.
apply rule_K_K_rev.
apply K_rule.
apply rule_OR_right_regular.
apply lambda_epsi_Exclu.
apply rule_STAR_Imp.
apply MP with (  K i (FALSE V epsi (m +1)) ==> K i (epsi (m +1)) ).
apply B.
apply rule_K_K_rev.
apply K_rule.
apply Transitivity_of_Imp with (epsi (m+1) V FALSE).
apply OR_comm.
apply OR_FALSE.
apply rule_STAR_Imp.
apply MP with (muddy i ==> K i (epsi (m+1)) ==> K i (muddy i)).
apply Hilbert_S.
apply MC3.
Qed.

End Muddy_Children.