Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] how to proof in Z modulo?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] how to proof in Z modulo?


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] how to proof in Z modulo?
  • Date: Tue, 9 Aug 2016 09:23:09 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga09.intel.com
  • Ironport-phdr: 9a23:5/QzXxAyYfy1JSvSUP5+UyQJP3N1i/DPJgcQr6AfoPdwSP79osbcNUDSrc9gkEXOFd2CrakV06yH6eu5AyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+KyZXtnLnos7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0roGxsvKdr/MlZFK7+Yq4QTLpCDT1gPXp/rJngsgCGRg+S7FMdVH8Xm1xGGV6Wwgv9W8K7iSz3ufZn3zHedej3RrA9VDDop/NuSRTogSoDcSU+/W7LkMtopKNdvB+l4Rd4xtiHM8muKPNic/aFLpshTm1bU5MJWg==

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



Archive powered by MHonArc 2.6.18.

Top of Page