The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hi Abhishek,

You may define your own ring with "Add Ring".
see https://coq.inria.fr/refman/addendum/ring.html#adding-a-ring-structure

=> For example, if you start with the "default" Z-ring

Require Import ZArith.
Open Scope Z_scope.

=> you can prove this.

Goal forall a b c:Z,
    (a + b) * (a + b)  =
     a ^ 2 + b * b + 2 * a * b.
intros; ring.
Qed.


=> Then, adding my own ring as below, the same goal fails (because, I 
have not indicated how to deal with "constants" and "powers" in the ring 
definition).

Module MyWeakRing.

  Add Ring MyZr : Zth (decidable Zeq_bool_eq).

End MyWeakRing.

Import MyWeakRing.


=> But, this variant below succeeds.

Goal forall a b c:Z,
    (a + b) * (a + b)  =
    a * a + b * b + a * b + a * b.
intros; ring.
Qed.

=> Hence, ring seems to use the last "added" Ring in the environment.

Maybe, a (not very elegant) solution to your question is to put each 
ring definition in a separate module, as I have done above. Then, you 
may play with "Import" to have the good ring in the environment.

For example, "Import ZArith." restores the default Ring for Z. And the 
"ring" tactic is able to prove the first goal again...


Regards,

Sylvain.


Le 25/06/2022 à 00:32, Abhishek Anand a écrit :
> Often, the same type satisfies multiple ring structures. I dont see any 
> way to tell the ring and ring_simplify tactics which ring to use. Is 
> there a way?
>
> For example, one can define another ring structure on Z where equality 
> is a \equiv b := a mod = b mod d, and all operations are the same as the 
> Z ones (they are proper w.r.t. the equivalence).
> But how will I tell the ring_simplify tactic to use this ring instead of 
> the standard one on Z?
> --
> Abhishek Anand