Ssreflect Users Discussion List

[Robert Rand <>]

Hi all, 

I'm trying to use the Mathematical Components library to give semantics to the QWIRE quantum programming language (https://github.com/jpaykin/QWIRE). Part of this involves defining the core matrix operations for quantum computing, including the Kronecker product and conjugate (or Hermitian) transpose, along with a basic set of unitary matrices. 

There's some discussion of the Kronecker product at https://sympa.inria.fr/sympa/arc/ssreflect/2015-09/msg00005.html; I don't know if there's any definition of conjugate transpose for matrices containing closedFieldTypes. (I've been able to define conj_trmx for 'M[algC] - unfortunately, closedFieldType doesn't seem to have an associate conjugate operation?) We would then need some algebraic identities involving conjugate transpose and Kronecker products, plus the basic quantum matrices.

Just so I'm not reinventing the wheel: Has anyone done any of this in ssreflect? (We've done much of this using basic Coq and Coquelicot's complex numbers, but it's not suited to the kinds of verification we want.) If we develop the mathematics for quantum computing, would it be possible to include it in future versions of Mathematical Components (along with the existing mxutil library)?

Thanks,

Robert