什么是 Coq 中一个简单证明的好例子，其中结论有一个存在量词？

Question

我想看一些关于 Coq 形式证明的例子：

\exists A(x1,...,xn)

本质上，目标有一个存在量词。我在以有意义的方式操纵目标以在我的证明中取得进展时遇到问题，并希望看到一些常见操纵策略的示例。

Coq 中有哪些好的存在量词示例可以证明？

---

我的具体例子：

Theorem Big_Small_ForwardImpl   :
  forall (P : Program) (S' : State),
    (BigStepR (B_PgmConf P) (B_StateConf S')) -> (ConfigEquivR (S_PgmConf P) (S_BlkConf EmptyBlk S')).
Proof.
  intros.
  induction P.
  unfold ConfigEquivR.
  refine (ex_intro _ _ _) .

我的背景和目标是：

1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
exists N : nat, NSmallSteps N (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')

但后来改为：

1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
NSmallSteps ?Goal (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')

在使用refine (ex_intro _ _ _) 策略之后。由于我不确定发生了什么，我希望一些更简单的示例可以向我展示如何在我的 Coq 目标中操纵存在量词。

---

有用的评论：

?Goal 是 Coq 引入的，作为一些 N 的占位符，稍后必须在证明中推导。

Answer 1

以下示例基于this answer中提供的代码。

假设我们有一个类型 T 和一个二元关系 R 在类型为 T 的元素上。出于本示例的目的，我们可以将其定义如下。

Variable T : Type.
Variable R : T -> T -> Prop.

让我们证明以下简单的定理。

Theorem test : forall x y, R x y -> exists t, R x t.

这是一个可能的解决方案。

Proof.
  intros. exists y. apply H.
Qed.

我们可以依靠 Coq 强大的自动证明机制来自动推断出哪个变量满足 R x t，而不是明确指定 y 是我们正在寻找的元素：

Proof.
  intros.
  eexists. (* Introduce a temporary placeholder of the form ?t *)
  apply H. (* Coq can deduce from the hypothesis H that ?t must be y *)
Qed.

存在许多使用相同自动推理机制的策略，例如eexists、eapply、eauto 等。

请注意，它们的名称通常对应于以e 为前缀的常用策略。