Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • To: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Strange behaviour of ring_simplify.
  • Date: Sat, 18 Nov 2017 15:26:19 +0100

Hi,

This looks like a regression. You should report a bug at
https://github.com/coq/coq/issues.

Best,

Hugo Herbelin

On Fri, Nov 17, 2017 at 03:56:22PM +0200, Ilmārs Cīrulis wrote:
> (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
>
>



Archive powered by MHonArc 2.6.18.

Top of Page