coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] proving a simple equality
- Date: Tue, 22 Nov 2016 13:15:03 +0100
On 22/11/2016 10:36, noam neer wrote:
> thanx.
>
> BTW, what is the simplest way to prove simple goals like "0<=2"?
> "fourier" works but I wonder if it is not an overkill.
The cheapest way is to define a coercion from Z to R and to prove that
it is a morphism for the comparison operators. Then you can do the
following:
Goal (1234 <= 2345)%R.
now apply (Z2R_le 1234 2345).
Qed.
You can find such a definition in the Flocq library for instance.
Best regards,
Guillaume
- [Coq-Club] proving a simple equality, noam neer, 11/19/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/19/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/20/2016
- Re: [Coq-Club] proving a simple equality, Gaetan Gilbert, 11/21/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/21/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/22/2016
- [Coq-Club] Re : Re: proving a simple equality, Laurent Thery, 11/22/2016
- Re: [Coq-Club] proving a simple equality, Guillaume Melquiond, 11/22/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/22/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/20/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/19/2016
Archive powered by MHonArc 2.6.18.