Skip to content

inQWIRE/QuantumLib

Folders and files

NameName
Last commit message
Last commit date

Latest commit

5e0e4da · Jan 18, 2025
Jan 29, 2024
Jan 25, 2024
Jan 18, 2025
Jul 31, 2022
Jan 25, 2024
Jan 18, 2025
Jan 18, 2025
Jan 20, 2023
May 27, 2024
Jan 18, 2025
Jul 26, 2022
Jan 25, 2024
Jan 25, 2024
Jan 18, 2025
Jun 7, 2022
Jun 22, 2022
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 25, 2024
Jan 18, 2025
Jan 22, 2022
Jan 18, 2025
Apr 17, 2024
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Jan 18, 2025
Mar 9, 2024
Jan 18, 2025
May 17, 2022
Jan 18, 2025
Jan 6, 2022
Jan 18, 2025

Repository files navigation

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.

About

Coq library for reasoning about quantum programs

Resources

License

Citation

Stars

Watchers

Forks

Packages

No packages published

Languages