The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Dear Michael,

"Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 writes:

> I wanted to use the ring tactic in proofs of pretty much what you
> describe (various variants of standard library CycliyType), so to use
> it in this way I would have to define an intermediate type just for
> the proofs, which is not so convenient.
>
> So I either have to redefine the ring tactic from time to time or
> extend it to take an options ring structure name.

Of course making the tactic more flexible would be great.

Note that a more cumbersome solution if you really want to use the same
type is to scope the ring declaration inside a module. Example:

#+BEGIN_SRC coq
From Coq Require Import Reals.

Variables (T : Type).
Variables (z1 o1 z2 o2 : T).
Variables (a1 m1 a2 m2 : T -> T -> T).

Definition rm1 : semi_ring_theory z1 o1 a1 m1 eq.
Admitted.

Definition rm2 : semi_ring_theory z2 o2 a2 m2 eq.
Admitted.

Module M1.

Add Ring rm1 : rm1.

Lemma t1 : a1 z1 o1 = o1.
Proof. ring. Qed.

End M1.

Module M2.

Add Ring rm2 : rm2.

Lemma t2 : a2 z2 o2 = o2.
Proof. ring. Qed.

End M2.
#+END_SRC

But note that you will have to alias the lemmas declared inside the
modules as opening them should (*) bring the ring declaration back.

Best,
E.

(*) Actually it may be more complicated than that.