The Coq mailing list

[Marko Doko <mdoko AT mpi-sws.org>]

On 2019-01-08 07:17 UTC+0100 Jeremy Dawson wrote:
> 
> given a hypothesis, such as
> H : A -> B
> how do I get this to two subgoals, one with B as a hypothesis,
> and the other with A as the conclusion
> (where either A and B are too long to type in, or where I want to do 
> this inside an Ltac tactic, where A and B may vary)
> 

Here a tactic from Hahn library (https://github.com/vafeiadis/hahn) that
achieves the above (and a bit more):

Tactic Notation "specialize_full" ident(H) :=
  let foo := fresh in
  evar (foo : Prop); cut (foo); subst foo; cycle 1;
  [eapply H|try clear H; intro H].


If you call

  specialize_full H

you will get two goals. The first one will require you to prove A, and the
second one will contain hupothesis H: B.


-- 
Marko