coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Strange behaviour of ring_simplify.
Date: Fri, 17 Nov 2017 15:54:21 +0200
Authentication-results: mail3-smtp-sop.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-wr0-f173.google.com
Ironport-phdr: 9a23:g0Vq0RUr8VHx/WyBLh5cRZ5zJBrV8LGtZVwlr6E/grcLSJyIuqrYZRyDt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl8/LePsX4XWks6f1uao+pSVbR8CzG62Zqo3JxGrpy3QsNMXiM1sMPBi5AHOpy5pf+H933ggDlOJghL9/Y/k/Zpm+j5L/fkg7dNEUL7ScKExTLgeBzMjZTNmrPb3vAXOGFPcrkAXVX8bx0JF

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