The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

The problem is that the ring tactic treats "2" as just an arbitrary 
constant. There are two ways around it:

* Define "2" in an alternative way:

    Notation "2" := (1 + 1)%C : C_scope.

* Use the "constant" modifier of the "Add Ring" command, see

    https://coq.inria.fr/doc/Reference-Manual027.html#hevea_command357

On 03/27/2015 02:14 PM, Matej Kosik wrote:
> Hello,
>
> I have recently (again) stumbled upon the "Add Ring ..." command and decided 
> to make some experiments with it
> (mainly to see if I can define a custom ring from scratch and make sure that 
> the ring tactic works for the custom ring as successfully as in the other 
> usual cases).
>
> I have picked to define Gaussian integers.
> (the attached file contains the complete experiment)
>
> I had a partial success.
> Some of the goals can be solved automatically:
>
>         Goal forall x y, ((x+y)*(x+y)*(x-x) = 0)%C.
>         Proof.
>                 intros.
>                 ring.
>         Qed.
>
> However, there are cases when ring tactic fails, e.g.:
>
>         Goal forall x y, ((x+y)*(x+y) = x*x + 2*x*y + y*y)%C.
>         Proof.
>           intros.
>           ring.
>
> There I get
>
>         Error: Tactic failure: not a valid ring equation.
>
> On the other hand, the same goal on the Z-ring is handled by ring-tactic just 
> fine:
>
>         Goal forall x y, ((x+y)*(x+y) = x*x + 2*x*y + y*y)%Z.
>         Proof.
>           intros.
>           ring.
>         Qed.
>
> I would like to ask two (related) questions:
>
>    How come that "((x+y)*(x+y) = x*x + 2*x*y + y*y)%C" is not a valid ring 
> equation?
>
>    What exactly is meant by "ring equation"?
>
> Thank you very much for any help or hints.