Stream: math-comp users

Topic: Type matching between Reals and GRing.Zmodule

view this post on Zulip Emily Z. (Mar 29 2024 at 16:14):


I am trying to use addmx from mathcomp.algebra.matrix, but ran into the following type mismatch on the arguments I am inputting into the function:


Here, R is just the reals from Coq.Reals because I would like to work with matrices on real numbers. I am wondering if there is some way to specify that the reals are indeed an abelian group, or if there is another more compatible library for reals that I should try instead. I am newer to math-comp and would really appreciate any help or feedback.

view this post on Zulip Pierre Roux (Mar 29 2024 at 16:43):

You probably need the Rstruct.v file from mathcomp-analysis that provides mathcomp algebraic structures to the reals R from the stdlib.

view this post on Zulip Pierre Roux (Mar 29 2024 at 16:44):

But if you don't use anything specific to the reals from the stdlib, it could just be as good to use the reals provided by mathcomp analysis itself.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2024 at 13:37):

Indeed, as Pierre explained, the type for addmx is:

addmx : forall [V : nmodType] [m n : nat], 'M[V]_(m, n) -> 'M[V]_(m, n) -> 'M[V]_(m, n)

thus, you need to have in scope the instance so Coq knows that R is a nmodType.

(Note a bug in printing addmx type in Coq 8.19)

Last updated: Jul 25 2024 at 16:02 UTC