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 11:43:35 +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 mga03.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



Archive powered by MHonArc 2.6.18.

Top of Page