## Stream: Coq users

### Topic: Ring tactic using morphisms

#### Rasmus Holdsbjerg-Larsen (Jun 22 2021 at 09:03):

I am having some trouble understanding the intended functionality of the "morphism" keyword of adding rings.

Suppose I have two rings, R and S:

``````R : Set
R0 : R
R1 : R
Radd : R -> R -> R
Rmul : R -> R -> R
Rsub : R -> R -> R
Ropp : R -> R
R_ring : ring_theory R0 R1 Radd Rmul Rsub Ropp (@eq R)
``````

And similarly for S:

``````S : Set
S0 : S
...
S_eqb : S -> S -> bool
``````

Where S_eqb is a proof that equality in S is decidable.
I have also ring morphism

``````phi : S -> R
phi_morph : ring_morphism R0 R1 Radd Rmul Rsub Ropp (@eq R) S1 S0 Sadd Smul Ssub Sopp S_eqb phi
``````

Now, I would like to use the ring tactic to solve goals involving this morphism, so I add the ring using the morphism keyword:

``````Add Ring Rring : R_ring (morphism phi_morph)
``````

Hoping that the ring tactic will be able to prove my goal, but it fails, even on simple goals like

``````phi S0 = R0
``````

and

``````phi (Sadd x y)= Radd (phi x) (phi y)
``````

So my question is; what am I missing? Or is this not the intended use of ring morphisms?
@Assia Mahboubi

#### Cyril Cohen (Jun 22 2021 at 09:11):

Hi @Rasmus Holdsbjerg-Larsen
According to the doc the ring morphism is dedicated to the ring of coefficients -> the ring that you add, not from an arbitrary ring to another...

#### Cyril Cohen (Jun 22 2021 at 09:12):

I know some efforts are deployed to cover your usecase though, but in the specific context of the mathcomp library, CC @Kazuhiko Sakaguchi

#### Guillaume Melquiond (Jun 22 2021 at 09:13):

If you know that your morphism is only applied to constants (that is, no universally quantified variables of `S`), then you can use the `constants` parameter to force them to be recognized.

#### Guillaume Melquiond (Jun 22 2021 at 09:14):

(In other words, that would solve the `phi S0` case, but not the `phi (Sadd x y)` case.)

#### Bas Spitters (Jun 22 2021 at 11:47):

@Cyril Cohen Thanks! In the use case we are discussing with Rasmus, the ring S is indeed computational (in fact it could be Fp), so we are in the case of a customized ring, in the terminology of the refman.
I believe our use case is similar to the one described there: "one can consider the real numbers. The set of coefficients could be the rational numbers, upon which the ring operations can be implemented." In fact, it is a bit better, as the other ring is also computational (it could be a field extension of Fp).
Is the example of the use of the ring tactic with ring morphisms for real numbers elaborated somewhere?

Last updated: Oct 03 2023 at 21:01 UTC