The Coq mailing list

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

OK I did my experiment wrong. If you do the following it works, but if
you replace the various T' by T it doesn't work, see comments.

(the original experiment I did had the [Add Ring rm2] after t1 so
didn't detect failure properly)

#+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'). (* if returning T the call in t2 fails *)

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

Definition rm2 : @semi_ring_theory T' z2 o2 a2 m2 eq. (* explicit T' can 
be left implicit if z2 : T'. otherwise the call in t1 fails. *)
Admitted.

Add Ring rm1 : rm1.
Add Ring rm2 : rm2.

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

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

This is with a minimum of T' to get it to work so that we can see
where they're necessary, in practice you would want [z2 : T'] (or get
failures whenever it is on the left hand side of an equation) and
[a2 : T' -> T' -> T'] (for consistency).

So it looks like the type a ring is registered as is the implicit
argument to the semi_ring_theory (the type of the zero if left
implicit), and when it looks at a type [h e1 e2] (where h may itself
be an application) it gets the type T of e1 and if that's a known ring
checks if h is the registered identity.

Gaëtan Gilbert

On 17/07/2017 18:39, Soegtrop, Michael wrote:
> Dear Gaetan,
>
> > > If this doesn't match your expectation, I can prepare a sample.
> > Please do.
> attached please find a Z modulo ring example which shows two unexpected 
> behaviors of the ring tactic:
>
> 1.) it looks like the ring operators applied to literal coefficients need to 
> compute with simpl, which is a serious restriction since simpl does not 
> behave in a very consistent way. It is not sufficient that operators applied 
> on literal coefficients compute with cbv.
>
> 2.) addition of ring structures for the same type hides previously defined 
> ring structures, even if all relations are different.
>
> Best regards,
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928