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: Apr 18 2024 at 12:01 UTC