Library infinite_extensive_games

© Pierre Lescanne
Developed in V8.1 February 2008 --- June 2009
Section InfiniteExtensiveGames.
  • Requirements
Require Import Relations.

Agents, utilities, preference, choices

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.
Inductive Choice : Set := | l | r.

Histories

CoInductive History: Set :=
| HNil: History
| HCons: Choice -> History -> History.

CoInductive hBisimilar:History ->History -> Prop :=
| bisim_HNil:hBisimilar HNil HNil
| bisim_HCons: forall (a:Choice)(h h':History),
  hBisimilar h h' -> hBisimilar (HCons a h) (HCons a h').

Definition History_identity (h:History): History :=
match h with
| HNil => HNil
| HCons a h => HCons a h
end.

Lemma History_decomposition: forall h: History,
  History_identity h = h.

Notation "h =hbis= h'" := (hBisimilar h h') (at level 80).

Games

CoInductive Game : Set :=
| gLeaf: Utility_fun -> Game
| gNode : Agent -> Game -> Game -> Game.
  • Tools
Lemma Game_Left: forall a a' gl gl' gr gr',
  gNode a gl gr = gNode a' gl' gr' -> gl = gl'.

Lemma Game_Right: forall a a' gl gl' gr gr',
  gNode a gl gr = gNode a' gl' gr' -> gr = gr'.

Definition Game_identity (g:Game): Game :=
match g with
| gLeaf f => gLeaf f
| gNode a gl gr => gNode a gl gr
end.

Lemma Game_decomposition: forall g: Game, Game_identity g = g.
  • Finiteness
Inductive FiniteGame: Game -> Prop :=
| Fin_gLeaf: forall f:Utility_fun, FiniteGame (gLeaf f)
| Fin_gNode: forall (a:Agent) (gl gr:Game),
     FiniteGame gl -> FiniteGame gr -> FiniteGame (gNode a gl gr).
  • Bisimilarity
CoInductive gBisimilar: Game -> Game -> Prop :=
| bisim_gLeaf: forall f, gBisimilar (gLeaf f) (gLeaf f)
| bisim_gNode: forall a gl gl' gr gr',
  gBisimilar gl gl' -> gBisimilar gr gr' -> gBisimilar (gNode a gl gr) (gNode a gl' gr').

Notation "g =gbis= g'" := (gBisimilar g g') (at level 80).

Lemma gBis_refl: forall g, g =gbis= g.

Lemma gBis_sym: forall g g', g =gbis= g' -> g' =gbis= g.
  • Histories of a game
CoInductive IsHistoryOf: History -> Game -> Prop :=
| hist_Leaf: forall (f:Utility_fun), IsHistoryOf HNil (gLeaf f)
| hist_NodeLeft: forall (a:Agent)(gl gr:Game)(h:History),
    (IsHistoryOf h gl) -> IsHistoryOf (HCons l h) (gNode a gl gr)
| hist_NodeRight: forall (a:Agent)(gl gr:Game)(h:History),
    (IsHistoryOf h gr) -> IsHistoryOf (HCons r h) (gNode a gl gr).

Notation "h !s_history_of g" := (IsHistoryOf h g) (at level 80).

CoInductive uf_of_h_in_g: Utility_fun -> History -> Game -> Prop :=
| uhgLeaf: forall (f:Utility_fun), uf_of_h_in_g f HNil (gLeaf f)
| uhgLeft: forall (a:Agent)(gl gr:Game)(h:History)(f:Utility_fun),
    (uf_of_h_in_g f h gl) -> uf_of_h_in_g f (HCons l h) (gNode a gl gr)
| uhgRight: forall (a:Agent)(gl gr:Game)(h:History)(f:Utility_fun),
    (uf_of_h_in_g f h gr) -> uf_of_h_in_g f (HCons r h) (gNode a gl gr).

Strategy Profiles

CoInductive StratProf : Set :=
| sLeaf : Utility_fun -> StratProf
| sNode : Agent -> Choice -> StratProf -> StratProf -> StratProf.

Notation "<< a , c , sl , sr >>" := (sNode a c sl sr) (at level 80).
    Notation "<< f >>" := (sLeaf f) (at level 80).
  • Tools
Lemma StratProf_Leaf: forall f f', <<f>> = (<<f'>>) -> f = f'.

Lemma StratProf_Left: forall a a' c c' sl sl' sr sr',
  (<<a,c,sl,sr>> = <<a',c',sl',sr'>>) -> sl = sl'.

Lemma StratProf_Right: forall a a' c c' sl sl' sr sr',
  (<<a,c,sl,sr>> = <<a',c',sl',sr'>>) -> sr = sr'.

Definition StratProf_identity (s:StratProf): StratProf :=
match s with
| <<f>> => <<f>>
| <<a,c,sl,sr>> => <<a,c,sl,sr>>
end.

Lemma StratProf_decomposition: forall s: StratProf,
  StratProf_identity s = s.
  • Finiteness
Inductive FiniteStrat: StratProf -> Prop :=
| Fin_sLeaf: forall f:Utility_fun, FiniteStrat (<<f>>)
| Fin_sNode: forall (a:Agent) (c:Choice) (sl sr:StratProf),
     FiniteStrat sl -> FiniteStrat sr -> FiniteStrat (<<a,c,sl,sr>>).

CoInductive hasInfiniteHistory: StratProf -> Prop :=
| InfHistLeft: forall a sl sr, hasInfiniteHistory sl -> hasInfiniteHistory (<<a,l,sl,sr>>)
| InfHistRight: forall a sl sr, hasInfiniteHistory sr -> hasInfiniteHistory (<<a,r,sl,sr>>).

Lemma Finite_notInfinite: forall s, FiniteStrat s -> ~hasInfiniteHistory s.

Lemma hasInfiniteHistory_NotFinite: forall s, hasInfiniteHistory s -> ~FiniteStrat s.
  • Bisimilarity
CoInductive sBisimilar: StratProf -> StratProf -> Prop :=
| bisim_sLeaf: forall f, sBisimilar (<<f>>) (<<f>>)
| bisim_sNode: forall a c sl sl' sr sr',
  sBisimilar sl sl' -> sBisimilar sr sr' -> sBisimilar (<<a,c,sl,sr>>) (<<a, c,sl',sr'>>).

The game of a strategy
  • From strategies to games
CoFixpoint s2g (s:StratProf) : Game :=
match s with
| <<f>> => gLeaf f
| <<a,_,sl,sr>> => (gNode a (s2g sl) (s2g sr))
end.

Lemma s2g_decomp: forall a c sl sr,
    s2g (<<a, c, sl, sr>>) = gNode a (s2g sl) (s2g sr).
  • Strategies with bisimilar associated games
CoInductive BisGame: StratProf -> StratProf -> Prop :=
| BGLeaf: forall f, BisGame (<<f>>) (<<f>>)
| BGNode: forall (a:Agent)(c c':Choice)(sl sr sl' sr':StratProf),
  BisGame sl sl' -> BisGame sr sr' -> BisGame (sNode a c sl sr) (sNode a c' sl' sr').

Notation "s =sbisg= s'":= (BisGame s s') (at level 70).

Lemma BisGame_refl: forall s, s=sbisg=s.

Lemma BisGame_then_Biss2g: forall s s':StratProf, s =sbisg= s' -> (s2g s) =gbis= (s2g s').

Lemma Biss2g_then_Bisgame: forall s s':StratProf, (s2g s) =gbis= (s2g s') -> s =sbisg= s'.

Lemma Biss2g_is_Bisgame: forall s s':StratProf, (s2g s) =gbis= (s2g s') <-> s =sbisg= s'.

Utilities, histories, and strategies

CoInductive s2u : StratProf -> Agent -> Utility -> Prop :=
| s2uLeaf: forall a f, s2u (<<f>>) a (f a)
| s2uLeft: forall (a a':Agent) (u:Utility) (sl sr:StratProf),
    s2u sl a u -> s2u (<<a',l,sl,sr>>) a u
| s2uRight: forall (a a':Agent) (u:Utility) (sl sr:StratProf),
    s2u sr a u -> s2u (<<a',r,sl,sr>>) a u.

Lemma s2uLeft_rev : forall (a a':Agent) (u:Utility) (sl: StratProf) (sr:StratProf),
  s2u (<<a',l,sl,sr>>) a u -> s2u sl a u.

Lemma s2uRight_rev : forall (a a':Agent) (u:Utility) (sl sr: StratProf),
  s2u (<<a',r,sl,sr>>) a u -> s2u sr a u.
  • The history of a strategy
CoFixpoint s2h (s:StratProf): History:=
match s with
| <<f>> => HNil
| <<a,l,sl,sr>> => HCons l (s2h sl)
| <<a,r,sl,sr>> => HCons r (s2h sr)
end.

Lemma s2h_and_g: forall (s:StratProf),(s2h s) !s_history_of (s2g s).

Leads to Leaf and Always Leads to Leaf

  • Leads to a Leaf

Inductive LeadsToLeaf: StratProf -> Prop :=
| LtLLeaf: forall f, LeadsToLeaf (<<f>>)
| LtLLeft: forall (a:Agent)(sl: StratProf) (sr:StratProf),
    LeadsToLeaf sl -> LeadsToLeaf (<<a,l,sl,sr>>)
| LtLRight: forall (a:Agent)(sl: StratProf) (sr:StratProf),
     LeadsToLeaf sr -> LeadsToLeaf (<<a,r,sl,sr>>).
  • Existence and uniqueness of the utility of a strategy
Lemma Existence_s2u: forall (a:Agent) (s:StratProf),
  LeadsToLeaf s -> exists u:Utility, s2u s a u.

Lemma Uniqueness_s2u: forall (a:Agent) (u v:Utility) (s:StratProf),
   LeadsToLeaf s -> s2u s a u -> s2u s a v -> u=v.
  • Leads Always to a Leaf

CoInductive AlwLeadsToLeaf: StratProf -> Prop :=
| ALtLeaf : forall (f:Utility_fun), AlwLeadsToLeaf (<<f>>)
| ALtL : forall (a:Agent)(c:Choice)(sl sr:StratProf),
    LeadsToLeaf (<<a,c,sl,sr>>) -> AlwLeadsToLeaf sl ->AlwLeadsToLeaf sr ->
    AlwLeadsToLeaf (<<a,c,sl,sr>>).

Lemma ALtL_then_LtL: forall (s: StratProf), AlwLeadsToLeaf s -> LeadsToLeaf s.

Lemma ALtLLeft: forall a c sl sr, AlwLeadsToLeaf (<<a,c,sl,sr>>) -> AlwLeadsToLeaf sl.

Lemma ALtLRight: forall a c sl sr, AlwLeadsToLeaf (<<a,c,sl,sr>>) -> AlwLeadsToLeaf sr.

Convertibilities

  • An inductive convertibility
Inductive IndAgentConv: Agent -> StratProf -> StratProf -> Prop :=
| ConvRefl: forall (a:Agent)(s: StratProf), IndAgentConv a s s
| ConvAgent : forall (a:Agent)(c c':Choice)(sl sl' sr sr':StratProf),
  (IndAgentConv a sl sl') -> (IndAgentConv a sr sr') ->
  IndAgentConv a (<<a,c,sl,sr>>) (<<a,c',sl',sr'>>)
| ConvChoice : forall (a a':Agent) (c: Choice) (sl sl' sr sr':StratProf),
  IndAgentConv a sl sl' -> (IndAgentConv a sr sr') ->
  IndAgentConv a (<<a',c,sl,sr>>) (<<a',c,sl',sr'>>).

Notation "sl |-- a --| sr" := (IndAgentConv a sl sr) (at level 70).
  • Some Lemmas
Lemma IndConvSameGame: forall a s s', s |--a--| s' -> s =sbisg= s'.

Lemma IndConvSym: forall a s s', s|--a--|s' -> s'|--a--|s.

Lemma IndConvSameHeadAgent:
forall (a a' a'':Agent)(c c':Choice)(sl sl' sr sr': StratProf),
  (<<a,c,sl,sr>>) |--a''--| (<<a',c',sl',sr'>>) -> a=a'.

Lemma IndConvLeaf: forall a f s, s|--a--|(<<f>>) -> s = <<f>>.

Lemma IndConvProjL: forall (a a' a'':Agent)(c c':Choice)(sl sl' sr sr':StratProf),
  (<<a,c,sl,sr>>)|--a''--|(<<a',c',sl',sr'>>) -> sl |--a''--| sl'.

Lemma IndConvProjR: forall (a a' a'':Agent)(c c':Choice)(sl sl' sr sr':StratProf),
  (<<a,c,sl,sr>>)|--a''--|(<<a',c',sl',sr'>>) -> sr |--a''--|sr'.

Lemma IndConvTrans: forall (a:Agent)(s s': StratProf),
  s|--a--|s' -> forall (s'': StratProf), s'|--a--| s'' -> s|--a--|s''.

Lemma AlwLeadsToLeaf_Preservation: forall (a:Agent)(s s':StratProf),
  AlwLeadsToLeaf s -> s|--a--|s' -> AlwLeadsToLeaf s'.
  • A coinductive convertibility
CoInductive CoIndAgentConv: Agent -> StratProf -> StratProf -> Prop :=
| ConvLeafCo: forall (a:Agent)(f:Utility_fun), CoIndAgentConv a (<<f>>) (<<f>>)
| ConvAgentCo : forall (a:Agent)(c c':Choice)(sl sl' sr sr':StratProf),
  (CoIndAgentConv a sl sl') -> (CoIndAgentConv a sr sr') ->
  CoIndAgentConv a (<<a,c,sl,sr>>) (<<a,c',sl',sr'>>)
| ConvChoiceCo : forall (a a':Agent) (c: Choice) (sl sl' sr sr':StratProf),
  CoIndAgentConv a sl sl' -> (CoIndAgentConv a sr sr') ->
  CoIndAgentConv a (<<a',c,sl,sr>>) (<<a',c,sl',sr'>>).

Notation "sl <<-- a -->> sr" := (CoIndAgentConv a sl sr) (at level 70).

Lemma CoIndConvRefl: forall a s, s <<--a-->> s.

Lemma IndConv_then_CoIndConv: forall a s s', s |--a--| s' -> s <<--a-->> s'.

Lemma CoIndConvSameGame': forall a s s', s <<--a-->> s' -> s =sbisg= s'.

Lemma CoIndConvSameGame: forall a s s', s <<--a-->> s' -> (s2g s) =gbis= (s2g s').

Equilibria

  • Nash equilibria for infinite games
Definition NashEq (s: StratProf): Prop :=
  forall a s' u u', s'|--a--|s ->
    LeadsToLeaf s' -> (s2u s' a u') ->
    LeadsToLeaf s -> (s2u s a u) ->
    (u' =< u).

Definition better (a: Agent) (s s' : StratProf): Prop :=
forall u u',
LeadsToLeaf s' -> (s2u s' a u') ->
LeadsToLeaf s -> (s2u s a u) ->
(u' =< u).
  • SubGame Perfect Equilibrium (SGPE) for infinite games
CoInductive SGPE: StratProf -> Prop :=
| SGPE_leaf: forall f:Utility_fun, SGPE (<<f>>)
| SGPE_left: forall (a:Agent)(u v: Utility) (sl sr: StratProf),
    AlwLeadsToLeaf (<<a,l,sl,sr>>) ->
    SGPE sl -> SGPE sr ->
    s2u sl a u -> s2u sr a v -> (v =< u) ->
    SGPE (<<a,l,sl,sr>>)
| SGPE_right: forall (a:Agent) (u v:Utility) (sl sr: StratProf),
    AlwLeadsToLeaf (<<a,r,sl,sr>>) ->
    SGPE sl -> SGPE sr ->
    s2u sl a u -> s2u sr a v -> (u =< v) ->
    SGPE (<<a,r,sl,sr>>).

Lemma SGPE_then_AlwLeadsToLeaf: forall s:StratProf, SGPE s -> AlwLeadsToLeaf s.

Lemma SGPE_then_LtL : forall (s : StratProf), SGPE s -> LeadsToLeaf s.

Lemma SGPE_rev_Left: forall (a:Agent) (c:Choice) (sl sr: StratProf),
     SGPE (<<a,c,sl,sr>>) -> SGPE sl.

Lemma SGPE_rev_Right: forall (a:Agent) (c:Choice) (sl sr: StratProf),
     SGPE (<<a,c,sl,sr>>) -> SGPE sr.

Lemma SGPE_then_SubStrat_SGPE: forall (a:Agent) (c:Choice) (sl sr: StratProf),
     SGPE (<<a,c,sl,sr>>) -> SGPE sl /\ SGPE sr.

Lemma SGPE_implies_Better: forall (s s': StratProf) (a: Agent), s |-- a --| s' -> SGPE s -> better a s s'.

Theorem SGPE_Implies_NashEq: forall (s: StratProf), SGPE s -> NashEq s.

End InfiniteExtensiveGames.
Index
This page has been generated by coqdoc