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

(****************************************************************************)
(*                              muddy.v                                     *)
(*                                                                          *)
(*                             Pierre Lescanne                              *)
(*                                                                          *)
(*		       LIP (ENS-Lyon, CNRS, INRIA)                          *)
(*                                                                          *)
(*                                                                          *)
(* Developed in V7.0   January 2001  --- March   2004                       *)
(****************************************************************************)

Section Muddy_Children.


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

Require PolyList.
Require Arith.
Require classic.
Require epistemic.

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

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

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

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

Fixpoint list_of [n:nat] : (list nat) :=
    Cases n of
        O => (nil nat)
     | (S m) => (cons m (list_of m))
    end.

Notation "< n >" := (list_of n) (at level 3).

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

Variable At_least : nat -> nat -> proposition.
Definition Exactly := [n,p:nat] (At_least n p) & ¬(At_least n (S p)).
Variable NobodyKnows : nat -> proposition.

Lemma At_least_n_and_not_Exactly_n: (n,p:nat) 
    |- (At_least n p) & ¬(Exactly n p) => (At_least n (S p)).
Proof.
Intros. 
Unfold Exactly.
Apply Cut_rule with ((At_least n p) & ¬(At_least n p)) V  ((At_least n p) & (At_least n (S p))).
Apply Cut_rule with (At_least n p) & (¬(At_least n p) V (At_least n (S p))).
Apply rule_AND_left_regular.
Apply Cut_rule with ¬(At_least n p) V ¬¬(At_least n (S p)).
Apply Class_OR_Not.
Apply rule_OR_left_regular.
Apply Classic_NotNot.
Apply dist_AND.
Apply rule_OR0.
Apply Cut_rule with FALSE.
Unfold Not.
Apply rule_Imp_AND.
Apply rule_C.
Apply I.
Apply False_Imp_everything.
Apply AND2.
Qed.

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

Axiom Knowledge_Diffusion : (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 : (n,p,k:nat) (le k n) ->
    |- (E <n> (At_least n p)) => (E <n> ¬(Exactly n p)) 
        => (E (list_of k) (E <n> ¬(Exactly n p))).
Proof.
Intros n p k. 
Elim k.
Intro.
Simpl. Apply Drop_hyp. Apply Drop_hyp. Apply theorem_True.

Intros. 
Simpl.
Apply rule_rev_AND_Imp.
Apply rule_AND_Imp.
Apply rule_Imp_AND.
Apply Knowledge_Diffusion.
Apply rule_Imp_AND.
Apply H.
Apply le_trans_S. Assumption.
Qed.

Lemma E_Awareness : (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 : (n,p:nat) 
    |- (C (list_of (S n)) (At_least (S n) p)) => (E (list_of (S n)) ¬((Exactly (S n) p)))
              => ((C (list_of (S n)) ¬(Exactly (S n) p))).
Proof.
Intros. 
Apply rule_rev_AND_Imp.
Apply Rule_for_C.
Apply rule_AND_Imp.
Apply rule_Imp_AND_right.
Unfold list_of.
Apply E_T.
Apply Cut_rule with 
    (E (list_of (S n)) (C (list_of (S n))(At_least (S n) p)))  
  & (E (list_of (S n)) (E (list_of (S n)) ¬(Exactly (S n) p))).
Apply rule_AND_Imp.
Apply rule_Imp_AND_left.
Apply C_EC.
Apply Cut_rule with 
    (E (list_of (S n)) (At_least (S n) p)) & (E (list_of (S n)) ¬(Exactly (S n) p)).
Apply rule_AND_right_regular.
Apply C_E.
Apply rule_Imp_AND.
Apply E_Awareness.
Auto.
Apply ANDE.
Qed.

Lemma Progress : (n,p:nat) 
    |- (C (list_of (S n)) (At_least (S n) p)) & (E (list_of (S n)) ¬(Exactly (S n) p))
                    => (C (list_of (S n)) (At_least (S n) (S p))).
Proof.
Intros. Apply Cut_rule with (C (list_of (S n)) (At_least (S n) p)) & (C (list_of (S n)) ¬(Exactly (S n) p)).
Apply rule_AND_Imp.
Apply AND1.
Apply rule_Imp_AND.
Apply C_Awareness.
Apply rule_Imp_AND.
Apply Cut_rule with (C (list_of (S n)) ¬(Exactly (S n) p) => (At_least (S n) (S p))).
Apply rule_C_K_rev.
Apply C_rule.
Apply rule_rev_AND_Imp.
Apply At_least_n_and_not_Exactly_n.
Apply C_K_rev.
Qed.

End  Muddy_Children.