The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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.
Require Import ZArith Ring Setoid.
Open Scope Z_scope.

Record C : Set := complex {real : Z; imaginary : Z}.

Notation "0" := (complex 0 0) : C_scope.
Notation "1" := (complex 1 0) : C_scope.

Delimit Scope C_scope with C.

Definition C_sym (c : C) : C :=
  complex (- (real c)) (- (imaginary c)).
Notation "- x" := (C_sym x) : C_scope.

Definition C_plus (c1 c2 : C) : C :=
  match c1, c2 with
  | {| real := real1; imaginary := imaginary1 |},
    {| real := real2; imaginary := imaginary2 |}
    => complex (real1 + real2) (imaginary1 + imaginary2)
  end.
Infix "+" := C_plus : C_scope.

Definition C_minus (c1 c2 : C) : C :=
  match c1, c2 with
  | {| real := real1; imaginary := imaginary1 |},
    {| real := real2; imaginary := imaginary2 |}
    => complex (real1 - real2) (imaginary1 - imaginary2)
  end.
Infix "-" := C_minus : C_scope.

Definition C_mult (c1 c2 : C) : C :=
  match c1, c2 with
  | {| real := real1; imaginary := imaginary1 |},
    {| real := real2; imaginary := imaginary2 |}
    => complex (real1 * real2 - imaginary1 * imaginary2)
               (imaginary1 * real2 + real1 * imaginary2)
  end.
Infix "*" := C_mult : C_scope.

Open Scope C_scope.

Theorem add_0_l : forall x, 0 + x = x.
Proof.
  intros [re im].
  simpl.
  split; ring.
Qed.

Theorem add_comm : forall x y, x + y = y + x.
Proof.
  intros [re1 im1] [re2 im2].
  simpl.
  pattern (re1 + re2)%Z.
  rewrite Z.add_comm.
  pattern (im1 + im2)%Z.
  rewrite Z.add_comm.
  reflexivity.
Qed.

Theorem add_assoc : forall x y z, x + (y + z) = (x + y) + z.
Proof.
  intros [re1 im1] [re2 im2] [re3 im3].
  simpl.
  pattern (re1 + (re2 + re3))%Z.
  rewrite Z.add_assoc.
  pattern (im1 + (im2 + im3))%Z.
  rewrite Z.add_assoc.
  reflexivity.
Qed.

Theorem mul_1_l : forall x, 1 * x = x.
Proof.
  intros [re im].
  unfold C_mult.
  f_equal; ring.
Qed.

Theorem mul_comm : forall x y, x * y = y * x.
Proof.
  intros [re1 im1] [re2 im2].
  simpl.
  f_equal; ring.
Qed.

Theorem mul_assoc : forall x y z, x * (y * z) = (x * y) * z.
Proof.
  intros [re1 im1] [re2 im2] [re3 im3].
  simpl.
  f_equal; ring.
Qed.

Theorem distr_l : forall x y z, (x + y) * z = (x * z) + (y * z).
Proof.
  intros [re1 im1] [re2 im2] [re3 im3].
  simpl.
  f_equal; ring.
Qed.

Theorem sub_def : forall x y, x - y = x + -y.
Proof.
  intros [re1 im1] [re2 im2].
  simpl.
  f_equal; ring.
Qed.

Theorem opp_def : forall x, x + (- x) = 0.
Proof.  
  intros [re im].
  simpl.
  f_equal; ring.
Qed.

Definition rt := mk_rt 0 1 C_plus C_mult C_minus C_sym (@eq C)
                       add_0_l add_comm add_assoc mul_1_l mul_comm mul_assoc 
distr_l sub_def opp_def.
                       
Check rt.

Add Ring Complex_Z_Ring : rt.

Goal complex 0 0 = complex 0 0.
Proof.
  ring.
Qed.

Notation "2" := (complex 2 0) : C_scope.

Goal forall x y : C, ((x+y)*(x+y)*(x-x) = 0)%C.
Proof.
  intros.
  ring.
Qed.

Goal forall x y, ((x+y)*(x+y) = x*x + 2*x*y + y*y)%Z.
Proof.
  intros.
  ring.
Qed.

Print Unnamed_thm1.

Print Rings.

Goal forall x y, ((x+y)*(x+y) = x*x + 2*x*y + y*y)%C.
Proof.
  intros.
  ring.     (* Error: Tactic failure: not a valid ring equation. *)
Qed.