| © Pierre Lescanne (February 2008) |
| Developed in V8.1 February 2008 --- January 2009 |
Preliminaries |
Set Implicit Arguments.
Require Import Relations.
Require Import Arith.
Require Import Omega.
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].
|
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).
Illogic escalation |
StratProf "Never Give Up" |
Definition add_Alice_Bob_esc (cA cB:Choice) (n:nat) (s:Strat) :=
<<Alice,cA,<<Bob, cB,s,[2*n+1, 2*n+2]>>,[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) = <<Alice,l,<<Bob, l, (ngu (S n)),[2*n+1, 2*n+2]>>,[2*n+1,2*n]>>.
CoInductive NeverLeaf: Strat -> Prop :=
| NvLLeft: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf sl -> NeverLeaf (<<a,l,sl,sr>>)
| NvLRight: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf sr -> NeverLeaf (<<a,r,sl,sr>>).
Lemma NLLeft: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf (<<a,l,sl,sr>>) -> NeverLeaf sl.
Lemma NLRight: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf (<<a,r,sl,sr>>) -> NeverLeaf sr.
Lemma NeverLeaf_then_not_LeadsToLeaf: forall s: Strat,
NeverLeaf s -> ~LeadsToLeaf s.
Lemma NeverLeaf_ngu: forall (n:nat), NeverLeaf (ngu n).
Lemma Not_LeadsToLeaf_ngu: forall (n:nat), ~LeadsToLeaf (ngu n).
Lemma NotSGPE_NGU: forall (n:nat), ~SGPE ge (ngu n).
Lemma Nasheq_NGU: forall (n:nat), NashEq Alice_Bob nat ge (ngu n).
StratProf "Always Give Up" |
|
CoFixpoint agu (n:nat):(Strat) := add_Alice_Bob_esc r r n (agu (S n)).
|
Lemma AlwLeadsToLeaf_agu: forall (n:nat), AlwLeadsToLeaf (agu n).
Lemma LeadsToLeaf_agu: forall (n:nat), LeadsToLeaf (agu n).
Lemma S2u_agu_Alice: forall (n:nat), s2u (agu n) Alice (2*n+1).
Lemma S2u_agu_Bob: forall (n:nat), s2u (agu n) Bob (2*n).
|
Theorem SGPEAGU: forall (n:nat), SGPE ge (agu n).
|
Lemma conv_agu_s2u_Alice: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat),
s|--a--| (agu n) -> s2u s Alice u -> u=2*n+1.
Lemma conv_agu_s2u_Bob: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat),
s|--a--| (agu n) -> s2u s Bob u -> u=2*n \/ u=2*n+2.
Lemma NashEq_agu: forall (n:nat), NashEq Alice_Bob nat ge (agu n).
Centiped |
Definition add_Alice_Bob_cent (cA cB:Choice) (n:nat) (s:Strat) :=
<<Alice,cA,<<Bob, cB,s,[2*n-1, 2*n+3]>>,[2*n,2*n]>>.
|
CoFixpoint cent_ngu (n:nat): (Strat) := add_Alice_Bob_cent l l n (cent_ngu (S n)).
Lemma cent_ngu_decomposition: forall n:nat,
(cent_ngu n) = <<Alice,l,<<Bob, l, (cent_ngu (S n)),[2*n-1, 2*n+3]>>,[2*n,2*n]>>.
Lemma NeverLeaf_cent_ngu: forall (n:nat), NeverLeaf (cent_ngu n).
Lemma Not_LeadsToLeaf_cent_ngu: forall (n:nat), ~LeadsToLeaf (cent_ngu n).
Lemma Nasheq_CENT_NGU: forall (n:nat), NashEq Alice_Bob nat le (cent_ngu n).
|
CoFixpoint cent_agu (n:nat): (Strat) := add_Alice_Bob_cent r r n (cent_agu (S n)).
Lemma AlwLeadsToLeaf_cent_agu: forall (n:nat), AlwLeadsToLeaf (cent_agu n).
Lemma LeadsToLeaf_cent_agu: forall (n:nat), LeadsToLeaf (cent_agu n).
Lemma S2u_cent_agu_Alice: forall (n:nat), s2u (cent_agu n) Alice (2*n).
Lemma S2u_cent_agu_Bob: forall (n:nat), s2u (cent_agu n) Bob (2*n).
Theorem SGPE_cent_AGU: forall (n:nat), SGPE le (cent_agu n).
Lemma conv_cent_agu_s2u_Alice: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat),
s|--a--| (cent_agu n) -> s2u s Alice u -> u=2*n \/ u=2*n-1.
Lemma conv_cent_agu_s2u_Bob: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat),
s|--a--| (cent_agu n) -> s2u s Bob u -> u=2*n \/ u=2*n+3.
Lemma NashEq_cent_agu: forall (n:nat), NashEq Alice_Bob nat le (cent_agu n).