Coq: how to apply one hypothesis to another

问题:

Assume I have two hypotheses in the context, a_b : A -> B and a : A. I should be able to apply a_b to a to gain a further hypothesis, b : B.

That is, given the following state:

1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
______________________________________(1/1)
C

There should be some tactic, foo (a_b a), to transform this into the following state:

1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
b : B
______________________________________(1/1)
C

But I don't know what foo is.

One thing I can do is this:

 assert B as b.
 apply a_b.
 exact a.

but this is rather long-winded, and scales badly if instead of a_b a I have some larger expression.

Another thing I can do is:

specialize (a_b a).

but this replaces the a_b hypothesis, which I don't want to do.

回答1:

pose proof (a_b a) as B.

should do what you want.

回答2:

You can just use "apply a_b in a."