Coq：如何将一个假设应用于另一个 [英] Coq: how to apply one hypothesis to another

问题描述

假设我在上下文中有两个假设， a_b：A-> B 和 a：A 。我应该能够将 a_b 应用于 a 以获得进一步的假设， b：B 。

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.

即给出以下状态：

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

应该有一些策略，将 foo（a_b a）转换为以下状态：

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

但是我不知道 foo 是什么。

我能做的一件事是这样：

One thing I can do is this:

 assert B as b.
 apply a_b.
 exact a.

但这是一个漫长的过程，如果不是 a_b，扩展性很差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).

但是此替换 a_b 假设，这是我不想做的。

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

推荐答案

pose proof (a_b a) as B.

应该做你想做的事。

这篇关于Coq：如何将一个假设应用于另一个的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！