The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Dear Michael,

"Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 writes:

> I sometimes want to have two ring structures defined for one type
> using different operators. An example is the usual ring for Z and a
> modulo ring for Z. The ring tactic seems to select the ring structure
> to use based on the type of coefficients and variables, not on the
> operators used in the term. Also the ring tactic does not allow to
> specify a ring explicitly. So I wonder how I can use several ring
> structure for the same type in one proof.

One solution for this particular case is indeed to use two different
types, as done in mathcomp. `int` is the usual Z and `'Z_p` is the type
of integers modulo `p`.

Without knowing more details, I would indeed attack the problem in
general by providing two datatypes and a coercion from one to the other;
however this may prove quite cumbersome in some scenarios.

Best,
E.