$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam install coq-mathcomp-real-closed coq-mathcomp-algebra-tactics
$ eval opam env
$ make
We have checked the compilation with the following versions of OPAM packages: coq 8.19.0 coq-core 8.19.0 coq-elpi 2.0.2 coq-hierarchy-builder 1.7.0 coq-mathcomp-algebra 2.2.0 coq-mathcomp-algebra-tactics 1.2.3 coq-mathcomp-bigenough 1.0.1 coq-mathcomp-field 2.2.0 coq-mathcomp-fingroup 2.2.0 coq-mathcomp-real-closed 2.0.0 coq-mathcomp-solvable 2.2.0 coq-mathcomp-ssreflect 2.2.0 coq-mathcomp-zify 1.5.0+2.0+8.16 coq-stdlib 8.19.0
- mathcomp_extra.v: additions to mathcomp library
- lens.v: definition of lens, extract, merge, and lemmas
- dpower.v: definition of dpower, morphisms, focus, and lemmas
- unitary.v: definition of unitaryts and unitary_endo
- endo_monoid.v: non-commutative and commutative morphism composition monoids for use with big operators
- density.v: definition of the density matrix interpretation
- kqm.v: some experiments with caps and cups
- qexamples_common.v: definition of basic gates
- qexamples_shor.v: proof of Shor's 9-qubit code
- qexamples_ghz.v: proof of Greenberger-Horne-Zeilinger preparation
- qexamples_rev_circuit.v: proof of the reverse circuit (using swap gates)
- qexamples_qutrit.v: examples with qutrit gates, including CNOT and SWAP