coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: How to prove that a nonnegreal plus a posreal is a posreal?

From: Daniel Schepler <dschepler AT gmail.com>
To: coq-club AT inria.fr
Cc: "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>, "Lucian M. Patcas" <lucian.patcas AT gmail.com>
Subject: Re: [Coq-Club] Re: How to prove that a nonnegreal plus a posreal is a posreal?
Date: Mon, 1 Aug 2011 10:24:29 -0700

On Friday, July 29, 2011 02:18:49 PM gallais @ ensl.org wrote:
> Hi Lucian,
>
> You can also do something like this (that does not use fourier).
> I guess that records are handled in a special way that allows
> to use apply when you actually just want to apply one of the
> projections.

There's nothing special about records in this. It seems to work on any
inductive type with one constructor, and can even handle some nesting:

Goal forall P Q R:Prop, P/\(Q/\R) -> Q.
Proof.
intros P Q R H.
apply H.
Qed.
--
Daniel Schepler

Re: [Coq-Club] Re: How to prove that a nonnegreal plus a posreal is a posreal?, Lucian M. Patcas
- <Possible follow-ups>
- Re: [Coq-Club] Re: How to prove that a nonnegreal plus a posreal is a posreal?, Daniel Schepler