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

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...

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

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.

(In other words, that would solve the `phi S0`

case, but not the `phi (Sadd x y)`

case.)

@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: Jun 23 2024 at 01:02 UTC