Skip to content

Latest commit

 

History

History
58 lines (41 loc) · 3.09 KB

README.md

File metadata and controls

58 lines (41 loc) · 3.09 KB
Raw

QuantumLib

CI coqdoc

QuantumLib is a Coq library for reasoning about quantum programs. It was co-developed with (and is used in) several other projects in inQWIRE including QWIRE, SQIR, and VyZX.

Compilation

QuantumLib is currently compatible with Coq 8.16 -- 8.19.

This project requires opam & dune to be installed.

Install dune using opam install dune

To compile run make all.

Stable versions of QuantumLib may be installed using opam install coq-quantumlib

Using With Other Projects

Official Release

To install the official release of QuantumLib, run the following.

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-quantumlib

Dev

To install the development version of QuantumLib, run opam pin coq-quantumlib https://github.com/inQWIRE/QuantumLib.git. This should allow you to import QuantumLib files into other Coq files. To pull subsequent updates, run opam install coq-quantumlib. When importing/exporting specific files, refer to QuantumLib files as QuantumLib.FILENAME.

Directory Contents

Auto-generated documentation is available at https://inqwire.github.io/QuantumLib/toc.html.

  • Complex.v - Definition of Complex numbers, extending Coquelicot's.
  • Ctopology.v - A topology of open/closed sets is defined for the complex numbers, with lemmas about compactness.
  • DiscreteProb.v - Theory of discrete probability distributions and utility to describe running a quantum program ("apply_u") and sampling from the output distribution.
  • Eigenvectors.v - A continuation of VecSet.v, this file contains more linear algebra that is sort of specific to quantum.
  • FTA.v - This file is mostly just a messy proof of the fundamental theorem of algebra.
  • Matrix.v - Definition of matrices of complex numbers, associated lemmas and automation.
  • Measurement.v - Useful predicates for describing the result of measurement.
  • Pad.v - Definition of "pad" function to extend a matrix to a larger space.
  • Permutations.v - Facts about permutation matrices.
  • Polar.v - Defining polar complex numbers and showing that they are isomorphic to rectangular complex numbers.
  • Polynomial.v - Definition of polynomials and corresponding lemmas.
  • Prelim.v - Basic utility definitions and proofs.
  • Proportional.v - Definition of equality up to a global phase.
  • Quantum.v - Definitions of and proofs about common matrices used in quantum computing.
  • RealAux.v - Supplement to Coq's axiomatized Reals.
  • VecSet.v - More advanced linear algebra definitions such as linear independence, invertability, etc. and corresponding lemmas.
  • VectorStates.v - Abstractions for reasoning about quantum states as vectors.