The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Jeremy,

On 1/8/19 7:17 AM, Jeremy Dawson wrote:
> Hi coq-club,
>
> two questions:
>
> (1) given a hypothesis, such as
> H : forall x : A x -> B x
>
> how do I get it into the form
> A ?x -> B ?x
> where ?x is to be instantiated later

evar (z : nat). specialize (H z).

is one way. There may be a more idiomatic one.

> (2) 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)

You can use "match" to extract big terms from your context/goal to use 
in other tactics:

match type of H with
| ?A -> _ =>
  assert (I : A); [| apply H in I ]
end.

or you can encode the underlying propositional reasoning as an explicit 
term:

apply (fun G2 G1 => G1 (H G2)).

Li-yao