2ControlVerification

This repository is a formal verification of the paper: Optimal Implementation of Quantum Gates with Two Controls.

All work is derivative of YT Jeong's original work. The fundamental linear algebra and quantum concepts are taken from QuantumLib.

Project Structure

The lemmas found in the main body of the paper (sections 3 through 7) can be found in Main.v.

The Appendix/ subdirectory contains proofs for the lemmas found in the appendix of the paper.

• Appendix 1: SquareMatrices
• Appendix 2: UnitaryMatrices
• Appendix 3: Swaps
• Appendix 4: Vectors
• Appendix 5: ControlledUnitaries
• Appendix 6: TensorProducts
• Appendix 7: OtherProperties

The Helpers/ subdirectory contains proofs for some helper lemmas used in proving parts of the appendix or main body of the paper:

• AlgebraHelpers - Helper lemmas having to do with real and complex numbers.
• UnitaryHelpers - Helper lemmas having to do with unitary matrices.
• EigenvalueHelpers - Helper lemmas having to do with eigenvalues, with hermitian and positive semi-definite matrices.
• ExplicitDecompositions - Helper lemmas for expanding fixed size calculations.
• GateHelpers - Helper lemmas for dealing with quantum gates.
• MatrixHelpers - Helper lemmas for matrix calculations.
• QubitHelpers - Helper lemmas for unit vectors.
• SwapHelpers - Helper lemmas for properties of swaps.
• PartialTraceDefinitions - Adding the functions for tracing out qubits, and properties of the function.
• TraceoutHelpers - Contains helper lemmas for tracing out qubits.
• DiagonalHelpers.v - Contains helpers lemmas that verify commutativity properties of diagonal matrices and diagonal properties control U and ccu U, where U is a diagonal matrix.
• WFHelpers.v - Contains the solve_WF_matrix automation tactic for solving well-formedness goals.
• Permutations.v - Helper lemmas for handling permutations, particularly useful in validating eigenvalue rearrangements and matrix decompositions.