1. Introduction
Formal verification is a technique for verifying the validity of proofs in mathematics, algorithms, computer sys- tems, and so on. In the formal verification by using logical reasoning, interactive theorem provers (HOL [1] , ACL2 [2] , Isabelle [3] , Coq [4] , just to a name a few) are used for verifying mathematical proofs. In accordance with the Curry-Howard correspondence [5] , the validity is verified through coding of the proofs in functional languages.
Formal verification by using the interactive theorem provers has been noticed as a technique for verifying proofs of theorems which are too large for humans to check the validity. Such a theorem as the Feit-Thompson theorem (also known as the odd order theorem) [6] can be enumerated as an example. This theorem was proven in 1963. However, the verification of the validity of the proof was highly difficult at 1980s [7] since its total number of pages are about 300. Gonthier et al. [8] verified the proof by using SSReflect which is an extension of the proof assistant Coq. The formalized theorem and lemmas which are formalized in the process of the veri- fication are utilized for the formalization of mathematical science. Therefore, the formal verification of rela- tively small lemmas which are used for large proofs is useful as a library for the verification of the other large proofs.
The formal verification is considered valid at information theory which is a branch of mathematical science. Affeldt et al. [9] formally verify basic definitions and theorems in information theory by using SSReflect, and also Shannon’s channel coding theorem and source coding theorem [10] which are famous theorems of all results of information theory. These formalized theorems are valuable not only toward the formally verification of integrity between coding and decoding algorithms and the software implemented ones, but also further facilitating of the formal verification by utilizing the formalized types.
In quantum information theory, the axioms of quantum physics are described mathematically [11] . Therefore, the formal verification can be applied to verifying the validity of quantum information theory. In this work, we verify the validity of uncertainty relation toward verifying unconditional security of quantum key distributions and encouraging the formal verification of large proofs in quantum information theory. Specifically, we verify the validity of Robertson-type uncertainty relation [12] by using the proof assistant Coq.
This paper is organized as follows. In Section 2, we review the theorem regarding Robertson-type uncertainty relation and its mathematically proof. In Section 3, we formally verify the validity of the theorem with Coq. In Section 4, this paper is summarized. Coq source code is printed in Appendix.
2. Robertson-Type Uncertainty Relation
Robertson-type uncertainty relation imposes a restriction on probability distributions of measurement outcomes with observables. In this type, uncertainty of the measurement is characterized by standard deviation of the dis- tribution.
In quantum information theory, a quantum system and a quantum pure state in the system are regarded in the same light as a Hilbert space and a unit vector in the space, respectively. In addition, an observable is regarded as an Hermitian operator on the Hilbert space. Let be variance of outcomes which are obtained by measuring a quantum system in a quantum state with an observable A. Then,
(1)
holds. Standard deviation of the outcomes is defined as. The following theorem was given by Robertson [12] .
Theorem 1 ( [9] [12] ). For two observables A, B, and a quantum state,
(2)
holds, where.
Proof. We observe and from the definition of standard deviation and
Hermiticity of the observable. holds from the Schwarz inequality
. We obtain, where. We observe
where we thank to Hermiticity of and.
holds from. Then,
holds. Therefore, Equation (2) can be observed immediately.
A relation between two observables represented by Equation (2) is called Robertson-type uncertainty relation. The right-hand side of the inequality always takes 0 if the observables are commutative. Therefore, both of standard deviations of the observables may take 0. On the other hand, for non-commutative observables, the right-hand side of the inequality dose not take 0. Then, both of standard deviations of the observables dose not take 0. This implies that Equation (2) is a tradeoff between uncertainties of the observables. In this case, the uncertainty is characterized by standard deviation.
The relation between the non-commutative observables often plays crucial role in discussion of unconditional security of quantum key distributions. In BB84 [13] which is the most famous quantum key distribution protocol, eigenstates of non-commutative observables and are used for sharing secret key between a sender (called Alice) and a receiver (called Bob). Alice prepares random bits and sends quantum bits (qubits) to Bob, where each qubit is prepared in one of the eigenstates of and with a procedure of the protocol. Bob measures each qubit with or randomly and obtains outcomes as a candidate key. For obtaining a sifted key, Alice and Bob check the choices of the observables in the state preparation and the quantum measurement. They calculate error rate of a part of the sifted key. The protocol is aboded if the rate is grater than preset value (this implies that they presume the existence of some kind of eavesdropping). Otherwise, they perform the leftover sifted key to make the secret key with error correction and privacy amplification. A purpose of a eavesdropper (called Eve) is to gain information of the secret key without being detected by Alice and Bob on the channel. Eve can gain information if she can distinguish the eigenstates of and. However, there is a tradeoff between information gain for Eve and the error rate. That is, she cannot gain information of the secret key generated by without increasing the error rate of the part of the sifted key generated by, and vice versa. The fact is known as the information disturbance theorem [14] - [16] and this theorem is applied to a proof of unconditional security of BB84 [14] . The information disturbance theorem can be regarded as an information theoretic version of uncertainty relation [15] . The theorem is obtained directly [16] from entropic uncertainty relation [17] [18] which is a kind of types of uncertainty relation. In this work, we verify the validity of Robertson-type uncertainty relation using the proof assistant Coq toward verifying entropic uncertainty relation, the information disturbance theorem, and unconditional security of quantum key distributions.
3. Formal Verification of Robertson-Type Uncertainty Relation
In this section, we verify the validity of Robertson-type uncertainty relation by using the proof assistant Coq. We define types as follows:
・ C: a type of a complex number
・ Vec C n: a type of an n-dimensional complex vector
・ UnitVec C n: a type of an n-dimensional complex unit vector
・ Mat C v: a type of a v = complex matrix
・ HMat v: a type of a v = Hermitian matrix
We define functions as follows:
・ var: takes a pair of a variable of UnitVec C n and a variable of HMat v and returns variant with respect to the variables (see Equation (1))
・ cabs: takes a variable of C and returns absolute value of it
・ mMinus: takes a pair of variables of Mat C v and returns addition of them
・ mMinus: takes a pair of variables of Mat C v and returns subtraction of them
・ mMult: takes a pair of variables of Mat C v and returns product of them
・ innerProd: takes a pair of variables of Vec C n and returns inner product of them
・ mvMult: takes a pair of a variable of Mat C v and a variable of Vec C n and returns product of them
Theorem 2. We declare a formalized statement of Robertson-type uncertainty relation in Coq:
Theorem RobertsonUR:
forall (n : nat) (v : mlenghts n) (A B: HMat v) (psi : UnitVec C n),
(sqrt (var psi A)) * (sqrt (var psi B)) >=
(1/2) * (cabs ( innerProd psi (mvMult (mMinus (mMult A B) (mMult B A)) psi))).
Before giving the formally proof described by Coq, we show the broad outlines of it. Firstly, we define the types and the functions in linear algebra. The types and functions are already shown above. The next step is to obtain subgoals through applying small lemmas to some inequalities. The subgoals are formally verified through interactive proof sessions. Finally, we complete the verification of the the theorem regarding Robertson-type uncertainty relation when we have no new subgoals.
Proof. We execute the above statement and obtain a response from Coq:
1 subgoals
______________________________________(1/1)
forall (n : nat) (v : mlengths n) (A B : HMat v) (psi : UnitVec),
sqrt (var psi A) * sqrt (var psi B) >=
1/2* cabs (innerProd psi (mvMult (mMinus (mMult A B) (mMult B A)) psi))
For the above subgoal (statement), a command called tactic is inputted and executed, then, new subgoal which is rewritten according to the tactic is obtained as a response from Coq. We prove the statement through interactive proof sessions until there no exist new subgoals (for complete Coq source code, see Appendix).
We input the following tactic and execute it:
intros.
where intros is a tactic which adds a condition described by universal quantifier to preconditions. Then, we get the following response from Coq:
1 subgoals
n : nat
v : nlengths n
A : HMat v
B : HMat v
psi : UnitVec C n
______________________________________(1/1)
sqrt (var psi A) * sqrt (var psi B) >=
1/2* cabs (innerProd psi (mvMult (mMinus (mMult A B) (mMult B A)) psi))
For readability, , , and are replaced with a, b, and c, respectively, by using a tactic set:
set ( a := sqrt (var psi A) ).
set ( b := sqrt (var psi B) ).
set ( c := (cabs (innerProd psi (mvMult (mMinus (mMult A B) (mMult B A)) psi)))).
Then, we get the following response from Coq:
1 subgoals
n: nat
v: mlengths n
A: HMat v
B: HMat v
psi: UnitVec C n
a:= sqrt (var psi A) : R
b:= sqrt (var psi B) : R
c:= cabs (innerProd psi (mvMult (mMinus (mMult A B) (mMult B A)) psi)):R
______________________________________(1/1)
a * b >= 1/2 * c
Hereafter, we show only subgoals which are responses from Coq. is observed from by using a tactic replace:
replace ( a * b >= 1 / 2 * c ) with ( (a * a) * (b * b) >= (1/4) * (c * c) ).
Then, we get the following response from Coq:
______________________________________(1/2)
a * a * (b * b) >= 1 / 4 * (c * c)
______________________________________(2/2)
(a * a * (b * b) >= 1 / 4 * (c * c)) = (a * b >= 1 / 2 * c)
For proving the inequality, we prove and from a
transitive relation. The transitive relation is added
to the preconditions by using a tactic assert:
assert ( a * a * (b * b) >=
(cabs ( innerProd psi (mvMult (mMult A B ) psi))) *
(cabs ( innerProd psi (mvMult (mMult A B ) psi))) /\
(cabs ( innerProd psi (mvMult (mMult A B ) psi))) *
(cabs ( innerProd psi (mvMult (mMult A B ) psi)))
>= (1 / 4) * (c * c) -> a * a * (b * b) >= 1 / 4 * (c * c)).
For proving the transitive relation, we use
lemma R_leq_eq2. The lemma is applied to the subgoal by using a tactic apply:
apply R_leq_eq2.
Then, we get the following response from Coq:
H : a * a * (b * b) >=
cabs (innerProd psi (mvMult (mMult A B) psi)) *
cabs (innerProd psi (mvMult (mMult A B) psi)) /\
cabs (innerProd psi (mvMult (mMult A B) psi)) *
cabs (innerProd psi (mvMult (mMult A B) psi)) >= 1/4 * (c*c)
-> a * a * (b * b) >= 1/4 * (c*c)
______________________________________(1/2)
a * a * (b * b) >= 1 / 4 * (c * c)
______________________________________(2/2)
(a * a * (b * b) >= 1 / 4 * (c * c)) = (a * b >= 1 / 2 * c)
Accordingly, the inequality which was performed with assert is added to the precondition as an assumption H. The assumption H is applied to the subgoal for proving:
apply H.
We input a tactic split to split into and
:
split.
For proving, RUR_Var_geq_InnerProd is applied to the subgoal:
apply RUR_Var_geq_InnerProd.
is replaced with d for readability:
set ( d := cabs ( innerProd psi (mvMult (mMult A B ) psi)) ).
We get the following response from Coq:
______________________________________(1/2)
d * d >= 1 / 4 * (c * c)
______________________________________(2/2)
(a * a * (b * b) >= 1 / 4 * (c * c)) = (a * b >= 1 / 2 * c)
and is replaced with and
, respectively:
replace ( d * d ) with ((((1/2) * (cabs ((innerProd psi (mvMult (mPlus
(mMult A B) (mMult B A) ) psi))))) * ((1/2) * (cabs ( (innerProd psi (mvMult
(mPlus (mMult A B) (mMult B A) ) psi)))))) + (( (1/2) * (cabs ( (innerProd psi (mvMult
(mMinus (mMult A B) (mMult B A)) psi))))) * ((1/2) * (cabs ( (innerProd psi (mvMult
(mMinus (mMult A B) (mMult B A)) psi))))))).
replace ((1/4) * (c * c)) with (((1/2) * (cabs ((innerProd psi
(mvMult (mMinus (mMult A B) (mMult B A)) psi))))) * ((1/2) *
(cabs ((innerProd psi (mvMult (mMinus (mMult A B) (mMult B A)) psi)))))).
For proving, we apply Square_
Plus_geq as follows:
apply Square_Plus_geq.
For proving and,
we apply RUR_eq_AB_0 and RUR_eq_AB_1 as follows:
apply RUR_eq_AB_0. apply RUR_eq_AB_1.
Then, we get the following response from Coq:
______________________________________(1/1)
(a * a * (b * b) >= 1 / 4 * (c * c)) = (a * b >= 1 / 2 * c)
For proving, we apply R_leq_eq
:
apply R_leq_eq.
Then, we get the following response from Coq:
No more subgoals.
All of the subgoals are proven. Input Qed and end the proof:
Qed.
The validity of Robertson-type uncertainty relation is verified formally.
4. Conclusion
In this work, we verified formally the validity of Robertson-type uncertainty relation by using the proof assistant Coq. We expect that the formalized theorem utilizes for facilitating the formal verification of the other theorems in quantum information theory. In future work, we will verify entropic uncertainty relation and the information disturbance theorem toward verifying unconditional security of quantum key distributions formally.
Acknowledgements
This work was partly supported by JSPS KAKENHI (24300030) Grant-in-Aid for Scientific Research (B), and MEXT-Supported Program for the Strategic Research Foundation at Private Universities (2014-2018, S1411030).
Appendix: Coq Source Code