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

Section eAumann_nat.

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

Definition U := Set.

Inductive eBool : U :=
| eTrue : eBool
| eFalse : eBool.

Inductive Nat : U :=
| Zero : Nat
| Succ : Nat -> Nat.

Inductive eProp : Type :=
| decprop : eBool -> eProp
| Imp     : eProp -> eProp -> eProp
| And     : eProp -> eProp -> eProp
| nKn     : eProp -> eProp.

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

Inductive eThm0 : eProp -> Prop :=
| dec_T :  forall b : eBool, 
            eThm0 (nKn (decprop b) ==> (decprop b))
| e_id :   forall p : eProp,  
            eThm0 (p ==> p) 
| prj_33 : forall p1 p2 q1 q2 r1 r2 : eProp,
            (eThm0 (p1 ==> p2)) 
             -> (eThm0 (q1 ==> q2)) 
             -> (eThm0 (r1 ==> r2)) 
             -> (eThm0 (p1 && q1 && r1 ==> p2 && q2 && r2)).

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

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

Variable G : U.
Definition payoff := Nat.
Definition payoffs := G -> payoff.

Fixpoint eLeqDP (n1 n2:Nat) {struct n1} : eBool :=
match n1,n2 with
| Zero    , _     => eTrue
| Succ n1a, Zero     => eFalse
| Succ n1a, Succ n2a => eLeqDP n1a n2a
end.

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) => decprop eTrue
| (sNode a c sl sr)
    => (eBI sl) && (eBI sr)
        && match c with
           | lchoice => decprop (eLeqDP ((stratPO sr) a) ((stratPO sl) a))
           | rchoice => decprop (eLeqDP ((stratPO sl) a) ((stratPO sr) a))
           end
end.

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

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

(* === Theorems: Aumann w/o C === *)

Theorem nat_LRat_BI : forall s : strategy , |-0  (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; apply dec_T.
Qed.

End eAumann_nat.