# Theory Quantum_Prisoners_Dilemma

(*
authors:
Yijun He, University of Cambridge, yh403@cam.ac.uk
with contributions by Anthony Bordg and Hanna Lachnitt.
*)

section ‹Quantum Prisoner's Dilemma›

theory Quantum_Prisoners_Dilemma
imports
More_Tensor
Measurement
Basics
begin

text ‹
In the 2-parameter strategic space of Eisert, Wilkens and Lewenstein [EWL], Prisoner's Dilemma
ceases to pose a dilemma if quantum strategies are allowed for. Indeed, Alice and Bob both choosing
to defect is no longer a Nash equilibrium. However, a new Nash equilibrium appears which is at the
same time Pareto optimal. Moreover, there exists a quantum strategy which always gives reward if
played against any classical strategy.
Below the parameter @{text "γ"} can be seen as a measure of the game's entanglement. The game behaves
classically if @{text "γ"} = 0, and for the maximally entangled case (@{text "γ"} = 2*$\pi$) the dilemma disappears
as pointed out above.
›

subsection ‹The Set-Up›

locale prisoner =
fixes γ:: "real"
assumes "γ  pi/2" and "γ  0"

abbreviation (in prisoner) J ::  where
"J  mat_of_cols_list 4  [[cos(γ/2), 0, 0, 𝗂*sin(γ/2)],
[0, cos(γ/2), -𝗂*sin(γ/2), 0],
[0, -𝗂*sin(γ/2), cos(γ/2), 0],
[𝗂*sin(γ/2), 0, 0, cos(γ/2)]]"

abbreviation (in prisoner) ψ1 ::  where
"ψ1  mat_of_cols_list 4 [[cos(γ/2), 0, 0, 𝗂*sin(γ/2)]]"

lemma (in prisoner) psi_one:
shows
proof
fix i j assume a0:"i < dim_row ψ1" and a1:"j < dim_col ψ1"
then have "(J * |unit_vec 4 0) $$(i,j) = (k<4. (J$$ (i,k)) * ( |unit_vec 4 0 $$(k,j)))" using mat_of_cols_list_def ket_vec_def by auto also have "... = (k{0,1,2,3}. (J$$ (i,k)) * ( |unit_vec 4 0 $$(k,j)))" using set_4 atLeast0LessThan by simp also have "... = ψ1$$ (i,j)"
proof-
have "i{0,1,2,3}  j=0"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def by auto
qed
finally show "(J * |unit_vec 4 0) $$(i,j) = ψ1$$ (i,j)" by simp
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by (simp add: ket_vec_def)
qed

locale strategic_space_2p = prisoner +
fixes θA:: "real"
and φA:: "real"
and θB:: "real"
and φB:: "real"
assumes "0  θA  θA  pi"
and "0  φA  φA  pi/2"
and "0  θB  θB  pi"
and "0  φB  φB  pi/2"

abbreviation (in strategic_space_2p) UA ::  where
"UA  mat_of_cols_list 2 [[exp(𝗂*φA)*cos(θA/2), -sin(θA/2)],
[sin(θA/2), exp(-𝗂*φA)*cos(θA/2)]]"

abbreviation (in strategic_space_2p) UB ::  where
"UB  mat_of_cols_list 2 [[exp(𝗂*φB)*cos(θB/2), -sin(θB/2)],
[sin(θB/2), exp(-𝗂*φB)*cos(θB/2)]]"

abbreviation (in strategic_space_2p) ψ2 ::  where
"ψ2
mat_of_cols_list 4 [[exp(𝗂*φA)*cos(θA/2) * exp(𝗂*φB)*cos(θB/2) * cos(γ/2) + sin(θA/2) * sin(θB/2) * 𝗂*sin(γ/2),
exp(𝗂*φA)*cos(θA/2) * -sin(θB/2) * cos(γ/2) + sin(θA/2) * exp(-𝗂*φB)*cos(θB/2) * 𝗂*sin(γ/2),
-sin(θA/2) * exp(𝗂*φB)*cos(θB/2) * cos(γ/2) + exp(-𝗂*φA)*cos(θA/2) * sin(θB/2) * 𝗂*sin(γ/2),
sin(θA/2) * sin(θB/2) * cos(γ/2) + exp(-𝗂*φA)*cos(θA/2) * exp(-𝗂*φB)*cos(θB/2) * 𝗂*sin(γ/2)]]"

abbreviation (in strategic_space_2p) UAB ::  where
"UAB
mat_of_cols_list 4 [[exp(𝗂*φA)*cos(θA/2) * exp(𝗂*φB)*cos(θB/2), exp(𝗂*φA)*cos(θA/2) * -sin(θB/2),
-sin(θA/2) * exp(𝗂*φB)*cos(θB/2), -sin(θA/2) * -sin(θB/2)],
[exp(𝗂*φA)*cos(θA/2) * sin(θB/2), exp(𝗂*φA)*cos(θA/2) * exp(-𝗂*φB)*cos(θB/2),
-sin(θA/2) * sin(θB/2), -sin(θA/2) * exp(-𝗂*φB)*cos(θB/2)],
[sin(θA/2) * exp(𝗂*φB)*cos(θB/2), -sin(θA/2) * sin(θB/2),
exp(-𝗂*φA)*cos(θA/2) * exp (𝗂*φB)*cos(θB/2), exp(-𝗂*φA)*cos(θA/2) * -sin(θB/2)],
[sin(θA/2) * sin(θB/2), sin(θA/2) * exp(-𝗂*φB)*cos(θB/2),
exp(-𝗂*φA)*cos(θA/2) * sin(θB/2), exp (-𝗂*φA)*cos(θA/2) * exp(-𝗂*φB)*cos(θB/2)]]"

lemma (in strategic_space_2p) UA_tensor_UB:
shows "(UA  UB) = UAB"
proof
fix i j assume a0:  and a1:
then have "i{0,1,2,3}  j{0,1,2,3}"
using mat_of_cols_list_def by auto
then show "(UA  UB) $$(i,j) = UAB$$ (i,j)"
using mat_of_cols_list_def by auto
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by simp
qed

lemma (in strategic_space_2p) psi_two:
shows "(UA  UB) * ψ1 = ψ2"
proof
fix i j
assume a0:"i < dim_row ψ2" and a1:"j < dim_col ψ2"
then show "((UA  UB) * ψ1) $$(i,j) = ψ2$$ (i,j)"
proof-
have "i{0,1,2,3}  j=0"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def UA_tensor_UB set_4 by auto
qed
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by simp
qed

abbreviation (in prisoner) J_cnj ::  where
"J_cnj  mat_of_cols_list 4 [[cos(γ/2), 0, 0, -𝗂*sin(γ/2)],
[0, cos(γ/2), 𝗂*sin(γ/2), 0],
[0, 𝗂*sin(γ/2), cos(γ/2), 0],
[-𝗂*sin(γ/2), 0, 0, cos(γ/2)]]"

lemma (in prisoner) hermite_cnj_of_J [simp]:
shows
proof
fix i j assume a0: and a1:
then show "J $$(i,j) = J_cnj$$ (i,j)"
proof-
have "i{0,1,2,3}  j{0,1,2,3}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def dagger_def by auto
qed
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by simp
qed

abbreviation (in strategic_space_2p) ψf ::  where
"ψf  mat_of_cols_list 4 [[
cos(γ/2) * (exp(𝗂*φA)*cos(θA/2) * exp(𝗂*φB)*cos(θB/2) * cos(γ/2) + sin(θA/2) * sin(θB/2) * 𝗂*sin(γ/2))
+ (-𝗂*sin(γ/2)) * (sin(θA/2) * sin(θB/2) * cos(γ/2) + exp(-𝗂*φA)*cos(θA/2) * exp(-𝗂*φB)*cos(θB/2) * 𝗂*sin(γ/2)),

cos(γ/2) * (exp(𝗂*φA)*cos(θA/2) * -sin(θB/2) * cos(γ/2) + sin(θA/2) * exp(-𝗂*φB)*cos(θB/2) * 𝗂*sin(γ/2))
+ (𝗂*sin(γ/2)) * (-sin(θA/2) * exp(𝗂*φB)*cos(θB/2) * cos(γ/2) + exp(-𝗂*φA)*cos(θA/2) * sin(θB/2) * 𝗂*sin(γ/2)),

(𝗂*sin(γ/2)) * (exp(𝗂*φA)*cos(θA/2) * -sin(θB/2) * cos(γ/2) + sin(θA/2) * exp(-𝗂*φB)*cos(θB/2) * 𝗂*sin(γ/2))
+ cos(γ/2) * (-sin(θA/2) * exp(𝗂*φB)*cos(θB/2) * cos(γ/2) + exp(-𝗂*φA)*cos(θA/2) * sin(θB/2) * 𝗂*sin(γ/2)),

(-𝗂*sin(γ/2)) * (exp(𝗂*φA)*cos(θA/2) * exp(𝗂*φB)*cos(θB/2) * cos(γ/2) + sin(θA/2) * sin(θB/2) * 𝗂*sin(γ/2))
+ cos(γ/2) * (sin(θA/2) * sin(θB/2) * cos(γ/2) + exp(-𝗂*φA)*cos(θA/2) * exp(-𝗂*φB)*cos(θB/2) * 𝗂*sin(γ/2))
]]"

lemma (in strategic_space_2p) psi_f:
shows "(J) * ψ2 = ψf"
proof
fix i j assume a0:"i < dim_row ψf" and a1:"j < dim_col ψf"
then show "((J) * ψ2) $$(i,j) = ψf$$ (i,j)"
proof-
have "i{0,1,2,3}  j=0"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def set_4 hermite_cnj_of_J by auto
qed
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by simp
qed

lemma (in prisoner) unit_vec_4_0_ket_is_state:
shows "state 2 |unit_vec 4 0"
using state_def cpx_vec_length_def ket_vec_def unit_vec_def by (auto simp add: set_4)

"complex_of_real (cos (γ/2)) * complex_of_real (cos (γ/2)) -
𝗂*complex_of_real (sin (γ/2)) * (𝗂*complex_of_real (sin (γ/2))) = 1"

"𝗂*complex_of_real (sin (γ/2)) * (𝗂*complex_of_real (sin (γ/2))) -
complex_of_real (cos (γ/2)) * complex_of_real (cos (γ/2)) = -1"

lemma (in prisoner) J_cnj_times_J:
shows "J * J = 1m 4"
proof
fix i j assume a0:"i < dim_row (1m 4)" and a1:"j < dim_col (1m 4)"
then show "(J * J) $$(i,j) = 1m 4$$ (i,j)"
proof-
have "i{0,1,2,3}  j{0,1,2,3}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def hermite_cnj_of_J set_4 cos_sin_squared_add_cpx by auto
qed
next
show "dim_row (J * J) = dim_row (1m 4)"
using mat_of_cols_list_def by simp
next
show "dim_col (J * J) = dim_col (1m 4)"
using mat_of_cols_list_def by simp
qed

lemma (in prisoner) J_times_J_cnj:
shows "J * (J) = 1m 4"
proof
fix i j assume a0:"i < dim_row (1m 4)" and a1:"j < dim_col (1m 4)"
then show "(J * (J)) $$(i,j) = 1m 4$$ (i,j)"
proof-
have "i{0,1,2,3}  j{0,1,2,3}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def hermite_cnj_of_J set_4 cos_sin_squared_add_cpx by auto
qed
next
show "dim_row (J * (J)) = dim_row (1m 4)"
using mat_of_cols_list_def by simp
next
show "dim_col (J * (J)) = dim_col (1m 4)"
using mat_of_cols_list_def by simp
qed

lemma (in prisoner) J_is_gate:
shows "gate 2 J"
proof
show "dim_row J = 22"
using mat_of_cols_list_def by simp
moreover show
using mat_of_cols_list_def by simp
ultimately show "unitary J"
using mat_of_cols_list_def unitary_def J_cnj_times_J J_times_J_cnj by auto
qed

lemma (in strategic_space_2p) psi_one_is_state:
shows "state 2 ψ1"
proof-
have "state 2 (J * |unit_vec 4 0)"
using unit_vec_4_0_ket_is_state J_is_gate by auto
then show ?thesis
using psi_one by simp
qed

abbreviation (in strategic_space_2p) UA_cnj ::  where
"UA_cnj  mat_of_cols_list 2 [[(exp(-𝗂*φA))*cos(θA/2), sin(θA/2)],
[-sin(θA/2), (exp (𝗂*φA))*cos(θA/2)]]"

abbreviation (in strategic_space_2p) UB_cnj ::  where
"UB_cnj  mat_of_cols_list 2 [[(exp(-𝗂*φB))*cos(θB/2), sin(θB/2)],
[-sin(θB/2), (exp(𝗂*φB))*cos(θB/2)]]"

lemma (in strategic_space_2p) hermite_cnj_of_UA:
shows
proof
fix i j assume a0: and a1:
then show "UA $$(i,j) = UA_cnj$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def dagger_def exp_of_real_cnj exp_of_real_cnj2 by auto
qed
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by simp
qed

lemma (in strategic_space_2p) hermite_cnj_of_UB:
shows
proof
fix i j assume a0: and a1:
then show "UB $$(i,j) = UB_cnj$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def dagger_def exp_of_real_cnj exp_of_real_cnj2 by auto
qed
next
show
using mat_of_cols_list_def by simp
next
show
using mat_of_cols_list_def by simp
qed

fixes x y :: real
shows "exp (- (𝗂 * x)) * cos (y) * (exp (𝗂 * x) * cos (y)) + sin(y) * sin(y) = 1"
proof-
have "exp (- (𝗂 * x)) * cos (y) * (exp (𝗂 * x) * cos (y)) = cos(y) * cos(y)"
using exp_minus_inverse by (auto simp add: algebra_simps)
then show ?thesis
qed

lemma (in strategic_space_2p) UA_cnj_times_UA:
shows
proof
fix i j assume a0:"i < dim_row (1m 2)" and a1:"j < dim_col (1m 2)"
then show "(UA * UA) $$(i,j) = 1m 2$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (UA * UA) = dim_row (1m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (UA * UA) = dim_col (1m 2)"
using mat_of_cols_list_def by simp
qed

lemma (in strategic_space_2p) UA_times_UA_cnj:
shows "UA * (UA) = 1m 2"
proof
fix i j assume a0:"i < dim_row (1m 2)" and a1:"j < dim_col (1m 2)"
then show "(UA * (UA)) $$(i,j) = 1m 2$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (UA * (UA)) = dim_row (1m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (UA * (UA)) = dim_col (1m 2)"
using mat_of_cols_list_def by simp
qed

lemma (in strategic_space_2p) UB_cnj_times_UB:
shows
proof
fix i j assume a0:"i < dim_row (1m 2)" and a1:"j < dim_col (1m 2)"
then show "(UB * UB) $$(i,j) = 1m 2$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (UB * UB) = dim_row (1m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (UB * UB) = dim_col (1m 2)"
using mat_of_cols_list_def by simp
qed

lemma (in strategic_space_2p) UB_times_UB_cnj:
shows "UB * (UB) = 1m 2"
proof
fix i j assume a0:"i < dim_row (1m 2)" and a1:"j < dim_col (1m 2)"
then show "(UB * (UB)) $$(i,j) = 1m 2$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
by (auto simp add: set_2 algebra_simps)
qed
next
show "dim_row (UB * (UB)) = dim_row (1m 2)"
using mat_of_cols_list_def by simp
next
show "dim_col (UB * (UB)) = dim_col (1m 2)"
using mat_of_cols_list_def by simp
qed

lemma (in strategic_space_2p) UA_is_gate:
shows "gate 1 UA"
proof
show
using mat_of_cols_list_def by simp
moreover show
using mat_of_cols_list_def by simp
ultimately show
using mat_of_cols_list_def unitary_def UA_cnj_times_UA UA_times_UA_cnj by auto
qed

lemma (in strategic_space_2p) UB_is_gate:
shows "gate 1 UB"
proof
show
using mat_of_cols_list_def by simp
moreover show
using mat_of_cols_list_def by simp
ultimately show
using mat_of_cols_list_def unitary_def UB_cnj_times_UB UB_times_UB_cnj by auto
qed

lemma (in strategic_space_2p) UAB_is_gate:
shows "gate 2 (UA  UB)"
proof-
have "gate (1+1) (UA  UB)"
using UA_is_gate UB_is_gate tensor_gate[of "1" "UA" "1" "UB"] by auto
then show ?thesis
qed

lemma (in strategic_space_2p) psi_two_is_state:
shows "state 2 ψ2"
proof-
have "state 2 ((UA  UB) * ψ1)"
using psi_one_is_state UAB_is_gate by auto
then show ?thesis
using psi_two by simp
qed

lemma (in strategic_space_2p) J_cnj_is_gate:
shows "gate 2 (J)"
proof
show "dim_row (J) = 22"
using mat_of_cols_list_def by simp
moreover show "square_mat (J)"
using mat_of_cols_list_def by simp
moreover have "(J) = J"
using dagger_of_dagger_is_id by auto
ultimately show "unitary (J)"
using mat_of_cols_list_def unitary_def J_cnj_times_J J_times_J_cnj by auto
qed

lemma (in strategic_space_2p) psi_f_is_state:
shows "state 2 ψf"
proof-
have "state 2 ((J) * ψ2)"
using psi_two_is_state J_cnj_is_gate by auto
then show ?thesis
using psi_f by simp
qed

(* equation (1) in the paper *)
lemma (in strategic_space_2p) equation_one:
shows "(J) * ((UA  UB) * (J * |unit_vec 4 0)) = ψf"
using psi_one psi_two psi_f by auto

abbreviation (in strategic_space_2p) prob00 ::  where
"prob00 v  if state 2 v then (cmod (v $$(0,0)))2 else undefined" abbreviation (in strategic_space_2p) prob01 :: where "prob01 v if state 2 v then (cmod (v$$ (1,0)))2 else undefined"

abbreviation (in strategic_space_2p) prob10 ::  where
"prob10 v  if state 2 v then (cmod (v $$(2,0)))2 else undefined" abbreviation (in strategic_space_2p) prob11 :: where "prob11 v if state 2 v then (cmod (v$$ (3,0)))2 else undefined"

definition (in strategic_space_2p) alice_payoff :: "real" where
"alice_payoff  3 * (prob00 ψf) + 1 * (prob11 ψf) + 0 * (prob01 ψf) + 5 * (prob10 ψf)"

definition (in strategic_space_2p) bob_payoff :: "real" where
"bob_payoff  3 * (prob00 ψf) + 1 * (prob11 ψf) + 5 * (prob01 ψf) + 0 * (prob10 ψf)"

definition (in strategic_space_2p) is_nash_eq :: "bool" where
"is_nash_eq
(tA pA. strategic_space_2p γ tA pA θB φB
alice_payoff  strategic_space_2p.alice_payoff γ tA pA θB φB)

(tB pB. strategic_space_2p γ θA φA tB pB
bob_payoff  strategic_space_2p.bob_payoff γ θA φA tB pB)"

definition (in strategic_space_2p) is_pareto_opt :: "bool" where
"is_pareto_opt  tA pA tB pB. strategic_space_2p γ tA pA tB pB
((strategic_space_2p.alice_payoff γ tA pA tB pB > alice_payoff
strategic_space_2p.bob_payoff γ tA pA tB pB < bob_payoff)
(strategic_space_2p.bob_payoff γ tA pA tB pB > bob_payoff
strategic_space_2p.alice_payoff γ tA pA tB pB < alice_payoff))"

lemma (in strategic_space_2p) sum_of_prob:
fixes v ::
assumes "state 2 v"
shows "(prob00 v) + (prob11 v) + (prob01 v) + (prob10 v) = 1"
proof-
have "(prob00 v) + (prob11 v) + (prob01 v) + (prob10 v) =
(cmod (v $$(0,0)))2 + (cmod (v$$ (1,0)))2 + (cmod (v $$(2,0)))2 + (cmod (v$$ (3,0)))2"
using assms by auto
then show ?thesis
using state_def assms cpx_vec_length_def by (auto simp add: set_4)
qed

lemma (in strategic_space_2p) sum_payoff_le_6:
fixes tA pA tB pB :: real
shows
proof-
have
using alice_payoff_def bob_payoff_def psi_f_is_state by auto
then have
using psi_f_is_state by (auto simp add: algebra_simps)
moreover have
using sum_of_prob[of "ψf"] psi_f_is_state by auto
ultimately show ?thesis
by auto
qed

lemma (in strategic_space_2p) coop_is_pareto_opt:
assumes
shows
using is_pareto_opt_def strategic_space_2p.sum_payoff_le_6 assms by fastforce

subsection ‹The Separable Case›

lemma (in strategic_space_2p) separable_case_CC: (* both player cooperate *)
assumes "γ = 0"
shows "φA = 0  θA = 0  φB = 0  θB = 0  alice_payoff = 3  bob_payoff = 3"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx psi_f_is_state by auto

lemma (in strategic_space_2p) separable_case_DD: (* both player defect *)
assumes "γ = 0"
shows "φA = 0  θA = pi  φB = 0  θB = pi  alice_payoff = 1  bob_payoff = 1"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx psi_f_is_state by auto

lemma (in strategic_space_2p) separable_case_DC: (* Alice defects, and Bob cooperates *)
assumes "γ = 0"
shows "φA = 0  θA = pi  φB = 0  θB = 0  alice_payoff = 5  bob_payoff = 0"
using alice_payoff_def bob_payoff_def sin_cos_squared_add_cpx psi_f_is_state by auto

lemma (in strategic_space_2p) separable_alice_payoff_DB:
(* Alice's payoff in the separable case given that Bob defects *)
assumes "γ = 0" and "φB = 0  θB = pi"
shows
using alice_payoff_def assms sin_squared_le_one psi_f_is_state by auto

lemma (in strategic_space_2p) separable_bob_payoff_DA:
(* Bob's payoff in the separable case given that Alice defects *)
assumes "γ = 0" and "φA = 0  θA = pi"
shows
using bob_payoff_def assms sin_squared_le_one psi_f_is_state by auto

lemma (in strategic_space_2p) separable_case_DD_alice_opt:
assumes "γ = 0" and "φA = 0  θA = pi  φB = 0  θB = pi"
shows "tA pA. strategic_space_2p γ tA pA θB φB  strategic_space_2p.alice_payoff γ tA pA θB φB  alice_payoff"
proof
fix tA pA assume "strategic_space_2p γ tA pA θB φB"
then show "strategic_space_2p.alice_payoff γ tA pA θB φB  alice_payoff"
using separable_case_DD strategic_space_2p.separable_alice_payoff_DB assms by auto
qed

lemma (in strategic_space_2p) separable_case_DD_bob_opt:
assumes "γ = 0" and "φA = 0  θA = pi  φB = 0  θB = pi"
shows "tB pB. strategic_space_2p γ θA φA tB pB  strategic_space_2p.bob_payoff γ θA φA tB pB  bob_payoff"
proof
fix tB pB assume "strategic_space_2p γ θA φA tB pB"
then show "strategic_space_2p.bob_payoff γ θA φA tB pB  bob_payoff"
using separable_case_DD strategic_space_2p.separable_bob_payoff_DA assms by auto
qed

lemma (in strategic_space_2p) separable_case_DD_is_nash_eq:
assumes "γ = 0"
shows "φA = 0  θA = pi  φB = 0  θB = pi  is_nash_eq"
using is_nash_eq_def separable_case_DD_alice_opt separable_case_DD_bob_opt assms by auto

lemma (in strategic_space_2p) separable_case_CC_is_not_nash_eq:
assumes "γ = 0"
shows "φA = 0  θA = 0  φB = 0  θB = 0  ¬ is_nash_eq"
proof
assume asm:"φA = 0  θA = 0  φB = 0  θB = 0"
then have f0:"strategic_space_2p γ pi 0 θB φB"
using strategic_space_2p_def strategic_space_2p_axioms_def prisoner_def asm by (simp add: assms)
then have "strategic_space_2p.alice_payoff γ pi 0 θB φB = 5"
using strategic_space_2p.separable_case_DC assms asm by blast
moreover have
using separable_case_CC assms asm by blast
ultimately have
using f0 by simp
then show
using is_nash_eq_def by fastforce
qed

lemma (in strategic_space_2p) separable_case_CC_is_pareto_optimal:
assumes "γ = 0"
shows "φA = 0  θA = 0  φB = 0  θB = 0  is_pareto_opt"
using coop_is_pareto_opt separable_case_CC assms by auto

subsection ‹The Maximally Entangled Case›

lemma exp_to_sin:
fixes x:: real
shows "exp (𝗂 * x) - exp (-(𝗂 * x)) = 2 * 𝗂 * (sin x)"
using exp_of_real exp_of_real_inv by simp

lemma exp_to_cos:
fixes x:: real
shows "exp (𝗂 * x) + exp (-(𝗂 * x)) = 2 * (cos x)"
using exp_of_real exp_of_real_inv by simp

lemma cmod_real_prod_squared:
fixes x y:: real
shows

lemma quantum_payoff_simp:
fixes x y:: real
shows "3 * (cmod (complex_of_real (sin x) * complex_of_real (cos y)))2 +
(cmod (complex_of_real (cos x) * complex_of_real (cos y)))2 =
2 * (sin x)2 * (cos y)2 + (cos y)2"
proof-
have "3 * (sin x)2 * (cos y)2 + (cos x)2 * (cos y)2 =
(2 * (sin x)2 * (cos y)2) + ((sin x)2 + (cos x)2) * (cos y)2"
then show ?thesis
qed

lemma quantum_payoff_le_3:
fixes x y:: real
shows "2 * (sin x)2 * (cos y)2 + (cos y)2  3"
proof-
have "(sin x)2 * (cos y)2  1" by (simp add: sin_squared_le_one cos_squared_le_one mult_le_one)
then have "2 * (sin x)2 * (cos y)2  2" by simp
moreover have "(cos y)2  1"
using cos_squared_le_one[of "y"] by simp
ultimately show ?thesis by simp
qed

lemma sqrt_two_squared_cpx:
by (metis mult_2_right numeral_Bit0 of_real_mult of_real_numeral real_sqrt_four real_sqrt_mult)

lemma hidden_sqrt_two_squared_cpx: "complex_of_real (sqrt 2) * (complex_of_real (sqrt 2) * x) / 4 = x/2"
using sqrt_two_squared_cpx by (auto simp add: algebra_simps)

lemma (in strategic_space_2p) max_entangled_DD:
(* both players defects in the maximally entangled case *)
assumes "γ = pi/2"
shows "φA = 0  θA = pi  φB = 0  θB = pi  alice_payoff = 1  bob_payoff = 1"
by auto

lemma (in strategic_space_2p) max_entangled_QQ:
(* both players play the move Q in the maximally entangled case *)
assumes "γ = pi/2"
shows "φA = pi/2  θA = 0  φB = pi/2  θB = 0  alice_payoff = 3  bob_payoff = 3"
using alice_payoff_def bob_payoff_def sin_cos_squared_add_cpx exp_of_half_pi exp_of_minus_half_pi psi_f_is_state
by auto

lemma (in strategic_space_2p) max_entangled_QD:
(* Alice plays the move Q, and Bob defects in the maximally entangled case *)
assumes "γ = pi/2"
shows "φA = pi/2  θA = 0  φB = 0  θB = pi  alice_payoff = 5  bob_payoff = 0"
using alice_payoff_def bob_payoff_def cos_sin_squared_add_cpx exp_of_half_pi exp_of_minus_half_pi
psi_f_is_state sqrt_two_squared_cpx
by (auto simp add: assms algebra_simps sin_45 cos_45)

lemma (in strategic_space_2p) max_entangled_alice_payoff_QB:
(* Alice's payoff in the maximally entangled case given that Bob plays the move Q *)
assumes "γ = pi/2"
shows "φB = pi/2  θB = 0  alice_payoff  3"
proof
assume asm:"φB = pi/2  θB = 0"
have "ψf $$(0,0) = -(sin φA) * (cos (θA/2))" proof- have "ψf$$ (0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θA/2)) * exp (𝗂 * φA) +
𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θA/2)) * -exp (-(𝗂 * φA))"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψf $$(0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θA/2)) * (exp (𝗂 * φA) - exp (-(𝗂 * φA)))" by (auto simp add: algebra_simps) then have "ψf$$ (0,0) = 𝗂 * (cos (θA/2)) * (1/2) * (exp (𝗂 * φA) - exp (-(𝗂 * φA)))"
using sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_sin by (simp add: algebra_simps)
qed
moreover have "ψf $$(1,0) = sin (θA/2)" using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"]) moreover have "ψf$$ (2,0) = 0"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
moreover have "ψf $$(3,0) = (cos φA) * (cos (θA/2))" proof- have "ψf$$ (3,0) = exp (𝗂 * φA) * (cos (θA/2)) * (sqrt 2/2) * (sqrt 2/2) +
exp (- (𝗂 * φA)) * (cos (θA/2)) * (sqrt 2/2) * (sqrt 2/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψf $$(3,0) = (exp (𝗂 * φA) + exp (-(𝗂 * φA))) * (cos (θA/2)) * (sqrt 2/2) * (sqrt 2/2)" by (auto simp add: algebra_simps) then have "ψf$$ (3,0) = (exp (𝗂 * φA) + exp (-(𝗂 * φA))) * (cos (θA/2)) * (1/2)"
using sqrt_two_squared_cpx hidden_sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_cos by (simp add: algebra_simps)
qed
ultimately show
using alice_payoff_def psi_f_is_state quantum_payoff_simp quantum_payoff_le_3
by auto
qed

lemma (in strategic_space_2p) max_entangled_bob_payoff_QA:
(* Bob's payoff in the maximally entangled case given that Alice plays the move Q *)
assumes "γ = pi/2"
shows "φA = pi/2  θA = 0  bob_payoff  3"
proof
assume asm:"φA = pi/2  θA = 0"
have "ψf $$(0,0) = -(sin φB) * (cos (θB/2))" proof- have "ψf$$ (0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θB/2)) * exp (𝗂 * φB) +
𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θB/2)) * -exp (-(𝗂 * φB))"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψf $$(0,0) = 𝗂 * (sqrt 2/2) * (sqrt 2/2) * (cos (θB/2)) * (exp (𝗂 * φB) - exp (-(𝗂 * φB)))" by (auto simp add: algebra_simps) then have "ψf$$ (0,0) = 𝗂 * (cos (θB/2)) * (1/2) * (exp (𝗂 * φB) - exp (-(𝗂 * φB)))"
using sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_sin by (simp add: algebra_simps)
qed
moreover have "ψf $$(1,0) = 0" using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps) moreover have "ψf$$ (2,0) = sin (θB/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi sqrt_two_squared_cpx
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
moreover have "ψf $$(3,0) = (cos φB) * (cos (θB/2))" proof- have "ψf$$ (3,0) = exp (𝗂 * φB) * (cos (θB/2)) * (sqrt 2/2) * (sqrt 2/2) +
exp (- (𝗂 * φB)) * (cos (θB/2)) * (sqrt 2/2) * (sqrt 2/2)"
using mat_of_cols_list_def asm assms exp_of_half_pi exp_of_minus_half_pi
by (auto simp add: sin_of_quarter_pi[of "γ"] cos_of_quarter_pi[of "γ"] algebra_simps)
then have "ψf $$(3,0) = (exp (𝗂 * φB) + exp (-(𝗂 * φB))) * (cos (θB/2)) * (sqrt 2/2) * (sqrt 2/2)" by (auto simp add: algebra_simps) then have "ψf$$ (3,0) = (exp (𝗂 * φB) + exp (-(𝗂 * φB))) * (cos (θB/2)) * (1/2)"
using sqrt_two_squared_cpx hidden_sqrt_two_squared_cpx by (auto simp add: algebra_simps)
then show ?thesis
using exp_to_cos by (simp add: algebra_simps)
qed
ultimately show "bob_payoff  3"
using bob_payoff_def psi_f_is_state quantum_payoff_simp quantum_payoff_le_3
by auto
qed

lemma (in strategic_space_2p) max_entangled_DD_is_not_nash_eq:
assumes "γ = pi/2"
shows "φA = 0  θA = pi  φB = 0  θB = pi  ¬is_nash_eq"
proof
assume asm:"φA = 0  θA = pi  φB = 0  θB = pi"
then have f0:"strategic_space_2p γ 0 (pi/2) θB φB"
using strategic_space_2p_def strategic_space_2p_axioms_def prisoner_def asm by (simp add: assms)
then have "strategic_space_2p.alice_payoff γ 0 (pi/2) θB φB = 5"
using strategic_space_2p.max_entangled_QD assms asm by blast
moreover have
using max_entangled_DD assms asm by blast
ultimately have "strategic_space_2p γ 0 (pi/2) θB φB  strategic_space_2p.alice_payoff γ 0 (pi/2) θB φB > alice_payoff"
using f0 by simp
then show
using is_nash_eq_def by fastforce
qed

lemma (in strategic_space_2p) max_entangled_alice_opt:
assumes "γ = pi/2" and "φA = pi/2  θA = 0  φB = pi/2  θB = 0"
shows "tA pA. strategic_space_2p γ tA pA θB φB  strategic_space_2p.alice_payoff γ tA pA θB φB  alice_payoff"
proof
fix tA pA assume "strategic_space_2p γ tA pA θB φB"
then have "strategic_space_2p.alice_payoff γ tA pA θB φB  3"
using strategic_space_2p.max_entangled_alice_payoff_QB assms by blast
moreover have
using max_entangled_QQ assms by blast
ultimately show "strategic_space_2p.alice_payoff γ tA pA θB φB  alice_payoff"
by simp
qed

lemma (in strategic_space_2p) max_entangled_bob_opt:
assumes "γ = pi/2" and "φA = pi/2  θA = 0  φB = pi/2  θB = 0"
shows "tB pB. strategic_space_2p γ θA φA tB pB  strategic_space_2p.bob_payoff γ θA φA tB pB  bob_payoff"
proof
fix tB pB assume "strategic_space_2p γ θA φA tB pB"
then have "strategic_space_2p.bob_payoff γ θA φA tB pB  3"
using strategic_space_2p.max_entangled_bob_payoff_QA assms by blast
moreover have "bob_payoff = 3"
using max_entangled_QQ assms by blast
ultimately show "strategic_space_2p.bob_payoff γ θA φA tB pB  bob_payoff"
by simp
qed

lemma (in strategic_space_2p) max_entangled_QQ_is_nash_eq:
assumes "γ = pi/2"
shows "φA = pi/2  θA = 0  φB = pi/2  θB = 0  is_nash_eq"
using max_entangled_alice_opt max_entangled_bob_opt is_nash_eq_def assms by blast

lemma (in strategic_space_2p) max_entangled_QQ_is_pareto_optimal:
assumes "γ = pi/2"
shows "φA = pi/2  θA = 0  φB = pi/2  θB = 0  is_pareto_opt"
using coop_is_pareto_opt max_entangled_QQ assms by blast

subsection ‹The Unfair Strategy Case›

lemma half_sqrt_two_squared: "2 * (sqrt 2 / 2)2 = 1"

lemma (in strategic_space_2p) max_entangled_MD:
(* Alice plays the "miracle move", and Bob plays the classical defect move in the maximally entangled case *)
assumes "γ = pi/2"
shows "φA = pi/2  θA = pi/2  φB = 0  θB = pi  alice_payoff = 3  bob_payoff = 1/2"
proof
assume asm:"φA = pi/2  θA = pi/2  φB = 0  θB = pi"
show
using alice_payoff_def bob_payoff_def sqrt_two_squared_cpx half_sqrt_two_squared
exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] psi_f_is_state
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
qed

lemma (in strategic_space_2p) max_entangled_MC:
(* Alice plays the "miracle move", and Bob plays the classical defect move in the maximally entangled case *)
assumes "γ = pi/2"
shows "φA = pi/2  θA = pi/2  φB = 0  θB = 0  alice_payoff = 3  bob_payoff = 1/2"
proof
assume asm:"φA = pi/2  θA = pi/2  φB = 0  θB = 0"
show
using alice_payoff_def bob_payoff_def sqrt_two_squared_cpx half_sqrt_two_squared
exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] psi_f_is_state
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
qed

lemma (in strategic_space_2p) max_entangled_MH:
(* Alice plays the "miracle move", and Bob plays the classical half move in the maximally entangled case *)
assumes "γ = pi/2"
shows "φA = pi/2  θA = pi/2  φB = 0  θB = pi/2  alice_payoff = 1  bob_payoff = 1"
proof
assume asm:"φA = pi/2  θA = pi/2  φB = 0  θB = pi/2"
show
using alice_payoff_def bob_payoff_def sqrt_two_squared_cpx half_sqrt_two_squared
exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] psi_f_is_state
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
qed

(* This is the definition of M in equation (9) *)
abbreviation M ::  where
"M  mat_of_cols_list 2 [[𝗂 * sqrt(2)/2, -1 * sqrt(2)/2],
[1 * sqrt(2)/2, -𝗂 * sqrt(2)/2]]"

lemma (in strategic_space_2p) M_correct:
assumes "φA = pi/2  θA = pi/2"
shows "UA = M"
proof
show  using mat_of_cols_list_def by simp
show  using mat_of_cols_list_def by simp
fix i j assume a0:"i < dim_row M" and a1:"j < dim_col M"
then show "UA $$(i,j) = M$$ (i,j)"
proof-
have "i{0,1}  j{0,1}"
using a0 a1 mat_of_cols_list_def by auto
thus ?thesis
using mat_of_cols_list_def exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"]
by (auto simp add: assms sin_45 cos_45)
qed
qed

lemma hidden_sqrt_two_squared_cpx2:
fixes x y :: complex
shows "(sqrt 2) * ((sqrt 2) * (x * y)) / 2 = x * y"
using sqrt_two_squared_cpx by auto

lemma (in strategic_space_2p) unfair_strategy_no_benefit:
(* Two players' payoffs in the maximally entangled case given that Alice plays a quantum move and Bob
plays a classical move with the same θ *)
assumes "γ = pi/2"
shows "φA = pi/2  φB = 0  θA = θB  alice_payoff = 1  bob_payoff = 1"
proof
assume asm:"φA = pi/2  φB = 0  θA = θB"
have "ψf $$(0,0) = 0" using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] by (auto simp add: asm assms sin_45 cos_45 algebra_simps) moreover have "ψf$$ (1,0) = 0"
using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"]
by (auto simp add: asm assms sin_45 cos_45 algebra_simps)
moreover have "ψf $$(2,0) = 0" using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] by (auto simp add: asm assms sin_45 cos_45 hidden_sqrt_two_squared_cpx2 algebra_simps) moreover have "ψf$$ (3,0) = 1"
using exp_of_half_pi[of "pi/2"] exp_of_minus_half_pi[of "pi/2"] cos_sin_squared_add_cpx
by (auto simp add: asm assms sin_45 cos_45 hidden_sqrt_two_squared_cpx2 algebra_simps)
ultimately show
using alice_payoff_def bob_payoff_def psi_f_is_state
by auto
qed

(*
Bibliography:

@ARTICLE{EWL,
author = {{Eisert}, J. and {Wilkens}, M. and {Lewenstein}, M.},
title = "{Quantum Games and Quantum Strategies}",
journal = {Physical Review Letters},
eprint = {quant-ph/9806088},
year = 1999,
month = oct,
volume = 83,
pages = {3077-3080},
doi = {10.1103/PhysRevLett.83.3077},