Theory Quantum_Hoare
section ‹Partial and total correctness›
theory Quantum_Hoare
imports Quantum_Program
begin
context state_sig
begin
definition density_states :: "state set" where
"density_states = {ρ ∈ carrier_mat d d. partial_density_operator ρ}"
lemma denote_density_states:
"ρ ∈ density_states ⟹ well_com S ⟹ denote S ρ ∈ density_states"
by (simp add: denote_dim_pdo density_states_def)
definition is_quantum_predicate :: "complex mat ⇒ bool" where
"is_quantum_predicate P ⟷ P ∈ carrier_mat d d ∧ positive P ∧ P ≤⇩L 1⇩m d"
lemma trace_measurement2:
assumes m: "measurement n 2 M" and dA: "A ∈ carrier_mat n n"
shows "trace ((M 0) * A * adjoint (M 0)) + trace ((M 1) * A * adjoint (M 1)) = trace A"
proof -
from m have dM0: "M 0 ∈ carrier_mat n n" and dM1: "M 1 ∈ carrier_mat n n" and id: "adjoint (M 0) * (M 0) + adjoint (M 1) * (M 1) = 1⇩m n"
using measurement_def measurement_id2 by auto
have "trace (M 1 * A * adjoint (M 1)) + trace (M 0 * A * adjoint (M 0))
= trace ((adjoint (M 0) * M 0 + adjoint (M 1) * M 1) * A)"
using dM0 dM1 dA by (mat_assoc n)
also have "… = trace (1⇩m n * A)" using id by auto
also have "… = trace A" using dA by auto
finally show ?thesis
using dA dM0 dM1 local.id state_sig.trace_measure2_id by blast
qed
lemma qp_close_under_unitary_operator:
fixes U P :: "complex mat"
assumes dU: "U ∈ carrier_mat d d"
and u: "unitary U"
and qp: "is_quantum_predicate P"
shows "is_quantum_predicate (adjoint U * P * U)"
unfolding is_quantum_predicate_def
proof (auto)
have dP: "P ∈ carrier_mat d d" using qp is_quantum_predicate_def by auto
show "adjoint U * P * U ∈ carrier_mat d d" using dU dP by fastforce
have "positive P" using qp is_quantum_predicate_def by auto
then show "positive (adjoint U * P * U)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dU] dP, simplified adjoint_adjoint] by fastforce
have "adjoint U * U = 1⇩m d" apply (subgoal_tac "inverts_mat (adjoint U) U")
subgoal unfolding inverts_mat_def using dU by auto
using u unfolding unitary_def using inverts_mat_symm[OF dU adjoint_dim[OF dU]] by auto
then have u': "adjoint U * 1⇩m d * U = 1⇩m d" using dU by auto
have le: "P ≤⇩L 1⇩m d" using qp is_quantum_predicate_def by auto
show "adjoint U * P * U ≤⇩L 1⇩m d"
using lowner_le_keep_under_measurement[OF dU dP one_carrier_mat le] u' by auto
qed
lemma qps_after_measure_is_qp:
assumes m: "measurement d n M " and qpk: "⋀k. k < n ⟹ is_quantum_predicate (P k)"
shows "is_quantum_predicate (matrix_sum d (λk. adjoint (M k) * P k * M k) n)"
unfolding is_quantum_predicate_def
proof (auto)
have dMk: "k < n ⟹ M k ∈ carrier_mat d d" for k using m measurement_def by auto
moreover have dPk: "k < n ⟹ P k ∈ carrier_mat d d" for k using qpk is_quantum_predicate_def by auto
ultimately have dk: "k < n ⟹ adjoint (M k) * P k * M k ∈ carrier_mat d d" for k by fastforce
then show d: "matrix_sum d (λk. adjoint (M k) * P k * M k) n ∈ carrier_mat d d"
using matrix_sum_dim[of n "λk. adjoint (M k) * P k * M k"] by auto
have "k < n ⟹ positive (P k)" for k using qpk is_quantum_predicate_def by auto
then have "k < n ⟹ positive (adjoint (M k) * P k * M k)" for k
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dMk] dPk, simplified adjoint_adjoint] by fastforce
then show "positive (matrix_sum d (λk. adjoint (M k) * P k * M k) n)" using matrix_sum_positive dk by auto
have "k < n ⟹ P k ≤⇩L 1⇩m d" for k using qpk is_quantum_predicate_def by auto
then have "k < n ⟹ positive (1⇩m d - P k)" for k using lowner_le_def by auto
then have p: "k < n ⟹ positive (adjoint (M k) * (1⇩m d - P k) * M k)" for k
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dMk], simplified adjoint_adjoint, of _ "1⇩m d - P k"] dPk by fastforce
{
fix k assume k: "k < n"
have "adjoint (M k) * (1⇩m d - P k) * M k = adjoint (M k) * M k - adjoint (M k) * P k * M k"
apply (mat_assoc d) using dMk dPk k by auto
}
note split = this
have dk': "k < n ⟹ adjoint (M k) * M k - adjoint (M k) * P k * M k ∈ carrier_mat d d" for k using dMk dPk by fastforce
have "k < n ⟹ positive (adjoint (M k) * M k - adjoint (M k) * P k * M k)" for k using p split by auto
then have p': "positive (matrix_sum d (λk. adjoint (M k) * M k - adjoint (M k) * P k * M k) n)"
using matrix_sum_positive[OF dk', of n id, simplified] by auto
have daMMk: "k < n ⟹ adjoint (M k) * M k ∈ carrier_mat d d" for k using dMk by fastforce
have daMPMk: "k < n ⟹ adjoint (M k) * P k * M k ∈ carrier_mat d d" for k using dMk dPk by fastforce
have "matrix_sum d (λk. adjoint (M k) * M k - adjoint (M k) * P k * M k) n
= matrix_sum d (λk. adjoint (M k) * M k) n - matrix_sum d (λk. adjoint (M k) * P k * M k) n"
using matrix_sum_minus_distrib[OF daMMk daMPMk] by auto
also have "… = 1⇩m d - matrix_sum d (λk. adjoint (M k) * P k * M k) n" using m measurement_def by auto
finally have "positive (1⇩m d - matrix_sum d (λk. adjoint (M k) * P k * M k) n)" using p' by auto
then show "matrix_sum d (λk. adjoint (M k) * P k * M k) n ≤⇩L 1⇩m d" using lowner_le_def d by auto
qed
definition hoare_total_correct :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" (‹⊨⇩t {(1_)}/ (_)/ {(1_)}› 50) where
"⊨⇩t {P} S {Q} ⟷ (∀ρ∈density_states. trace (P * ρ) ≤ trace (Q * denote S ρ))"
definition hoare_partial_correct :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" (‹⊨⇩p {(1_)}/ (_)/ {(1_)}› 50) where
"⊨⇩p {P} S {Q} ⟷ (∀ρ∈density_states. trace (P * ρ) ≤ trace (Q * denote S ρ) + (trace ρ - trace (denote S ρ)))"
lemma total_implies_partial:
assumes S: "well_com S"
and total: "⊨⇩t {P} S {Q}"
shows "⊨⇩p {P} S {Q}"
proof -
have "trace (P * ρ) ≤ trace (Q * denote S ρ) + (trace ρ - trace (denote S ρ))" if ρ: "ρ ∈ density_states" for ρ
proof -
have "trace (P * ρ) ≤ trace (Q * denote S ρ)"
using total hoare_total_correct_def ρ by auto
moreover have "trace (denote S ρ) ≤ trace ρ"
using denote_trace[OF S] ρ density_states_def by auto
ultimately show ?thesis by (auto simp: less_eq_complex_def)
qed
then show ?thesis
using hoare_partial_correct_def by auto
qed
lemma predicate_prob_positive:
assumes "0⇩m d d ≤⇩L P"
and "ρ ∈ density_states"
shows "0 ≤ trace (P * ρ)"
proof -
have "trace (0⇩m d d * ρ) ≤ trace (P * ρ)"
apply (rule lowner_le_traceD)
using assms unfolding lowner_le_def density_states_def by auto
then show ?thesis
using assms(2) density_states_def by auto
qed
lemma total_pre_zero:
assumes S: "well_com S"
and Q: "is_quantum_predicate Q"
shows "⊨⇩t {0⇩m d d} S {Q}"
proof -
have "trace (0⇩m d d * ρ) ≤ trace (Q * denote S ρ)" if ρ: "ρ ∈ density_states" for ρ
proof -
have 1: "trace (0⇩m d d * ρ) = 0"
using ρ unfolding density_states_def by auto
show ?thesis
apply (subst 1)
apply (rule predicate_prob_positive)
subgoal apply (simp add: lowner_le_def, subgoal_tac "Q - 0⇩m d d = Q") using Q is_quantum_predicate_def[of Q] by auto
subgoal using denote_density_states ρ S by auto
done
qed
then show ?thesis
using hoare_total_correct_def by auto
qed
lemma partial_post_identity:
assumes S: "well_com S"
and P: "is_quantum_predicate P"
shows "⊨⇩p {P} S {1⇩m d}"
proof -
have "trace (P * ρ) ≤ trace (1⇩m d * denote S ρ) + (trace ρ - trace (denote S ρ))" if ρ: "ρ ∈ density_states" for ρ
proof -
have "denote S ρ ∈ carrier_mat d d"
using S denote_dim ρ density_states_def by auto
then have "trace (1⇩m d * denote S ρ) = trace (denote S ρ)"
by auto
moreover have "trace (P * ρ) ≤ trace (1⇩m d * ρ)"
apply (rule lowner_le_traceD)
using ρ unfolding density_states_def apply auto
using P is_quantum_predicate_def by auto
ultimately show ?thesis
using density_states_def that by auto
qed
then show ?thesis
using hoare_partial_correct_def by auto
qed
subsection ‹Weakest liberal preconditions›
definition is_weakest_liberal_precondition :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" where
"is_weakest_liberal_precondition W S P ⟷
is_quantum_predicate W ∧ ⊨⇩p {W} S {P} ∧ (∀Q. is_quantum_predicate Q ⟶ ⊨⇩p {Q} S {P} ⟶ Q ≤⇩L W)"
definition wlp_measure :: "nat ⇒ (nat ⇒ complex mat) ⇒ ((complex mat ⇒ complex mat) list) ⇒ complex mat ⇒ complex mat" where
"wlp_measure n M WS P = matrix_sum d (λk. adjoint (M k) * ((WS!k) P) * (M k)) n"
fun wlp_while_n :: "complex mat ⇒ complex mat ⇒ (complex mat ⇒ complex mat) ⇒ nat ⇒ complex mat ⇒ complex mat" where
"wlp_while_n M0 M1 WS 0 P = 1⇩m d"
| "wlp_while_n M0 M1 WS (Suc n) P = adjoint M0 * P * M0 + adjoint M1 * (WS (wlp_while_n M0 M1 WS n P)) * M1"
lemma measurement2_leq_one_mat:
assumes dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d"
and leP: "P ≤⇩L 1⇩m d" and leQ: "Q ≤⇩L 1⇩m d" and m: "measurement d 2 M"
shows "(adjoint (M 0) * P * (M 0) + adjoint (M 1) * Q * (M 1)) ≤⇩L 1⇩m d"
proof -
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m M0_def M1_def measurement_def by auto
have "adjoint M1 * Q * M1 ≤⇩L adjoint M1 * 1⇩m d * M1"
using lowner_le_keep_under_measurement[OF dM1 dQ _ leQ] by auto
then have le1: "adjoint M1 * Q * M1 ≤⇩L adjoint M1 * M1" using dM1 dQ by fastforce
have "adjoint M0 * P * M0 ≤⇩L adjoint M0 * 1⇩m d * M0"
using lowner_le_keep_under_measurement[OF dM0 dP _ leP] by auto
then have le0: "adjoint M0 * P * M0 ≤⇩L adjoint M0 * M0"
using dM0 dP by fastforce
have "adjoint M0 * P * M0 + adjoint M1 * Q * M1 ≤⇩L adjoint M0 * M0 + adjoint M1 * M1"
apply (rule lowner_le_add[of "adjoint M0 * P * M0" d "adjoint M0 * M0" "adjoint M1 * Q * M1" "adjoint M1 * M1"])
using dM0 dP dM1 dQ le0 le1 by auto
also have "… = 1⇩m d" using m M0_def M1_def measurement_id2 by auto
finally show "adjoint M0 * P * M0 + adjoint M1 * Q * M1 ≤⇩L 1⇩m d".
qed
lemma wlp_while_n_close:
assumes close: "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and m: "measurement d 2 M" and qpP: "is_quantum_predicate P"
shows "is_quantum_predicate (wlp_while_n (M 0) (M 1) WS k P)"
proof (induct k)
case 0
then show ?case
unfolding wlp_while_n.simps is_quantum_predicate_def using positive_one[of d] lowner_le_refl[of "1⇩m d"] by fastforce
next
case (Suc k)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
define W where "W k = wlp_while_n M0 M1 WS k P" for k
show ?case unfolding wlp_while_n.simps is_quantum_predicate_def
proof (fold M0_def M1_def, fold W_def, auto)
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m M0_def M1_def measurement_def by auto
have dP: "P ∈ carrier_mat d d" using qpP is_quantum_predicate_def by auto
have qpWk: "is_quantum_predicate (W k)" using Suc M0_def M1_def W_def by auto
then have qpWWk: "is_quantum_predicate (WS (W k))" using close by auto
from qpWk have dWk: "W k ∈ carrier_mat d d" using is_quantum_predicate_def by auto
from qpWWk have dWWk: "WS (W k) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
show "adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1 ∈ carrier_mat d d" using dM0 dP dM1 dWWk by auto
have pP: "positive P" using qpP is_quantum_predicate_def by auto
then have pM0P: "positive (adjoint M0 * P * M0)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM0]] dM0 dP adjoint_adjoint[of M0] by auto
have pWWk: "positive (WS (W k))" using qpWWk is_quantum_predicate_def by auto
then have pM1WWk: "positive (adjoint M1 * WS (W k) * M1)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM1]] dM1 dWWk adjoint_adjoint[of M1] by auto
then show "positive (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)"
using positive_add[OF pM0P pM1WWk] dM0 dP dM1 dWWk by fastforce
have leWWk: "WS (W k) ≤⇩L 1⇩m d" using qpWWk is_quantum_predicate_def by auto
have leP: "P ≤⇩L 1⇩m d" using qpP is_quantum_predicate_def by auto
show "(adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1) ≤⇩L 1⇩m d "
using measurement2_leq_one_mat[OF dP dWWk leP leWWk m] M0_def M1_def by auto
qed
qed
lemma wlp_while_n_mono:
assumes "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and "⋀P Q. is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ WS P ≤⇩L WS Q"
and "measurement d 2 M"
and "is_quantum_predicate P"
and "is_quantum_predicate Q"
and "P ≤⇩L Q"
shows "(wlp_while_n (M 0) (M 1) WS k P) ≤⇩L (wlp_while_n (M 0) (M 1) WS k Q)"
proof (induct k)
case 0
then show ?case unfolding wlp_while_n.simps using lowner_le_refl[of "1⇩m d"] by fastforce
next
case (Suc k)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using assms M0_def M1_def measurement_def by auto
define W where "W P k = wlp_while_n M0 M1 WS k P" for k P
have dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d" using assms is_quantum_predicate_def by auto
have eq1: "W P (Suc k) = adjoint M0 * P * M0 + adjoint M1 * (WS (W P k)) * M1" unfolding W_def wlp_while_n.simps by auto
have eq2: "W Q (Suc k) = adjoint M0 * Q * M0 + adjoint M1 * (WS (W Q k)) * M1" unfolding W_def wlp_while_n.simps by auto
have le1: "adjoint M0 * P * M0 ≤⇩L adjoint M0 * Q * M0" using lowner_le_keep_under_measurement dM0 dP dQ assms by auto
have leWk: "(W P k) ≤⇩L (W Q k)" unfolding W_def M0_def M1_def using Suc by auto
have qpWPk: "is_quantum_predicate (W P k)" unfolding W_def M0_def M1_def using wlp_while_n_close assms by auto
then have "is_quantum_predicate (WS (W P k))" unfolding W_def M0_def M1_def using assms by auto
then have dWWPk: "(WS (W P k)) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have qpWQk: "is_quantum_predicate (W Q k)" unfolding W_def M0_def M1_def using wlp_while_n_close assms by auto
then have "is_quantum_predicate (WS (W Q k))" unfolding W_def M0_def M1_def using assms by auto
then have dWWQk: "(WS (W Q k)) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "(WS (W P k)) ≤⇩L (WS (W Q k))" using qpWPk qpWQk leWk assms by auto
then have le2: "adjoint M1 * (WS (W P k)) * M1 ≤⇩L adjoint M1 * (WS (W Q k)) * M1"
using lowner_le_keep_under_measurement dM1 dWWPk dWWQk by auto
have "(adjoint M0 * P * M0 + adjoint M1 * (WS (W P k)) * M1) ≤⇩L (adjoint M0 * Q * M0 + adjoint M1 * (WS (W Q k)) * M1)"
using lowner_le_add[OF _ _ _ _ le1 le2] dM0 dP dM1 dQ dWWPk dWWQk le1 le2 by fastforce
then have "W P (Suc k) ≤⇩L W Q (Suc k)" using eq1 eq2 by auto
then show ?case unfolding W_def M0_def M1_def by auto
qed
definition wlp_while :: "complex mat ⇒ complex mat ⇒ (complex mat ⇒ complex mat) ⇒ complex mat ⇒ complex mat" where
"wlp_while M0 M1 WS P = (THE Q. limit_mat (λn. wlp_while_n M0 M1 WS n P) Q d)"
lemma wlp_while_exists:
assumes "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and "⋀P Q. is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ WS P ≤⇩L WS Q"
and m: "measurement d 2 M"
and qpP: "is_quantum_predicate P"
shows "is_quantum_predicate (wlp_while (M 0) (M 1) WS P)
∧ (∀n. (wlp_while (M 0) (M 1) WS P) ≤⇩L (wlp_while_n (M 0) (M 1) WS n P))
∧ (∀W'. (∀n. W' ≤⇩L (wlp_while_n (M 0) (M 1) WS n P)) ⟶ W' ≤⇩L (wlp_while (M 0) (M 1) WS P))
∧ limit_mat (λn. wlp_while_n (M 0) (M 1) WS n P) (wlp_while (M 0) (M 1) WS P) d"
proof (auto)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using assms M0_def M1_def measurement_def by auto
define W where "W k = wlp_while_n M0 M1 WS k P" for k
have leP: "P ≤⇩L 1⇩m d" and dP: "P ∈ carrier_mat d d" and pP: "positive P" using qpP is_quantum_predicate_def by auto
have pM0P: "positive (adjoint M0 * P * M0)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM0]] adjoint_adjoint[of "M0"] dP pP by auto
have le_qp: "W (Suc k) ≤⇩L W k ∧ is_quantum_predicate (W k)" for k
proof (induct k)
case 0
have "is_quantum_predicate (1⇩m d)"
unfolding is_quantum_predicate_def using positive_one lowner_le_refl[of "1⇩m d"] by fastforce
then have "is_quantum_predicate (WS (1⇩m d))" using assms by auto
then have "(WS (1⇩m d)) ∈ carrier_mat d d" and "(WS (1⇩m d)) ≤⇩L 1⇩m d" using is_quantum_predicate_def by auto
then have "W 1 ≤⇩L W 0" unfolding W_def wlp_while_n.simps M0_def M1_def
using measurement2_leq_one_mat[OF dP _ leP _ m] by auto
moreover have "is_quantum_predicate (W 0)" unfolding W_def wlp_while_n.simps is_quantum_predicate_def
using positive_one lowner_le_refl[of "1⇩m d"] by fastforce
ultimately show ?case by auto
next
case (Suc k)
then have leWSk: "W (Suc k) ≤⇩L W k" and qpWk: "is_quantum_predicate (W k)" by auto
then have "is_quantum_predicate (WS (W k))" using assms by auto
then have dWWk: "WS (W k) ∈ carrier_mat d d" and leWWk1: "(WS (W k)) ≤⇩L 1⇩m d" and pWWk: "positive (WS (W k))"
using is_quantum_predicate_def by auto
then have leWSk1: "W (Suc k) ≤⇩L 1⇩m d" using measurement2_leq_one_mat[OF dP dWWk leP leWWk1 m]
unfolding W_def wlp_while_n.simps M0_def M1_def by auto
then have dWSk: "W (Suc k) ∈ carrier_mat d d" using lowner_le_def by fastforce
have pM1WWk: "positive (adjoint M1 * (WS (W k)) * M1)"
using positive_close_under_left_right_mult_adjoint[OF adjoint_dim[OF dM1] dWWk pWWk] adjoint_adjoint[of "M1"] by auto
have pWSk: "positive (W (Suc k))" unfolding W_def wlp_while_n.simps apply (fold W_def)
using positive_add[OF pM0P pM1WWk] dM0 dP dM1 by fastforce
have qpWSk:"is_quantum_predicate (W (Suc k))" unfolding is_quantum_predicate_def using dWSk pWSk leWSk1 by auto
then have qpWWSk: "is_quantum_predicate (WS (W (Suc k)))" using assms(1) by auto
then have dWWSk: "(WS (W (Suc k))) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "WS (W (Suc k)) ≤⇩L WS (W k)" using assms(2)[OF qpWSk qpWk] leWSk by auto
then have "adjoint M1 * WS (W (Suc k)) * M1 ≤⇩L adjoint M1 * WS (W k) * M1"
using lowner_le_keep_under_measurement[OF dM1 dWWSk dWWk] by auto
then have "(adjoint M0 * P * M0 + adjoint M1 * WS (W (Suc k)) * M1)
≤⇩L (adjoint M0 * P * M0 + adjoint M1 * WS (W k) * M1)"
using lowner_le_add[of _ d _ "adjoint M1 * WS (W (Suc k)) * M1" "adjoint M1 * WS (W k) * M1",
OF _ _ _ _ lowner_le_refl[of "adjoint M0 * P * M0"]] dM0 dM1 dP dWWSk dWWk by fastforce
then have "W (Suc (Suc k)) ≤⇩L W (Suc k)" unfolding W_def wlp_while_n.simps by auto
with qpWSk show ?case by auto
qed
then have dWk: "W k ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
then have dmWk: "- W k ∈ carrier_mat d d" for k by auto
have incmWk: "- (W k) ≤⇩L - (W (Suc k))" for k using lowner_le_swap[of "W (Suc k)" d "W k"] dWk le_qp by auto
have pWk: "positive (W k)" for k using le_qp is_quantum_predicate_def by auto
have ubmWk: "- W k ≤⇩L 0⇩m d d" for k
proof -
have "0⇩m d d ≤⇩L W k" for k using zero_lowner_le_positiveI dWk pWk by auto
then have "- W k ≤⇩L - 0⇩m d d" for k using lowner_le_swap[of "0⇩m d d" d "W k"] dWk by auto
moreover have "(- 0⇩m d d :: complex mat) = (0⇩m d d)" by auto
ultimately show ?thesis by auto
qed
have "∃B. lowner_is_lub (λk. - W k) B ∧ limit_mat (λk. - W k) B d"
using mat_inc_seq_lub[of "λk. - W k" d "0⇩m d d"] dmWk incmWk ubmWk by auto
then obtain B where lubB: "lowner_is_lub (λk. - W k) B" and limB: "limit_mat (λk. - W k) B d" by auto
then have dB: "B ∈ carrier_mat d d" using limit_mat_def by auto
define A where "A = - B"
then have dA: "A ∈ carrier_mat d d" using dB by auto
have "limit_mat (λk. (-1) ⋅⇩m (- W k)) (-1 ⋅⇩m B) d" using limit_mat_scale[OF limB] by auto
moreover have "W k = -1 ⋅⇩m (- W k)" for k using dWk by auto
moreover have "-1 ⋅⇩m B = - B" by auto
ultimately have limA: "limit_mat W A d" using A_def by auto
moreover have "(limit_mat W A' d ⟹ A' = A)" for A' using limit_mat_unique[of W A d] limA by auto
ultimately have eqA: "(wlp_while (M 0) (M 1) WS P) = A" unfolding wlp_while_def W_def M0_def M1_def
using the_equality[of "λX. limit_mat (λn. wlp_while_n (M 0) (M 1) WS n P) X d" A] by fastforce
show "limit_mat (λn. wlp_while_n (M 0) (M (Suc 0)) WS n P) (wlp_while (M 0) (M (Suc 0)) WS P) d"
using limA eqA unfolding W_def M0_def M1_def by auto
have "- W k ≤⇩L B" for k using lubB lowner_is_lub_def by auto
then have glbA: "A ≤⇩L W k" for k unfolding A_def using lowner_le_swap[of "- W k" d] dB dWk by fastforce
then show "⋀n. wlp_while (M 0) (M (Suc 0)) WS P ≤⇩L wlp_while_n (M 0) (M (Suc 0)) WS n P" using eqA unfolding W_def M0_def M1_def by auto
have "W k ≤⇩L 1⇩m d" for k using le_qp unfolding is_quantum_predicate_def by auto
then have "positive (1⇩m d - W k)" for k using lowner_le_def by auto
moreover have "limit_mat (λk. 1⇩m d - W k) (1⇩m d - A) d" using mat_minus_limit limA by auto
ultimately have "positive (1⇩m d - A)" using pos_mat_lim_is_pos by auto
then have leA1: "A ≤⇩L 1⇩m d" using dA lowner_le_def by auto
have pA: "positive A" using pos_mat_lim_is_pos limA pWk by auto
show "is_quantum_predicate (wlp_while (M 0) (M (Suc 0)) WS P)" unfolding is_quantum_predicate_def using pA dA leA1 eqA by auto
{
fix W' assume asmW': "∀k. W' ≤⇩L W k"
then have dW': "W' ∈ carrier_mat d d" unfolding lowner_le_def using carrier_matD[OF dWk] by auto
then have "- W k ≤⇩L - W'" for k using lowner_le_swap dWk asmW' by auto
then have "B ≤⇩L - W'" using lubB unfolding lowner_is_lub_def by auto
then have "W' ≤⇩L A" unfolding A_def
using lowner_le_swap[of "B" d "- W'"] dB dW' by auto
then have "W' ≤⇩L wlp_while (M 0) (M 1) WS P" using eqA by auto
}
then show "⋀W'. ∀n. W' ≤⇩L wlp_while_n (M 0) (M (Suc 0)) WS n P ⟹ W' ≤⇩L wlp_while (M 0) (M (Suc 0)) WS P"
unfolding W_def M0_def M1_def by auto
qed
lemma wlp_while_mono:
assumes "⋀P. is_quantum_predicate P ⟹ is_quantum_predicate (WS P)"
and "⋀P Q. is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ WS P ≤⇩L WS Q"
and "measurement d 2 M"
and "is_quantum_predicate P"
and "is_quantum_predicate Q"
and "P ≤⇩L Q"
shows "wlp_while (M 0) (M 1) WS P ≤⇩L wlp_while (M 0) (M 1) WS Q"
proof -
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using assms M0_def M1_def measurement_def by auto
define Wn where "Wn P k = wlp_while_n M0 M1 WS k P" for P k
define W where "W P = wlp_while M0 M1 WS P" for P
have lePQk: "Wn P k ≤⇩L Wn Q k" for k unfolding Wn_def M0_def M1_def
using wlp_while_n_mono assms by auto
have "is_quantum_predicate (Wn P k)" for k unfolding Wn_def M0_def M1_def using wlp_while_n_close assms by auto
then have dWPk: "Wn P k ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
have "is_quantum_predicate (Wn Q k)" for k unfolding Wn_def M0_def M1_def using wlp_while_n_close assms by auto
then have dWQk:"Wn Q k ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
have "is_quantum_predicate (W P)" and lePk: "(W P) ≤⇩L (Wn P k)" and "limit_mat (Wn P) (W P) d" for k
unfolding W_def Wn_def M0_def M1_def using wlp_while_exists assms by auto
then have dWP: "W P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "is_quantum_predicate (W Q)" and "(W Q) ≤⇩L (Wn Q k)"
and glb:"(∀k. W' ≤⇩L (Wn Q k)) ⟶ W' ≤⇩L (W Q)" and "limit_mat (Wn Q) (W Q) d" for k W'
unfolding W_def Wn_def M0_def M1_def using wlp_while_exists assms by auto
have "W P ≤⇩L Wn Q k" for k using lowner_le_trans[of "W P" d "Wn P k" "Wn Q k"] lePk lePQk dWPk dWQk dWP by auto
then show "W P ≤⇩L W Q" using glb by auto
qed
fun wlp :: "com ⇒ complex mat ⇒ complex mat" where
"wlp SKIP P = P"
| "wlp (Utrans U) P = adjoint U * P * U"
| "wlp (Seq S1 S2) P = wlp S1 (wlp S2 P)"
| "wlp (Measure n M S) P = wlp_measure n M (map wlp S) P"
| "wlp (While M S) P = wlp_while (M 0) (M 1) (wlp S) P"
lemma wlp_measure_expand_m:
assumes m: "m ≤ n" and wc: "well_com (Measure n M S)"
shows "wlp (Measure m M S) P = matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * (M k)) m"
unfolding wlp.simps wlp_measure_def
proof -
have "k < m ⟹ map wlp S ! k = wlp (S!k)" for k using wc m by auto
then have "k < m ⟹ (map wlp S ! k) P = wlp (S!k) P" for k by auto
then show "matrix_sum d (λk. adjoint (M k) * ((map wlp S ! k) P) * (M k)) m
= matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * (M k)) m"
using matrix_sum_cong[of m "λk. adjoint (M k) * ((map wlp S ! k) P) * (M k)" "λk. adjoint (M k) * (wlp (S!k) P) * (M k)"] by auto
qed
lemma wlp_measure_expand:
assumes wc: "well_com (Measure n M S)"
shows "wlp (Measure n M S) P = matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * (M k)) n"
using wlp_measure_expand_m[OF Nat.le_refl[of n]] wc by auto
lemma wlp_mono_and_close:
shows "well_com S ⟹ is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q
⟹ is_quantum_predicate (wlp S P) ∧ wlp S P ≤⇩L wlp S Q"
proof (induct S arbitrary: P Q)
case SKIP
then show ?case by auto
next
case (Utrans U)
then have dU: "U ∈ carrier_mat d d" and u: "unitary U" and qp: "is_quantum_predicate P" and le: "P ≤⇩L Q"
and dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then have qp': "is_quantum_predicate (wlp (Utrans U) P)" using qp_close_under_unitary_operator by auto
moreover have "adjoint U * P * U ≤⇩L adjoint U * Q * U" using lowner_le_keep_under_measurement[OF dU dP dQ le] by auto
ultimately show ?case by auto
next
case (Seq S1 S2)
then have qpP: "is_quantum_predicate P" and qpQ: "is_quantum_predicate Q" and wc1: "well_com S1" and wc2: "well_com S2"
and dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d" and le: "P ≤⇩L Q"using is_quantum_predicate_def by auto
have qpP2: "is_quantum_predicate (wlp S2 P)" using Seq qpP wc2 by auto
have qpQ2: "is_quantum_predicate (wlp S2 Q)" using Seq(2)[OF wc2 qpQ qpQ] lowner_le_refl dQ by blast
have qpP1: "is_quantum_predicate (wlp S1 (wlp S2 P))"
using Seq(1)[OF wc1 qpP2 qpP2] qpP2 is_quantum_predicate_def[of "wlp S2 P"] lowner_le_refl by auto
have "wlp S2 P ≤⇩L wlp S2 Q" using Seq(2) wc2 qpP qpQ le by auto
then have "wlp S1 (wlp S2 P) ≤⇩L wlp S1 (wlp S2 Q)" using Seq(1) wc1 qpP2 qpQ2 by auto
then show ?case using qpP1 by auto
next
case (Measure n M S)
then have wc: "well_com (Measure n M S)" and wck: "k < n ⟹ well_com (S!k)" and l: "length S = n"
and m: "measurement d n M" and le: "P ≤⇩L Q"
and qpP: "is_quantum_predicate P" and dP: "P ∈ carrier_mat d d"
and qpQ: "is_quantum_predicate Q" and dQ: "Q ∈ carrier_mat d d"
for k using measure_well_com is_quantum_predicate_def by auto
have dMk: "k < n ⟹ M k ∈ carrier_mat d d" for k using m measurement_def by auto
have set: "k < n ⟹ S!k ∈ set S" for k using l by auto
have qpk: "k < n ⟹ is_quantum_predicate (wlp (S!k) P)" for k
using Measure(1)[OF set wck qpP qpP] lowner_le_refl[of P] dP by auto
then have dWkP: "k < n ⟹ wlp (S!k) P ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
then have dMkP: "k < n ⟹ adjoint (M k) * (wlp (S!k) P) * (M k) ∈ carrier_mat d d" for k using dMk by fastforce
have "k < n ⟹ is_quantum_predicate (wlp (S!k) Q)" for k
using Measure(1)[OF set wck qpQ qpQ] lowner_le_refl[of Q] dQ by auto
then have dWkQ: "k < n ⟹ wlp (S!k) Q ∈ carrier_mat d d" for k using is_quantum_predicate_def by auto
then have dMkQ: "k < n ⟹ adjoint (M k) * (wlp (S!k) Q) * (M k) ∈ carrier_mat d d" for k using dMk by fastforce
have "k < n ⟹ wlp (S!k) P ≤⇩L wlp (S!k) Q" for k
using Measure(1)[OF set wck qpP qpQ le] by auto
then have "k < n ⟹ adjoint (M k) * (wlp (S!k) P) * (M k) ≤⇩L adjoint (M k) * (wlp (S!k) Q) * (M k)" for k
using lowner_le_keep_under_measurement[OF dMk dWkP dWkQ] by auto
then have le': "wlp (Measure n M S) P ≤⇩L wlp (Measure n M S) Q" unfolding wlp_measure_expand[OF wc]
using lowner_le_matrix_sum dMkP dMkQ by auto
have qp': "is_quantum_predicate (wlp (Measure n M S) P)" unfolding wlp_measure_expand[OF wc]
using qps_after_measure_is_qp[OF m] qpk by auto
show ?case using le' qp' by auto
next
case (While M S)
then have m: "measurement d 2 M" and wcs: "well_com S"
and qpP: "is_quantum_predicate P"
by auto
have closeWS: "is_quantum_predicate P ⟹ is_quantum_predicate (wlp S P)" for P
proof -
assume asm: "is_quantum_predicate P"
then have dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then show "is_quantum_predicate (wlp S P)" using While(1)[OF wcs asm asm lowner_le_refl] dP by auto
qed
have monoWS: "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ wlp S P ≤⇩L wlp S Q" for P Q
using While(1)[OF wcs] by auto
have "is_quantum_predicate (wlp (While M S) P)"
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP by auto
moreover have "wlp (While M S) P ≤⇩L wlp (While M S) Q"
using wlp_while_mono[of "wlp S" M P Q] closeWS monoWS m While by auto
ultimately show ?case by auto
qed
lemma wlp_close:
assumes wc: "well_com S" and qp: "is_quantum_predicate P"
shows "is_quantum_predicate (wlp S P)"
using wlp_mono_and_close[OF wc qp qp] is_quantum_predicate_def[of P] qp lowner_le_refl by auto
lemma wlp_soundness:
"well_com S ⟹
(⋀P. (is_quantum_predicate P ⟹
(∀ρ ∈ density_states. trace (wlp S P * ρ) = trace (P * (denote S ρ)) + trace ρ - trace (denote S ρ))))"
proof (induct S)
case SKIP
then show ?case by auto
next
case (Utrans U)
then have dU: "U ∈ carrier_mat d d" and u: "unitary U" and wc: "well_com (Utrans U)"
and qp: "is_quantum_predicate P" and dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have qp': "is_quantum_predicate (wlp (Utrans U) P)" using wlp_close[OF wc qp] by auto
have eq1: "trace (adjoint U * P * U * ρ) = trace (P * (U * ρ * adjoint U))" if dr: "ρ ∈ carrier_mat d d" for ρ
using dr dP apply (mat_assoc d) using wc by auto
have eq2: "trace (U * ρ * adjoint U) = trace ρ" if dr: "ρ ∈ carrier_mat d d" for ρ
using unitary_operator_keep_trace[OF adjoint_dim[OF dU] dr unitary_adjoint[OF dU u]] adjoint_adjoint[of U] by auto
show ?case using qp' eq1 eq2 density_states_def by auto
next
case (Seq S1 S2)
then have qp: "is_quantum_predicate P" and wc1: "well_com S1" and wc2: "well_com S2" by auto
then have qp2: "is_quantum_predicate (wlp S2 P)" using wlp_close by auto
then have qp1: "is_quantum_predicate (wlp S1 (wlp S2 P))" using wlp_close wc1 by auto
have eq1: "trace (wlp S2 P * ρ) = trace (P * denote S2 ρ) + trace ρ - trace (denote S2 ρ)"
if ds: "ρ ∈ density_states" for ρ using Seq(2) wc2 qp ds by auto
have eq2: "trace (wlp S1 (wlp S2 P) * ρ) = trace ((wlp S2 P) * denote S1 ρ) + trace ρ - trace (denote S1 ρ)"
if ds: "ρ ∈ density_states" for ρ using Seq(1) wc1 qp2 ds by auto
have eq3: "trace (wlp S1 (wlp S2 P) * ρ) = trace (P * (denote S2 (denote S1 ρ))) + trace ρ - trace (denote S2 (denote S1 ρ))"
if ds: "ρ ∈ density_states" for ρ
proof -
have "denote S1 ρ ∈ density_states"
using ds denote_density_states wc1 by auto
then have "trace ((wlp S2 P) * denote S1 ρ) = trace (P * denote S2 (denote S1 ρ)) + trace (denote S1 ρ) - trace (denote S2 (denote S1 ρ))"
using eq1 by auto
then show "trace (wlp S1 (wlp S2 P) * ρ) = trace (P * (denote S2 (denote S1 ρ))) + trace ρ - trace (denote S2 (denote S1 ρ))"
using eq2 ds by auto
qed
then show ?case using qp1 by auto
next
case (Measure n M S)
then have wc: "well_com (Measure n M S)"
and wck: "k < n ⟹ well_com (S!k)"
and qpP: "is_quantum_predicate P"
and dP: "P ∈ carrier_mat d d"
and qpWk: "k < n ⟹ is_quantum_predicate (wlp (S!k) P)"
and dWk: "k < n ⟹ (wlp (S!k) P) ∈ carrier_mat d d"
and c: "k < n ⟹ ρ ∈ density_states ⟹ trace (wlp (S!k) P * ρ) = trace (P * denote (S!k) ρ) + trace ρ - trace (denote (S!k) ρ)"
and m: "measurement d n M"
and aMMkleq: "k < n ⟹ adjoint (M k) * M k ≤⇩L 1⇩m d"
and dMk: "k < n ⟹ M k ∈ carrier_mat d d"
for k ρ using is_quantum_predicate_def measurement_def measure_well_com measurement_le_one_mat wlp_close by auto
{
fix ρ assume ρ: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have dsr: "k < n ⟹ (M k) * ρ * adjoint (M k) ∈ density_states" for k unfolding density_states_def
using dMk pdo_close_under_measurement[OF dMk dr pdor aMMkleq] dr by fastforce
then have leqk: "k < n ⟹ trace (wlp (S!k) P * ((M k) * ρ * adjoint (M k))) =
trace (P * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" for k
using c by auto
have "k < n ⟹ M k * ρ * adjoint (M k) ∈ carrier_mat d d" for k using dMk dr by fastforce
then have dsMrk: "k < n ⟹ matrix_sum d (λk. (M k * ρ * adjoint (M k))) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. (M k * ρ * adjoint (M k))" d] by fastforce
have "k < n ⟹ adjoint (M k) * (wlp (S!k) P) * M k ∈ carrier_mat d d" for k using dMk by fastforce
then have dsMW: "k < n ⟹ matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. adjoint (M k) * (wlp (S!k) P) * M k" d] by fastforce
have dSMrk: "k < n ⟹ denote (S ! k) (M k * ρ * adjoint (M k)) ∈ carrier_mat d d" for k
using denote_dim[OF wck, of k "M k * ρ * adjoint (M k)"] dsr density_states_def by fastforce
have dsSMrk: "k < n ⟹ matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. denote (S ! k) (M k * ρ * adjoint (M k))" d, OF dSMrk] by fastforce
have "k ≤ n ⟹
trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) k * ρ)
= trace (P * (denote (Measure k M S) ρ)) + (trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) k) - trace (denote (Measure k M S) ρ))" for k
unfolding denote_measure_expand[OF _ wc]
proof (induct k)
case 0
then show ?case unfolding matrix_sum.simps using dP dr by auto
next
case (Suc k)
then have k: "k < n" by auto
have eq1: "trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) (Suc k) * ρ)
= trace (adjoint (M k) * (wlp (S!k) P) * M k * ρ) + trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) k * ρ)"
unfolding matrix_sum.simps
using dMk[OF k] dWk[OF k] dr dsMW[OF k] by (mat_assoc d)
have "trace (adjoint (M k) * (wlp (S!k) P) * M k * ρ) = trace ((wlp (S!k) P) * (M k * ρ * adjoint (M k)))"
using dMk[OF k] dWk[OF k] dr by (mat_assoc d)
also have "… = trace (P * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" using leqk k by auto
finally have eq2: "trace (adjoint (M k) * (wlp (S!k) P) * M k * ρ) = trace (P * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" .
have eq3: "trace (P * matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) (Suc k))
= trace (P * (denote (S!k) (M k * ρ * adjoint (M k)))) + trace (P * matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)"
unfolding matrix_sum.simps
using dP dSMrk[OF k] dsSMrk[OF k] by (mat_assoc d)
have eq4: "trace (denote (S ! k) (M k * ρ * adjoint (M k)) + matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)
= trace (denote (S ! k) (M k * ρ * adjoint (M k))) + trace (matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)"
using dSMrk[OF k] dsSMrk[OF k] by (mat_assoc d)
show ?case
apply (subst eq1) apply (subst eq3)
apply (simp del: less_eq_complex_def)
apply (subst trace_add_linear[of "M k * ρ * adjoint (M k)" d "matrix_sum d (λk. M k * ρ * adjoint (M k)) k"])
apply (simp add: dMk adjoint_dim[OF dMk] dr mult_carrier_mat[of _ d d _ d] k)
apply (simp add: dsMrk k)
apply (subst eq4)
apply (insert eq2 Suc(1) k, fastforce)
done
qed
then have leq: "trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) n * ρ)
= trace (P * denote (Measure n M S) ρ) +
(trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) n) - trace (denote (Measure n M S) ρ))"
by auto
have "trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) n) = trace ρ" using trace_measurement m dr by auto
with leq have "trace (matrix_sum d (λk. adjoint (M k) * (wlp (S!k) P) * M k) n * ρ)
= trace (P * denote (Measure n M S) ρ) + (trace ρ - trace (denote (Measure n M S) ρ))"
unfolding denote_measure_def by auto
}
then show ?case unfolding wlp_measure_expand[OF wc] by auto
next
case (While M S)
then have qpP: "is_quantum_predicate P" and dP: "P ∈ carrier_mat d d"
and wcS: "well_com S" and m: "measurement d 2 M" and wc: "well_com (While M S)"
using is_quantum_predicate_def by auto
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m measurement_def M0_def M1_def by auto
have leM1: "adjoint M1 * M1 ≤⇩L 1⇩m d" using measurement_le_one_mat m M1_def by auto
define W where "W k = wlp_while_n M0 M1 (wlp S) k P" for k
define DS where "DS = denote S"
define D0 where "D0 = denote_while_n M0 M1 DS"
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
define D where "D = denote_while_n_iter M0 M1 DS"
have eqk: "ρ ∈ density_states ⟹ trace ((W k) * ρ) = (∑k=0..<k. trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<k. trace (D0 k ρ))" for k ρ
proof (induct k arbitrary: ρ)
case 0
then have dsr: "ρ ∈ density_states" by auto
show ?case unfolding W_def wlp_while_n.simps using dsr density_states_def by auto
next
case (Suc k)
then have dsr: "ρ ∈ density_states" and dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
then have dsM1r: "M1 * ρ * adjoint M1 ∈ density_states" unfolding density_states_def using pdo_close_under_measurement[OF dM1 dr pdor leM1] dr dM1 by auto
then have dsDSM1r: "(DS (M1 * ρ * adjoint M1)) ∈ density_states" unfolding density_states_def DS_def
using denote_dim[OF wcS] denote_partial_density_operator[OF wcS] dsM1r by auto
have qpWk: "is_quantum_predicate (W k)"
using wlp_while_n_close[OF _ m qpP, folded M0_def M1_def, of "wlp S", folded W_def] wlp_close[OF wcS] by auto
then have "is_quantum_predicate (wlp S (W k))" using wlp_close[OF wcS] by auto
then have dWWk: "wlp S (W k) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have "trace (P * (M0 * ρ * adjoint M0)) + (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1)))))
= trace (P * (D0 0 ρ)) + (∑k=0..<k. trace (P * (D0 (Suc k) ρ)))"
unfolding D0_def by auto
also have "… = trace (P * (D0 0 ρ)) + (∑k=1..<(Suc k). trace (P * (D0 k ρ)))"
using sum.shift_bounds_Suc_ivl[symmetric, of "λk. trace (P * (D0 k ρ))"] by auto
also have "… = (∑k=0..<(Suc k). trace (P * (D0 k ρ)))" using sum.atLeast_Suc_lessThan[of 0 "Suc k" "λk. trace (P * (D0 k ρ))"] by auto
finally have eq1: "trace (P * (M0 * ρ * adjoint M0)) + (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1)))))
= (∑k=0..<(Suc k). trace (P * (D0 k ρ)))".
have eq2: "trace (M1 * ρ * adjoint M1) = trace ρ - trace (M0 * ρ * adjoint M0)"
unfolding M0_def M1_def using m trace_measurement2[OF m dr] dr by (simp add: algebra_simps)
have "trace (M0 * ρ * adjoint M0) + (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))
= trace (D0 0 ρ) + (∑k=0..<k. trace (D0 (Suc k) ρ))" unfolding D0_def by auto
also have "… = trace (D0 0 ρ) + (∑k=1..<(Suc k). trace (D0 k ρ))"
using sum.shift_bounds_Suc_ivl[symmetric, of "λk. trace (D0 k ρ)"] by auto
also have "… = (∑k=0..<(Suc k). trace (D0 k ρ))"
using sum.atLeast_Suc_lessThan[of 0 "Suc k" "λk. trace (D0 k ρ)"] by auto
finally have eq3: "trace (M0 * ρ * adjoint M0) + (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1)))) = (∑k=0..<(Suc k). trace (D0 k ρ))".
then have "trace (M1 * ρ * adjoint M1) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))
= trace ρ - (trace (M0 * ρ * adjoint M0) + (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1)))))"
by (simp add: algebra_simps eq2)
then have eq4: "trace (M1 * ρ * adjoint M1) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1)))) = trace ρ - (∑k=0..<(Suc k). trace (D0 k ρ))"
by (simp add: eq3)
have "trace ((W (Suc k)) * ρ) = trace (P * (M0 * ρ * adjoint M0)) + trace ((wlp S (W k)) * (M1 * ρ * adjoint M1))"
unfolding W_def wlp_while_n.simps
apply (fold W_def) using dM0 dP dM1 dWWk dr by (mat_assoc d)
also have "… = trace (P * (M0 * ρ * adjoint M0)) + trace ((W k) * (DS (M1 * ρ * adjoint M1))) + trace (M1 * ρ * adjoint M1) - trace (DS (M1 * ρ * adjoint M1))"
using While(1)[OF wcS, of "W k"] qpWk dsM1r DS_def by auto
also have "… = trace (P * (M0 * ρ * adjoint M0))
+ (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1))))) + trace (DS (M1 * ρ * adjoint M1)) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))
+ trace (M1 * ρ * adjoint M1) - trace (DS (M1 * ρ * adjoint M1))"
using Suc(1)[OF dsDSM1r] by auto
also have "… = trace (P * (M0 * ρ * adjoint M0)) + (∑k=0..<k. trace (P * (D0 k (DS (M1 * ρ * adjoint M1)))))
+ trace (M1 * ρ * adjoint M1) - (∑k=0..<k. trace (D0 k (DS (M1 * ρ * adjoint M1))))"
by auto
also have "… = (∑k=0..<(Suc k). trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<(Suc k). trace (D0 k ρ))"
by (simp add: eq1 eq4)
finally show ?case.
qed
{
fix ρ assume dsr: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have limDW: "limit_mat (λn. matrix_sum d (λk. D0 k ρ) (n)) (denote (While M S) ρ) d"
using limit_mat_denote_while_n[OF wc dr pdor] unfolding D0_def M0_def M1_def DS_def by auto
then have "limit_mat (λn. (P * (matrix_sum d (λk. D0 k ρ) (n)))) (P * (denote (While M S) ρ)) d"
using mat_mult_limit[OF dP] unfolding mat_mult_seq_def by auto
then have limtrPm: "(λn. trace (P * (matrix_sum d (λk. D0 k ρ) (n)))) ⇢ trace (P * (denote (While M S) ρ))"
using mat_trace_limit by auto
with limDW have limtrDW:"(λn. trace (matrix_sum d (λk. D0 k ρ) (n))) ⇢ trace (denote (While M S) ρ)"
using mat_trace_limit by auto
have limm: "(λn. trace (matrix_sum d (λk. D0 k ρ) (n))) ⇢ trace (denote (While M S) ρ)"
using mat_trace_limit limDW by auto
have closeWS: "is_quantum_predicate P ⟹ is_quantum_predicate (wlp S P)" for P
proof -
assume asm: "is_quantum_predicate P"
then have dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then show "is_quantum_predicate (wlp S P)" using wlp_mono_and_close[OF wcS asm asm] lowner_le_refl by auto
qed
have monoWS: "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ P ≤⇩L Q ⟹ wlp S P ≤⇩L wlp S Q" for P Q
using wlp_mono_and_close[OF wcS] by auto
have "is_quantum_predicate (wlp (While M S) P)"
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP by auto
have "limit_mat W (wlp_while M0 M1 (wlp S) P) d" unfolding W_def M0_def M1_def
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP by auto
then have "limit_mat (λk. (W k) * ρ) ((wlp_while M0 M1 (wlp S) P) * ρ) d" using mult_mat_limit dr by auto
then have lim1: "(λk. trace ((W k) * ρ)) ⇢ trace ((wlp_while M0 M1 (wlp S) P) * ρ)"
using mat_trace_limit by auto
have dD0kr: "D0 k ρ ∈ carrier_mat d d" for k unfolding D0_def
using denote_while_n_dim[OF dr dM0 dM1 pdor] denote_positive_trace_dim[OF wcS, folded DS_def] by auto
then have "(P * (matrix_sum d (λk. D0 k ρ) (n))) = matrix_sum d (λk. P * (D0 k ρ)) n" for n
using matrix_sum_distrib_left[OF dP] by auto
moreover have "trace (matrix_sum d (λk. P * (D0 k ρ)) n) = (∑k=0..<n. trace (P * (D0 k ρ)))" for n
using trace_matrix_sum_linear dD0kr dP by auto
ultimately have eqPsD0kr: "trace (P * (matrix_sum d (λk. D0 k ρ) (n))) = (∑k=0..<n. trace (P * (D0 k ρ)))" for n by auto
with limtrPm have lim2: "(λk. (∑k=0..<k. trace (P * (D0 k ρ)))) ⇢ trace (P * (denote (While M S) ρ))" by auto
have "trace (matrix_sum d (λk. D0 k ρ) (n)) = (∑k=0..<n. trace (D0 k ρ))" for n
using trace_matrix_sum_linear dD0kr by auto
with limtrDW have lim3: "(λk. (∑k=0..<k. trace (D0 k ρ))) ⇢ trace (denote (While M S) ρ)" by auto
have "(λk. (∑k=0..<k. trace (P * (D0 k ρ))) + trace ρ) ⇢ trace (P * (denote (While M S) ρ)) + trace ρ"
using tendsto_add[of "λk. (∑k=0..<k. trace (P * (D0 k ρ)))"] lim2 by auto
then have "(λk. (∑k=0..<k. trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<k. trace (D0 k ρ)))
⇢ trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)"
using tendsto_diff[of _ _ _ "λk. (∑k=0..<k. trace (D0 k ρ))"] lim3 by auto
then have lim4: "(λk. trace ((W k) * ρ)) ⇢ trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)"
using eqk[OF dsr] by auto
then have "trace ((wlp_while M0 M1 (wlp S) P) * ρ) = trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)"
using eqk[OF dsr] tendsto_unique[OF _ lim1 lim4] by auto
}
then show ?case unfolding M0_def M1_def DS_def wlp.simps by auto
qed
lemma denote_while_split:
assumes wc: "well_com (While M S)" and dsr: "ρ ∈ density_states"
shows "denote (While M S) ρ = (M 0) * ρ * adjoint (M 0) + denote (While M S) (denote S (M 1 * ρ * adjoint (M 1)))"
proof -
have m: "measurement d 2 M" using wc by auto
have wcs: "well_com S" using wc by auto
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m measurement_def M0_def M1_def by auto
have M1leq: "adjoint M1 * M1 ≤⇩L 1⇩m d" using measurement_le_one_mat m M1_def by auto
define DS where "DS = denote S"
define D0 where "D0 = denote_while_n M0 M1 DS"
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
define D where "D = denote_while_n_iter M0 M1 DS"
define DW where "DW ρ = denote (While M S) ρ" for ρ
{
fix ρ assume dsr: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have pdoDkr: "⋀k. partial_density_operator (D k ρ)" unfolding D_def
using pdo_denote_while_n_iter[OF dr pdor dM1 M1leq]
denote_partial_density_operator[OF wcs] denote_dim[OF wcs, folded DS_def]
apply (fold DS_def) by auto
then have pDkr: "⋀k. positive (D k ρ)" unfolding partial_density_operator_def by auto
have dDkr: "⋀k. D k ρ ∈ carrier_mat d d"
using denote_while_n_iter_dim[OF dr pdor dM1 M1leq denote_dim_pdo[OF wcs, folded DS_def], of id M0, simplified, folded D_def] by auto
then have dD0kr: "⋀k. D0 k ρ ∈ carrier_mat d d" unfolding D0_def denote_while_n.simps apply (fold D_def) using dM0 by auto
}
note dD0k = this
have "matrix_sum d (λk. D0 k ρ) k ∈ carrier_mat d d" if dsr: "ρ ∈ density_states" for ρ k
using matrix_sum_dim[OF dD0k, of _ "λk. ρ" id, OF dsr] dsr by auto
{
fix k
have "matrix_sum d (λk. D0 k ρ) (Suc k) = (D0 0 ρ) + matrix_sum d (λk. D0 (Suc k) ρ) k"
using matrix_sum_shift_Suc[of _ "λk. D0 k ρ"] dD0k[OF dsr] by fastforce
also have "… = M0 * ρ * adjoint M0 + matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1))) k"
unfolding D0_def by auto
finally have "matrix_sum d (λk. D0 k ρ) (Suc k) = M0 * ρ * adjoint M0 + matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1))) k".
}
note eqk = this
have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def dsr by auto
then have "M1 * ρ * adjoint M1 ∈ carrier_mat d d" and "partial_density_operator (M1 * ρ * adjoint M1)"
using dM1 dr pdo_close_under_measurement[OF dM1 dr pdor M1leq] by auto
then have dSM1r: "(DS (M1 * ρ * adjoint M1)) ∈ carrier_mat d d" and pdoSM1r: "partial_density_operator (DS (M1 * ρ * adjoint M1))"
unfolding DS_def using denote_dim_pdo[OF wcs] by auto
have "limit_mat (matrix_sum d (λk. D0 k ρ)) (DW ρ) d" unfolding M0_def M1_def D0_def DS_def DW_def
using limit_mat_denote_while_n[OF wc dr pdor] by auto
then have liml: "limit_mat (λk. matrix_sum d (λk. D0 k ρ) (Suc k)) (DW ρ) d"
using limit_mat_ignore_initial_segment[of "matrix_sum d (λk. D0 k ρ)" "DW ρ" d 1] by auto
have dM0r: "M0 * ρ * adjoint M0 ∈ carrier_mat d d" using dM0 dr by fastforce
have "limit_mat (matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1)))) (DW (DS (M1 * ρ * adjoint M1))) d"
using limit_mat_denote_while_n[OF wc dSM1r pdoSM1r] unfolding M0_def M1_def D0_def DS_def DW_def by auto
then have
limr: "limit_mat
(mat_add_seq (M0 * ρ * adjoint M0) (matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1)))))
(M0 * ρ * adjoint M0 + (DW (DS (M1 * ρ * adjoint M1))))
d"
using mat_add_limit[OF dM0r] by auto
moreover have
"(λk. matrix_sum d (λk. D0 k ρ) (Suc k))
= (mat_add_seq (M0 * ρ * adjoint M0) (matrix_sum d (λk. D0 k (DS (M1 * ρ * adjoint M1)))))"
using eqk mat_add_seq_def by auto
ultimately have
"limit_mat
(λk. matrix_sum d (λk. D0 k ρ) (Suc k))
(M0 * ρ * adjoint M0 + (DW (DS (M1 * ρ * adjoint M1))))
d" by auto
with liml limit_mat_unique have
"DW ρ = (M0 * ρ * adjoint M0 + (DW (DS (M1 * ρ * adjoint M1))))" by auto
then show ?thesis unfolding DW_def M0_def M1_def DS_def by auto
qed
lemma wlp_while_split:
assumes wc: "well_com (While M S)" and qpP: "is_quantum_predicate P"
shows "wlp (While M S) P = adjoint (M 0) * P * (M 0) + adjoint (M 1) * (wlp S (wlp (While M S) P)) * (M 1)"
proof -
have m: "measurement d 2 M" using wc by auto
have wcs: "well_com S" using wc by auto
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
have dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d" using m measurement_def M0_def M1_def by auto
have M1leq: "adjoint M1 * M1 ≤⇩L 1⇩m d" using measurement_le_one_mat m M1_def by auto
define DS where "DS = denote S"
define D0 where "D0 = denote_while_n M0 M1 DS"
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
define D where "D = denote_while_n_iter M0 M1 DS"
define DW where "DW ρ = denote (While M S) ρ" for ρ
have dP: "P ∈ carrier_mat d d" using qpP is_quantum_predicate_def by auto
have qpWP: "is_quantum_predicate (wlp (While M S) P)" using qpP wc wlp_close[OF wc qpP] by auto
then have "is_quantum_predicate (wlp S (wlp (While M S) P))" using wc wlp_close[OF wcs] by auto
then have dWWP: "(wlp S (wlp (While M S) P)) ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have dWP: "(wlp (While M S) P) ∈ carrier_mat d d" using qpWP is_quantum_predicate_def by auto
{
fix ρ assume dsr: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have dsM1r: "M1 * ρ * adjoint M1 ∈ density_states" unfolding density_states_def
using pdo_close_under_measurement[OF dM1 dr pdor] M1leq dM1 dr by fastforce
then have dsDSM1r: "DS (M1 * ρ * adjoint M1) ∈ density_states" unfolding density_states_def DS_def
using denote_dim_pdo[OF wcs] by auto
have dM0r: "M0 * ρ * adjoint M0 ∈ carrier_mat d d" using dM0 dr by fastforce
have dDWDSM1r: "DW (DS (M1 * ρ * adjoint M1)) ∈ carrier_mat d d"
unfolding DW_def using denote_dim[OF wc] dsDSM1r density_states_def by auto
have eq2: "trace ((wlp (While M S) P) * DS (M1 * ρ * adjoint M1))
= trace (P * (DW (DS (M1 * ρ * adjoint M1)))) + trace (DS (M1 * ρ * adjoint M1)) - trace (DW (DS (M1 * ρ * adjoint M1)))"
unfolding DW_def using wlp_soundness[OF wc qpP] dsDSM1r by auto
have eq3: "trace (M1 * ρ * adjoint M1) = trace ρ - trace (M0 * ρ * adjoint M0)"
unfolding M0_def M1_def using m trace_measurement2[OF m dr] dr by (simp add: algebra_simps)
have "trace (adjoint M1 * (wlp S (wlp (While M S) P)) * M1 * ρ)
= trace ((wlp S (wlp (While M S) P)) * (M1 * ρ * adjoint M1))" using dWWP dM1 dr by (mat_assoc d)
also have "… = trace ((wlp (While M S) P) * DS (M1 * ρ * adjoint M1))
+ trace (M1 * ρ * adjoint M1) - trace (DS (M1 * ρ * adjoint M1))"
unfolding DS_def using wlp_soundness[OF wcs qpWP] dsM1r by auto
also have "… = trace (P * (DW (DS (M1 * ρ * adjoint M1))))
+ trace (M1 * ρ * adjoint M1) - trace (DW (DS (M1 * ρ * adjoint M1)))"
using eq2 by auto
also have "… = trace (P * (DW (DS (M1 * ρ * adjoint M1)))) + trace ρ - (trace (M0 * ρ * adjoint M0) + trace (DW (DS (M1 * ρ * adjoint M1))))"
using eq3 by auto
finally have eq4: "trace (adjoint M1 * (wlp S (wlp (While M S) P)) * M1 * ρ)
= trace (P * (DW (DS (M1 * ρ * adjoint M1)))) + trace ρ - (trace (M0 * ρ * adjoint M0) + trace (DW (DS (M1 * ρ * adjoint M1))))".
have "trace (adjoint M0 * P * M0 * ρ) + trace (P * (DW (DS (M1 * ρ * adjoint M1))))
= trace (P * ((M0 * ρ * adjoint M0) + (DW (DS (M1 * ρ * adjoint M1)))))"
using dP dr dM0 dDWDSM1r by (mat_assoc d)
also have "… = trace (P * (DW ρ))" unfolding DW_def M0_def M1_def DS_def using denote_while_split[OF wc dsr] by auto
finally have eq5: "trace (adjoint M0 * P * M0 * ρ) + trace (P * (DW (DS (M1 * ρ * adjoint M1)))) = trace (P * (DW ρ))".
have "trace (M0 * ρ * adjoint M0) + trace (DW (DS (M1 * ρ * adjoint M1)))
= trace (M0 * ρ * adjoint M0 + (DW (DS (M1 * ρ * adjoint M1))))"
using dr dM0 dDWDSM1r by (mat_assoc d)
also have "… = trace (DW ρ)"
unfolding DW_def DS_def M0_def M1_def denote_while_split[OF wc dsr] by auto
finally have eq6: "trace (M0 * ρ * adjoint M0) + trace (DW (DS (M1 * ρ * adjoint M1))) = trace (DW ρ)".
from eq5 eq4 eq6 have
eq7: "trace (adjoint M0 * P * M0 * ρ) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * ρ)
= trace (P * DW ρ) + trace ρ - trace (DW ρ)" by auto
have eq8: "trace (adjoint M0 * P * M0 * ρ) + trace (adjoint M1 * wlp S (wlp (While M S) P) * M1 * ρ)
= trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ρ)"
using dM0 dM1 dr dP dWWP by (mat_assoc d)
from eq7 eq8 have
eq9: "trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ρ) = trace (P * DW ρ) + trace ρ - trace (DW ρ)" by auto
have eq10: "trace ((wlp (While M S) P) * ρ) = trace (P * DW ρ) + trace ρ - trace (DW ρ)"
unfolding DW_def using wlp_soundness[OF wc qpP] dsr by auto
with eq9 have "trace ((wlp (While M S) P) * ρ) = trace ((adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1) * ρ)" by auto
}
then have "(wlp (While M S) P) = (adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1)"
using trace_pdo_eq_imp_eq[OF dWP, of "adjoint M0 * P * M0 + adjoint M1 * wlp S (wlp (While M S) P) * M1"]
dM0 dP dM1 dWWP density_states_def by fastforce
then show ?thesis using M0_def M1_def by auto
qed
lemma wlp_is_weakest_liberal_precondition:
assumes "well_com S" and "is_quantum_predicate P"
shows "is_weakest_liberal_precondition (wlp S P) S P"
unfolding is_weakest_liberal_precondition_def
proof (auto)
show qpWP: "is_quantum_predicate (wlp S P)" using wlp_close assms by auto
have eq: "trace (wlp S P * ρ) = trace (P * (denote S ρ)) + trace ρ - trace (denote S ρ)" if dsr: "ρ ∈ density_states" for ρ
using wlp_soundness assms dsr by auto
then show "⊨⇩p {wlp S P} S {P}" unfolding hoare_partial_correct_def by auto
fix Q assume qpQ: "is_quantum_predicate Q" and p: "⊨⇩p {Q} S {P}"
{
fix ρ assume dsr: "ρ ∈ density_states"
then have "trace (Q * ρ) ≤ trace (P * (denote S ρ)) + trace ρ - trace (denote S ρ)"
using hoare_partial_correct_def p by (auto simp: less_eq_complex_def)
then have "trace (Q * ρ) ≤ trace (wlp S P * ρ)" using eq[symmetric] dsr by auto
}
then show "Q ≤⇩L wlp S P" using lowner_le_trace density_states_def qpQ qpWP is_quantum_predicate_def by auto
qed
subsection ‹Hoare triples for partial correctness›
inductive hoare_partial :: "complex mat ⇒ com ⇒ complex mat ⇒ bool" (‹⊢⇩p ({(1_)}/ (_)/ {(1_)})› 50) where
"is_quantum_predicate P ⟹ ⊢⇩p {P} SKIP {P}"
| "is_quantum_predicate P ⟹ ⊢⇩p {adjoint U * P * U} Utrans U {P}"
| "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ is_quantum_predicate R ⟹
⊢⇩p {P} S1 {Q} ⟹ ⊢⇩p {Q} S2 {R} ⟹
⊢⇩p {P} Seq S1 S2 {R}"
| "(⋀k. k < n ⟹ is_quantum_predicate (P k)) ⟹ is_quantum_predicate Q ⟹
(⋀k. k < n ⟹ ⊢⇩p {P k} S ! k {Q}) ⟹
⊢⇩p {matrix_sum d (λk. adjoint (M k) * P k * M k) n} Measure n M S {Q}"
| "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹
⊢⇩p {Q} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1} ⟹
⊢⇩p {adjoint (M 0) * P * M 0 + adjoint (M 1) * Q * M 1} While M S {P}"
| "is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ is_quantum_predicate P' ⟹ is_quantum_predicate Q' ⟹
P ≤⇩L P' ⟹ ⊢⇩p {P'} S {Q'} ⟹ Q' ≤⇩L Q ⟹ ⊢⇩p {P} S {Q}"
theorem hoare_partial_sound:
"⊢⇩p {P} S {Q} ⟹ well_com S ⟹ ⊨⇩p {P} S {Q}"
proof (induction rule: hoare_partial.induct)
case (1 P)
then show ?case
unfolding hoare_partial_correct_def by auto
next
case (2 P U)
then have dU: "U ∈ carrier_mat d d" and "unitary U" and dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def by auto
then have uU: "adjoint U * U = 1⇩m d" using unitary_def by auto
show ?case
unfolding hoare_partial_correct_def denote.simps(2)
proof
fix ρ assume "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" using density_states_def by auto
have e1: "trace (U * ρ * adjoint U) = trace ((adjoint U * U) * ρ)"
using dr dU by (mat_assoc d)
also have "… = trace ρ"
using uU dr by auto
finally have e1: "trace (U * ρ * adjoint U) = trace ρ" .
have e2: "trace (P * (U * ρ * adjoint U)) = trace (adjoint U * P * U * ρ)"
using dU dP dr by (mat_assoc d)
with e1 have "trace (P * (U * ρ * adjoint U)) + (trace ρ - trace (U * ρ * adjoint U)) = trace (adjoint U * P * U * ρ)"
using e1 by auto
then show "trace (adjoint U * P * U * ρ) ≤ trace (P * (U * ρ * adjoint U)) + (trace ρ - trace (U * ρ * adjoint U))" by auto
qed
next
case (3 P Q R S1 S2)
then have wc1: "⊨⇩p {P} S1 {Q}" and wc2: "⊨⇩p {Q} S2 {R}" by auto
show ?case
unfolding hoare_partial_correct_def denote.simps(3)
proof clarify
fix ρ assume ρ: "ρ ∈ density_states"
have 1: "trace (P * ρ) ≤ trace (Q * denote S1 ρ) + (trace ρ - trace (denote S1 ρ))"
using wc1 hoare_partial_correct_def ρ by auto
have ρ': "denote S1 ρ ∈ density_states"
using 3(8) denote_density_states ρ by auto
have 2: "trace (Q * denote S1 ρ) ≤ trace (R * denote S2 (denote S1 ρ)) + (trace (denote S1 ρ) - trace (denote S2 (denote S1 ρ)))"
using wc2 hoare_partial_correct_def ρ' by auto
show "trace (P * ρ) ≤ trace (R * denote S2 (denote S1 ρ)) + (trace ρ - trace (denote S2 (denote S1 ρ)))"
using 1 2 by (auto simp: less_eq_complex_def)
qed
next
case (4 n P Q S M)
then have wc: "k < n ⟹ well_com (S!k)"
and c: "k < n ⟹ ⊨⇩p {P k} (S!k) {Q}" and m: "measurement d n M"
and dMk: "k < n ⟹ M k ∈ carrier_mat d d"
and aMMkleq: "k < n ⟹ adjoint (M k) * M k ≤⇩L 1⇩m d"
and dPk: "k < n ⟹ P k ∈ carrier_mat d d"
and dQ: "Q ∈ carrier_mat d d"
for k using is_quantum_predicate_def measurement_def measure_well_com measurement_le_one_mat by auto
{
fix ρ assume ρ: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ" using density_states_def by auto
have dsr: "k < n ⟹ (M k) * ρ * adjoint (M k) ∈ density_states" for k unfolding density_states_def
using dMk pdo_close_under_measurement[OF dMk dr pdor aMMkleq] dr by fastforce
then have leqk: "k < n ⟹ trace ((P k) * ((M k) * ρ * adjoint (M k))) ≤
trace (Q * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" for k
using c unfolding hoare_partial_correct_def by auto
have "k < n ⟹ M k * ρ * adjoint (M k) ∈ carrier_mat d d" for k using dMk dr by fastforce
then have dsMrk: "k < n ⟹ matrix_sum d (λk. (M k * ρ * adjoint (M k))) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. (M k * ρ * adjoint (M k))" d] by fastforce
have "k < n ⟹ adjoint (M k) * P k * M k ∈ carrier_mat d d" for k using dMk dPk by fastforce
then have dsMP: "k < n ⟹ matrix_sum d (λk. adjoint (M k) * P k * M k) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. adjoint (M k) * P k * M k" d] by fastforce
have dSMrk: "k < n ⟹ denote (S ! k) (M k * ρ * adjoint (M k)) ∈ carrier_mat d d" for k
using denote_dim[OF wc, of k "M k * ρ * adjoint (M k)"] dsr density_states_def by fastforce
have dsSMrk: "k < n ⟹ matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k ∈ carrier_mat d d" for k
using matrix_sum_dim[of k "λk. denote (S ! k) (M k * ρ * adjoint (M k))" d, OF dSMrk] by fastforce
have "k ≤ n ⟹
trace (matrix_sum d (λk. adjoint (M k) * P k * M k) k * ρ)
≤ trace (Q * (denote (Measure k M S) ρ)) + (trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) k) - trace (denote (Measure k M S) ρ))" for k
unfolding denote_measure_expand[OF _ 4(5)]
proof (induct k)
case 0
then show ?case using dQ dr pdor partial_density_operator_def positive_trace by auto
next
case (Suc k)
then have k: "k < n" by auto
have eq1: "trace (matrix_sum d (λk. adjoint (M k) * P k * M k) (Suc k) * ρ)
= trace (adjoint (M k) * P k * M k * ρ) + trace (matrix_sum d (λk. adjoint (M k) * P k * M k) k * ρ)"
unfolding matrix_sum.simps
using dMk[OF k] dPk[OF k] dr dsMP[OF k] by (mat_assoc d)
have "trace (adjoint (M k) * P k * M k * ρ) = trace (P k * (M k * ρ * adjoint (M k)))"
using dMk[OF k] dPk[OF k] dr by (mat_assoc d)
also have "… ≤ trace (Q * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))" using leqk k by auto
finally have eq2: "trace (adjoint (M k) * P k * M k * ρ) ≤ trace (Q * (denote (S!k) ((M k) * ρ * adjoint (M k)))) +
(trace ((M k) * ρ * adjoint (M k)) - trace (denote (S ! k) ((M k) * ρ * adjoint (M k))))".
have eq3: "trace (Q * matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) (Suc k))
= trace (Q * (denote (S!k) (M k * ρ * adjoint (M k)))) + trace (Q * matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)"
unfolding matrix_sum.simps
using dQ dSMrk[OF k] dsSMrk[OF k] by (mat_assoc d)
have eq4: "trace (denote (S ! k) (M k * ρ * adjoint (M k)) + matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)
= trace (denote (S ! k) (M k * ρ * adjoint (M k))) + trace (matrix_sum d (λk. denote (S!k) (M k * ρ * adjoint (M k))) k)"
using dSMrk[OF k] dsSMrk[OF k] by (mat_assoc d)
show ?case
apply (subst eq1) apply (subst eq3)
apply (simp del: less_eq_complex_def)
apply (subst trace_add_linear[of "M k * ρ * adjoint (M k)" d "matrix_sum d (λk. M k * ρ * adjoint (M k)) k"])
apply (simp add: dMk adjoint_dim[OF dMk] dr mult_carrier_mat[of _ d d _ d] k)
apply (simp add: dsMrk k)
apply (subst eq4)
apply (insert eq2 Suc(1) k, fastforce simp: less_eq_complex_def)
done
qed
then have leq: "trace (matrix_sum d (λk. adjoint (M k) * P k * M k) n * ρ)
≤ trace (Q * denote (Measure n M S) ρ) +
(trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) n) - trace (denote (Measure n M S) ρ))"
by auto
have "trace (matrix_sum d (λk. (M k) * ρ * adjoint (M k)) n) = trace ρ" using trace_measurement m dr by auto
with leq have "trace (matrix_sum d (λk. adjoint (M k) * P k * M k) n * ρ)
≤ trace (Q * denote (Measure n M S) ρ) + (trace ρ - trace (denote (Measure n M S) ρ))"
unfolding denote_measure_def by auto
}
then show ?case unfolding hoare_partial_correct_def by auto
next
case (5 P Q S M)
define M0 where "M0 = M 0"
define M1 where "M1 = M 1"
from 5 have wcs: "well_com S" and c: "⊨⇩p {Q} S {adjoint M0 * P * M0 + adjoint M1 * Q * M1}"
and m: "measurement d 2 M"
and dM0: "M0 ∈ carrier_mat d d" and dM1: "M1 ∈ carrier_mat d d"
and dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d"
and qpQ: "is_quantum_predicate Q"
and wc: "well_com (While M S)"
using measurement_def is_quantum_predicate_def M0_def M1_def by auto
then have M0leq: "adjoint M0 * M0 ≤⇩L 1⇩m d" and M1leq: "adjoint M1 * M1 ≤⇩L 1⇩m d" using measurement_le_one_mat[OF m] M0_def M1_def by auto
define DS where "DS = denote S"
have "∀ρ ∈ density_states. trace (Q * ρ) ≤ trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * DS ρ) + trace ρ - trace (DS ρ)"
using hoare_partial_correct_def[of Q S "adjoint M0 * P * M0 + adjoint M1 * Q * M1"] c DS_def
by (auto simp: less_eq_complex_def)
define D0 where "D0 = denote_while_n M0 M1 DS"
define D1 where "D1 = denote_while_n_comp M0 M1 DS"
define D where "D = denote_while_n_iter M0 M1 DS"
{
fix ρ assume dsr: "ρ ∈ density_states"
then have dr: "ρ ∈ carrier_mat d d" and pr: "positive ρ" and pdor: "partial_density_operator ρ"
using density_states_def partial_density_operator_def by auto
have pdoDkr: "⋀k. partial_density_operator (D k ρ)" unfolding D_def
using pdo_denote_while_n_iter[OF dr pdor dM1 M1leq]
denote_partial_density_operator[OF wcs] denote_dim[OF wcs, folded DS_def]
apply (fold DS_def) by auto
then have pDkr: "⋀k. positive (D k ρ)" unfolding partial_density_operator_def by auto
have dDkr: "⋀k. D k ρ ∈ carrier_mat d d"
using denote_while_n_iter_dim[OF dr pdor dM1 M1leq denote_dim_pdo[OF wcs, folded DS_def], of id M0, simplified, folded D_def] by auto
then have dD0kr: "⋀k. D0 k ρ ∈ carrier_mat d d" unfolding D0_def denote_while_n.simps apply (fold D_def) using dM0 by auto
then have dPD0kr: "⋀k. P * (D0 k ρ) ∈ carrier_mat d d" using dP by auto
have "⋀k. positive (D0 k ρ)" unfolding D0_def denote_while_n.simps
by (fold D_def, rule positive_close_under_left_right_mult_adjoint[OF dM0 dDkr pDkr])
then have trge0: "⋀k. trace (D0 k ρ) ≥ 0" using positive_trace dD0kr by blast
have DSr: "ρ ∈ density_states ⟹ DS ρ ∈ density_states" for "ρ" unfolding DS_def density_states_def
using denote_partial_density_operator denote_dim wcs by auto
have dsD1nr: "D1 n ρ ∈ density_states" for n unfolding D1_def denote_while_n_comp.simps
apply (fold D_def) unfolding density_states_def
apply (auto)
apply (insert dDkr dM1 adjoint_dim[OF dM1], auto)
apply (rule pdo_close_under_measurement[OF dM1 spec[OF allI[OF dDkr], of "λx. n"] spec[OF allI[OF pdoDkr], of "λx. n"] M1leq])
done
have leQn: "trace (Q * D1 n ρ)
≤ trace (P * D0 (Suc n) ρ) + trace (Q * D1 (Suc n) ρ)
+ trace (D1 n ρ) - trace (D (Suc n) ρ)" for n
proof -
have "(∀ρ∈density_states. trace (Q * ρ) ≤ trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * denote S ρ) + (trace ρ - trace (denote S ρ)))"
using c hoare_partial_correct_def by auto
then have leQn': "trace (Q * (D1 n ρ))
≤ trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * (DS (D1 n ρ)))
+ (trace (D1 n ρ) - trace (DS (D1 n ρ)))"
using dsD1nr[of n] DS_def by auto
have "(DS (D1 n ρ)) ∈ carrier_mat d d" unfolding DS_def using denote_dim[OF wcs] dsD1nr density_states_def by auto
then have "trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * (DS (D1 n ρ)))
= trace (P * (M0 * (DS (D1 n ρ)) * adjoint M0))
+ trace (Q * (M1 * (DS (D1 n ρ)) * adjoint M1))" using dP dQ dM0 dM1 by (mat_assoc d)
moreover have "trace (P * (M0 * (DS (D1 n ρ)) * adjoint M0)) = trace (P * D0 (Suc n) ρ)"
unfolding D0_def denote_while_n.simps
apply (subst denote_while_n_iter_assoc)
by (fold denote_while_n_comp.simps D1_def, auto)
moreover have "trace (Q * (M1 * (DS (D1 n ρ)) * adjoint M1)) = trace (Q * D1 (Suc n) ρ)"
apply (subst (2) D1_def) unfolding denote_while_n_comp.simps
apply (subst denote_while_n_iter_assoc)
by (fold denote_while_n_comp.simps D1_def, auto)
ultimately have "trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * (DS (D1 n ρ)))
= trace (P * D0 (Suc n) ρ) + trace (Q * D1 (Suc n) ρ)" by auto
moreover have "trace (DS (D1 n ρ)) = trace (D (Suc n) ρ)"
unfolding D_def
apply (subst denote_while_n_iter_assoc)
by (fold denote_while_n_comp.simps D1_def, auto)
ultimately show ?thesis using leQn' by (auto simp: less_eq_complex_def)
qed
have 12: "trace (P * (M0 * ρ * adjoint M0)) + trace (Q * (M1 * ρ * adjoint M1))
≤ (∑k=0..<(n+2). trace (P * (D0 k ρ))) + trace (Q * (D1 (n+1) ρ))
+ (∑k=0..<(n+1). trace (D1 k ρ) - trace (D (k+1) ρ))" for n
proof (induct n)
case 0
show ?case apply (simp del: less_eq_complex_def)
unfolding D0_def D1_def D_def denote_while_n_comp.simps denote_while_n.simps denote_while_n_iter.simps
using leQn[of 0] unfolding D1_def D0_def D_def denote_while_n.simps denote_while_n_comp.simps denote_while_n_iter.simps
by (auto simp: less_eq_complex_def)
next
case (Suc n)
have "trace (Q * D1 (n + 1) ρ)
≤ trace (P * D0 (Suc (Suc n)) ρ) + trace (Q * D1 (Suc (Suc n)) ρ)
+ trace (D1 (Suc n) ρ) - trace (D (Suc (Suc n)) ρ)" using leQn[of "n + 1"] by auto
with Suc show ?case apply (simp del: less_eq_complex_def) by (auto simp: less_eq_complex_def)
qed
have tr_measurement: "ρ ∈ carrier_mat d d
⟹ trace (M0 * ρ * adjoint M0) + trace (M1 * ρ * adjoint M1) = trace ρ" for ρ
using trace_measurement2[OF m, folded M0_def M1_def] by auto
have 14: "(∑k=0..<(n+1). trace (D1 k ρ) - trace (D (k+1) ρ)) = trace ρ - trace (D (n+1) ρ) - (∑k=0..<(n+1). trace (D0 k ρ))" for n
proof (induct n)
case 0
show ?case apply (simp) unfolding D1_def D0_def denote_while_n_comp.simps denote_while_n.simps denote_while_n_iter.simps
using tr_measurement[OF dr] by (auto simp add: algebra_simps)
next
case (Suc n)
have "trace (D0 (Suc n) ρ) + trace (D1 (Suc n) ρ) = trace (D (Suc n) ρ)"
unfolding D0_def D1_def denote_while_n.simps denote_while_n_comp.simps apply (fold D_def)
using tr_measurement dDkr by auto
then have "trace (D1 (Suc n) ρ) = trace (D (Suc n) ρ) - trace (D0 (Suc n) ρ)"
by (auto simp add: algebra_simps)
then show ?case using Suc by simp
qed
have 15: "trace (Q * (D1 n ρ)) ≤ trace (D n ρ) - trace (D0 n ρ)" for n
proof -
have QleId: "Q ≤⇩L 1⇩m d" using is_quantum_predicate_def qpQ by auto
then have "trace (Q * (D1 n ρ)) ≤ trace (1⇩m d * (D1 n ρ))" using
dsD1nr[of n] unfolding density_states_def lowner_le_trace[OF dQ one_carrier_mat] by auto
also have "… = trace (D1 n ρ)" using dsD1nr[of n] unfolding density_states_def by auto
also have "… = trace (M1 * (D n ρ) * adjoint M1)" unfolding D1_def denote_while_n_comp.simps D_def by auto
also have "… = trace (D n ρ) - trace (M0 * (D n ρ) * adjoint M0)"
using tr_measurement[OF dDkr[of n]] by (simp add: algebra_simps)
also have "… = trace (D n ρ) - trace (D0 n ρ)" unfolding D0_def denote_while_n.simps by (fold D_def, auto)
finally show ?thesis.
qed
have tmp: "⋀a b c. 0 ≤ a ⟹ b ≤ c - a ⟹ b ≤ (c::complex)"
by (simp add: less_eq_complex_def)
then have 151: "⋀n. trace (Q * (D1 n ρ)) ≤ trace (D n ρ)"
by (auto simp add: tmp[OF trge0 15] simp del: less_eq_complex_def)
have main_leq: "⋀n. trace (P * (M0 * ρ * adjoint M0)) + trace (Q * (M1 * ρ * adjoint M1))
≤ trace (P * (matrix_sum d (λk. D0 k ρ) (n+2))) + trace ρ - trace (matrix_sum d (λk. D0 k ρ) (n+2))"
proof -
fix n
have "(∑k=0..<(n+2). trace (P * (D0 k ρ))) + trace (Q * (D1 (n+1) ρ))
+ (∑k=0..<(n+1). trace (D1 k ρ) - trace (D (k+1) ρ))
≤ (∑k=0..<(n+2). trace (P * (D0 k ρ))) + trace (Q * (D1 (n+1) ρ))
+ trace ρ - trace (D (n+1) ρ) - (∑k=0..<(n+1). trace (D0 k ρ))"
by (subst 14, auto)
also have
"… ≤ (∑k=0..<(n+2). trace (P * (D0 k ρ))) + trace (D (n+1) ρ) - trace (D0 (n+1) ρ)
+ trace ρ - trace (D (n+1) ρ) - (∑k=0..<(n+1). trace (D0 k ρ))"
using 15[of "n+1"] by (auto simp: less_eq_complex_def)
also have "… = (∑k=0..<(n+2). trace (P * (D0 k ρ))) + trace ρ - (∑k=0..<(n+2). trace (D0 k ρ))" by auto
also have "… = trace (matrix_sum d (λk. (P * (D0 k ρ))) (n+2)) + trace ρ - (∑k=0..<(n+2). trace (D0 k ρ))"
using trace_matrix_sum_linear[of "n+2" "λk. (P * (D0 k ρ))" d, symmetric] dPD0kr by auto
also have "… = trace (matrix_sum d (λk. (P * (D0 k ρ))) (n+2)) + trace ρ - trace (matrix_sum d (λk. D0 k ρ) (n+2))"
using trace_matrix_sum_linear[of "n+2" "λk. D0 k ρ" d, symmetric] dD0kr by auto
also have "… = trace (P * (matrix_sum d (λk. D0 k ρ) (n+2))) + trace ρ - trace (matrix_sum d (λk. D0 k ρ) (n+2))"
using matrix_sum_distrib_left[OF dP dD0kr, of id "n+2"] by auto
finally have
"(∑k=0..<(n+2). trace (P * (D0 k ρ))) + trace (Q * (D1 (n+1) ρ))
+ (∑k=0..<(n+1). trace (D1 k ρ) - trace (D (k+1) ρ))
≤ trace (P * (matrix_sum d (λk. D0 k ρ) (n+2))) + trace ρ - trace (matrix_sum d (λk. D0 k ρ) (n+2))" .
then show "trace (P * (M0 * ρ * adjoint M0)) + trace (Q * (M1 * ρ * adjoint M1))
≤ trace (P * (matrix_sum d (λk. D0 k ρ) (n+2))) + trace ρ - trace (matrix_sum d (λk. D0 k ρ) (n+2))" using 12[of n] by auto
qed
have "limit_mat (λn. matrix_sum d (λk. D0 k ρ) (n)) (denote (While M S) ρ) d"
using limit_mat_denote_while_n[OF wc dr pdor] unfolding D0_def M0_def M1_def DS_def by auto
then have limp2: "limit_mat (λn. matrix_sum d (λk. D0 k ρ) (n + 2)) (denote (While M S) ρ) d"
using limit_mat_ignore_initial_segment[of "λn. matrix_sum d (λk. D0 k ρ) (n)" "(denote (While M S) ρ)" d 2] by auto
then have "limit_mat (λn. (P * (matrix_sum d (λk. D0 k ρ) (n+2)))) (P * (denote (While M S) ρ)) d"
using mat_mult_limit[OF dP] unfolding mat_mult_seq_def by auto
then have limPm: "(λn. trace (P * (matrix_sum d (λk. D0 k ρ) (n+2)))) ⇢ trace (P * (denote (While M S) ρ))"
using mat_trace_limit by auto
have limm: "(λn. trace (matrix_sum d (λk. D0 k ρ) (n+2))) ⇢ trace (denote (While M S) ρ)"
using mat_trace_limit limp2 by auto
have leq_lim: "trace (P * (M0 * ρ * adjoint M0)) + trace (Q * (M1 * ρ * adjoint M1))
≤ trace (P * (denote (While M S) ρ)) + trace ρ - trace (denote (While M S) ρ)" (is "?lhs ≤ ?rhs")
using main_leq
proof -
define seq where "seq n = trace (P * matrix_sum d (λk. D0 k ρ) (n + 2)) - trace (matrix_sum d (λk. D0 k ρ) (n + 2)) " for n
define seqlim where "seqlim = trace (P * (denote (While M S) ρ)) - trace (denote (While M S) ρ)"
have main_leq': "?lhs ≤ trace ρ + seq n" for n
unfolding seq_def using main_leq by (simp add: algebra_simps)
have limseq: "seq ⇢ seqlim"
unfolding seq_def seqlim_def using tendsto_diff[OF limPm limm] by auto
have limrs: "(λn. trace ρ + seq n) ⇢ (trace ρ + seqlim)" using tendsto_add[OF _ limseq] by auto
have limrsRe: "(λn. Re (trace ρ + seq n)) ⇢ Re (trace ρ + seqlim)" using tendsto_Re[OF limrs] by auto
have main_leq_Re: "Re ?lhs ≤ Re (trace ρ + seq n)" for n using main_leq'
by (auto simp: less_eq_complex_def)
have Re: "Re ?lhs ≤ Re (trace ρ + seqlim)"
using Lim_bounded2[OF limrsRe ] main_leq_Re by (auto simp: less_eq_complex_def)
have limrsIm: "(λn. Im (trace ρ + seq n)) ⇢ Im (trace ρ + seqlim)" using tendsto_Im[OF limrs] by auto
have main_leq_Im: "Im ?lhs = Im (trace ρ + seq n)" for n using main_leq' unfolding less_eq_complex_def by auto
then have limIm: "(λn. Im (trace ρ + seq n)) ⇢ Im ?lhs" using tendsto_intros(1) by auto
have Im: "Im ?lhs = Im (trace ρ + seqlim)"
using tendsto_unique[OF _ limIm limrsIm] by auto
have "?lhs ≤ trace ρ + seqlim" using Re Im by (auto simp: less_eq_complex_def)
then show "?lhs ≤ ?rhs" unfolding seqlim_def by (auto simp: less_eq_complex_def)
qed
have "trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * ρ) =
trace (P * (M0 * ρ * adjoint M0)) + trace (Q * (M1 * ρ * adjoint M1))"
using dr dM0 dM1 dP dQ by (mat_assoc d)
then have "trace ((adjoint M0 * P * M0 + adjoint M1 * Q * M1) * ρ) ≤
trace (P * (denote (While M S) ρ)) + (trace ρ - trace (denote (While M S) ρ))"
using leq_lim by (auto simp: less_eq_complex_def)
}
then show ?case unfolding hoare_partial_correct_def denote.simps(5)
apply (fold M0_def M1_def DS_def D0_def D1_def) by auto
next
case (6 P Q P' Q' S)
then have wcs: "well_com S" and c: "⊨⇩p {P'} S {Q'}"
and dP: "P ∈ carrier_mat d d" and dQ: "Q ∈ carrier_mat d d"
and dP': "P' ∈ carrier_mat d d" and dQ': "Q' ∈ carrier_mat d d"
using is_quantum_predicate_def by auto
show ?case unfolding hoare_partial_correct_def
proof
fix ρ assume pds: "ρ ∈ density_states"
then have pdor: "partial_density_operator ρ" and dr: "ρ ∈ carrier_mat d d"
using density_states_def by auto
have pdoSr: "partial_density_operator (denote S ρ)"
using denote_partial_density_operator pdor dr wcs by auto
have dSr: "denote S ρ ∈ carrier_mat d d"
using denote_dim pdor dr wcs by auto
have "trace (P * ρ) ≤ trace (P' * ρ)" using lowner_le_trace[OF dP dP'] 6 dr pdor by auto
also have "… ≤ trace (Q' * denote S ρ) + (trace ρ - trace (denote S ρ))"
using c unfolding hoare_partial_correct_def using pds by auto
also have "… ≤ trace (Q * denote S ρ) + (trace ρ - trace (denote S ρ))" using lowner_le_trace[OF dQ' dQ] 6 dSr pdoSr by auto
finally show "trace (P * ρ) ≤ trace (Q * denote S ρ) + (trace ρ - trace (denote S ρ)) ".
qed
qed
lemma wlp_complete:
"well_com S ⟹ is_quantum_predicate P ⟹ ⊢⇩p {wlp S P} S {P}"
proof (induct S arbitrary: P)
case SKIP
then show ?case unfolding wlp.simps using hoare_partial.intros by auto
next
case (Utrans U)
then show ?case unfolding wlp.simps using hoare_partial.intros by auto
next
case (Seq S1 S2)
then have wc1: "well_com S1" and wc2: "well_com S2" and qpP: "is_quantum_predicate P"
and p2: "⊢⇩p {wlp S2 P} S2 {P}" by auto
have qpW2P: "is_quantum_predicate (wlp S2 P)" using wlp_close[OF wc2 qpP] by auto
then have p1: "⊢⇩p {wlp S1 (wlp S2 P)} S1 {wlp S2 P}" using Seq by auto
have qpW1W2P: "is_quantum_predicate (wlp S1 (wlp S2 P))" using wlp_close[OF wc1 qpW2P] by auto
then show ?case unfolding wlp.simps using hoare_partial.intros qpW1W2P qpW2P qpP p1 p2 by auto
next
case (Measure n M S)
then have wc: "well_com (Measure n M S)" and qpP: "is_quantum_predicate P" by auto
have set: "k < n ⟹ (S!k) ∈ set S" for k using wc by auto
have wck: "k < n ⟹ well_com (S!k)" for k using wc measure_well_com by auto
then have qpWkP: "k < n ⟹ is_quantum_predicate (wlp (S!k) P)" for k using wlp_close qpP by auto
have pk: "k < n ⟹ ⊢⇩p {(wlp (S!k) P)} (S!k) {P}" for k using Measure(1) set wck qpP by auto
show ?case unfolding wlp_measure_expand[OF wc] using hoare_partial.intros qpWkP qpP pk by auto
next
case (While M S)
then have wc: "well_com (While M S)" and wcS: "well_com S" and qpP: "is_quantum_predicate P " by auto
have qpWP: "is_quantum_predicate (wlp (While M S) P)" using wlp_close[OF wc qpP] by auto
then have qpWWP: "is_quantum_predicate (wlp S (wlp (While M S) P))" using wlp_close wcS by auto
have "⊢⇩p {wlp S (wlp (While M S) P)} S {wlp (While M S) P}" using While(1) wcS qpWP by auto
moreover have eq: "wlp (While M S) P = adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1"
using wlp_while_split wc qpP by auto
ultimately have p: "⊢⇩p {wlp S (wlp (While M S) P)} S {adjoint (M 0) * P * M 0 + adjoint (M 1) * wlp S (wlp (While M S) P) * M 1}" by auto
then show ?case using hoare_partial.intros(5)[OF qpP qpWWP p] eq by auto
qed
theorem hoare_partial_complete:
"⊨⇩p {P} S {Q} ⟹ well_com S ⟹ is_quantum_predicate P ⟹ is_quantum_predicate Q ⟹ ⊢⇩p {P} S {Q}"
proof -
assume p: "⊨⇩p {P} S {Q}" and wc: "well_com S" and qpP: "is_quantum_predicate P" and qpQ: "is_quantum_predicate Q"
then have dQ: "Q ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have qpWP: "is_quantum_predicate (wlp S Q)" using wlp_close wc qpQ by auto
then have dWP: "wlp S Q ∈ carrier_mat d d" using is_quantum_predicate_def by auto
have eq: "trace (wlp S Q * ρ) = trace (Q * (denote S ρ)) + trace ρ - trace (denote S ρ)" if dsr: "ρ ∈ density_states" for ρ
using wlp_soundness wc qpQ dsr by auto
then have "⊨⇩p {wlp S Q} S {Q}" unfolding hoare_partial_correct_def by auto
{
fix ρ assume dsr: "ρ ∈ density_states"
then have "trace (P * ρ) ≤ trace (Q * (denote S ρ)) + trace ρ - trace (denote S ρ)"
using hoare_partial_correct_def p by (auto simp: less_eq_complex_def)
then have "trace (P * ρ) ≤ trace (wlp S Q * ρ)" using eq[symmetric] dsr by auto
}
then have le: "P ≤⇩L wlp S Q" using lowner_le_trace density_states_def qpP qpWP is_quantum_predicate_def by auto
moreover have wlp: "⊢⇩p {wlp S Q} S {Q}" using wlp_complete wc qpQ by auto
ultimately show "⊢⇩p {P} S {Q}" using hoare_partial.intros(6)[OF qpP qpQ qpWP qpQ] lowner_le_refl[OF dQ] by auto
qed
subsection ‹Consequences of completeness›
lemma hoare_patial_seq_assoc_sem:
shows "⊨⇩p {A} (S1 ;; S2) ;; S3 {B} ⟷ ⊨⇩p {A} S1 ;; (S2 ;; S3) {B}"
unfolding hoare_partial_correct_def denote.simps by auto
lemma hoare_patial_seq_assoc:
assumes "well_com S1" and "well_com S2" and "well_com S3"
and "is_quantum_predicate A" and "is_quantum_predicate B"
shows "⊢⇩p {A} (S1 ;; S2) ;; S3 {B} ⟷ ⊢⇩p {A} S1 ;; (S2 ;; S3) {B}"
proof
assume "⊢⇩p {A} S1;; S2;; S3 {B}"
then have "⊨⇩p {A} (S1 ;; S2) ;; S3 {B}" using hoare_partial_sound assms by auto
then have "⊨⇩p {A} S1 ;; (S2 ;; S3) {B}" using hoare_patial_seq_assoc_sem by auto
then show "⊢⇩p {A} S1 ;; (S2 ;; S3) {B}" using hoare_partial_complete assms by auto
next
assume "⊢⇩p {A} S1;; (S2;; S3) {B}"
then have "⊨⇩p {A} S1;; (S2;; S3) {B}" using hoare_partial_sound assms by auto
then have "⊨⇩p {A} S1;; S2;; S3 {B}" using hoare_patial_seq_assoc_sem by auto
then show "⊢⇩p {A} S1;; S2;; S3 {B}" using hoare_partial_complete assms by auto
qed
end
end