Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proving a simple equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving a simple equality


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page