Ssreflect Users Discussion List

[Robert Rand <>]

Hi Emilio,

I think your postscript is misunderstanding something. I'm not looking to instantiate matrices as a field (which they aren't), I'm looking to define the conjugate transpose on `'M[C]`s where C is a numClosedFieldType. It sounds from  Cyril as though this is possible in the development version of MathComp. 

As for the rest, I completely agree.

On Wed, Sep 13, 2017 at 11:03 AM, Emilio Jesús Gallego Arias <> wrote:

Hi,

Cyril <> writes:

> There is an upcomming generalization of numClosedFieldTypes (available
> only in the development version until now, but soon to be released)
> that contains conjugation.

Maybe I see Robert's question more as in

"would it make sense to add `conj_mx` and friend to math-comp, and if
 so, how to proceed?"

Indeed, I can count now 4 separate definitions of matrix conjugate /
unitary matrices, etc... all of the out of math-comp, so that looks bad
in terms of code/theory reuse.

Also, there are many other important blocks [such as the one
implementing the ssralg instances for Coq's R] of which several versions
are randomly floating around. I think this is pretty bad too.

I dunno how to proceed, but certainly math-comp seems to have become
quite static, with people preferring to carry around many extra files
instead of integrating them in the library.

Maybe this is what the maintainers want, maybe not, but even if the
effort to maintain code quality is understandable, I think the downside
today is pretty significant.

Maybe there should be another repository for all such "common",
non-mature theories? Something such as math-comp-extra or
math-comp-staging?

Best,
E.

p.s: Robert, unfortunately, I think you cannot instantiate the
numClosedFieldType machinery with the matrix transpose unless you have a
pretty specific matrix structure.

In particular, your matrices would need to form a field for a start, and
have a norm compatible with the current theories.

You can however made your development agnostic to the concrete
"complex-like" type, which is desirable I think.