如何在Coq中将蕴含式拆分为两个子目标？

先看初始代码：

Lemma my_lemma :
  forall a b c,
    a -> (b -> c) -> d.
Proof.
intros.

执行intros后，上下文区域显示：

X : a
X0 : b -> c

场景与现有解法 #

证明过程中需要用到c，已知可从a推导出b，但推导过程较复杂。目前的做法是：

assert b.
+ (* 此处证明b *)
+ (* 此处使用c进行证明 *)

这种方法在简单场景下很方便，但面对更复杂的前提时，手动在assert中输入前提过于繁琐，希望能无需显式指定b就能实现相同效果。

其他策略的局限性 #

• pose无法满足需求：它要求先完成前提的证明，自动化策略无法识别要证明的目标，效果很差。
• apply也不可行：它需要先将原目标转换为与蕴含式一致的形式，不利于自动化策略的使用。

核心需求 #

希望有一个策略，针对蕴含式类型的假设H，自动生成两个子目标：

1. 证明H的前提；
2. 在新增H的结论作为假设的前提下，证明原目标。
   并且无需手动输入H的前提。

内容的提问来源于stack exchange，提问作者markasoftware