(*******************************************************************)
(* Coq formalisation accompanying                                  *)
(* ["The Inductive and Modal Proof Theory of Aumann's Theorem"],   *)
(* Rene Vestergaard, Pierre Lescanne, Hiroakira Ono                *)
(*                                                                 *)
(* Part 1: Abstract development                                    *)
(*                                                                 *)
(* Developed in Coq, v8.0 by Rene Vestergaard, JAIST               *)
(*                                                                 *)
(* All rights reserved by the developer.                           *)
(*******************************************************************)

Section eAumann_abstract.

(* === Ad Hoc Epistemic Logic === *)

Definition U := Set.

(* Agents, uniquely identifiable *)
Variable G : U. 
Variable agentEq : G -> G -> bool.

Axiom agentEqual : forall a, (agentEq a a) = true.

(* Formulas *)
Inductive eProp : U :=
| eTrue : eProp
| Neg   : eProp -> eProp
| Imp   : eProp -> eProp -> eProp
| And   : eProp -> eProp -> eProp
| Or    : eProp -> eProp -> eProp
| K     : G -> eProp -> eProp
| C     : eProp -> eProp.

Definition nKn  (a:G) (P:eProp) := Neg (K a (Neg P)). 

Infix "==>" := Imp (right associativity, at level 85).
Infix "&&"  := And (left associativity, at level 50).
Infix "vv"  := Or  (left associativity, at level 50).

(* === Game Basics === *)

Variable payoff : U.
Variable eLeq : payoff -> payoff -> eProp.
Definition payoffs := G -> payoff.

Inductive choice : U :=
| lchoice
| rchoice.

Inductive strategy : U :=
| sLeaf : payoffs -> strategy
| sNode : G
          -> choice
          -> strategy -> strategy
          -> strategy.

Fixpoint stratPO (s:strategy) {struct s} : payoffs :=
match s with
| (sLeaf po) => po
| (sNode a c sl sr)
    => match c with
       | lchoice => (stratPO sl)
       | rchoice => (stratPO sr)
       end
end.

Fixpoint eBI (s:strategy) {struct s} : eProp :=
match s with
| (sLeaf po) => eTrue
| (sNode a c sl sr)
    => (eBI sl) && (eBI sr)
        && match c with
           | lchoice => eLeq ((stratPO sr) a) ((stratPO sl) a)
           | rchoice => eLeq ((stratPO sl) a) ((stratPO sr) a)
           end
end.

(* === Local Rationality === *)

Fixpoint eLRat (s:strategy) {struct s} : eProp :=
match s with
| (sLeaf po) => eTrue
| (sNode a c sl sr) 
    => (eLRat sl) && (eLRat sr)
        && match c with
           | lchoice => nKn a (eLeq ((stratPO sr) a) ((stratPO sl) a))
           | rchoice => nKn a (eLeq ((stratPO sl) a) ((stratPO sr) a))
           end
end. 

(* === Our Theorem  === *)

Definition eDec (P:eProp) := P vv (Neg P).

Inductive eThm : eProp -> Prop :=
| e_id :       forall p : eProp, eThm (p ==> p) 
| prj_33 :    forall p1 p2 q1 q2 r1 r2 : eProp,
                     (eThm (p1 ==> p2)) 
                      -> (eThm (q1 ==> q2)) 
                      -> (eThm (r1 ==> r2)) 
                      -> (eThm (p1 && q1 && r1 
                                ==> p2 && q2 && r2))
| dec_T_nKn : forall a : G, forall p : eProp, 
                     eThm ((eDec p) ==> (nKn a p) ==> p)
| e_MP :      forall p q : eProp,
                     eThm (p ==> q) -> eThm p -> eThm q.

Notation "|- p" := (eThm p) (at level 85).

Axiom decOrd : forall po1 po2 : payoff, |- (eDec ((eLeq po1) po2)).

Theorem Dec_LRat_BI : forall s : strategy , |-  (eLRat s ==> eBI s).
Proof.
induction s.
(* sLeaf case *) simpl. apply e_id.
(* sNode case *) simpl. 
     (* projs *) apply prj_33.  
       (*  l_rec *) apply IHs1. 
       (*  r_rec *) apply IHs2.
       (* clause *) induction c; (eapply e_MP ; [apply dec_T_nKn | apply decOrd]).
Qed.

(* === Aumann's Theorem: full rationality encapsulated in C ===*)

Fixpoint Comp_nKns (a:G) (s:strategy) (p:payoff) 
                   {struct s} : eProp :=
match s with
| (sLeaf po) => nKn a (eLeq (po a) p)
| (sNode a' c sl sr) 
   => if (agentEq a a')
      then (Comp_nKns a sl p) 
           && (Comp_nKns a sr p)
      else match c with
           | lchoice => (Comp_nKns a sl p)
           | rchoice => (Comp_nKns a sr p)
           end      
end.

Fixpoint eRat (s:strategy) {struct s} : eProp :=
match s with
| (sLeaf po) => eTrue
| (sNode a c sl sr) 
    => (eRat sl) && (eRat sr)
        && (Comp_nKns a s ((stratPO s) a))
end. 

Inductive eThm' : eProp -> Prop :=
| import :  forall p : eProp,
                   |- p -> eThm' p
| T_C :     forall p : eProp,
                   eThm' (C p ==> p)    
| eId' :    forall p : eProp,
                   eThm' (p ==> p)
| prj_33' : forall p1 p2 q1 q2 r1 r2 : eProp,
                   (eThm' (p1 ==> p2)) 
                    -> (eThm' (q1 ==> q2)) 
                    -> (eThm' (r1 ==> r2)) 
                    -> (eThm' (p1 && q1 && r1 
                               ==> p2 && q2 && r2))
| trans :   forall p q r : eProp,
                   (eThm' (p ==> q)) 
                    -> (eThm' (q ==> r))
                    -> (eThm' (p ==> r))  
| prj_l :   forall pl pr : eProp,
                   eThm' (pl && pr ==> pl)
| prj_r :   forall pl pr : eProp,
                   eThm' (pl && pr ==> pr).

Notation "|-' p" := (eThm' p) (at level 85).

Lemma nKns_is_nKn : forall a p s, |-' ((Comp_nKns a s p) ==> nKn a (eLeq ((stratPO s) a) p)).
Proof.
induction s.
(* sLeaf case *) simpl.  apply eId'.
(* sNode case *) simpl. case agentEq.
   (* a = a0 case *) case c. 
      (* lchoice case *) eapply trans. apply prj_l.
                         apply IHs1.
      (* rchoice case *) eapply trans. apply prj_r.
                         apply IHs2.
   (* a <> a0 case *) induction c. apply IHs1. apply IHs2.
Qed.

Lemma Rat_is_LRat : forall s : strategy, |-' (eRat s ==> eLRat s).
Proof.
induction s.  
(* sLeaf case *) simpl. apply eId'.
(* sNode case *) simpl.  apply prj_33'.
   (* l case *) apply IHs1.
   (* r case *) apply IHs2.
   (* body *) rewrite agentEqual. induction c.
      (* lchoice case *) eapply trans. apply prj_r. apply nKns_is_nKn.
      (* rchoice case *) eapply trans. apply prj_l. apply nKns_is_nKn.
Qed.

Theorem Aumann_noC  : forall s : strategy , |-' (eRat s ==> eBI s).
Proof.
intro.
eapply trans. 
apply Rat_is_LRat.
apply import. apply Dec_LRat_BI.
Qed.

Theorem Aumann : forall s : strategy, |-' (C (eRat s) ==> eBI s).
Proof.
intro.
eapply trans. 
apply T_C.
apply Aumann_noC.
Qed.

End eAumann_abstract.