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
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?
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: Jan 28 2023 at 07:30 UTC