Ssreflect Users Discussion List

[Robert Rand <>]

Hi Bas,

This is definitely one of the things I'm hoping to do, depending on whether CoqEAL is up to the task. (Apparently there were some issues with using CoqEAL to multiply matrices of algC?)

On Tue, Sep 12, 2017 at 4:29 AM, Bas Spitters <> wrote:

Hi Cyril, Robert,

With better integration of ssr in Coq. Can we now hope to run quantum
algorithms based on CoqEAL technology?
https://github.com/CoqEAL/CoqEAL

Best,

Bas

On Tue, Sep 12, 2017 at 8:22 AM, Cyril <> wrote:
> Hi,
>
> On 12/09/2017 00:32, Robert Rand wrote:
>>
>> 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.
>
>
> There is an upcomming generalization of numClosedFieldTypes (available only
> in the development version until now, but soon to be released) that contains
> conjugation.
> I used it in a development to prove the spectral theorem for normal
> operators:
> https://github.com/CohenCyril/spectral/blob/master/theories/spectral.v
>
> Best,
> --
> Cyril