coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>
>
- [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
- Re: [Coq-Club] Strange behaviour of ring_simplify., Ilmārs Cīrulis, 11/17/2017
Archive powered by MHonArc 2.6.18.