Ssreflect Users Discussion List

[Bas Spitters <>]

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