(********************************************************************************)
(*                               finite_games.v                                 *)
(*                                                                          	*)
(**               © Pierre Lescanne  (February-November 2008)        	        *)
(*                                                                          	*)
(*		       LIP (ENS-Lyon, CNRS, INRIA) 				*)
(*                                                                          	*)
(*                                                                          	*)
(* Developed in V8.1                 February-March-April-Octobre-November 2008 *)
(********************************************************************************)
Section Finiteextensivegames.

        (*  -------------- *)
        (** - Requirements *)
        (*  -------------- *)

Require Import Relations.


        (** * Agents, utilities, preference *)

Variable Agent : Set.
Variable Utility: Set.
Variable preference: relation Utility.  Infix "=<" := preference (at level 100).
Hypothesis preference_is_preorder: preorder Utility preference.
Definition Utility_fun := Agent -> Utility.

        (*  -------------- *)
        (** *   Games      *)
        (*  -------------- *)

Inductive FinGame : Set :=
| gLeaf : Utility_fun -> FinGame
| gNode : Agent -> FinGame -> FinGame -> FinGame.


        (** *  Strategies  *)


Inductive Choice : Set := | left | right. 

Inductive FinStrategy : Set :=
| sLeaf : Utility_fun -> FinStrategy
| sNode : Agent -> Choice -> FinStrategy -> FinStrategy -> FinStrategy.

        (** ** The game of a strategy *)

Fixpoint f2g (s:FinStrategy) : FinGame :=
match s with
| (sLeaf uf)        => (gLeaf uf)
| (sNode a c sl sr) => (gNode a (f2g sl) (f2g sr))
end.


        (** **   Utilities and strategies     *)

Fixpoint f2u (s:FinStrategy): Utility_fun :=
match s with
| (sLeaf uf)            => uf
| (sNode a left sl sr)  =>  (f2u sl)
| (sNode a right sl sr) =>  (f2u sr)
  end.


        (*    ----------------  *)
        (** * Convertibility    *)
        (*    ----------------  *)

Inductive FinAgentConv: Agent -> FinStrategy -> FinStrategy -> Prop :=
| ConvLeaf: forall (a:Agent) (uf: Utility_fun), FinAgentConv a (sLeaf uf) (sLeaf uf)
| ConvNode1:  forall (a:Agent) (c c': Choice) (s1 s2 s1' s2':FinStrategy),
   (FinAgentConv a s1 s1') -> (FinAgentConv a s2 s2') ->
    FinAgentConv a (sNode a c s1 s2) (sNode a c' s1' s2') 
| ConvNode2:  forall (a a':Agent) (c: Choice) (s1 s2 s1' s2':FinStrategy),
   (FinAgentConv a s1 s1') -> (FinAgentConv a s2 s2') -> 
    FinAgentConv a (sNode a' c s1 s2) (sNode a' c s1' s2').

Notation "s1 <<- a ->> s2" := (FinAgentConv a s1 s2) (at level 70).

Lemma ConvFinSameHeadAgent: 
forall (a a' a'':Agent)(c c':Choice)(s1 s2 s1' s2':  FinStrategy),
  sNode a c s1 s2 <<-a''->> sNode a' c' s1' s2'  -> a = a'.
Proof.
intros.
inversion H; trivial.
Qed.

Lemma ConFinLeafEq: forall (a:Agent) (s: FinStrategy) (uf: Utility_fun),
  s<<- a ->> (sLeaf uf) -> s = (sLeaf uf).
Proof.
intros.
inversion H.
trivial.
Qed.

Lemma ConvFinSameGame: forall (a:Agent) (s s': FinStrategy), s<<-a->>s' -> f2g s = f2g s'.
Proof.
induction s.
  induction 1.
    trivial.
    simpl.
    rewrite IHFinAgentConv1.
    rewrite IHFinAgentConv2.
    trivial.
  simpl.
  rewrite IHFinAgentConv1.
  rewrite IHFinAgentConv2.
  trivial.
induction 1.
    trivial.
    simpl.
    rewrite IHFinAgentConv1.
    rewrite IHFinAgentConv2.
    trivial.
    assumption.
    assumption.
    assumption.
  assumption.
simpl.
    rewrite IHFinAgentConv1.
    rewrite IHFinAgentConv2.
    trivial.
    assumption.
    assumption.
  assumption.
assumption.
Qed.

Lemma ConvFinRefl: forall (a:Agent) (s: FinStrategy), s<<-a->>s. 
Proof.
induction s.
apply ConvLeaf.
apply ConvNode2; assumption.
Qed.

Lemma ConvFinSym: forall (s s': FinStrategy)(a:Agent), s <<-a->> s' -> s'<<-a->>s. 
Proof.
induction 1.
apply ConvLeaf.
intros; apply ConvNode1;  assumption. 
intros; apply ConvNode2; assumption.
Qed.

Lemma ConvFinTrans: forall (s s': FinStrategy)(a:Agent),
  s <<-a->> s' ->  forall (s'': FinStrategy), s'<<-a->>s'' -> s<<-a->>s''.
Proof.
induction 1. 

(* ConvLeaf *)
trivial.

(* ConvNode1 *)
induction s''.
intros.
inversion H1.
intros.
replace a0 with a.
apply ConvNode1.
apply IHFinAgentConv1. 
inversion H1; assumption.
apply IHFinAgentConv2. 
inversion H1; assumption. 
apply ConvFinSameHeadAgent with (a'':=a)(c:=c')(c':=c0)(s1:=s1')(s2:=s2')(s1':=s''1)(s2':=s''2).
assumption.

(* ConvNode2 *)
induction s''.
intros.
inversion H1.
case c. 
case c0.
intros.
replace a0 with a'.
apply ConvNode2.
apply IHFinAgentConv1. 
inversion H1; assumption.
apply IHFinAgentConv2. 
inversion H1; assumption.
inversion H1; trivial.
intros. 
replace a' with a.
replace a0 with a.
apply ConvNode1.
apply IHFinAgentConv1. 
inversion H1. assumption. 
apply IHFinAgentConv2. 
inversion H1. assumption. 
inversion H1. trivial. 
inversion H1. trivial. 
case c0.
intros.
replace a' with a.
replace a0 with a.
apply ConvNode1.
apply IHFinAgentConv1. 
inversion H1. assumption. 
apply IHFinAgentConv2. 
inversion H1. assumption. 
inversion H1. trivial. 
inversion H1. trivial. 
intros. 
replace a0 with a'.
apply ConvNode2.
apply IHFinAgentConv1. 
inversion H1; assumption.  
apply IHFinAgentConv2. 
inversion H1; assumption.
inversion H1; trivial. 
Qed.



   (*    ---------------------------------  *)
   (** * Equilibria and Backward Induction *)
   (*    ---------------------------------  *)

    (** -  Nash equilibria for finite games *) 

Definition FinNashEq (s:FinStrategy): Prop :=  forall (a:Agent) (s':FinStrategy), 
  s<<-a->>s' -> (f2u s' a =< f2u s a).

Lemma FinNashEq_rev1: forall (a:Agent) (s s':FinStrategy), 
  s'<<-a->>s -> FinNashEq s -> (f2u s' a =< f2u s a).
Proof.
unfold FinNashEq.
intros.
apply H0.
apply ConvFinSym. assumption.
Qed.

Lemma FinNashEq_rev2: forall (a:Agent) (s s':FinStrategy), 
  s<<-a->>s' -> FinNashEq s -> (f2u s' a =< f2u s a).
Proof.
unfold FinNashEq.
intros.
apply H0.
assumption.
Qed.

Lemma FinNashEqLeaf : forall (uf:Utility_fun), FinNashEq (sLeaf uf).
Proof.
intros. unfold FinNashEq. 
intros. inversion H. apply (preord_refl Utility preference preference_is_preorder).
Qed.

Lemma FinNashEq_fixpt_left : forall  (a:Agent) (s1 s2: FinStrategy), 
  FinNashEq s1 -> FinNashEq s2 -> (f2u s2 a =< f2u s1 a) -> 
  FinNashEq (sNode a left s1 s2).
Proof.
intros. unfold FinNashEq. intros. 
inversion H2.
  elim c'; simpl.
    apply FinNashEq_rev2. assumption...
    assumption.
  apply (preord_trans Utility preference preference_is_preorder) with (f2u s2 a).
    apply FinNashEq_rev2; assumption...
  assumption...
simpl; apply FinNashEq_rev2; assumption.
Qed.

Lemma FinNashEq_fixpt_right : forall  (a:Agent) (s1 s2: FinStrategy), 
  FinNashEq s1 -> FinNashEq s2 -> (f2u s1 a =< f2u s2 a) -> 
  FinNashEq (sNode a right s1 s2).
Proof.
intros; unfold FinNashEq; intros. 
inversion H2.
  elim c'; simpl.
    apply (preord_trans Utility preference preference_is_preorder) with (f2u s1 a).
      apply FinNashEq_rev2; assumption...
    assumption.
  apply FinNashEq_rev2; assumption...
simpl; apply FinNashEq_rev2; assumption.
Qed.


    (** - Backward Induction for finite games *) 
Inductive BI: FinStrategy -> Prop :=
| BILeaf: forall uf:Utility_fun, BI (sLeaf uf)
| BINode_left: forall (a:Agent) (sl sr: FinStrategy), 
    BI sl -> BI sr -> (f2u sr a =< f2u sl a) ->
    BI (sNode a left sl sr)
| BINode_right: forall (a:Agent) (sl sr: FinStrategy), 
    BI sl -> BI sr -> (f2u sl a =< f2u sr a) ->
    BI (sNode a right sl sr).

(**  - Backward Induction is Nash equilibrium *)
Theorem BI_is_FinNashEq : forall s, BI s -> FinNashEq s.
Proof.
induction s.
  intros; apply FinNashEqLeaf...
induction c; intros; 
  [apply FinNashEq_fixpt_left | apply FinNashEq_fixpt_right]; 
  [apply IHs1 | apply IHs2 | idtac | apply IHs1 | apply IHs2 | idtac]; 
  inversion H; assumption.
Qed.

End Finiteextensivegames.