coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- Re: [Coq-Club] how to proof in Z modulo?, (continued)
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Clément Pit--Claudel, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Gaetan Gilbert, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Clément Pit--Claudel, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
Archive powered by MHonArc 2.6.18.