Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Dear Cyril,

Thank you for your answer and the pointers to polyOver and mxOver.

It looks like mxOver uses the predicate approach to define matrices over 
the subring. In this respect, we could define the type of these matrices 
as a subtype of 'M[R]_(m,n). But this construction is quite different 
from the type 'M[R']_(m,n). How can I connect the two types?

Le 23/05/2018 à 13:00, Cyril a écrit :
> Whenever you want to show something that requires to work on 'M[R']
> because R' is a field, I guess that in the current state of the library,
> you must work on R'. But try to do so in a delimited way, and you may
> then use map_mx to explicitly coerce from R' to R.
So, as far as I understand, I need to have an explicit coercion from 
matrices over R' to matrices over R, say matR_of_matR'. However, I like 
to get rid of these coercions as much as possible. For instance, I'd 
like to rewrite expressions of the form
(matR_of_matR' A) + (matR_of_matR' B)
into matR_of_matR' (A + B). Same for matrix multiplications, opposite, 
constant matrices, etc. Is there any way to do it easily? It reminds me 
the kind of mechanisms introduced in generic_quotient (where the piE 
rewriting rule factors many expressions). Is it the "right way" to do it?

Best,
Xavier