如何在 Coq 中将蕴涵分解为两个子目标？

Question

说我有以下内容：

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

然后，在线上方，我得到：

X : a
X0 : b -> c

假设在我的证明中，我知道我将在某处需要

c

。而且我知道如何从

b

证明

a

，但这不是很容易。一种可能是：

assert b.
+ (* proof of b here *)
+ (* proof using c here *)

在这个简单的案例中，这很轻松。但是，我想在不指定

b

的情况下达到相同的效果，因为我经常有更复杂前提的假设，我不想在

assert

中明确输入。

pose

没有做我想做的事，因为它需要我先证明

a

，所以自动化策略也不起作用，因为他们不知道我正在尝试证明

a

。

apply

也没有做我想做的事，因为它要求我首先将我的目标变成与暗示相同的形式，这也不适合自动化策略。

总而言之，我希望能够采取假设

H

这是一个暗示，并得到两个子目标：

• 一个证明

  H

  的前提。
• 一个证明我已经拥有的相同目标，给出

  H

  的结论作为一个新的假设。 而且我想在不明确输入

  H

  的前提的情况下执行此操作。

Answer 1

我认为

lapply

最接近期望的行为：

变体

lapply <term>

此策略适用于任何目标，例如

G

。参数术语必须在当前上下文中格式正确，其类型可简化为非依赖产品

A -> B

和

B

可能包含产品。然后它生成两个子目标

B->G

和

A

。应用

lapply H

（其中

H

具有类型

A->B

并且

B

不以产品开头）与给出序列

cut B. 2:apply H.

相同，其中

cut

如下所述。

在你的例子中，我们得到：

Lemma my_lemma :
  forall a b c d,
    a -> (b -> c) -> d.
Proof.
  intros.
  lapply X0.
  + intro.
    (* prove d using c *)
    admit.
  + (* prove b *)
    admit.
Admitted.