(* Time-stamp: "modifie le 6 Sep 2009 a 19:23 par Pierre Lescanne sur boucherotte" *) (* ~/Documents/COQ/GAMES/EXTENSIVE/dollar_auction.v *) (********************************************************************************) (* dollar_auction.v *) (* *) (** © Pierre Lescanne (February 2008) *) (* *) (* LIP (ENS-Lyon, CNRS, INRIA) *) (* *) (* *) (** Developed in V8.1 June-August 2009 *) (********************************************************************************) (* --------------- *) (** * Preliminaries *) (* --------------- *) Set Implicit Arguments. Require Import Relations. Require Import Arith. Require Import Omega. (* begin hide *) Add LoadPath ".". (* end hide *) Require Import infinite_extensive_games. Require Import Le. Implicit Arguments sLeaf [Agent Utility]. Implicit Arguments sNode [Agent Utility]. Implicit Arguments s2u [Agent Utility]. Implicit Arguments LeadsToLeaf [Agent Utility]. Implicit Arguments AlwLeadsToLeaf [Agent Utility]. Implicit Arguments SGPE [Agent Utility]. Implicit Arguments NashEq [Agent Utility]. (* ----------------- *) (** - Data and tools *) (* ----------------- *) Inductive Alice_Bob :Set := Alice :Alice_Bob | Bob: Alice_Bob. Definition Strat := StratProf Alice_Bob nat. Notation "s1 |-- a --| s2" := (IndAgentConv Alice_Bob nat a s1 s2) (at level 70). Notation "<< a , c , sl , sr >>" := (sNode a c sl sr) (at level 80). Notation "[ x , y ]" := (sLeaf (fun a:Alice_Bob => match a with Alice => x | Bob => y end)) (at level 80). (* A cA ---- B cB------- s | | | | add_Alice_Bob_esc(cA,cB,n,s) = | | | | | | 2n+1 2n+1 2*n 2n+2 *) (* ===================== *) (** * Illogic escalation *) (* ===================== *) (* --------------------------- *) (** ** StratProf "Never Give Up" *) (* --------------------------- *) (* A +++++++ B ++++++++ ngu n+1 | | | | ngu n = | | | | | | 2n+1 2n+1 2*n 2n+2 A +++++++ B ++++++++ A +++++++ B +++++++ A ++++++++ B +++... | | | | | | | | | | | | = | | | | | | ... | | | | | | | | | | | | 2n+1 2n+1 2n+3 2n+3 2n+5 2n+5 2*n 2n+2 2n+2 2n+4 2n+4 2n+6 *) Definition add_Alice_Bob_esc (cA cB:Choice) (n:nat) (s:Strat) := <>,[2*n+1,2*n]>>. CoFixpoint ngu (n:nat): (Strat) := add_Alice_Bob_esc l l n (ngu (S n)). Lemma ngu_decomposition: forall n:nat, (ngu n) = <>,[2*n+1,2*n]>>. Proof. intros. replace (ngu n) with (StratProf_identity Alice_Bob nat (ngu n)). simpl. trivial. apply StratProf_decomposition. Qed. CoInductive NeverLeaf: Strat -> Prop := | NvLLeft: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf sl -> NeverLeaf (<>) | NvLRight: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf sr -> NeverLeaf (<>). Lemma NLLeft: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf (<>) -> NeverLeaf sl. Proof. intros. inversion H. assumption. Qed. Lemma NLRight: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf (<>) -> NeverLeaf sr. Proof. intros. inversion H. assumption. Qed. Lemma NeverLeaf_then_not_LeadsToLeaf: forall s: Strat, NeverLeaf s -> ~LeadsToLeaf s. Proof. unfold not. intros s H_NL. induction 1. inversion H_NL. apply IHLeadsToLeaf. apply NLLeft with (a:=a) (sr:=sr). assumption. apply IHLeadsToLeaf. apply NLRight with (a:=a) (sl:=sl). assumption. Qed. Lemma NeverLeaf_ngu: forall (n:nat), NeverLeaf (ngu n). Proof. cofix H. intros. rewrite ngu_decomposition. apply NvLLeft. apply NvLLeft. apply H. Qed. Lemma Not_LeadsToLeaf_ngu: forall (n:nat), ~LeadsToLeaf (ngu n). Proof. intros. apply NeverLeaf_then_not_LeadsToLeaf. apply NeverLeaf_ngu. Qed. Lemma NotSGPE_NGU: forall (n:nat), ~SGPE ge (ngu n). Proof. unfold not. intros. elim Not_LeadsToLeaf_ngu with (n:=n). apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf with (preference:=ge). assumption. Qed. Lemma Nasheq_NGU: forall (n:nat), NashEq ge (ngu n). Proof. unfold NashEq. intros. cut False. intuition. generalize H2. apply Not_LeadsToLeaf_ngu. Qed. (* ---------------------------- *) (** ** StratProf "Always Give Up" *) (* ---------------------------- *) (* A ------- B -------- ngu n+1 + + + + ngu n = + + + + + + 2n+1 2n+1 2*n 2n+2 A ------- B -------- A ------- B ------- A -------- B ---... + + + + + + + + + + + + = + + + + + + ... + + + + + + + + + + + + 2n+1 2n+1 2n+3 2n+3 2n+5 2n+5 2*n 2n+2 2n+2 2n+4 2n+4 2n+6 *) (* --------------------------- *) (** - StratProf "always give up" *) (* --------------------------- *) CoFixpoint agu (n:nat):(Strat) := add_Alice_Bob_esc r r n (agu (S n)). (* -------------------- *) (** - Preliminary lemmas *) (* -------------------- *) Lemma AlwLeadsToLeaf_agu: forall (n:nat), AlwLeadsToLeaf (agu n). Proof. cofix H. intros. replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma LeadsToLeaf_agu: forall (n:nat), LeadsToLeaf (agu n). Proof. intros. apply ALtL_then_LtL. apply AlwLeadsToLeaf_agu. Qed. Lemma S2u_agu_Alice: forall (n:nat), s2u (agu n) Alice (2*n+1). Proof. intros; replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_agu_Bob: forall (n:nat), s2u (agu n) Bob (2*n). Proof. intros; replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. (* ---------------------------------------------------------- *) (** - StratProf Always Give Up is a Subgame Perfect Equilibrium *) (* ---------------------------------------------------------- *) Theorem SGPEAGU: forall (n:nat), SGPE ge (agu n). Proof. cofix H. intros n. replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply SGPE_right with (u:= 2*n+1) (v:=2*n+1). apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_agu. apply ALtLeaf. apply ALtLeaf. apply SGPE_right with (u:= 2*n+2) (v:=2*n+2). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_agu. apply ALtLeaf. apply H. apply SGPE_leaf. replace (2*n+2) with (2*(S n)). apply S2u_agu_Bob. auto. replace (2*n+2) with (n+(n+0)+2). apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end). auto. auto. apply SGPE_leaf. apply s2uRight. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end). apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end). auto. rewrite <- StratProf_decomposition; trivial. Qed. (* ------------------------------------------------------------ *) (** ** StratProf "Alice always gives up and Bob always continues" *) (* ------------------------------------------------------------ *) CoFixpoint agubc (n:nat):(Strat) := add_Alice_Bob_esc r l n (agubc (S n)). Lemma AlwLeadsToLeaf_agubc: forall (n:nat), AlwLeadsToLeaf (agubc n). Proof. cofix H. intros. replace (agubc n) with (StratProf_identity Alice_Bob nat (agubc n)). simpl. apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLLeft. replace (agubc (S n)) with (StratProf_identity Alice_Bob nat (agubc (S n))). simpl. apply LtLRight. apply LtLLeaf. rewrite <- StratProf_decomposition; trivial. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_agubc_Alice: forall (n:nat), s2u (agubc n) Alice (2*n+1). Proof. intros; replace (agubc n) with (StratProf_identity Alice_Bob nat (agubc n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_agubc_Bob: forall (n:nat), s2u (agubc n) Bob (2*n). Proof. intros; replace (agubc n) with (StratProf_identity Alice_Bob nat (agubc n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. Theorem SGPEAGUBC: forall (n:nat), SGPE ge (agubc n). Proof. cofix H. intros n. replace (agubc n) with (StratProf_identity Alice_Bob nat (agubc n)). simpl. apply SGPE_right with (u:= 2*n+3) (v:=2*n+1). replace (<< Alice, r, << Bob, l, agubc (S n), sLeaf (fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end) >>, sLeaf (fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end) >>) with (agubc n). apply AlwLeadsToLeaf_agubc. replace (agubc n) with (StratProf_identity Alice_Bob nat (agubc n)). simpl. trivial. rewrite <- StratProf_decomposition; trivial. apply SGPE_left with (u:= 2*n+2) (v:=2*n+2). apply ALtL. apply LtLLeft. replace (agubc (S n)) with (StratProf_identity Alice_Bob nat (agubc (S n))). simpl. apply LtLRight. apply LtLLeaf. rewrite <- StratProf_decomposition; trivial. apply AlwLeadsToLeaf_agubc. apply ALtLeaf. apply H. apply SGPE_leaf. replace (2*n+2) with (2*(S n)). apply S2u_agubc_Bob. auto. replace (2*n+2) with (n+(n+0)+2). apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end). auto. auto. apply SGPE_leaf. apply s2uLeft. replace (2*n+3) with (2 * (S n) + 1). apply S2u_agubc_Alice. omega. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end). omega. rewrite <- StratProf_decomposition; trivial. Qed. (* ----------------------------------------------------- *) (** ** StratProf "Alice continues and Bob gives up" *) (* ----------------------------------------------------- *) CoFixpoint acbgu (n:nat):(Strat) := add_Alice_Bob_esc l r n (acbgu (S n)). Lemma AlwLeadsToLeaf_acbgu: forall (n:nat), AlwLeadsToLeaf (acbgu n). Proof. cofix H. intros. replace (acbgu n) with (StratProf_identity Alice_Bob nat (acbgu n)). simpl. apply ALtL. apply LtLLeft. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_acbgu_Alice: forall (n:nat), s2u (acbgu n) Alice (2*n+1). Proof. intros; replace (acbgu n) with (StratProf_identity Alice_Bob nat (acbgu n)). simpl. apply s2uLeft. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_acbgu_Bob: forall (n:nat), s2u (acbgu n) Bob (2*n+2). Proof. intros; replace (acbgu n) with (StratProf_identity Alice_Bob nat (acbgu n)). simpl. apply s2uLeft. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. Theorem SGPEACBGU: forall (n:nat), SGPE ge (acbgu n). Proof. cofix H. intros n. replace (acbgu n) with (StratProf_identity Alice_Bob nat (acbgu n)). simpl. apply SGPE_left with (u:= 2*n+1) (v:=2*n+1). replace (<< Alice, l, << Bob, r, acbgu (S n), sLeaf (fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end) >>, sLeaf (fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end) >>) with (acbgu n). apply AlwLeadsToLeaf_acbgu. replace (acbgu n) with (StratProf_identity Alice_Bob nat (acbgu n)). simpl. trivial. rewrite <- StratProf_decomposition; trivial. apply SGPE_right with (u:= 2*n+4) (v:=2*n+2). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_acbgu. replace (acbgu (S n)) with (StratProf_identity Alice_Bob nat (acbgu (S n))). apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. apply H. apply SGPE_leaf. replace (2*n+4) with (2*(S n) + 2). apply S2u_acbgu_Bob. omega. apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end). omega. apply SGPE_leaf. apply s2uRight. replace (n + (n + 0) + 1) with (2 * n + 1). apply s2uLeaf with (a:=Alice)(f:=(fun a : Alice_Bob => match a with | Alice => 2 * n + 1 | Bob => n + (n + 0) + 2 end)). auto. replace (n + (n + 0) + 1) with (2 * n + 1). apply s2uLeaf with (a:=Alice)(f:=(fun a : Alice_Bob => match a with | Alice => 2 * n + 1 | Bob => n + (n + 0) end)). auto. auto. rewrite <- StratProf_decomposition; trivial. Qed. (* ===================== *) (** * Dollar auction *) (* ===================== *) Variable v:nat. Axiom v_pos: v > 0. (* This game is more realistically associated with the dollar auction game A ------- B -------- A ------- B ------- A -------- B ---... | | | | | | | | | | | | = | | | | | | ... | | | | | | | | | | | | v+n n+1 v+n+1 n+2 v+n+2 n+3 n v+n n+1 v+n+1 n+2 v+n+2 v is the value of the object. *) (* -------------------------------- *) (** ** Alice continues, Bob stops *) (* -------------------------------- *) Definition add_Alice_Bob_dol (cA cB:Choice) (n:nat) (s:Strat) := <>,[v+n,n]>>. CoFixpoint dolAcBs (n:nat): Strat := add_Alice_Bob_dol l r n (dolAcBs (n+1)). Lemma dolAcBs_decomposition: forall n:nat, (dolAcBs n) = <>,[v+n,n]>>. Proof. intros. replace (dolAcBs n) with (StratProf_identity Alice_Bob nat (dolAcBs n)). simpl. trivial. apply StratProf_decomposition. Qed. Lemma AlwLeadsToLeaf_dolAcBs: forall (n:nat), AlwLeadsToLeaf (dolAcBs n). Proof. cofix H. intros. replace (dolAcBs n) with (StratProf_identity Alice_Bob nat (dolAcBs n)). simpl. apply ALtL. apply LtLLeft. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma LeadsToLeaf_dolAcBs: forall (n:nat), LeadsToLeaf (dolAcBs n). Proof. intros. apply ALtL_then_LtL. apply AlwLeadsToLeaf_dolAcBs. Qed. Lemma S2u_dolAcBs_Alice: forall (n:nat), s2u (dolAcBs n) Alice (n+1). Proof. intros; replace (dolAcBs n) with (StratProf_identity Alice_Bob nat (dolAcBs n)). simpl. apply s2uLeft. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + 1 | Bob => v + n end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_dolAcBs_Bob: forall (n:nat), s2u (dolAcBs n) Bob (v+n). Proof. intros; replace (dolAcBs n) with (StratProf_identity Alice_Bob nat (dolAcBs n)). simpl. apply s2uLeft. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + 1 | Bob => v+n end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. Theorem SGPE_dol_Ac_Bs: forall (n:nat), SGPE ge (dolAcBs n). Proof. cofix H. intros n. replace (dolAcBs n) with (StratProf_identity Alice_Bob nat (dolAcBs n)). simpl. apply SGPE_left with (u:= n+1) (v:=v+n). apply ALtL. apply LtLLeft. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_dolAcBs. apply ALtLeaf. apply ALtLeaf. apply SGPE_right with (u:= v+(n+1)) (v:=v+n). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_dolAcBs. apply ALtLeaf. apply H. apply SGPE_leaf. apply S2u_dolAcBs_Bob. apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice => n+1 | Bob => v+n end). omega. apply SGPE_leaf. apply s2uRight. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + 1 | Bob => v+n end). apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => v + n | Bob => n end). cut (v>0). omega. apply v_pos. rewrite <- StratProf_decomposition; trivial. Qed. (* ------------------------------- *) (** ** Alice stops, Bob continues *) (* ------------------------------- *) CoFixpoint dolAsBc (n:nat): Strat := add_Alice_Bob_dol r l n (dolAsBc (n+1)). Lemma dolAsBc_decomposition: forall n:nat, (dolAsBc n) = <>,[v+n,n]>>. Proof. intros. replace (dolAsBc n) with (StratProf_identity Alice_Bob nat (dolAsBc n)). simpl. trivial. apply StratProf_decomposition. Qed. Lemma AlwLeadsToLeaf_dolAsBc: forall (n:nat), AlwLeadsToLeaf (dolAsBc n). Proof. cofix H. intros. replace (dolAsBc n) with (StratProf_identity Alice_Bob nat (dolAsBc n)). simpl. apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLLeft. replace (dolAsBc (n+1)) with (StratProf_identity Alice_Bob nat (dolAsBc (n+1))). simpl. apply LtLRight. apply LtLLeaf. rewrite <- StratProf_decomposition; trivial. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma LeadsToLeaf_dolAsBc: forall (n:nat), LeadsToLeaf (dolAsBc n). Proof. intros. apply ALtL_then_LtL. apply AlwLeadsToLeaf_dolAsBc. Qed. Lemma S2u_dolAsBc_Alice: forall (n:nat), s2u (dolAsBc n) Alice (v+n). Proof. intros; replace (dolAsBc n) with (StratProf_identity Alice_Bob nat (dolAsBc n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => v+n | Bob => n end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_dolAsBc_Bob: forall (n:nat), s2u (dolAsBc n) Bob n. Proof. intros; replace (dolAsBc n) with (StratProf_identity Alice_Bob nat (dolAsBc n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => v+n | Bob => n end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. Theorem SGPE_dol_As_Bc: forall (n:nat), SGPE ge (dolAsBc n). Proof. cofix H. intros n. replace (dolAsBc n) with (StratProf_identity Alice_Bob nat (dolAsBc n)). simpl. apply SGPE_right with (u:= v+(n+1)) (v:=v+n). apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLLeft. apply LeadsToLeaf_dolAsBc. apply AlwLeadsToLeaf_dolAsBc. apply ALtLeaf. apply ALtLeaf. apply SGPE_left with (u:= (n+1)) (v:=v+n). apply ALtL. apply LtLLeft. apply LeadsToLeaf_dolAsBc. apply AlwLeadsToLeaf_dolAsBc. apply ALtLeaf. apply H. apply SGPE_leaf. apply S2u_dolAsBc_Bob. apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice => n+1 | Bob => v+n end). cut (v>0). omega. apply v_pos. apply SGPE_leaf. apply s2uLeft. apply S2u_dolAsBc_Alice. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => v+n | Bob => n end). cut (v>0). omega. apply v_pos. rewrite <- StratProf_decomposition; trivial. Qed. (* ------------------------------- *) (** ** Alice stops, Bob stops *) (* ------------------------------- *) CoFixpoint dolAsBs (n:nat): Strat := add_Alice_Bob_dol r r n (dolAsBs (n+1)). Lemma dolAsBs_decomposition: forall n:nat, (dolAsBs n) = <>,[v+n,n]>>. Proof. intros. replace (dolAsBs n) with (StratProf_identity Alice_Bob nat (dolAsBs n)). simpl. trivial. apply StratProf_decomposition. Qed. Lemma AlwLeadsToLeaf_dolAsBs: forall (n:nat), AlwLeadsToLeaf (dolAsBs n). Proof. cofix H. intros. replace (dolAsBs n) with (StratProf_identity Alice_Bob nat (dolAsBs n)). simpl. apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma LeadsToLeaf_dolAsBs: forall (n:nat), LeadsToLeaf (dolAsBs n). Proof. intros. apply ALtL_then_LtL. apply AlwLeadsToLeaf_dolAsBs. Qed. Lemma S2u_dolAsBs_Alice: forall (n:nat), s2u (dolAsBs n) Alice (v+n). Proof. intros; replace (dolAsBs n) with (StratProf_identity Alice_Bob nat (dolAsBs n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => v+n | Bob => n end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_dolAsBs_Bob: forall (n:nat), s2u (dolAsBs n) Bob n. Proof. intros; replace (dolAsBs n) with (StratProf_identity Alice_Bob nat (dolAsBs n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => v+n | Bob => n end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. Definition dolAsBs_0' := add_Alice_Bob_dol l r 0 (dolAsBs 1). Lemma conv_dolAsBs: dolAsBs_0' |-- Alice --| dolAsBs 0. Proof. replace (dolAsBs 0) with (StratProf_identity Alice_Bob nat (dolAsBs 0)). unfold dolAsBs_0'. unfold add_Alice_Bob_dol. simpl. apply ConvAgent. apply ConvRefl. apply ConvRefl. rewrite <- StratProf_decomposition; trivial. Qed. Lemma LeadsToLeaf_dolAsBs_0':LeadsToLeaf dolAsBs_0'. Proof. unfold dolAsBs_0'. unfold add_Alice_Bob_dol. simpl. apply LtLLeft. apply LtLRight. apply LtLLeaf. Qed. Lemma S2u_dolAsBs_0'_Alice: s2u dolAsBs_0' Alice 1. Proof. intros. unfold dolAsBs_0'. unfold add_Alice_Bob_dol. apply s2uLeft. apply s2uRight. apply s2uLeaf with (f:= fun a : Alice_Bob => match a with | Alice => 0 + 1 | Bob => v + 0 end)(a:=Alice). Qed. Theorem NotSGPE_dolAsBs: (v>1) -> ~(NashEq ge (dolAsBs 0)). Proof. unfold not. unfold NashEq. intros. cut (1 >= v). omega. apply H0 with (a:=Alice)(s':=dolAsBs_0'). apply conv_dolAsBs. apply LeadsToLeaf_dolAsBs_0'. apply S2u_dolAsBs_0'_Alice. apply LeadsToLeaf_dolAsBs. replace v with (v+0). apply S2u_dolAsBs_Alice. auto. Qed. (* ---------------------------------- *) (** ** Alice continues, Bob continues *) (* ---------------------------------- *) CoFixpoint dolAcBc (n:nat): Strat := add_Alice_Bob_dol l l n (dolAcBc (n+1)). Lemma dolAcBc_decomposition: forall n:nat, (dolAcBc n) = <>,[v+n,n]>>. Proof. intros. replace (dolAcBc n) with (StratProf_identity Alice_Bob nat (dolAcBc n)). simpl. trivial. apply StratProf_decomposition. Qed. Lemma NeverLeaf_AcBc: forall (n:nat), NeverLeaf (dolAcBc n). Proof. cofix H. intros. rewrite dolAcBc_decomposition. apply NvLLeft. apply NvLLeft. apply H. Qed. Lemma Not_LeadsToLeaf_AcBc: forall (n:nat), ~LeadsToLeaf (dolAcBc n). Proof. intros. apply NeverLeaf_then_not_LeadsToLeaf. apply NeverLeaf_AcBc. Qed. Lemma NotSGPE_dolAcBc: forall (n:nat), ~SGPE ge (dolAcBc n). Proof. unfold not. intros. elim Not_LeadsToLeaf_AcBc with (n:=n). apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf with (preference:=ge). assumption. Qed. Lemma NashEq_dolAcBc: forall (n:nat), NashEq ge (dolAcBc n). Proof. unfold NashEq. intros. cut False. intuition. generalize H2. apply Not_LeadsToLeaf_AcBc. Qed.