Profiles

A 'profile' is a dependent vector which contains a (X i) for all player i. Typically, a strategy profile is a strategy for each player i.

We represent profiles with dependent finite-support functions (dffun)

Section Profiles.

  Implicit Type (N : finType).

Profile for classical games

  Definition profile (N : finType) (X : N -> eqType) := {dffun forall i, X i}.

Finite profile

  Definition fprofile N (X : N -> finType) := {dffun forall i, X i}.

Change the strategy of a given player in a given profile

  Definition move N X (p : profile X) (i : N) (pi : X i) : profile X :=
    [ffun j => match boolP (i == j) with
               | AltTrue h => eq_rect _ X pi _ (eqP h)
               | AltFalse _ =>  p j
               end].

Profile for incomplete games

  Definition iprofile N (T : N -> finType) (X : N -> eqType) :=
    {dffun forall i, T i -> X i}.

Transform an iprofile to a profile such as support is the set of dependent pairs (i,t_i)

  Definition iprofile_flatten N (T : N -> finType) X (p : iprofile T X)
    : profile (fun it => X (projT1 it)) :=
    [ffun it => p (projT1 it) (projT2 it)].

Profile that will be played if player's types are known

  Definition proj_iprofile N (T : N -> finType) X (p : iprofile T X)
    : profile T -> profile X :=
    fun theta => [ffun i => p i (theta i)]
.
  Definition proj_flatprofile N (T : N -> finType) X
             (p : profile (fun it => X (projT1 it)))
    : profile T -> profile X :=
    fun theta => [ffun i => p (existT _ i (theta i))].

  Lemma proj_iprof_flatprof N (T : N -> finType) X (p : iprofile T X) theta :
    (proj_iprofile p theta) = (proj_flatprofile (iprofile_flatten p) theta).
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
theta:profile (fun x : N => T x)
proj_iprofile p theta =
proj_flatprofile (iprofile_flatten p) theta
  Proof.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
theta:profile (fun x : N => T x)
proj_iprofile p theta =
proj_flatprofile (iprofile_flatten p) theta
    by apply: eq_dffun => i; rewrite ffunE.
  Qed.

  Definition bmove N T X (p : iprofile T X) (i : N) ti xi
    : iprofile T X :=
    [ffun j => fun tj => match boolP (i == j) with
                         | AltTrue h =>
                           let ti' := eq_rect _ T ti _ (eqP h) in
                           if ti' == tj
                           then eq_rect i X xi j (eqP h)
                           else p j tj
                         | AltFalse _ => p j tj
                         end].

  Lemma move_bmove N T X (p : iprofile T X) (it : {i : N & T i})
        (xi : X (projT1 it)) :
    (@move _ _ (iprofile_flatten p) it xi)
    = (iprofile_flatten (bmove p (projT2 it) xi)).
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
move (iprofile_flatten p) xi =
iprofile_flatten (bmove p (projT2 it) xi)
  Proof.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
move (iprofile_flatten p) xi =
iprofile_flatten (bmove p (projT2 it) xi)
  apply eq_dffun => it' //=.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
match boolP (it == it') with
| @AltTrue _ _ h =>
    eq_rect it (fun x : {i : N & T i} => X (projT1 x))
      xi it' (eqP h)
| @AltFalse _ _ _ => iprofile_flatten p it'
end = bmove p (projT2 it) xi (projT1 it') (projT2 it')
  rewrite !ffunE.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
match boolP (it == it') with
| @AltTrue _ _ h =>
    eq_rect it (fun x : {i : N & T i} => X (projT1 x))
      xi it' (eqP h)
| @AltFalse _ _ _ => p (projT1 it') (projT2 it')
end =
match boolP (projT1 it == projT1 it') with
| @AltTrue _ _ h =>
    let ti' :=
      eq_rect (projT1 it) (fun x : N => T x)
        (projT2 it) (projT1 it') (eqP h) in
    if ti' == projT2 it'
    then
     eq_rect (projT1 it) (fun x : N => X x) xi
       (projT1 it') (eqP h)
    else p (projT1 it') (projT2 it')
| @AltFalse _ _ _ => p (projT1 it') (projT2 it')
end
  case (boolP (@eq_op (Finite.eqType (tag_finType T)) it it')) => H1;
                   case (boolP (projT1 it == projT1 it')) => H2 //=.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
  -
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it')) case (boolP ((eq_rect _ _ (projT2 it) (projT1 it')  (@elimT
      (@eq (Finite.sort N) _ _) _ eqP H2)) == (projT2 it'))) => H3.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) == projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) =
eq_rect (projT1 it) (fun x : N => X x) xi (projT1 it')
  (eqP H2)
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) != projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
    +
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) == projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) =
eq_rect (projT1 it) (fun x : N => X x) xi (projT1 it')
  (eqP H2)
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) != projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it')) rewrite (rew_map X _ (eqP H1) xi).
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) == projT2 it'
eq_rect (projT1 it) (fun x : N => X x) xi (projT1 it')
  (f_equal (projT1 (P:=fun i : N => T i)) (eqP H1)) =
eq_rect (projT1 it) (fun x : N => X x) xi (projT1 it')
  (eqP H2)
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) != projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
      by rewrite (Eqdep_dec.eq_proofs_unicity
                    (@eqType_dec N) (f_equal _ (eqP H1))(eqP H2)).
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) != projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
    +
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) != projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it')) move/eqP in H3.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) <> projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
      have Hcontra := projT2_eq (eqP H1).
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) <> projT2 it'
Hcontra:eq_rect (projT1 it) (fun a : N => T a)
  (projT2 it) (projT1 it')
  (projT1_eq (eqP H1)) = 
projT2 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) 
    (projT2 it) (projT1 it') 
    (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
      by rewrite (Eqdep_dec.eq_proofs_unicity (@eqType_dec N)
           (projT1_eq (eqP H1)) (eqP H2)) in Hcontra.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
  -
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it != projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it')) move/eqP in H2.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it == it'
H2:projT1 it <> projT1 it'
eq_rect it (fun x : {i : N & T i} => X (projT1 x)) xi
  it' (eqP H1) = p (projT1 it') (projT2 it')
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
    by rewrite (eqP H1) in H2.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it'))
  -
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
p (projT1 it') (projT2 it') =
(if
  eq_rect (projT1 it) (fun x : N => T x) (projT2 it)
    (projT1 it') (eqP H2) == projT2 it'
 then
  eq_rect (projT1 it) (fun x : N => X x) xi
    (projT1 it') (eqP H2)
 else p (projT1 it') (projT2 it')) case (boolP ((eq_rect _ _ (projT2 it) (projT1 it')  (@elimT
        (@eq (Finite.sort N) _ _) _ eqP H2)) == (projT2 it'))) => H3 //.
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) == projT2 it'
p (projT1 it') (projT2 it') =
eq_rect (projT1 it) (fun x : N => X x) xi (projT1 it')
  (eqP H2)
    have Hcontra := eq_sigT it it' (eqP H2) (eqP H3).
N:finType
T:N -> finType
X:N -> eqType
p:iprofile T X
it:{i : N & T i}
xi:X (projT1 it)
it':tag_finType T
H1:it != it'
H2:projT1 it == projT1 it'
H3:eq_rect (projT1 it) (fun i : N => T i)
  (projT2 it) (projT1 it') (eqP H2) == projT2 it'
Hcontra:it = it'
p (projT1 it') (projT2 it') =
eq_rect (projT1 it) (fun x : N => X x) xi (projT1 it')
  (eqP H2)
    by move/eqP in H1.
  Qed.

End Profiles.

Classical SNF games

We define simultaneous SNF games with abstract outcomes, that may be different for eaech player.

Module NFGame.

  Record game (player : finType) : Type :=
    { outcome : player -> Type;
      action : player -> finType;
      utility : forall i, profile action -> outcome i;
      preceq : forall i, rel (outcome i);
    }.

  Definition NashEqb player (g : game player)
    : pred (profile (action g)) :=
    fun p =>
    [forall i : player,
     forall ai : action g i,
        ~~ prec (@preceq _ _ _) (utility i p) (utility i (move p ai))].

  Definition NashEq player (g : game player) (p : profile (action g))
    : Prop :=
    forall (i : player) (ai : action g i),
    ~ prec (@preceq _ _ _) (utility i p) (utility i (move p ai)).

  Lemma NashEqP player (g : game player) (p : profile (action g)) :
    reflect (NashEq p) (NashEqb p).
player:finType
g:game player
p:profile (fun x : player => action g x)
reflect (NashEq p) (NashEqb p)
  Proof.
player:finType
g:game player
p:profile (fun x : player => action g x)
reflect (NashEq p) (NashEqb p)
  case (boolP (NashEqb p)); constructor; move: i.
player:finType
g:game player
p:profile (fun x : player => action g x)
NashEqb p -> NashEq p
player:finType
g:game player
p:profile (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
  -
player:finType
g:game player
p:profile (fun x : player => action g x)
NashEqb p -> NashEq p
player:finType
g:game player
p:profile (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p move/forallP => H i; move: (H i).
player:finType
g:game player
p:profile (fun x : player => action g x)
H:forall x : player,
[forall ai,
   ~~
   prec (preceq (i:=x)) 
     (utility x p) (utility x (move p ai))]
i:player
[forall ai,
   ~~
   prec (preceq (i:=i)) (utility i p)
     (utility i (move p ai))] ->
forall ai : action g i,
~
prec (preceq (i:=i)) (utility i p)
  (utility i (move p ai))
player:finType
g:game player
p:profile (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
    move/forallP => H2 ai; move: (H2 ai) => H0.
player:finType
g:game player
p:profile (fun x : player => action g x)
H:forall x : player,
[forall ai,
   ~~
   prec (preceq (i:=x)) 
     (utility x p) (utility x (move p ai))]
i:player
H2:forall x : action g i,
~~
prec (preceq (i:=i)) (utility i p)
  (utility i (move p x))
ai:action g i
H0:~~
prec (preceq (i:=i)) (utility i p)
  (utility i (move p ai))
~
prec (preceq (i:=i)) (utility i p)
  (utility i (move p ai))
player:finType
g:game player
p:profile (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
    exact: (negP H0).
player:finType
g:game player
p:profile (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
  -
player:finType
g:game player
p:profile (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p move/forallPn => [] x.
player:finType
g:game player
p:profile (fun x : player => action g x)
x:player
~~
[forall ai,
   ~~
   prec (preceq (i:=x)) (utility x p)
     (utility x (move p ai))] -> ~ NashEq p
    move/forallPn => [] y.
player:finType
g:game player
p:profile (fun x : player => action g x)
x:player
y:action g x
~~
~~
prec (preceq (i:=x)) (utility x p)
  (utility x (move p y)) -> ~ NashEq p
    move/negPn => [H Hne].
Nothing to inject.
player:finType
g:game player
p:profile (fun x : player => action g x)
x:player
y:action g x
H:prec (preceq (i:=x)) (utility x p)
  (utility x (move p y))
Hne:NashEq p
False
    by case: (Hne x y).
  Qed.

End NFGame.

Hypergraphical games

Hypergraphical games are succinct representation of SNF games, where players play in some local games. Their global utility is the (abstract) sum of their local utility.

Module HGGame.


  Record game (player : finType) : Type :=
    { local_game : finType;
      plays : local_game -> pred player;
      outcome : player -> Type;
      outcome0 : forall i, outcome i;
      oplus : forall i, Monoid.com_law (outcome0 i);
      preceq : forall i, rel (outcome i);
      action : player -> finType;
      local_utility : local_game ->
                      forall i, profile action -> outcome i;
    }.

  Definition global_utility player (g : game player) (i : player)
             (p : profile (action g)) :=
    \big[oplus g i/outcome0 g i]_(lg : local_game g | plays lg i)
     local_utility lg i p.

  Definition to_normal_form player (g : game player)
    : NFGame.game player :=
    {| NFGame.outcome := outcome g;
       NFGame.preceq := @preceq _ g;
       NFGame.action := action g;
       NFGame.utility := @global_utility _ g;
    |}.

  Definition NashEqb player (g : game player) :=
    @NFGame.NashEqb _ (to_normal_form g).

  Definition NashEq player (g : game player) :=
    @NFGame.NashEq _ (to_normal_form g).

  Lemma NashEqP player (g : game player) (p : profile (action g))
    : reflect (NashEq p) (NashEqb p).
player:finType
g:game player
p:profile (fun x : player => action g x)
reflect (NashEq p) (NashEqb p)
  Proof.
player:finType
g:game player
p:profile (fun x : player => action g x)
reflect (NashEq p) (NashEqb p) exact: NFGame.NashEqP. Qed.

  Lemma NashEq_HG_NFb player (g : game player) p :
    NashEqb p = @NFGame.NashEqb _ (to_normal_form g) p.
player:finType
g:game player
p:profile
  (fun x : player =>
   NFGame.action (to_normal_form g) x)
NashEqb p = NFGame.NashEqb p
  Proof.
player:finType
g:game player
p:profile
  (fun x : player =>
   NFGame.action (to_normal_form g) x)
NashEqb p = NFGame.NashEqb p by []. Qed.

  Lemma nashEq_HG_NF player (g : game player) p :
    NashEq p <-> @NFGame.NashEq _ (to_normal_form g) p.
player:finType
g:game player
p:profile
  (fun x : player =>
   NFGame.action (to_normal_form g) x)
NashEq p <-> NFGame.NashEq p
  Proof.
player:finType
g:game player
p:profile
  (fun x : player =>
   NFGame.action (to_normal_form g) x)
NashEq p <-> NFGame.NashEq p by []. Qed.

End HGGame.

Incomplete games

Incomplete games generalize Bayesian games and possibilistic games.

Players don't know perfectly the world i.e. they ignore which game they are playing.

Module IGame.


  Record game (player : finType) : Type :=
    { evalst : player -> eval_struct;
      signal : player -> finType;
      action : player -> finType;
      utility : forall i : player,
        profile action -> profile signal -> U (evalst i);
      belief : forall i : player, profile signal -> W (evalst i);
    }.

  Definition GEutility player (g : game player) (i : player) t p :=
    \big[oplus (evalst g i)/V0 (evalst g i)]_(
     theta : fprofile (signal g) | (theta i) == t)
     otimes (belief i theta) (utility i (proj_iprofile p theta) theta).

  Definition to_hggame player (g : game player) : HGGame.game _ :=
    {| HGGame.local_game := [finType of fprofile (signal g)];
       HGGame.plays := fun theta it => theta (projT1 it) == projT2 it;
       HGGame.outcome := fun it => V _;
       HGGame.outcome0 := fun it => V0 _;
       HGGame.oplus := fun it => oplus _;
       HGGame.preceq := fun it => @preceq_V _;
       HGGame.action := fun it => action g _;
       HGGame.local_utility := fun theta it p =>
           otimes (belief (projT1 it) theta)
              (utility (projT1 it) (proj_flatprofile p theta) theta);
    |}.

  Definition to_normal_form player (g : game player)
    : NFGame.game _ :=
    HGGame.to_normal_form (to_hggame g).

  Definition NashEqb player (g : game player)
    : pred (iprofile (signal g) (action g)) :=
    fun bp =>
    [forall i : player,
     forall t : signal g i,
     forall ai : action g i,
          ~~ prec (@preceq_V _) (GEutility t bp)
             (GEutility t (bmove bp t ai)) ].

  Definition NashEq player (g : game player) p : Prop :=
    forall i : player,
    forall t : signal g i,
    forall ai : action g i,
    ~ prec (@preceq_V _) (GEutility t p) (GEutility t (bmove p t ai)).

  Lemma NashEqP player (g : game player)
        (p : iprofile (signal g) (action g)) :
    reflect (NashEq p) (NashEqb p).
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
reflect (NashEq p) (NashEqb p)
  Proof.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
reflect (NashEq p) (NashEqb p)
  case (boolP (NashEqb p)); constructor; move: i.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
NashEqb p -> NashEq p
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
  -
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
NashEqb p -> NashEq p
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p move/forallP => H i; move: (H i).
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
H:forall x : player,
[forall t,
   forall ai,
   ~~
   prec (preceq_V (e:=evalst g x)) 
     (GEutility t p) (GEutility t (bmove p t ai))]
i:player
[forall t,
   forall ai,
   ~~
   prec (preceq_V (e:=evalst g i)) (GEutility t p)
     (GEutility t (bmove p t ai))] ->
forall (t : signal g i) (ai : action g i),
~
prec (preceq_V (e:=evalst g i)) (GEutility t p)
  (GEutility t (bmove p t ai))
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
    move/forallP => H2 t; move: (H2 t).
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
H:forall x : player,
[forall t,
   forall ai,
   ~~
   prec (preceq_V (e:=evalst g x)) 
     (GEutility t p) (GEutility t (bmove p t ai))]
i:player
H2:forall x : signal g i,
[forall ai,
   ~~
   prec (preceq_V (e:=evalst g i))
     (GEutility x p) (GEutility x (bmove p x ai))]
t:signal g i
[forall ai,
   ~~
   prec (preceq_V (e:=evalst g i)) (GEutility t p)
     (GEutility t (bmove p t ai))] ->
forall ai : action g i,
~
prec (preceq_V (e:=evalst g i)) (GEutility t p)
  (GEutility t (bmove p t ai))
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
    move/forallP => H3 ai; move: (H3 ai) => H0.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
H:forall x : player,
[forall t,
   forall ai,
   ~~
   prec (preceq_V (e:=evalst g x)) 
     (GEutility t p) (GEutility t (bmove p t ai))]
i:player
H2:forall x : signal g i,
[forall ai,
   ~~
   prec (preceq_V (e:=evalst g i))
     (GEutility x p) (GEutility x (bmove p x ai))]
t:signal g i
H3:forall x : action g i,
~~
prec (preceq_V (e:=evalst g i)) 
  (GEutility t p) (GEutility t (bmove p t x))
ai:action g i
H0:~~
prec (preceq_V (e:=evalst g i)) 
  (GEutility t p) (GEutility t (bmove p t ai))
~
prec (preceq_V (e:=evalst g i)) (GEutility t p)
  (GEutility t (bmove p t ai))
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
    exact: negP H0.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p
  -
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
~~ NashEqb p -> ~ NashEq p move/forallPn => [] x.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
x:player
~~
[forall t,
   forall ai,
   ~~
   prec (preceq_V (e:=evalst g x)) (GEutility t p)
     (GEutility t (bmove p t ai))] -> ~ NashEq p
    move/forallPn => [] y.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
x:player
y:signal g x
~~
[forall ai,
   ~~
   prec (preceq_V (e:=evalst g x)) (GEutility y p)
     (GEutility y (bmove p y ai))] -> ~ NashEq p
    move/forallPn => [] z.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
x:player
y:signal g x
z:action g x
~~
~~
prec (preceq_V (e:=evalst g x)) (GEutility y p)
  (GEutility y (bmove p y z)) -> ~ NashEq p
    move/negPn => H2 Hne.
player:finType
g:game player
p:iprofile (signal g) (fun x : player => action g x)
x:player
y:signal g x
z:action g x
H2:prec (preceq_V (e:=evalst g x)) 
  (GEutility y p) (GEutility y (bmove p y z))
Hne:NashEq p
False
    by move/(_ x y z) in Hne.
  Qed.

End IGame.

Howson-Rosenthal-like transformation

We cast any incomplete game to a graphical game where players are the dependent pairs (player,signal) of the initial I-Game.

We show that erevy 'expected utility' value in the IGame is equal its corresponding 'global utility' value in the HG-Game. Thus, Nash equilibria are in correspondance.

Section HR.

  Lemma HowsonRosenthal :
    forall player (g : IGame.game player) i t p,
    @IGame.GEutility player g i t p
    = @HGGame.global_utility _ (IGame.to_hggame g) (existT _ i t)
                             (iprofile_flatten p).
forall (player : finType) (g : IGame.game player)
  (i : player) (t : IGame.signal g i)
  (p : iprofile (IGame.signal g)
         (fun x : player => IGame.action g x)),
IGame.GEutility t p =
HGGame.global_utility
  (existT (fun i0 : player => IGame.signal g i0) i t)
  (iprofile_flatten p)
  Proof.
forall (player : finType) (g : IGame.game player)
  (i : player) (t : IGame.signal g i)
  (p : iprofile (IGame.signal g)
         (fun x : player => IGame.action g x)),
IGame.GEutility t p =
HGGame.global_utility
  (existT (fun i0 : player => IGame.signal g i0) i t)
  (iprofile_flatten p)
  rewrite /IGame.GEutility /HGGame.global_utility
          /IGame.to_hggame => player g i t p //=.
player:finType
g:IGame.game player
i:player
t:IGame.signal g i
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
\big[oplus (IGame.evalst g i)/V0 (IGame.evalst g i)]_(theta | 
theta i == t)
   otimes (IGame.belief i theta)
     (IGame.utility i (proj_iprofile p theta) theta) =
\big[oplus (IGame.evalst g i)/V0 (IGame.evalst g i)]_(lg | 
lg i == t)
   otimes (IGame.belief i lg)
     (IGame.utility i
        (proj_flatprofile (iprofile_flatten p) lg) lg)
  apply eq_bigr => theta Htheta.
player:finType
g:IGame.game player
i:player
t:IGame.signal g i
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
theta:fprofile (IGame.signal g)
Htheta:theta i == t
otimes (IGame.belief i theta)
  (IGame.utility i (proj_iprofile p theta) theta) =
otimes (IGame.belief i theta)
  (IGame.utility i
     (proj_flatprofile (iprofile_flatten p) theta)
     theta)
  by rewrite -proj_iprof_flatprof.
  Qed.

  Lemma HowsonRosenthal_NashEqb :
    forall player (g : IGame.game player),
    forall  (p : iprofile (IGame.signal g) (IGame.action g)),
    @HGGame.NashEqb _ (IGame.to_hggame g) (iprofile_flatten p)
    = IGame.NashEqb p.
forall (player : finType) (g : IGame.game player)
  (p : iprofile (IGame.signal g)
         (fun x : player => IGame.action g x)),
HGGame.NashEqb (iprofile_flatten p) = IGame.NashEqb p
  Proof.
forall (player : finType) (g : IGame.game player)
  (p : iprofile (IGame.signal g)
         (fun x : player => IGame.action g x)),
HGGame.NashEqb (iprofile_flatten p) = IGame.NashEqb p
  move => player g p.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
HGGame.NashEqb (iprofile_flatten p) = IGame.NashEqb p
  apply/NFGame.NashEqP /IGame.NashEqP => /=.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
NFGame.NashEq (iprofile_flatten p) -> IGame.NashEq p
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
IGame.NashEq p -> NFGame.NashEq (iprofile_flatten p)
  -
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
NFGame.NashEq (iprofile_flatten p) -> IGame.NashEq p
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
IGame.NashEq p -> NFGame.NashEq (iprofile_flatten p) rewrite /NFGame.NashEq /IGame.NashEq => /= H i t ai.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:forall (i : {i : player & IGame.signal g i})
  (ai : IGame.action g (projT1 i)),
~
prec (preceq_V (e:=IGame.evalst g (projT1 i)))
  (HGGame.global_utility i (iprofile_flatten p))
  (HGGame.global_utility i
     (move (iprofile_flatten p) ai))
i:player
t:IGame.signal g i
ai:IGame.action g i
~
prec (preceq_V (e:=IGame.evalst g i))
  (IGame.GEutility t p)
  (IGame.GEutility t (bmove p t ai))
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
IGame.NashEq p -> NFGame.NashEq (iprofile_flatten p)
    move : (H (existT _ i t) ai).
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:forall (i : {i : player & IGame.signal g i})
  (ai : IGame.action g (projT1 i)),
~
prec (preceq_V (e:=IGame.evalst g (projT1 i)))
  (HGGame.global_utility i (iprofile_flatten p))
  (HGGame.global_utility i
     (move (iprofile_flatten p) ai))
i:player
t:IGame.signal g i
ai:IGame.action g i
~
prec
  (preceq_V
     (e:=IGame.evalst g
           (projT1
              (existT
                 (fun i : player => IGame.signal g i)
                 i t))))
  (HGGame.global_utility
     (existT (fun i : player => IGame.signal g i) i t)
     (iprofile_flatten p))
  (HGGame.global_utility
     (existT (fun i : player => IGame.signal g i) i t)
     (move (iprofile_flatten p) ai)) ->
~
prec (preceq_V (e:=IGame.evalst g i))
  (IGame.GEutility t p)
  (IGame.GEutility t (bmove p t ai))
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
IGame.NashEq p -> NFGame.NashEq (iprofile_flatten p)
    by rewrite {1}/iprofile_flatten !HowsonRosenthal move_bmove.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
IGame.NashEq p -> NFGame.NashEq (iprofile_flatten p)
  -
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
IGame.NashEq p -> NFGame.NashEq (iprofile_flatten p) rewrite /NFGame.NashEq /IGame.NashEq => /= H it ai.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:forall (i : player) (t : IGame.signal g i)
  (ai : IGame.action g i),
~
prec (preceq_V (e:=IGame.evalst g i))
  (IGame.GEutility t p)
  (IGame.GEutility t (bmove p t ai))
it:{i : player & IGame.signal g i}
ai:IGame.action g (projT1 it)
~
prec (preceq_V (e:=IGame.evalst g (projT1 it)))
  (HGGame.global_utility it (iprofile_flatten p))
  (HGGame.global_utility it
     (move (iprofile_flatten p) ai))
    have H' := (H (projT1 it) (projT2 it) ai).
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:forall (i : player) (t : IGame.signal g i)
  (ai : IGame.action g i),
~
prec (preceq_V (e:=IGame.evalst g i))
  (IGame.GEutility t p)
  (IGame.GEutility t (bmove p t ai))
it:{i : player & IGame.signal g i}
ai:IGame.action g (projT1 it)
H':~
prec (preceq_V (e:=IGame.evalst g (projT1 it)))
  (IGame.GEutility (projT2 it) p)
  (IGame.GEutility (projT2 it)
     (bmove p (projT2 it) ai))
~
prec (preceq_V (e:=IGame.evalst g (projT1 it)))
  (HGGame.global_utility it (iprofile_flatten p))
  (HGGame.global_utility it
     (move (iprofile_flatten p) ai))
    by rewrite {1 2 3 4}(sigT_eta it) move_bmove -!HowsonRosenthal.
  Qed.

  Lemma HowsonRosenthal_NashEq :
    forall player (g : IGame.game player),
    forall  (p : iprofile (IGame.signal g) (IGame.action g)),
    @HGGame.NashEq _ (IGame.to_hggame g) (iprofile_flatten p)
    <-> IGame.NashEq p.
forall (player : finType) (g : IGame.game player)
  (p : iprofile (IGame.signal g)
         (fun x : player => IGame.action g x)),
HGGame.NashEq (iprofile_flatten p) <-> IGame.NashEq p
  Proof.
forall (player : finType) (g : IGame.game player)
  (p : iprofile (IGame.signal g)
         (fun x : player => IGame.action g x)),
HGGame.NashEq (iprofile_flatten p) <-> IGame.NashEq p
  split => H.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:HGGame.NashEq (iprofile_flatten p)
IGame.NashEq p
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:IGame.NashEq p
HGGame.NashEq (iprofile_flatten p)
  -
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:HGGame.NashEq (iprofile_flatten p)
IGame.NashEq p
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:IGame.NashEq p
HGGame.NashEq (iprofile_flatten p) apply/IGame.NashEqP; move/HGGame.NashEqP in H.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:HGGame.NashEqb (iprofile_flatten p)
IGame.NashEqb p
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:IGame.NashEq p
HGGame.NashEq (iprofile_flatten p)
    by rewrite -(HowsonRosenthal_NashEqb p).
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:IGame.NashEq p
HGGame.NashEq (iprofile_flatten p)
  -
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:IGame.NashEq p
HGGame.NashEq (iprofile_flatten p) apply/HGGame.NashEqP; move/IGame.NashEqP in H.
player:finType
g:IGame.game player
p:iprofile (IGame.signal g)
  (fun x : player => IGame.action g x)
H:IGame.NashEqb p
HGGame.NashEqb (iprofile_flatten p)
    by rewrite (HowsonRosenthal_NashEqb p).
  Qed.

End HR.