| © Pierre Lescanne (February 2008) |
| Developed in V8.1 June-August 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].
Implicit Arguments NashEq [Agent Utility].
|
Inductive Alice_Bob :Set := Alice :Alice_Bob | Bob: Alice_Bob.
Definition Strat := Strategy 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 |
Strategy "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 ge (ngu n).
Strategy "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).
Strategy "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).
Lemma S2u_agubc_Alice: forall (n:nat), s2u (agubc n) Alice (2*n+1).
Lemma S2u_agubc_Bob: forall (n:nat), s2u (agubc n) Bob (2*n).
Theorem SGPEAGUBC: forall (n:nat), SGPE ge (agubc n).
Strategy "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).
Lemma S2u_acbgu_Alice: forall (n:nat), s2u (acbgu n) Alice (2*n+1).
Lemma S2u_acbgu_Bob: forall (n:nat), s2u (acbgu n) Bob (2*n+2).
Theorem SGPEACBGU: forall (n:nat), SGPE ge (acbgu n).
Dollar auction |
Variable v:nat.
Axiom v_pos: v > 0.
Alice continues, Bob stops |
Definition add_Alice_Bob_dol (cA cB:Choice) (n:nat) (s:Strat) :=
<<Alice,cA,<<Bob, cB,s,[n+1, v+n]>>,[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) = <<Alice,l,<<Bob, r, (dolAcBs (n+1)),[n+1, v+n]>>,[v+n,n]>>.
Lemma AlwLeadsToLeaf_dolAcBs: forall (n:nat), AlwLeadsToLeaf (dolAcBs n).
Lemma LeadsToLeaf_dolAcBs: forall (n:nat), LeadsToLeaf (dolAcBs n).
Lemma S2u_dolAcBs_Alice: forall (n:nat), s2u (dolAcBs n) Alice (n+1).
Lemma S2u_dolAcBs_Bob: forall (n:nat), s2u (dolAcBs n) Bob (v+n).
Theorem SGPE_dol_Ac_Bs: forall (n:nat), SGPE ge (dolAcBs n).
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) = <<Alice,r,<<Bob, l, (dolAsBc (n+1)),[n+1, v+n]>>,[v+n,n]>>.
Lemma AlwLeadsToLeaf_dolAsBc: forall (n:nat), AlwLeadsToLeaf (dolAsBc n).
Lemma LeadsToLeaf_dolAsBc: forall (n:nat), LeadsToLeaf (dolAsBc n).
Lemma S2u_dolAsBc_Alice: forall (n:nat), s2u (dolAsBc n) Alice (v+n).
Lemma S2u_dolAsBc_Bob: forall (n:nat), s2u (dolAsBc n) Bob n.
Theorem SGPE_dol_As_Bc: forall (n:nat), SGPE ge (dolAsBc n).
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) = <<Alice,r,<<Bob, r, (dolAsBs (n+1)),[n+1, v+n]>>,[v+n,n]>>.
Lemma AlwLeadsToLeaf_dolAsBs: forall (n:nat), AlwLeadsToLeaf (dolAsBs n).
Lemma LeadsToLeaf_dolAsBs: forall (n:nat), LeadsToLeaf (dolAsBs n).
Lemma S2u_dolAsBs_Alice: forall (n:nat), s2u (dolAsBs n) Alice (v+n).
Lemma S2u_dolAsBs_Bob: forall (n:nat), s2u (dolAsBs n) Bob n.
Definition dolAsBs_0' := add_Alice_Bob_dol l r 0 (dolAsBs 1).
Lemma conv_dolAsBs: dolAsBs_0' |-- Alice --| dolAsBs 0.
Lemma LeadsToLeaf_dolAsBs_0':LeadsToLeaf dolAsBs_0'.
Lemma S2u_dolAsBs_0'_Alice: s2u dolAsBs_0' Alice 1.
Theorem NotSGPE_dolAsBs: (v>1) -> ~(NashEq ge (dolAsBs 0)).
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) = <<Alice,l,<<Bob, l, (dolAcBc (n+1)),[n+1, v+n]>>,[v+n,n]>>.
Lemma NeverLeaf_AcBc: forall (n:nat), NeverLeaf (dolAcBc n).
Lemma Not_LeadsToLeaf_AcBc: forall (n:nat), ~LeadsToLeaf (dolAcBc n).
Lemma NotSGPE_dolAcBc: forall (n:nat), ~SGPE ge (dolAcBc n).
Lemma NashEq_dolAcBc: forall (n:nat), NashEq ge (dolAcBc n).