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: Laurent Thery <Laurent.Thery AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] how to proof in Z modulo?
  • Date: Tue, 9 Aug 2016 13:22:53 +0200



On 08/09/2016 11:23 AM, Soegtrop, Michael wrote:
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.

It works but your ring somewhat misses the fact that 3 mod 3 = 0 but
applying it twice makes the trick

Lemma Test1 : 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.
apply sym_equal.
rewrite <- (Zmod_mod).
autorewrite with HdbMod.
ring_simplify.
ring.
Qed.




Archive powered by MHonArc 2.6.18.

Top of Page