Coq:如何将一个假设应用于另一个假设

Question

假设我在上下文中有两个假设,a_b : A -> B并且a : A.我应该能够申请a_b到a获得进一步的假设,b : B.

也就是说,给定以下状态:

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

应该有一些策略,foo (a_b a)将其转换为以下状态:

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

但我不知道是什么foo.

我能做的一件事是:

 assert B as b.
 apply a_b.
 exact a.

但这是相当冗长的,如果不是a_b a我有一些更大的表达,就会严重缩放.

我能做的另一件事是:

specialize (a_b a).

但这取代了a_b我不想做的假设.

Answer 1

pose proof (a_b a) as B.

应该做你想做的事.