The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> If you have
>   H1 : P -> Q
>   H2 : P
> 
> and you want to get a new hypothesis Q, there are several tactics.
> 
> (...)
>  
> Any others?

  There is also 

    Assert q := (H1 H2)

  which is equivalent to "Pose q := (H1 H2); ClearBody q".

  Hugo Herbelin


PS: Notice for people that are interested in proof rendering that Assert
and Pose (and Cut) are not rendered the same as Generalize (see the
HELM experimental rendering tool at http://mowgli.cs.unibo.it, link
HELM, link COQ Online). Indeed Generalize builds a beta-expanded term
while Assert, Pose and Cut uses a let-in.

  (* Goal is T *)
  Generalize (H1 H2).
  (* Goal is A->T *)
  ... a proof of A->T ...

is rendered into something like

  (h) ... the proof of A->T ...
      we proved A->T
  (h0) by (H1 H2) we proved A
  by (h h0) we proved T

while 

  (* Goal is T *)
  Assert q := (H1 H2).
  (* Goal is A *)
  ... a proof of A ...
  (* Goal is A |- T *)
  ... a proof of T ...

is rendered into something like

  (q) ... the proof of A ...
      we proved A
  ... the proof of T ...
  we proved T

Otherwise said, Generalize is not rendered in a forward-reasoning way,
while Assert is.