(*******************************************) (* *) (* slr_cla05.v *) (* *) (* St\u00e9phane Le Roux *) (* *) (* LIP (ENS Lyon, CNRS, INRIA) *) (* *) (* Coq v8.1 *) (* *) (* 2006/02 *) (* *) (*******************************************) (* ==================== *) (* === Importations === *) (* ==================== *) Require Import List. Require Import Bool. (* ================== *) (* === Hypotheses === *) (* ================== *) (* Agent is some set of "players" *) Variable Agent : Set. (* POD is some set of "outcomes" *) Variable Payoff : Set. (* Le is a decidable order over Payoff *) Variable Le : Payoff -> Payoff -> Prop. Variable Le_refl : forall p : Payoff, Le p p. Variable Le_trans : forall p1 p2 p3 : Payoff, Le p1 p2 -> Le p2 p3 -> Le p1 p3. Variable Le_antisym : forall p1 p2 : Payoff, Le p1 p2 -> Le p2 p1 -> p1=p2. Variable Le_dec : forall p1 p2 : Payoff, {Le p1 p2}+{~Le p1 p2}. (* =============================== *) (* === Preliminary definitions === *) (* =============================== *) (* The irreflexive core of Le *) Definition Lt (p p' : Payoff) : Prop := Le p p' /\ p<>p'. (* Is some element of the list l strictly smaller than one given payoff *) Fixpoint PreSomeLt (l : list Payoff)(p : Payoff){struct l} : Prop := match l with | nil => False | hd::tl => (Lt hd p) \/ (PreSomeLt tl p) end. (* Is some payoff of a list strictly smaller than some of another list *) Fixpoint SomeLt (l l' : list Payoff){struct l'} : Prop := match l' with | nil => False | hd'::tl' => (PreSomeLt l hd') \/ (SomeLt l tl') end. (* Is any payoff of a list smaller or equal to one given payoff *) Fixpoint PreAllLe (l : list Payoff)(p : Payoff){struct l} : Prop := match l with | nil => True | hd::tl => (Le hd p) /\ (PreAllLe tl p) end. (* Is any in a set of payoffs smaller or equal to any in a set of payoffs *) Fixpoint AllLe (l l' : list Payoff){struct l'} : Prop := match l' with | nil => True | hd'::tl' => (PreAllLe l hd') /\ (AllLe l tl') end. (* An binary relation over list Payoff *) Definition PrefL (l l' : list Payoff) : Prop := SomeLt l l' /\ AllLe l l'. (* ============================================= *) (* === Lemmas involving Le, Lt, and Equality === *) (* ============================================= *) Lemma Le_Equal : forall x y : Payoff, ~Le x y -> x<>y. repeat intro. absurd (Le x y). assumption. rewrite H0. apply Le_refl. Qed. Lemma Le_Equal' : forall x y : Payoff, ~Le x y -> y<>x. repeat intro. absurd (Le x y). assumption. rewrite H0. apply Le_refl. Qed. Lemma Lt_trans : forall p1 p2 p3 : Payoff, Lt p1 p2 ->Lt p2 p3 -> Lt p1 p3. unfold Lt. intros. split. apply Le_trans with p2; tauto. intro. rewrite H1 in H. absurd (p2=p3). tauto. apply Le_antisym; tauto. Qed. Lemma Lt_Le_Lt : forall p1 p2 p3 : Payoff, Lt p1 p2 -> Le p2 p3 -> Lt p1 p3. intros. unfold Lt in H |- * . split. apply Le_trans with p2; tauto. intro. rewrite <- H1 in H0. absurd (p1=p2). tauto. apply Le_antisym; tauto. Qed. Lemma Le_Lt_Lt : forall p1 p2 p3 : Payoff, Le p1 p2 -> Lt p2 p3 -> Lt p1 p3. intros. unfold Lt in H0 |- * . split. apply Le_trans with p2; tauto. intro. rewrite H1 in H. absurd (p2=p3). tauto. apply Le_antisym; tauto. Qed. (* Equality is decidable *) Lemma Equal_dec : forall x y : Payoff, {x=y}+{x<>y}. intros. destruct (Le_dec x y). destruct (Le_dec y x). assert (x=y). apply Le_antisym; tauto. tauto. assert (~x=y). apply Le_Equal'. assumption. tauto. assert (~x=y). apply Le_Equal. assumption. tauto. Qed. Lemma Le_Lt_Equal : forall p p' : Payoff, Le p p' -> ~Lt p p' -> p=p'. intros. unfold Lt in H0. destruct (Equal_dec p p'); tauto. Qed. (* =================================================================================== *) (* === Decidability lemmas about Lt, PreSomeLt, SomeLt, PreAllLe, AllLe, and PrefL === *) (* =================================================================================== *) Lemma Lt_dec : forall p1 p2 : Payoff, {Lt p1 p2}+{~Lt p1 p2}. intros p1 p2. (* Generation of four cases, two of them being solved by the tactic tauto*) elim (Le_dec p1 p2); elim (Le_dec p2 p1); intros; unfold Lt; try tauto. (* The third case *) assert (p1=p2). apply Le_antisym; assumption. tauto. (* The fourth case *) assert (p1<>p2). intro. assert (Le p2 p1). rewrite H. apply Le_refl. tauto. tauto. Qed. Lemma PreSomeLt_dec : forall (l : list Payoff)(p : Payoff), {PreSomeLt l p}+{~PreSomeLt l p}. intros. induction l; simpl. tauto. pose (Lt_dec a p). tauto. Qed. Lemma SomeLt_dec : forall l l' : list Payoff, {SomeLt l l'}+{~SomeLt l l'}. induction l'; simpl. tauto. pose (PreSomeLt_dec l a). tauto. Qed. Lemma PreAllLe_dec : forall (l : list Payoff)(p : Payoff), {PreAllLe l p}+{~PreAllLe l p}. intros. induction l; simpl. tauto. pose (Le_dec a p). tauto. Qed. Lemma AllLe_dec : forall l l' : list Payoff, {AllLe l l'}+{~AllLe l l'}. induction l'; simpl. tauto. pose (PreAllLe_dec l a). tauto. Qed. Lemma PrefL_dec : forall l l' : list Payoff, {PrefL l l'}+{~PrefL l l'}. intros. unfold PrefL. pose (SomeLt_dec l l'). pose (AllLe_dec l l'). tauto. Qed. (* ============================================== *) (* === Lemmas involving Le, PreAllLe or AllLe === *) (* ============================================== *) Lemma PreAllLe_Le_PreAllLe : forall (p p' : Payoff)(l : list Payoff), PreAllLe l p -> Le p p' -> PreAllLe l p'. induction l; simpl; intros. trivial. split. apply Le_trans with p; tauto. tauto. Qed. Lemma PreAllLe_appL : forall (p : Payoff)(l' l : list Payoff), PreAllLe (l++l') p -> PreAllLe l p. induction l; simpl; intros; tauto. Qed. Lemma PreAllLe_appR : forall (p : Payoff)(l' l : list Payoff), PreAllLe (l++l') p -> PreAllLe l' p. induction l; simpl; intros; tauto. Qed. Lemma AllLe_nil : forall l : list Payoff, AllLe nil l. induction l; simpl; tauto. Qed. Lemma AllLe_consR : forall (p : Payoff)(l l' : list Payoff), AllLe l (p::l') -> AllLe l l'. intros. unfold AllLe in H. tauto. Qed. Lemma AllLe_consL : forall (p : Payoff)(l l' : list Payoff), AllLe (p::l) l' -> AllLe l l'. induction l'; simpl; intros; tauto. Qed. Lemma AllLe_appRL : forall l1 l3 l2 : list Payoff, AllLe l1 (l2++l3) -> AllLe l1 l2. induction l2; simpl; intros; tauto. Qed. Lemma AllLe_appRR : forall l1 l3 l2 : list Payoff, AllLe l1 (l2++l3) -> AllLe l1 l3. induction l2; simpl; intros; tauto. Qed. Lemma AllLe_appLL : forall l1 l2 l3 : list Payoff, AllLe (l1++l2) l3 -> AllLe l1 l3. induction l3; simpl; intros. tauto. split. apply PreAllLe_appL with l2. tauto. tauto. Qed. Lemma AllLe_appLR : forall l1 l2 l3 : list Payoff, AllLe (l1++l2) l3 -> AllLe l2 l3. induction l3; simpl; intros. assumption. split. apply PreAllLe_appR with l1. tauto. tauto. Qed. Lemma AllLe_app_app : forall l1 l2 l3 l4 : list Payoff, AllLe (l1 ++ l2) (l3 ++ l4) -> AllLe l1 l3 /\ AllLe l1 l4 /\ AllLe l2 l3 /\ AllLe l2 l4. intros. assert (AllLe (l1 ++ l2) l3 ). apply AllLe_appRL with l4. assumption. assert (AllLe (l1 ++ l2) l4 ). apply AllLe_appRR with l3. assumption. assert (AllLe l1 l3). apply AllLe_appLL with l2. assumption. assert (AllLe l2 l3). apply AllLe_appLR with l1. assumption. assert (AllLe l1 l4). apply AllLe_appLL with l2. assumption. assert (AllLe l2 l4). apply AllLe_appLR with l1. assumption. tauto. Qed. Lemma AllLe_trans : forall (p : Payoff)(l1 l2 l3 : list Payoff), AllLe l1 (p::l2) -> AllLe (p::l2) l3 -> AllLe l1 l3. induction l3; simpl; intros. trivial. split. apply PreAllLe_Le_PreAllLe with p; tauto. simpl in IHl3. tauto. Qed. Lemma AllLe_PreAllLe_PreAllLe : forall (p p': Payoff)(l' l : list Payoff), AllLe l (p'::l') -> PreAllLe (p'::l') p -> PreAllLe l p. induction l; simpl; intros. tauto. assert (AllLe l l'). apply AllLe_consL with a; tauto. split. apply Le_trans with p'; tauto. simpl in IHl. tauto. Qed. Lemma AllLe_PreAllLe_Le_cons : forall (p1 p2 p3 : Payoff)(l l' : list Payoff), AllLe (p1::l) (p2::l') -> PreAllLe (p2::l') p3 -> Le p1 p3. induction l'; simpl; intros; apply Le_trans with p2; tauto. Qed. (* ================================================== *) (* === Lemmas involving So, PreSomeLt, or SomeLt === *) (* ================================================== *) Lemma PreSomeLt_app : forall (p : Payoff)(l' l : list Payoff), PreSomeLt (l++l') p -> PreSomeLt l p \/ PreSomeLt l' p. induction l; simpl; intros; tauto. Qed. Lemma SomeLt_nil : forall l : list Payoff, ~SomeLt nil l. induction l; simpl; intros; tauto. Qed. Lemma SomeLt_appR : forall l1 l3 l2 : list Payoff, SomeLt l1 (l2++l3) -> SomeLt l1 l2 \/ SomeLt l1 l3. induction l2; simpl; intros; tauto. Qed. Lemma SomeLt_appL : forall l1 l2 l3 : list Payoff, SomeLt (l1++l2) l3 -> SomeLt l1 l3 \/ SomeLt l2 l3. induction l3; simpl; intros. tauto. destruct H. assert (PreSomeLt l1 a \/ PreSomeLt l2 a). apply PreSomeLt_app. assumption. tauto. tauto. Qed. Lemma SomeLt_appLR : forall l1 l2 l3 l4 : list Payoff, SomeLt (l1++l2) (l3++l4) -> SomeLt l1 l3 \/ SomeLt l1 l4 \/ SomeLt l2 l3 \/ SomeLt l2 l4. intros. assert (SomeLt l1 (l3 ++ l4) \/ SomeLt l2 (l3 ++ l4)). apply SomeLt_appL. tauto. destruct H0. assert (SomeLt l1 l3 \/ SomeLt l1 l4). apply SomeLt_appR. tauto. tauto. assert (SomeLt l2 l3 \/ SomeLt l2 l4). apply SomeLt_appR. tauto. tauto. Qed. (* Below, "n-dimension" means involving functions taking n lists as arguments *) (* Below, "mixing" and "mixed" mean that both Le and Lt are somehow involved *) (* ================================== *) (* === 1-dimension mixing lemmas === *) (* ================================== *) Lemma PreAllLe_Lt_PreSomeLt : forall (p1 p2 p : Payoff)(l : list Payoff), PreAllLe (p::l) p1 -> Lt p1 p2 -> PreSomeLt (p::l) p2. induction l; simpl; intros. assert (Lt p p2). apply Le_Lt_Lt with p1; tauto. tauto. simpl in IHl. tauto. Qed. Lemma PreSomeLt_Le_PreSomeLt : forall (p p' : Payoff)(l : list Payoff), PreSomeLt l p -> Le p p' -> PreSomeLt l p'. induction l; simpl; intros. assumption. destruct H. assert (Lt a p'). apply Lt_Le_Lt with p; tauto. tauto. tauto. Qed. (* ========================== *) (* === Disjunction lemma === *) (* ========================== *) Lemma PreAllLe_SomeLt_cons : forall (p p': Payoff)(l1 l2 l3 : list Payoff), PreAllLe (p'::l1) p -> SomeLt (p::l2) l3 -> SomeLt (p'::l1) l3 \/ SomeLt l2 l3. induction l3; simpl; intros. tauto. simpl in IHl3. destruct H0. destruct H0. assert (Lt p' a). apply Le_Lt_Lt with p; tauto. tauto. tauto. tauto. Qed. (* ============================================= *) (* === 2-dimension mixed transitivity lemmas === *) (* ============================================= *) Lemma AllLe_PreSomeLt_PreSomeLt : forall (p p': Payoff)(l l' : list Payoff), AllLe (p::l) l' -> PreSomeLt l' p' -> PreSomeLt (p::l) p'. induction l'; simpl; intros. tauto. destruct H0. assert (Lt p p' ). apply Le_Lt_Lt with a; tauto. tauto. tauto. Qed. Lemma SomeLt_PreAllLe_PreSomeLt : forall (p : Payoff)(l l': list Payoff), SomeLt l l' -> PreAllLe l' p -> PreSomeLt l p. induction l'; simpl; intros. tauto. destruct H. apply PreSomeLt_Le_PreSomeLt with a; tauto. tauto. Qed. Lemma AllLe_SomeLt_SomeLt : forall (p : Payoff)(l1 l3 l2 : list Payoff), AllLe (p::l1) l2 -> SomeLt l2 l3 -> SomeLt (p::l1) l3. induction l2; simpl; intros. absurd (SomeLt nil l3). apply SomeLt_nil. assumption. simpl in IHl2. assert (SomeLt (p::l1) l3 \/ SomeLt l2 l3 ). apply PreAllLe_SomeLt_cons with a; simpl; tauto. tauto. Qed. Lemma SomeLt_AllLe_SomeLt : forall (p : Payoff)(l1 l3 l2 : list Payoff), SomeLt l1 l2 -> AllLe l2 (p::l3) -> SomeLt l1 (p::l3). induction l2; simpl; intros. tauto. destruct H. assert (PreSomeLt l1 p). apply PreSomeLt_Le_PreSomeLt with a; tauto. tauto. assert (AllLe l2 (p :: l3)). split. tauto. apply AllLe_consL with a; tauto. tauto. Qed. (* ================================= *) (* === 2-dimension mixing lemmas === *) (* ================================= *) Lemma Not_PreSomeLt_AllLe : forall (p : Payoff)(l' l : list Payoff), PreSomeLt l p -> AllLe (p::l') l -> False. induction l; simpl; intros. assumption. destruct H. absurd (Lt p p). unfold Lt. tauto. apply Le_Lt_Lt with a; tauto. tauto. Qed. Lemma Not_SomeLt_AllLe: forall (l1 l2 : list Payoff), SomeLt l1 l2 -> AllLe l2 l1 -> False. induction l2; simpl; intros. assumption. destruct H. apply Not_PreSomeLt_AllLe with a l2 l1; tauto. apply IHl2. assumption. apply AllLe_consL with a. assumption. Qed. Lemma PreSomeLt2_PreAllLe_SomeLt : forall (p p': Payoff)(l' l : list Payoff), ~PreSomeLt (p::l) p' -> PreAllLe (p::l) p' -> PreSomeLt l' p' -> SomeLt l' (p::l). simpl. intros. assert (p=p'). apply Le_Lt_Equal; tauto. rewrite H2. tauto. Qed. Lemma PreSomeLt_PreAllLe2_AllLe : forall (p : Payoff)(l' l : list Payoff), ~PreSomeLt l p -> PreAllLe l p -> PreAllLe l' p -> AllLe l' l. induction l; simpl; intros. tauto. assert (a=p). apply Le_Lt_Equal; tauto. rewrite H2. tauto. Qed. Lemma SomeLt3_AllLe : forall (p :Payoff)(l1 l2 l3 : list Payoff), ~SomeLt (p::l1) l3 -> AllLe (p::l1) l3 -> SomeLt l2 l3 -> SomeLt l2 (p::l1). induction l3; simpl; intros. tauto. destruct H1. apply PreSomeLt2_PreAllLe_SomeLt with a; simpl; tauto. tauto. Qed. Lemma SomeLt3_AllLe2 : forall (p1 p4 :Payoff)(l1 l2 l3 l4: list Payoff), ~SomeLt (p1::l1) l3 -> AllLe (p1::l1) l3 -> SomeLt l2 l3 -> AllLe (p1::l1) (p4::l4) -> SomeLt l2 (p4::l4). intros. apply SomeLt_AllLe_SomeLt with (p1::l1). apply SomeLt3_AllLe with l3; tauto. assumption. Qed. Lemma SomeLt3_AllLe3 : forall (p :Payoff)(l1 l2 l3 : list Payoff), ~SomeLt (p::l1) l3 -> AllLe (p::l1) l3 -> SomeLt l2 l3 -> AllLe l2 l3 -> SomeLt l2 (p::l1) /\ AllLe l2 (p::l1). induction l3; intros. tauto. simpl in * |- . destruct H1. split. apply PreSomeLt2_PreAllLe_SomeLt with a; simpl; tauto. apply PreSomeLt_PreAllLe2_AllLe with a; simpl; tauto. simpl. tauto. Qed. (* ========================== *) (* === Lemmas about PrefL === *) (* ========================== *) Lemma PrefL_irrefl : forall (l : list Payoff), ~PrefL l l. unfold PrefL. repeat intro. apply Not_SomeLt_AllLe with l l; tauto. Qed. Lemma PrefL_trans : forall (l1 l2 l3 : list Payoff), PrefL l1 l2 -> PrefL l2 l3 -> PrefL l1 l3. unfold PrefL. induction l3; simpl; intros. assumption. destruct l2. simpl in H. tauto. split. destruct H0. destruct H0. assert (PreSomeLt l1 a). apply SomeLt_PreAllLe_PreSomeLt with (p::l2); tauto. tauto. tauto. split. apply AllLe_PreAllLe_PreAllLe with p l2; tauto. apply AllLe_trans with p l2; tauto. Qed. Lemma PrefL_appR : forall l l2 l1 : list Payoff, PrefL l (l1++l2) -> PrefL l l1 \/ PrefL l l2. unfold PrefL. intros. assert (SomeLt l l1 \/ SomeLt l l2). apply SomeLt_appR. tauto. assert ( AllLe l l1 /\ AllLe l l2). split. apply AllLe_appRL with l2. tauto. apply AllLe_appRR with l1. tauto. tauto. Qed. Lemma PrefL_appLR : forall l1 l2 l3 l4 : list Payoff, PrefL (l1++l2) (l3++l4) -> PrefL l1 l3 \/ PrefL l1 l4 \/ PrefL l2 l3 \/ PrefL l2 l4. unfold PrefL. intros. assert (SomeLt l1 l3 \/ SomeLt l1 l4 \/ SomeLt l2 l3 \/ SomeLt l2 l4). apply SomeLt_appLR. tauto. assert (AllLe l1 l3 /\ AllLe l1 l4 /\ AllLe l2 l3 /\ AllLe l2 l4). apply AllLe_app_app. tauto. tauto. Qed. Lemma PrePrefL_compL : forall (p : Payoff)(l1 l2 l : list Payoff), ~(PrefL l2 (p::l1)) -> ~(PrefL (p::l1) l) -> (PrefL ((p::l1)++l2) l) -> False. unfold PrefL. intros. assert (SomeLt (p::l1) l \/ SomeLt l2 l). apply SomeLt_appL. tauto. assert (AllLe (p::l1) l). apply AllLe_appLL with l2. tauto. assert (AllLe l2 l). apply AllLe_appLR with (p::l1). tauto. destruct (SomeLt_dec (p::l1) l). tauto. assert (SomeLt l2 l). tauto. assert (SomeLt l2 (p::l1) /\ AllLe l2 (p::l1)). apply SomeLt3_AllLe3 with l; tauto. tauto. Qed. Lemma PrefL_compL : forall (l1 l2 l : list Payoff), nil<>l1 -> ~(PrefL l2 l1) -> ~(PrefL l1 l) -> (PrefL (l1++l2) l) -> False. intros. destruct l1. tauto. apply PrePrefL_compL with p l1 l2 l; tauto. Qed. Lemma PrePrefL_compL' : forall (p : Payoff)(l1 l2 l : list Payoff), ~(PrefL l1 (p::l2)) -> ~(PrefL (p::l2) l) -> (PrefL (l1++(p::l2)) l) -> False. unfold PrefL. intros. assert (SomeLt l1 l \/ SomeLt (p::l2) l). apply SomeLt_appL. tauto. assert (AllLe l1 l). apply AllLe_appLL with (p::l2). tauto. assert (AllLe (p::l2) l). apply AllLe_appLR with l1. tauto. destruct (SomeLt_dec (p::l2) l). tauto. assert (SomeLt l1 l). tauto. assert (SomeLt l1 (p::l2) /\ AllLe l1 (p::l2)). apply SomeLt3_AllLe3 with l; tauto. tauto. Qed. Lemma PrefL_compL' : forall (l1 l2 l : list Payoff), nil<>l2 -> ~(PrefL l1 l2) -> ~(PrefL l2 l) -> (PrefL (l1++l2) l) -> False. intros. destruct l2. tauto. apply PrePrefL_compL' with p l1 l2 l; tauto. Qed. Lemma PrePrefL_compLR : forall (p1 p2 p3 p4 : Payoff)(l1 l2 l3 l4 : list Payoff), ~PrefL (p1::l1) (p3::l3) -> ~PrefL (p2::l2) (p4::l4) -> PrefL ((p1::l1)++(p2::l2)) ((p3::l3)++(p4::l4)) -> False. unfold PrefL. intros. assert (SomeLt (p1::l1) (p3::l3) \/ SomeLt (p1::l1) (p4::l4) \/ SomeLt (p2::l2) (p3::l3) \/ SomeLt (p2::l2) (p4::l4)). apply SomeLt_appLR; tauto. assert (AllLe (p1::l1) (p3::l3) /\ AllLe (p1::l1) (p4::l4) /\ AllLe (p2::l2) (p3::l3) /\ AllLe (p2::l2) (p4::l4)). apply AllLe_app_app; tauto. assert (~SomeLt (p1::l1) (p3::l3)). tauto. assert (~SomeLt (p2::l2) (p4::l4)). tauto. destruct H2. tauto. destruct H2. assert (SomeLt (p1::l1) (p3 :: l3)). apply SomeLt3_AllLe2 with p2 l2 (p4::l4); tauto. tauto. assert (SomeLt (p2::l2) (p4 :: l4)). apply SomeLt3_AllLe2 with p1 l1 (p3::l3); tauto. tauto. Qed. Lemma PrefL_compLR : forall (l1 l2 l3 l4 : list Payoff), nil<>l1 -> nil<>l2 -> nil<>l3 -> nil<>l4 -> ~PrefL l1 l3 -> ~PrefL l2 l4 -> PrefL (l1++l2) (l3++l4) -> False. destruct l1; destruct l2; destruct l3; destruct l4; try tauto. intros. apply PrePrefL_compLR with p p0 p1 p2 l1 l2 l3 l4; tauto. Qed. (* ========================= *) (* === Basic definitions === *) (* ========================= *) (* PayoffF is the set of "payoff functions" *) Definition PayoffF := Agent -> Payoff. (* A game *) Inductive Game : Set := | gL : PayoffF -> Game | gN : Agent -> Game -> Game -> Game. (* A choice *) Inductive Choice : Set := l | r | b. (* A strategy *) Inductive NDS : Type := | sL : PayoffF -> NDS | sN : Agent -> Choice -> NDS -> NDS -> NDS. (* The game a strategy has been built on *) Fixpoint nds2g (s : NDS) : Game := match s with | sL pf => gL pf | sN a c sl sr => gN a (nds2g sl)(nds2g sr) end. (* Agent Convertibility between strategies *) Fixpoint NDAgentConv (a0: Agent) (s s': NDS) {struct s} : Prop := match s with | (sL pf) => match s' with | (sL pf') => forall a, pf a= pf' a | _ => False end | (sN a c sl sr) => match s' with |(sN a' c' sl' sr') => (a = a') /\ (c=c' \/ a = a0) /\ NDAgentConv a0 sl sl' /\ NDAgentConv a0 sr sr' | _ => False end end. (* All possible outcomes of a strategy for a specific agent *) Fixpoint NDPayoff (s : NDS)(a : Agent){struct s} : list Payoff := match s with | sL p => (p a)::nil | sN a' c sl sr => match c with | l => (NDPayoff sl a) | r => (NDPayoff sr a) | b => (NDPayoff sl a)++(NDPayoff sr a) end end. (* A preference relation between two strategies for a specific agent *) Definition PrefS (a : Agent)(s1 s2 : NDS) : Prop := PrefL (NDPayoff s1 a)(NDPayoff s2 a). (* ======================================= *) (* === Lemmas about PrefS and NDPayoff === *) (* ======================================= *) (* PrefS is decidable *) Lemma PrefS_dec : forall (a : Agent)(s1 s2 : NDS), {PrefS a s1 s2}+{~PrefS a s1 s2}. intros. unfold PrefS. pose (PrefL_dec (NDPayoff s1 a) (NDPayoff s2 a )). assumption. Qed. (* PrefS is transitive *) Lemma PrefS_trans : forall (a : Agent)(s1 s2 s3 : NDS), PrefS a s1 s2 -> PrefS a s2 s3 -> PrefS a s1 s3. unfold PrefS. intros. apply PrefL_trans with (NDPayoff s2 a); tauto. Qed. (* PrefS is irreflexive *) Lemma PrefS_irrefl : forall (a : Agent)(s : NDS), ~PrefS a s s. intros. unfold PrefS, PrefL. intro. apply Not_SomeLt_AllLe with (NDPayoff s a) (NDPayoff s a); tauto. Qed. (* NDPayoff returns a non-empty list *) Lemma NDPayoff_nil : forall (s : NDS)(a : Agent), ~(nil=NDPayoff s a). repeat intro. induction s. inversion H. induction c; inversion H. tauto. tauto. assert ( NDPayoff s1 a =nil /\ NDPayoff s2 a=nil). apply app_eq_nil. symmetry. assumption. absurd (nil=NDPayoff s1 a). tauto. symmetry. tauto. Qed. (* ============================ *) (* === Advanced definitions === *) (* ============================ *) (* Definition of Nash equilibirum *) Definition NDEq (s : NDS) : Prop := forall a, forall s', NDAgentConv a s s' -> ~PrefS a s s'. (* The "backward induction" function*) Fixpoint NDBIF (g : Game) : NDS := match g with | gL pf => sL pf | gN a gl gr => let sl := NDBIF gl in let sr := NDBIF gr in let c:= (if (PrefS_dec a sl sr) then r else if (PrefS_dec a sr sl) then l else b) in sN a c sl sr end. (* =========================== *) (* === Results about NDBIF === *) (* =========================== *) (* NDBIF returns a strategy built on the initial game *) Lemma nds2g_NDBIF : forall g : Game, nds2g (NDBIF g)=g. induction g; simpl. tauto. rewrite IHg1. rewrite IHg2. trivial. Qed. (* NDBIF returns a strategy that is NDEq *) Lemma NDBIF_NDEq : forall g : Game, NDEq (NDBIF g). unfold NDEq. induction g; intros until s' ; destruct s'; simpl; repeat intro; try assumption. (* Leaf-Leaf case *) pose (H1:= H a). unfold PrefS in H0. unfold NDPayoff in H0. rewrite H1 in H0. simpl in H. elim PrefS_irrefl with a (sL p0). assumption. (* Node-Node case *) (* Use of induction hypotheses *) assert (~ PrefS a0 (NDBIF g1) s'1). apply IHg1; tauto. assert (~ PrefS a0 (NDBIF g2) s'2). apply IHg2; tauto. destruct H. rewrite <- H in H0. clear IHg1 IHg2 a1 H. destruct H3. clear H3. (* Case splitting on the relation between the NDBIF on the left and on the right*) destruct (PrefS_dec a (NDBIF g1) (NDBIF g2)); destruct (PrefS_dec a (NDBIF g2) (NDBIF g1)). (* Subcase 1: both are bigger than each other *) absurd (PrefS a (NDBIF g1) (NDBIF g1)). apply PrefS_irrefl. apply PrefS_trans with (NDBIF g2); assumption. (* Subcase 2: right is bigger *) destruct c. (* c=l *) (* a=a0 must hold *) destruct H. inversion H. rewrite H in p. absurd (PrefS a0 (NDBIF g1) s'1). assumption. apply PrefS_trans with (NDBIF g2); tauto. (* c=r *) tauto. (* c=b *) (* a=a0 must hold *) destruct H. inversion H. rewrite H in p. (* Disjunction creation for case spitting *) assert (PrefL (NDPayoff (NDBIF g2) a0) (NDPayoff s'1 a0) \/ PrefL (NDPayoff (NDBIF g2) a0) (NDPayoff s'2 a0)). apply PrefL_appR; tauto. destruct H3. absurd (PrefL (NDPayoff (NDBIF g1) a0) (NDPayoff s'1 a0)). assumption. apply PrefL_trans with (NDPayoff (NDBIF g2) a0); tauto. tauto. (* Subcase 3: left is bigger *) destruct c. (* c=l *) tauto. (* c=r *) (* a=a0 must hold *) destruct H. inversion H. rewrite H in p. absurd (PrefS a0 (NDBIF g2) s'2). tauto. apply PrefS_trans with (NDBIF g1); tauto. (* c=b *) (* a=a0 must hold *) destruct H. inversion H. rewrite H in p. (* Disjunction creation for case spitting *) assert (PrefL (NDPayoff (NDBIF g1) a0) (NDPayoff s'1 a0) \/ PrefL (NDPayoff (NDBIF g1) a0) (NDPayoff s'2 a0)). apply PrefL_appR; tauto. destruct H3. tauto. absurd (PrefL (NDPayoff (NDBIF g2) a0) (NDPayoff s'2 a0)). assumption. apply PrefL_trans with (NDPayoff (NDBIF g1) a0); tauto. (* Subcase 4: none is bigger *) (* The four lists below need to be non empty in order to apply a lemma*) assert (nil<>(NDPayoff (NDBIF g1) a0)). apply NDPayoff_nil. assert (nil<>(NDPayoff (NDBIF g2) a0)). apply NDPayoff_nil. assert (nil<>(NDPayoff s'1 a0)). apply NDPayoff_nil. assert (nil<>(NDPayoff s'2 a0)). apply NDPayoff_nil. (* Subcase splitting on c*) destruct c. (* c=l *) (* a=a0 must hold *) destruct H. inversion H. rewrite H in n0. apply PrefL_compL with (NDPayoff (NDBIF g1) a0) (NDPayoff (NDBIF g2) a0) (NDPayoff s'1 a0); tauto. (* c= r *) (* a=a0 must hold *) destruct H. inversion H. rewrite H in n. apply PrefL_compL' with (NDPayoff (NDBIF g1) a0) (NDPayoff (NDBIF g2) a0) (NDPayoff s'2 a0); tauto. (* c=b *) apply PrefL_compLR with (NDPayoff (NDBIF g1) a0) (NDPayoff (NDBIF g2) a0)(NDPayoff s'1 a0) (NDPayoff s'2 a0); (tauto || apply NDPayoff_nil). Qed. Theorem Equilibrium_constructive_existence : forall g : Game, nds2g (NDBIF g)=g /\ NDEq (NDBIF g). intros. split. apply nds2g_NDBIF. apply NDBIF_NDEq. Qed.