coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strange behaviour of ring_simplify.

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Strange behaviour of ring_simplify.
Date: Fri, 17 Nov 2017 15:56:22 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
Ironport-phdr: 9a23:P8+CYxIZT52NCW/7cNmcpTZWNBhigK39O0sv0rFitYgXIvjxwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uHQZHQy6Pg5oLMz0HJTThoK5zar6r5bUekBDgCe3SbJ0NhS/6wvL4Jo4m4xnf4c1z7DTuTNjev5LwWJzbQaSmxP1/Nz295957iBRoNou8sdBVePxeKFuHu8QNygvL21gvJ6jjhLEVwbavnY=

(The version is the latest - Coq 8.7.0.)

On Fri, Nov 17, 2017 at 3:54 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Hello.

Require Import Omega ArithRing.

Goal (2+2=4).
Proof.
ring_simplify (2+2).
try omega. compute. omega.
Qed.

Tactic ring_simplify results in such goal:
N.to_nat 4 = 4

I included omega tactic to show, how this change could break older proofs. For example, it actually broke my tiny proof of "forall n m, 2 * n * n = m * m -> m = 0", that I accidentally revisited.

Best regards,
Ilmars

[Coq-Club] Strange behaviour of ring_simplify., Ilmārs Cīrulis, 11/17/2017
- Re: [Coq-Club] Strange behaviour of ring_simplify., Ilmārs Cīrulis, 11/17/2017
  - Re: [Coq-Club] Strange behaviour of ring_simplify., Hugo Herbelin, 11/18/2017