The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

You can also  use a type alias.

#+BEGIN_SRC coq
From Coq Require Import Reals.

Variables (T : Type).
Variables (z1 o1 : T).
Variables (a1 m1 : T -> T -> T).

Definition T' := T.
Variables (z2 o2 : T).
Variables (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 T').
Admitted.

Add Ring rm1 : rm1.

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

Add Ring rm2 : rm2.

Lemma t2 : a2 z2 o2 = o2 :> T'.
Proof. ring. Qed.
#+END_SRC

This works because ring uses the relation to figure out which
structure should be used.

If you declare the operations foo2 in T' you won't need the explicit
T' annotations in the rm2 definition and in t2's type.

Gaëtan Gilbert

On 17/07/2017 12:50, Emilio Jesús Gallego Arias wrote:
> 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.