The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

As far as i understand, the very value of H may be useful
and defining it in one step may be hard.

Example:

Goal forall x : X, exists y: Y, complicated_property x y.
intros x. pose (y: Y).
  apply many_functions_in_order_to_build_y_from_x.
  exists y. apply many_lemmas_for_proving_complicated_property_x_y.
Qed.

Here neither cut nor assert is the answer. 

JF

On Tue, Apr 06, 2010 at 01:32:57PM +0200, Stéphane Lescuyer wrote:
> I don't see what is the problem with assert, "assert (H : P)" is
> basically "cut P" with the goals generated the other way, so it is
> exactly what you asked for in your first message ; in particular, it
> does add an hypothesis named H of type P in the second goal.
> Note that assert can be used as pose as well : "assert (H := t)" will
> act as "pose (H := t); clearbody H".
> 
> HTH,
> 
> Stéphane
> 
> On Tue, Apr 6, 2010 at 1:22 PM, andré hirschowitz 
>Â <ah AT unice.fr>
>  wrote:
> > no, if I experiment correctly.
> >
> > assert generates two goals and does not forward to the second one the
> > formula produced for the first one.
> >
> > Thanks for your answer.
> >
> > ah
> >
> >>
> >>
> >> I think you are looking for the following?
> >>
> >>  assert (myname : mytype).
> >>
> >>
> >
> >
> 
> 
> 

-- 
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458