(********************************************************************************) (* infinite_extensive_games.v *) (* *) (** © Pierre Lescanne *) (* *) (* LIP (ENS-Lyon, CNRS, INRIA) *) (* *) (* © Matthieu Perrinel (SGPE => Nash 06/09) *) (* *) (** 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. Proof. intros h; case h; trivial. Qed. (* notation *) 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'. Proof. intros. inversion H. trivial. Qed. Lemma Game_Right: forall a a' gl gl' gr gr', gNode a gl gr = gNode a' gl' gr' -> gr = gr'. Proof. intros. inversion H. trivial. Qed. 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. Proof. intros g; case g; trivial. Qed. (** - 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 *) Notation "g =gbis= g'" := (gBisimilar g g') (at level 80). Lemma gBis_refl: forall g, g =gbis= g. Proof. cofix H_bref. intros g. case g. apply bisim_gLeaf. intros. apply bisim_gNode; apply H_bref. Qed. Lemma gBis_sym: forall g g', g =gbis= g' -> g' =gbis= g. Proof. cofix H_bref. intros g g'. case g. case g'. intros; inversion H. apply bisim_gLeaf. intros. inversion H. intros. inversion H. apply bisim_gNode; apply H_bref; assumption. Qed. (** - 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 *) 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 *) 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'. Proof. intros. inversion H. trivial. Qed. Lemma StratProf_Left: forall a a' c c' sl sl' sr sr', (<> = <>) -> sl = sl'. Proof. intros. inversion H. trivial. Qed. Lemma StratProf_Right: forall a a' c c' sl sl' sr sr', (<> = <>) -> sr = sr'. Proof. intros. inversion H. trivial. Qed. Definition StratProf_identity (s:StratProf): StratProf := match s with | <> => <> | <> => <> end. Lemma StratProf_decomposition: forall s: StratProf, StratProf_identity s = s. Proof. intros s; case s; trivial. Qed. (** - Finiteness *) Inductive FiniteStrat: StratProf -> Prop := | Fin_sLeaf: forall f:Utility_fun, FiniteStrat (<>) | Fin_sNode: forall (a:Agent) (c:Choice) (sl sr:StratProf), FiniteStrat sl -> FiniteStrat sr -> FiniteStrat (<>). CoInductive hasInfiniteHistory: StratProf -> Prop := | InfHistLeft: forall a sl sr, hasInfiniteHistory sl -> hasInfiniteHistory (<>) | InfHistRight: forall a sl sr, hasInfiniteHistory sr -> hasInfiniteHistory (<>). Lemma Finite_notInfinite: forall s, FiniteStrat s -> ~hasInfiniteHistory s. Proof. intros. elim H. unfold not. intros. inversion H0. intros. destruct c. unfold not. intros. inversion H4. apply H1. assumption. unfold not. intros. inversion H4. apply H3. assumption. Qed. Lemma hasInfiniteHistory_NotFinite: forall s, hasInfiniteHistory s -> ~FiniteStrat s. Proof. unfold not. intros s HInf HFin. generalize HInf. apply Finite_notInfinite. assumption. Qed. (** - Bisimilarity *) CoInductive sBisimilar: StratProf -> StratProf -> Prop := | bisim_sLeaf: forall f, sBisimilar (<>) (<>) | bisim_sNode: forall a c sl sl' sr sr', sBisimilar sl sl' -> sBisimilar sr sr' -> sBisimilar (<>) (<>). (** ** The game of a strategy *) (** - From strategies to games *) CoFixpoint s2g (s:StratProf) : Game := match s with | <> => gLeaf f | <> => (gNode a (s2g sl) (s2g sr)) end. Lemma s2g_decomp: forall a c sl sr, s2g (<>) = gNode a (s2g sl) (s2g sr). Proof. intros. replace (s2g (<< a, c, sl, sr >>)) with (Game_identity (s2g (<< a, c, sl, sr >>))). simpl. trivial. apply Game_decomposition. Qed. (** - Strategies with bisimilar associated games *) CoInductive BisGame: StratProf -> StratProf -> Prop := | BGLeaf: forall f, BisGame (<>) (<>) | 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 *) Notation "s =sbisg= s'":= (BisGame s s') (at level 70). Lemma BisGame_refl: forall s, s=sbisg=s. Proof. cofix H. intros. case s. intros. apply BGLeaf. intros. apply BGNode; apply H. Qed. Lemma BisGame_then_Biss2g: forall s s':StratProf, s =sbisg= s' -> (s2g s) =gbis= (s2g s'). Proof. cofix H. intros. replace (s2g s) with (Game_identity (s2g s)). replace (s2g s') with (Game_identity (s2g s')). destruct s. destruct s'. simpl. replace u with u0. apply bisim_gLeaf. inversion H0; trivial. inversion H0. destruct s'. inversion H0. simpl. replace a0 with a. apply bisim_gNode. apply H; inversion H0; assumption. apply H; inversion H0; assumption. inversion H0. trivial. apply Game_decomposition. apply Game_decomposition. Qed. Lemma Biss2g_then_Bisgame: forall s s':StratProf, (s2g s) =gbis= (s2g s') -> s =sbisg= s'. Proof. cofix H. intros s s'. replace (s2g s) with (Game_identity (s2g s)). replace (s2g s') with (Game_identity (s2g s')). simpl. intro H_gBis. destruct s. destruct s'. replace u with u0. apply BGLeaf. inversion H_gBis. trivial. inversion H_gBis. destruct s'. inversion H_gBis. replace a0 with a. apply BGNode. apply H. inversion H_gBis. assumption. apply H. inversion H_gBis. assumption. inversion H_gBis. trivial. apply Game_decomposition. apply Game_decomposition. Qed. Lemma Biss2g_is_Bisgame: forall s s':StratProf, (s2g s) =gbis= (s2g s') <-> s =sbisg= s'. Proof. split. apply Biss2g_then_Bisgame. apply BisGame_then_Biss2g. Qed. (** ** Utilities, histories, and strategies *) CoInductive s2u : StratProf -> Agent -> Utility -> Prop := | s2uLeaf: forall a f, s2u (<>) a (f a) | s2uLeft: forall (a a':Agent) (u:Utility) (sl sr:StratProf), s2u sl a u -> s2u (<>) a u | s2uRight: forall (a a':Agent) (u:Utility) (sl sr:StratProf), s2u sr a u -> s2u (<>) a u. Lemma s2uLeft_rev : forall (a a':Agent) (u:Utility) (sl: StratProf) (sr:StratProf), s2u (<>) a u -> s2u sl a u. Proof. intros a a' u sl sr H. inversion H. assumption. Qed. Lemma s2uRight_rev : forall (a a':Agent) (u:Utility) (sl sr: StratProf), s2u (<>) a u -> s2u sr a u. Proof. intros a a' u sl sr H. inversion H. assumption. Qed. (** - The history of a strategy *) CoFixpoint s2h (s:StratProf): History:= match s with | <> => HNil | <> => HCons l (s2h sl) | <> => HCons r (s2h sr) end. Lemma s2h_and_g: forall (s:StratProf),(s2h s) !s_history_of (s2g s). Proof. cofix H. intros. replace (s2g s) with (Game_identity (s2g s)). replace (s2h s) with (History_identity (s2h s)). destruct s. simpl. apply hist_Leaf. case c. simpl. apply hist_NodeLeft. apply H. simpl. apply hist_NodeRight. apply H. apply History_decomposition. apply Game_decomposition. Qed. (* --------------------------------------- *) (** * Leads to Leaf and Always Leads to Leaf *) (* --------------------------------------- *) (** - Leads to a Leaf *) Inductive LeadsToLeaf: StratProf -> Prop := | LtLLeaf: forall f, LeadsToLeaf (<>) | LtLLeft: forall (a:Agent)(sl: StratProf) (sr:StratProf), LeadsToLeaf sl -> LeadsToLeaf (<>) | LtLRight: forall (a:Agent)(sl: StratProf) (sr:StratProf), LeadsToLeaf sr -> LeadsToLeaf (<>). (** - 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. Proof. intros a s. induction 1. exists (f a). apply s2uLeaf. elim IHLeadsToLeaf. intros u Hs2u. exists u. apply s2uLeft with (a:=a)(a':=a0)(sl:=sl)(sr:=sr). assumption. elim IHLeadsToLeaf. intros u Hs2u. exists u. apply s2uRight with (a:=a)(a':=a0)(sl:=sl)(sr:=sr). assumption. Qed. Lemma Uniqueness_s2u: forall (a:Agent) (u v:Utility) (s:StratProf), LeadsToLeaf s -> s2u s a u -> s2u s a v -> u=v. Proof. intros a u v s. induction 1. intros Hu Hv. inversion Hu. inversion Hv. trivial. intros; apply IHLeadsToLeaf; apply s2uLeft_rev with (a':=a0) (sr:=sr); trivial. intros. apply IHLeadsToLeaf. apply s2uRight_rev with (a':=a0) (sl:=sl); trivial. apply s2uRight_rev with (a':=a0) (sl:=sl); trivial. Qed. (** - Leads Always to a Leaf **) CoInductive AlwLeadsToLeaf: StratProf -> Prop := | ALtLeaf : forall (f:Utility_fun), AlwLeadsToLeaf (<>) | ALtL : forall (a:Agent)(c:Choice)(sl sr:StratProf), LeadsToLeaf (<>) -> AlwLeadsToLeaf sl ->AlwLeadsToLeaf sr -> AlwLeadsToLeaf (<>). Lemma ALtL_then_LtL: forall (s: StratProf), AlwLeadsToLeaf s -> LeadsToLeaf s. Proof. intros. inversion H. apply LtLLeaf. assumption. Qed. Lemma ALtLLeft: forall a c sl sr, AlwLeadsToLeaf (<>) -> AlwLeadsToLeaf sl. Proof. intros. inversion H. assumption. Qed. Lemma ALtLRight: forall a c sl sr, AlwLeadsToLeaf (<>) -> AlwLeadsToLeaf sr. Proof. intros. inversion H. assumption. Qed. (* ----------------- *) (** * 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 (<>) (<>) | ConvChoice : forall (a a':Agent) (c: Choice) (sl sl' sr sr':StratProf), IndAgentConv a sl sl' -> (IndAgentConv a sr sr') -> IndAgentConv a (<>) (<>). (* Notation *) 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'. Proof. intros. elim H. intros. apply BisGame_refl. intros. apply BGNode; assumption. intros. apply BGNode; assumption. Qed. Lemma IndConvSym: forall a s s', s|--a--|s' -> s'|--a--|s. Proof. intros a s s' H. elim H. apply ConvRefl. intros. apply ConvAgent. assumption. assumption. intros; apply ConvChoice. assumption. assumption. Qed. Lemma IndConvSameHeadAgent: forall (a a' a'':Agent)(c c':Choice)(sl sl' sr sr': StratProf), (<>) |--a''--| (<>) -> a=a'. Proof. intros. inversion H; trivial. Qed. Lemma IndConvLeaf: forall a f s, s|--a--|(<>) -> s = <>. Proof. intros. inversion H. trivial. Qed. Lemma IndConvProjL: forall (a a' a'':Agent)(c c':Choice)(sl sl' sr sr':StratProf), (<>)|--a''--|(<>) -> sl |--a''--| sl'. Proof. intros. inversion H. apply ConvRefl. assumption. assumption. Qed. Lemma IndConvProjR: forall (a a' a'':Agent)(c c':Choice)(sl sl' sr sr':StratProf), (<>)|--a''--|(<>) -> sr |--a''--|sr'. Proof. intros. inversion H. apply ConvRefl. assumption. assumption. Qed. Lemma IndConvTrans: forall (a:Agent)(s s': StratProf), s|--a--|s' -> forall (s'': StratProf), s'|--a--| s'' -> s|--a--|s''. Proof. induction 1. trivial. intros s''. case s''. intros. inversion H1. intros a' c0 sl'' sr'' Hyp. replace a' with a. apply ConvAgent. apply IHIndAgentConv1. apply IndConvProjL with (a:=a)(a':=a')(a'':=a)(c:=c')(c':=c0)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IHIndAgentConv2. apply IndConvProjR with (a:=a)(a':=a')(a'':=a)(c:=c')(c':=c0)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IndConvSameHeadAgent with (a'':=a)(c:=c')(c':=c0)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. intros s''. case s''. intros. inversion H1. intros a'' c'' sl'' sr'' Hyp. replace a'' with a'. generalize Hyp. case c. case c''. intros. apply ConvChoice. apply IHIndAgentConv1. apply IndConvProjL with (a:=a')(a':=a'')(a'':=a)(c:=l)(c':=l)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IHIndAgentConv2. apply IndConvProjR with (a:=a')(a':=a'')(a'':=a)(c:=l)(c':=l)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. intros. replace a' with a. apply ConvAgent. apply IHIndAgentConv1. apply IndConvProjL with (a:=a')(a':=a'')(a'':=a)(c:=c)(c':=c'')(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IHIndAgentConv2. apply IndConvProjR with (a:=a')(a':=a'')(a'':=a)(c:=c)(c':=c'')(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. inversion Hyp0; trivial. case c''. intros. replace a' with a. apply ConvAgent. apply IHIndAgentConv1. apply IndConvProjL with (a:=a')(a':=a'')(a'':=a)(c:=r)(c':=l)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IHIndAgentConv2. apply IndConvProjR with (a:=a')(a':=a'')(a'':=a)(c:=r)(c':=l)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. inversion Hyp0. trivial. intros. apply ConvChoice. apply IHIndAgentConv1. apply IndConvProjL with (a:=a')(a':=a'')(a'':=a)(c:=r)(c':=r)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IHIndAgentConv2. apply IndConvProjR with (a:=a')(a':=a'')(a'':=a)(c:=r)(c':=r)(sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. apply IndConvSameHeadAgent with (a'':=a) (c:=c) (c':=c'') (sl:=sl')(sr:=sr')(sl':=sl'')(sr':=sr''). assumption. Qed. Lemma AlwLeadsToLeaf_Preservation: forall (a:Agent)(s s':StratProf), AlwLeadsToLeaf s -> s|--a--|s' -> AlwLeadsToLeaf s'. Proof. induction 2. (* Refl *) assumption. (* Agent *) apply ALtL. case c'. apply LtLLeft. apply ALtL_then_LtL. apply IHIndAgentConv1. inversion H. apply ALtLLeft with (a:=a)(c:=c)(sl:=sl)(sr:=sr). assumption. apply LtLRight. apply ALtL_then_LtL. apply IHIndAgentConv2. inversion H. apply ALtLRight with (a:=a)(c:=c)(sl:=sl)(sr:=sr). assumption. apply IHIndAgentConv1. apply ALtLLeft with (a:=a)(c:=c)(sl:=sl)(sr:=sr). assumption. apply IHIndAgentConv2. apply ALtLRight with (a:=a)(c:=c)(sl:=sl)(sr:=sr). assumption. (* Choice *) apply ALtL. case c. apply LtLLeft. apply ALtL_then_LtL. apply IHIndAgentConv1. inversion H. apply ALtLLeft with (a:=a')(c:=c)(sl:=sl)(sr:=sr). assumption. apply LtLRight. apply ALtL_then_LtL. apply IHIndAgentConv2. inversion H. apply ALtLRight with (a:=a')(c:=c)(sl:=sl)(sr:=sr). assumption. apply IHIndAgentConv1. apply ALtLLeft with (a:=a')(c:=c)(sl:=sl)(sr:=sr). assumption. apply IHIndAgentConv2. apply ALtLRight with (a:=a')(c:=c)(sl:=sl)(sr:=sr). assumption. Qed. (** - A coinductive convertibility *) CoInductive CoIndAgentConv: Agent -> StratProf -> StratProf -> Prop := | ConvLeafCo: forall (a:Agent)(f:Utility_fun), CoIndAgentConv a (<>) (<>) | ConvAgentCo : forall (a:Agent)(c c':Choice)(sl sl' sr sr':StratProf), (CoIndAgentConv a sl sl') -> (CoIndAgentConv a sr sr') -> CoIndAgentConv a (<>) (<>) | ConvChoiceCo : forall (a a':Agent) (c: Choice) (sl sl' sr sr':StratProf), CoIndAgentConv a sl sl' -> (CoIndAgentConv a sr sr') -> CoIndAgentConv a (<>) (<>). (* Notation *) Notation "sl <<-- a -->> sr" := (CoIndAgentConv a sl sr) (at level 70). Lemma CoIndConvRefl: forall a s, s <<--a-->> s. Proof. cofix H. intros. case s. apply ConvLeafCo. intros. apply ConvChoiceCo. apply H. apply H. Qed. Lemma IndConv_then_CoIndConv: forall a s s', s |--a--| s' -> s <<--a-->> s'. Proof. induction 1; [apply CoIndConvRefl | apply ConvAgentCo | apply ConvChoiceCo]; assumption. Qed. Lemma CoIndConvSameGame': forall a s s', s <<--a-->> s' -> s =sbisg= s'. Proof. cofix H. intros. destruct s. destruct s'. inversion H0. apply BGLeaf. inversion H0. destruct s'. inversion H0. replace a0 with a1. apply BGNode. apply H with (a:=a). inversion H0; assumption. apply H with (a:=a). inversion H0; assumption. inversion H0; apply refl_equal. Qed. Lemma CoIndConvSameGame: forall a s s', s <<--a-->> s' -> (s2g s) =gbis= (s2g s'). Proof. intros. apply BisGame_then_Biss2g. apply CoIndConvSameGame' with (a:=a). assumption. Qed. (* ----------- *) (** * 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 (<>) | SGPE_left: forall (a:Agent)(u v: Utility) (sl sr: StratProf), AlwLeadsToLeaf (<>) -> SGPE sl -> SGPE sr -> s2u sl a u -> s2u sr a v -> (v =< u) -> SGPE (<>) | SGPE_right: forall (a:Agent) (u v:Utility) (sl sr: StratProf), AlwLeadsToLeaf (<>) -> SGPE sl -> SGPE sr -> s2u sl a u -> s2u sr a v -> (u =< v) -> SGPE (<>). Lemma SGPE_then_AlwLeadsToLeaf: forall s:StratProf, SGPE s -> AlwLeadsToLeaf s. Proof. intros. inversion H. apply ALtLeaf. assumption. assumption. Qed. Lemma SGPE_then_LtL : forall (s : StratProf), SGPE s -> LeadsToLeaf s. Proof. intros s SGPE_s. apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf. assumption. Qed. Lemma SGPE_rev_Left: forall (a:Agent) (c:Choice) (sl sr: StratProf), SGPE (<>) -> SGPE sl. Proof. intros; case c; inversion H; assumption. Qed. Lemma SGPE_rev_Right: forall (a:Agent) (c:Choice) (sl sr: StratProf), SGPE (<>) -> SGPE sr. Proof. intros; case c; inversion H; assumption. Qed. Lemma SGPE_then_SubStrat_SGPE: forall (a:Agent) (c:Choice) (sl sr: StratProf), SGPE (<>) -> SGPE sl /\ SGPE sr. Proof. intros. split. apply SGPE_rev_Left with (a:=a)(c:=c)(sr:=sr). assumption. apply SGPE_rev_Right with (a:=a)(c:=c)(sl:=sl). assumption. Qed. (* This theorem has been proved by Matthieu Perrinel *) Lemma SGPE_implies_Better: forall (s s': StratProf) (a: Agent), s |-- a --| s' -> SGPE s -> better a s s'. Proof. intros s s' a conv. induction conv. intro SGPE_s. unfold better. intros u u' ltl_s s2u_s' ltl_s' s2u_s. replace u with u'. apply (preord_refl Utility preference preference_is_preorder). apply Uniqueness_s2u with (a:=a)(s:=s) (u:=u')(v:=u). apply ltl_s. apply s2u_s'. apply s2u_s. intros SGPE_s. cut (LeadsToLeaf sl). cut (LeadsToLeaf sl'). cut (LeadsToLeaf sr). cut (LeadsToLeaf sr'). intros ltl_sr' ltl_sr ltl_sl' ltl_sl. unfold better. intros u u' ltl_s' s2u_s' ltl_s s2u_s. cut (exists ul, s2u sl a ul). cut (exists ul', s2u sl' a ul'). cut (exists ur, s2u sr a ur). cut (exists ur', s2u sr' a ur'). intros s2u_sr' s2u_sr s2u_sl' s2u_sl. elim s2u_sr'. elim s2u_sr. elim s2u_sl'. elim s2u_sl. intros ul s2ul ul' s2ul' ur s2ur ur' s2ur'. cut (ul' =< ul). cut (ur' =< ur). intros ur'_inf_ur ul'_inf_ur. inversion SGPE_s. cut ( ul = u0). cut (ur = v). intros ur_equal_v ul_equal_u0. cut (u=ul). intros u_equal_ul. rewrite u_equal_ul. inversion s2u_s'. cut (u' = ul'). intros u'_equal_ul'. rewrite u'_equal_ul'. exact ul'_inf_ur. eapply Uniqueness_s2u. apply ltl_sl'. apply H15. apply s2ul'. cut (ur' = u'). intro ur'_equal_u'. rewrite<-ur'_equal_u'. cut (ur =< ul). intro ur_inf_ul. inversion preference_is_preorder. apply preord_trans with ur. apply ur'_inf_ur. apply ur_inf_ul. rewrite ur_equal_v. rewrite ul_equal_u0. exact H8. eapply Uniqueness_s2u. apply ltl_sr'. apply s2ur'. apply H15. eapply Uniqueness_s2u. apply ltl_sl. eapply s2uLeft_rev. rewrite H0. apply s2u_s. apply s2ul. eapply Uniqueness_s2u. eapply ALtL_then_LtL. eapply ALtLRight. apply H3. apply s2ur. apply H7. eapply Uniqueness_s2u. apply ltl_sl. apply s2ul. apply H6. (* If c = r *) inversion SGPE_s. (*If c = l, is impossible*) cut False. intro false. intuition. cut (l=r). intro l_equal_r. inversion l_equal_r. rewrite H10. rewrite H0. reflexivity. cut (u=ur). intros u_equal_ul. rewrite u_equal_ul. inversion s2u_s'. cut (u' = ul'). intros u'_equal_ul'. rewrite u'_equal_ul'. inversion preference_is_preorder. apply preord_trans with ul. exact ul'_inf_ur. cut (ul = u0). cut (ur = v). intros ur_equal_v ul_equal_u0. rewrite ur_equal_v. rewrite ul_equal_u0. exact H8. eapply Uniqueness_s2u. apply ltl_sr. apply s2ur. apply H7. eapply Uniqueness_s2u. apply ltl_sl. apply s2ul. apply H6. eapply Uniqueness_s2u. apply ltl_sl'. apply H25. apply s2ul'. cut (u'= ur'). intro u'_equal_ur'. rewrite u'_equal_ur'. apply ur'_inf_ur. eapply Uniqueness_s2u. apply ltl_sr'. apply H25. apply s2ur'. eapply Uniqueness_s2u. apply ltl_sr. eapply s2uRight_rev. rewrite H10. apply s2u_s. apply s2ur. cut (better a sr sr'). unfold better. intros unfolded_better. apply unfolded_better. apply ltl_sr'. apply s2ur'. apply ltl_sr. apply s2ur. apply IHconv2. eapply SGPE_rev_Right with (a:=a)(c:=c)(sr:=sr). apply SGPE_s. cut (better a sl sl'). unfold better. intros unfolded_better. apply unfolded_better. apply ltl_sl'. apply s2ul'. apply ltl_sl. apply s2ul. apply IHconv1. eapply SGPE_rev_Left with (a:=a)(c:=c)(sl:=sl). apply SGPE_s. apply Existence_s2u. apply ltl_sr'. apply Existence_s2u. apply ltl_sr. apply Existence_s2u. apply ltl_sl'. apply Existence_s2u. apply ltl_sl. apply ALtL_then_LtL. eapply AlwLeadsToLeaf_Preservation. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Right. apply SGPE_s. apply conv2. apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Right. apply SGPE_s. apply ALtL_then_LtL. eapply AlwLeadsToLeaf_Preservation. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Left. apply SGPE_s. apply conv1. apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Left. apply SGPE_s. intros SGPE_s. cut (LeadsToLeaf sl). cut (LeadsToLeaf sl'). cut (LeadsToLeaf sr). cut (LeadsToLeaf sr'). intros ltl_sr' ltl_sr ltl_sl' ltl_sl. unfold better. intros u u' ltl_s' s2u_s' ltl_s s2u_s. cut (exists ul, s2u sl a ul). cut (exists ul', s2u sl' a ul'). cut (exists ur, s2u sr a ur). cut (exists ur', s2u sr' a ur'). intros s2u_sr' s2u_sr s2u_sl' s2u_sl. elim s2u_sr'. elim s2u_sr. elim s2u_sl'. elim s2u_sl. intros ul s2ul ul' s2ul' ur s2ur ur' s2ur'. induction c. cut (u'= ul'). cut (u=ul). intros u_equal_ul u'_equal_ul'. rewrite u_equal_ul. rewrite u'_equal_ul'. cut (better a sl sl'). unfold better. intros better_sl_sl'. apply better_sl_sl'. apply ltl_sl'. apply s2ul'. apply ltl_sl. apply s2ul. apply IHconv1. eapply SGPE_rev_Left. apply SGPE_s. eapply Uniqueness_s2u. apply ltl_sl. eapply s2uLeft_rev. apply s2u_s. apply s2ul. eapply Uniqueness_s2u. apply ltl_sl'. eapply s2uLeft_rev. apply s2u_s'. apply s2ul'. cut (u'= ur'). cut (u=ur). intros u_equal_ur u'_equal_ur'. rewrite u_equal_ur. rewrite u'_equal_ur'. cut (better a sr sr'). unfold better. intros better_sr_sr'. apply better_sr_sr'. apply ltl_sr'. apply s2ur'. apply ltl_sr. apply s2ur. apply IHconv2. eapply SGPE_rev_Right. apply SGPE_s. eapply Uniqueness_s2u. apply ltl_sr. eapply s2uRight_rev. apply s2u_s. apply s2ur. eapply Uniqueness_s2u. apply ltl_sr'. eapply s2uRight_rev. apply s2u_s'. apply s2ur'. apply Existence_s2u. apply ltl_sr'. apply Existence_s2u. apply ltl_sr. apply Existence_s2u. apply ltl_sl'. apply Existence_s2u. apply ltl_sl. apply ALtL_then_LtL. eapply AlwLeadsToLeaf_Preservation. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Right. apply SGPE_s. apply conv2. apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Right. apply SGPE_s. apply ALtL_then_LtL. eapply AlwLeadsToLeaf_Preservation. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Left. apply SGPE_s. apply conv1. apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf. eapply SGPE_rev_Left. apply SGPE_s. Qed. Theorem SGPE_Implies_NashEq: forall (s: StratProf), SGPE s -> NashEq s. Proof. intros s SGPE_s. unfold NashEq. intros a s' u u' conv ltl_s' s2u_s' ltl_s s2u_s. cut (better a s s'). unfold better. intro better_s_s'. apply better_s_s'. assumption. assumption. assumption. assumption. apply SGPE_implies_Better. apply IndConvSym. assumption. assumption. Qed. End InfiniteExtensiveGames.