The Coq mailing list

[Robert R Schneck <schneck AT math.berkeley.edu>]

> I would like to know if COQ supports the forward and backward proof in
> the same proof. In other word, it is possible to build new hypothesis
> from the assumptions and to make use of it to prove the goal.

If you have
  H1 : P -> Q
  H2 : P

and you want to get a new hypothesis Q, there are several tactics.

You can use "Assert Q".  This creates two subgoals, the first Q, and the
second the original subgoal with an extra hypothesis Q.

You can use "Cut Q", which is almost identical.

You can use "Pose (H1 H2)".  This creates a hypothesis
  q := (H1 H2) : Q
If you want to forget how you proved q : Q, you can say "ClearBody q".

Finally you can use "Generalize (H1 H2)".  If the original subgoal
is R, the new subgoal is Q -> R.  From habit this is the way I usually do
it: "Generalize (H1 H2); Intro".  (This may be undesirable if H1 and H2
actually appear as terms in the goal.)

Any others?

Robert