coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Easy proofs complicated with reals

From: Evgeny Makarov <emakarov AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Easy proofs complicated with reals
Date: Thu, 26 Aug 2010 15:18:56 +0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=nh8dS/BND8deTwIJGSJNtYD8GnllagC4sqkPSpImeO9q73qNGquTw7Fxnt7Jo68ogC DRdH6OS6YIc3SMRM5QoDbNi8g6BG+3V4Skrk3c5Otw2+vqE9A0NEqXapJBdasXxaSF6V Cy0IJ+zkcPgX3mk6X3IaRoc1DFBQUkws4CchM=

Hi, Michael,

The facts you gave can be proved automatically using Micromega plugin
(see Reference Manual, chapter 20).

Require Import Psatz.

Open Scope R_scope.

Goal forall x : R, 1 <= x -> x <> 0.
intros. psatzl R.

They also can be proved from scratch using the standard library. For example:

Goal forall x : R, 1 <= x -> x <> 0.
intros x H1 H2. rewrite H2 in H1. apply (Rlt_irrefl 1).
apply Rle_lt_trans with (r2 := 0); [assumption | apply Rlt_0_1].

Evgeny

[Coq-Club] Easy proofs complicated with reals, Michael
- Re: [Coq-Club] Easy proofs complicated with reals, Evgeny Makarov
- <Possible follow-ups>
- Re: Re: [Coq-Club] Easy proofs complicated with reals, Michael
  - Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu
    - Re: [Coq-Club] Easy proofs complicated with reals, Fr�d�ric Besson
    - Re: [Coq-Club] Easy proofs complicated with reals, gallais @ EnsL
      - Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu