The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

another approach is to show that these modulo operations form a ring and use 
a rewrite database to transform normal mod expressions into expression using 
modulo arithmetic operators.  As an exercise I proved, together with an 
intern student working on similar topics, the ring theory, but then when I 
want to add the ring, Coq complains I guess about the non-standard equality " 
Error: cannot find setoid relation". Can someone explain what exactly I need 
in addition to add this as ring?

The rewrite databases given below can be used to convert expressions 
automatically in both directions:

Lemma Test : forall x : Z,
  (x mod 3)%Z = (((x mod 3 - (- x) mod 3) mod 3 - ((- x) mod 3 - x mod 3) mod 
3) mod 3)%Z.
Proof.
  intros x.
  autorewrite with HdbMod.

results in 

eqmod 3 x (submod 3 x (negmod 3 x) - submod 3 (negmod 3 x) x)

which should be solvable by ring. Also

    autorewrite with HdbModR.

converts this back into

x mod 3 = ((x - - x mod 3) mod 3 - (- x mod 3 - x) mod 3) mod 3


Here is the ring proof:

Require Import ZArith Psatz.
Require Import Ring.

Open Scope Z_scope.

Definition addmod (m a b : Z) := (a+b) mod m.
Definition submod (m a b : Z) := (a-b) mod m.
Definition mulmod (m a b : Z) := (a*b) mod m.
Definition negmod (m a : Z) := (-a) mod m.
Definition eqmod (m a b : Z) := (a mod m) = (b mod m).

Lemma addmod_eq : forall (m a b : Z), (a+b) mod m = addmod m a b. 
Proof.
  intros; unfold addmod; reflexivity.
Qed.

Lemma submod_eq : forall (m a b : Z), (a-b) mod m = submod m a b. 
Proof.
  intros; unfold submod; reflexivity.
Qed.

Lemma mulmod_eq : forall (m a b : Z), (a*b) mod m = mulmod m a b. 
Proof.
  intros; unfold mulmod; reflexivity.
Qed.

Lemma negmod_eq : forall (m a: Z), (-a) mod m = negmod m a. 
Proof.
  intros; unfold negmod; reflexivity.
Qed.

Lemma eqmod_eq : forall (m a b: Z), (a mod m = b mod m) = eqmod m a b. 
Proof.
  intros; unfold eqmod; reflexivity.
Qed.

Lemma submod_red_l : forall (m a b : Z), submod m (a mod m) b = submod m a b. 
Proof.
  intros. unfold submod. apply Zminus_mod_idemp_l.
Qed.

Lemma submod_red_r : forall (m a b : Z), submod m a (b mod m) = submod m a b. 
Proof.
  intros. unfold submod. apply Zminus_mod_idemp_r.
Qed.

Hint Rewrite addmod_eq : HdbMod.
Hint Rewrite submod_eq : HdbMod.
Hint Rewrite mulmod_eq : HdbMod.
Hint Rewrite negmod_eq : HdbMod.
Hint Rewrite eqmod_eq : HdbMod.
Hint Rewrite submod_red_l : HdbMod.
Hint Rewrite submod_red_r : HdbMod.

Hint Rewrite <- addmod_eq : HdbModR.
Hint Rewrite <- submod_eq : HdbModR.
Hint Rewrite <- mulmod_eq : HdbModR.
Hint Rewrite <- negmod_eq : HdbModR.
Hint Rewrite <- eqmod_eq : HdbModR.

Lemma ModRing : forall (m : Z), ring_theory 0%Z 1%Z (addmod m) (mulmod m) 
(submod m) (negmod m) (eqmod m).
Proof.
  intros m.
  apply mk_rt.
  - intros x. autorewrite with HdbModR. simpl. apply Zmod_mod.
  - intros x y. autorewrite with HdbModR. rewrite Z.add_comm. reflexivity.
  - intros x y z. autorewrite with HdbModR. rewrite Zplus_mod_idemp_l. 
rewrite Zplus_mod_idemp_r. rewrite <- Z.add_assoc. reflexivity.
  - intros x. autorewrite with HdbModR. rewrite Z.mul_1_l. apply Zmod_mod.
  - intros x y. autorewrite with HdbModR. rewrite Z.mul_comm. reflexivity.
  - intros x y z. autorewrite with HdbModR. rewrite Zmult_mod_idemp_l. 
rewrite Zmult_mod_idemp_r. rewrite <- Z.mul_assoc. reflexivity.
  - intros x y z. autorewrite with HdbModR. rewrite Zmult_mod_idemp_l. 
rewrite <- Zplus_mod. rewrite Z.mul_add_distr_r. reflexivity.
  - intros x y. autorewrite with HdbModR. rewrite Zplus_mod_idemp_r. rewrite 
Z.add_opp_r. reflexivity.
  - intros x. autorewrite with HdbModR. rewrite Zplus_mod_idemp_r. rewrite 
Z.add_opp_diag_r. apply Zmod_mod.
Qed.

Definition ModRing3 := ModRing 3.

Add Ring ModRing3 : ModRing3.

This results in " Error: cannot find setoid relation"



Best regards,

Valentin  & 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