The Coq mailing list

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

Dear Laurent, dear Coq Users,

with the proper setoid instances as suggested by Laurent (not sure why none 
is required for submod), one can define a ring structure and use it to solve 
the goal like this:

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.
  ring_simplify.
  ring.
Qed.

But I think ring and ring_simplify have bugs. Applying ring_simplifiy on the 
converted goal results in:

eqmod 3 (addmod 3 0 x) (mulmod 3 1 x)

I think ring_simplifiy should be able to handle 0+x and 1*x. Also ring can 
solve the goal after ring_simplifiy, but not immediately, which I think is 
also a bug. I will write a bug report.

But basically this technique seems to work. Please find the complete example 
below.

Best regards,

Michael



Require Import ZArith Psatz.
Require Import Ring.

Open Scope Z_scope.

(* Define modulo arithmetic operators *)

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).

(* Conversion from usual Z operators to modulo operators *)

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.

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.

(* Show that the modulo arithmetic opertors form a ring *)

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.

(* Since the ring equality is a non standard equality, we need to show that 
the operators are compatible with eqmod and that eqmod id an Equality *)

Require Export Coq.Setoids.Setoid.
Require Export Coq.Classes.Morphisms.

Instance eqmod_proper (m : Z) : Equivalence (eqmod m).
Proof.
  apply Build_Equivalence.
  - unfold Reflexive. intros x. autorewrite with HdbModR. reflexivity. 
  - unfold Symmetric. intros x y H. autorewrite with HdbModR in *. symmetry. 
assumption.
  - unfold Transitive. intros x y z H1 H2. autorewrite with HdbModR in *. 
rewrite H1. assumption.
Qed.

Instance addmod_proper (m : Z) : Proper (eqmod m ==> eqmod m ==> eqmod m) 
(addmod m).
Proof.
  unfold Proper; unfold respectful.
  intros x1 y1 H1 x2 y2 H2; autorewrite with HdbModR in *.
  rewrite (Zplus_mod x1 x2); rewrite (Zplus_mod y1 y2). 
  rewrite H1; rewrite H2; reflexivity.
Qed.

Instance mulmod_proper (m : Z) : Proper (eqmod m ==> eqmod m ==> eqmod m) 
(mulmod m).
Proof.
  unfold Proper; unfold respectful.
  intros x1 y1 H1 x2 y2 H2; autorewrite with HdbModR in *.
  rewrite (Zmult_mod x1 x2). rewrite (Zmult_mod y1 y2). 
  rewrite H1; rewrite H2; reflexivity.
Qed.

Instance negmod_proper (m : Z) : Proper (eqmod m ==> eqmod m) (negmod m).
Proof.
  unfold Proper; unfold respectful.
  intros x1 y1 H1; autorewrite with HdbModR in *.
  rewrite <- (Z.sub_0_l x1).
  rewrite <- (Z.sub_0_l y1).
  rewrite Zminus_mod. rewrite H1. rewrite <- Zminus_mod. reflexivity.
Qed.

(* Some extra rewriting lemmas needed to get more Z arithemtic trms to modulo 
operator terms *)

Lemma idmod : forall (m a : Z), a mod m = addmod m 0 a.
Proof. 
  intros; unfold addmod. reflexivity.
Qed.

(* Alternatively to idmod, have individual reduction lemmas
Lemma addmod_red_l : forall (m a b : Z), addmod m (a mod m) b = addmod m a b. 
Proof.
  intros; unfold addmod; apply Zplus_mod_idemp_l.
Qed.

Lemma addmod_red_r : forall (m a b : Z), addmod m a (b mod m) = addmod m a b. 
Proof.
  intros; unfold addmod; apply Zplus_mod_idemp_r.
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.

Lemma mulmod_red_l : forall (m a b : Z), mulmod m (a mod m) b = mulmod m a b. 
Proof.
  intros; unfold mulmod; apply Zmult_mod_idemp_l.
Qed.

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

(* We would need 16 lemmas (add/sub/mul/neg on both sides) of this type: *)
Lemma addsubmod_eq_eq : forall (m a b c d: Z), (addmod m a b = submod m c d) 
= eqmod m (addmod m a b) (submod m c d).
Proof. 
  intros; autorewrite with HdbModR. repeat rewrite Zmod_mod. reflexivity.
Qed.

Hint Rewrite addsubmod_eq_eq : HdbMod.
Hint Rewrite eqmod_eq  : HdbMod.
Hint Rewrite idmod     : HdbMod.
Hint Rewrite negmod_eq : HdbMod.
Hint Rewrite mulmod_eq : HdbMod.
Hint Rewrite addmod_eq : HdbMod.
Hint Rewrite submod_eq : HdbMod.

(* Define the ring for m=3 *)

Definition ModRing3 := ModRing 3.
Add Ring ModRing3 : ModRing3.

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.
  ring_simplify.
  ring.
Qed.
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