存在性命题断言某个满足特定性质的对象存在。在 Coq 的命题即类型对应中，证明 ∃ x, P x 等价于构造一个依值对 ⟨w, p⟩，其中 w 是具体见证项，p : P w 是该见证满足性质的证明。这种"构造即证明"的机制直接决定了存在性证明的操作方式。

存在性命题的底层结构

Coq 标准库中 ex 的定义如下：

1
2
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
  | ex_intro : forall x : A, P x -> ex A P.

语法糖 ∃ x : A, P x 展开为 ex A (fun x => P x)。构造证明的唯一方式是应用 ex_intro，给出见证 x 和 P x 的证明。tactic 层面的 exists w 等价于 apply ex_intro with (x := w)，然后留下 P w 作为子目标。

1
2
3
4
5
6
(* 最基础的存在性证明 *)
Lemma ex_basic : exists n : nat, n + 2 = 5.
Proof.
  exists 3.
  reflexivity.
Qed.

运行 Print ex_basic. 可看到项 ex_intro nat (fun n => n + 2 = 5) 3 eq_refl，见证 3 被直接编码在证明项中。

exists tactic：显式提供见证

exists w 将当前目标 ∃ x, P x 变换为 P w，见证必须在此处完全给出。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(* 见证涉及表达式 *)
Lemma exists_expr : exists n : nat, n * n = 16.
Proof.
  exists 4.
  reflexivity.
Qed.

(* 嵌套存在量词 *)
Lemma nested_exists : exists (n m : nat), n + m = 10 /\ n < m.
Proof.
  exists 3, 7.
  split.
  - reflexivity.
  - omega.
Qed.

多层嵌套的 exists 可连写为 exists 3, 7，等价于依次调用两次 exists。

失败示例与修正

常见错误是在不知道具体见证时贸然给出错误值：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
(* 失败尝试：见证选错 *)
Lemma wrong_witness : exists n : nat, n + 3 = 7.
Proof.
  exists 3.
  (* 目标变成 3 + 3 = 7，无法完成 *)
  Fail reflexivity.
Abort.

(* 正确版本 *)
Lemma correct_witness : exists n : nat, n + 3 = 7.
Proof.
  exists 4.
  reflexivity.
Qed.

见证的选取在数学上等同于"找到满足条件的具体值"，这步无法由自动化 tactic 替代——至少需要提供计算策略或借助决策过程。

eexists：延迟见证填写

当见证依赖后续证明步骤中才能确定的信息时，可用 eexists 引入一个元变量 ?n 占位，待后续约束将其实例化。

1
2
3
4
5
6
7
Lemma eexists_demo : exists n : nat, n + 5 = 8.
Proof.
  eexists.
  (* 目标：?n + 5 = 8，?n 是元变量 *)
  omega.
  (* omega 解方程，将 ?n 实例化为 3 *)
Qed.

omega（或 Coq 8.14+ 推荐的 lia）能求解线性整数算术，并在过程中对元变量赋值。整个流程在逻辑上是：先承诺"某个 n 存在"，再由求解器倒推 n 的值。

1
2
3
4
5
6
7
8
9
10
11
(* 更复杂的例子：见证藏在列表操作里 *)
Require Import List.
Import ListNotations.

Lemma exists_in_list : exists l : list nat, In 5 l /\ length l = 3.
Proof.
  eexists [5; 0; 0].
  split.
  - left. reflexivity.
  - reflexivity.
Qed.

此处也可直接用 exists [5; 0; 0]，因为见证已经明确。eexists 的价值在于见证依赖中间计算结果时。

econstructor：构造子驱动的存在性

若存在性目标的见证类型是归纳类型，econstructor 自动选择合适的构造子并引入元变量。

1
2
3
4
5
6
7
(* 用 econstructor 证明 ex *)
Lemma econstructor_ex : exists n : nat, n = 42.
Proof.
  econstructor.
  (* 等价于 eexists，引入 ?n *)
  reflexivity.
Qed.

econstructor 对于 ex 等价于 eexists，但在更复杂的归纳类型上优势更明显：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Inductive Reachable : nat -> nat -> Prop :=
  | reach_refl : forall n, Reachable n n
  | reach_step : forall n m k, Reachable n m -> m + 1 = k -> Reachable n k.

Lemma reachable_example : exists k, Reachable 0 k /\ k > 3.
Proof.
  exists 4.
  split.
  - (* 构造 Reachable 0 4 *)
    econstructor.
    econstructor.
    econstructor.
    econstructor.
    + apply reach_refl.
    + reflexivity.
    + reflexivity.
    + reflexivity.
    + reflexivity.
  - omega.
Qed.

econstructor 对 Reachable 的目标会枚举构造子（reach_refl 或 reach_step）并选择能匹配当前目标的那个，行为类似 constructor 但允许留元变量。

refine：带洞的部分证明项

refine t 接受一个带 _ 占位符的证明项，将每个 _ 转变为独立子目标。这在见证复杂、或证明项结构已知但部分细节待填时非常有用。

1
2
3
4
5
6
7
(* 用 refine 直接写出 ex_intro 结构 *)
Lemma refine_exists : exists n : nat, n * 2 = 10.
Proof.
  refine (ex_intro _ 5 _).
  (* 子目标：5 * 2 = 10 *)
  reflexivity.
Qed.

ex_intro _ 5 _ 中第一个 _ 是谓词（Coq 可推断），5 是见证，第二个 _ 是待证的 P 5。

refine 在处理依值类型（第05篇讨论的 sigT、sig 等）时尤为关键，因为这些类型的构造子参数之间存在依值关系，直接写项比拼凑 tactic 更清晰：

1
2
3
4
5
6
7
8
9
10
11
12
13
(* sig 类型：计算相关的存在性 *)
Definition even_number : { n : nat | Nat.even n = true }.
Proof.
  refine (exist _ 4 _).
  reflexivity.
Defined.

(* 用 refine 处理更复杂的依值结构 *)
Definition double_of_3 : { n : nat | n = 3 * 2 }.
Proof.
  refine (exist _ _ eq_refl).
  (* 此处 eq_refl 要求 ?n = 3 * 2，Coq 归约后实例化 ?n := 6 *)
Defined.

注意最后用 Defined 而非 Qed，因为 sig 类型的项在计算层面是透明的（第05篇中对透明性与不透明性有完整讨论）。

通过计算找到见证

数学直觉上，证明 ∃ x, P x 最直接的办法是计算出 x 然后验证。Coq 支持反射式证明（proof by reflection）和决策过程：

1
2
3
4
5
6
7
8
9
Require Import Arith.
Require Import Decidable.

(* decide 处理可判定命题 *)
Lemma exists_via_decide : exists n : nat, n < 10 /\ n * n > 50.
Proof.
  exists 8.
  split; omega.
Qed.

对于更复杂的搜索，可写一个计算函数然后提取见证：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
(* 通过计算函数找见证 *)
Fixpoint find_witness (n : nat) : option nat :=
  match n with
  | 0 => None
  | S k =>
    if Nat.eqb (k * k) 25 then Some k
    else find_witness k
  end.

Lemma sqrt_5_exists : exists n : nat, n * n = 25.
Proof.
  exists 5.
  reflexivity.
Qed.

这里 find_witness 仅用于说明"计算见证"的思路；实际证明仍需显式给出 5，因为从 find_witness 提取并转化为命题级别的见证需要额外的正确性证明。

使用 omega/lia 关闭算术副目标

存在性证明通常产生算术侧条件，omega（处理 Peano 算术）或 lia（线性整数/自然数算术）可以自动关闭：

1
2
3
4
5
6
7
8
9
10
11
12
Lemma arith_witness : exists n : nat, 3 * n + 7 = 22.
Proof.
  eexists.
  lia.  (* 实例化 ?n := 5 并验证 *)
Qed.

(* 带约束的见证 *)
Lemma bounded_witness : exists n : nat, n <= 100 /\ n * n >= 9000.
Proof.
  exists 95.
  split; lia.
Qed.

Show Proof. 观察证明项结构

在交互式证明过程中随时调用 Show Proof. 可查看当前已构造的项，有助于理解 tactic 的底层语义：

1
2
3
4
5
6
7
8
9
10
11
Lemma show_proof_demo : exists n : nat, n + n = 8.
Proof.
  Show Proof.
  (* 输出：?Goal，表示整个目标尚未开始 *)
  exists 4.
  Show Proof.
  (* 输出：ex_intro nat (fun n => n + n = 8) 4 ?Goal *)
  reflexivity.
  Show Proof.
  (* 输出：ex_intro nat (fun n => n + n = 8) 4 eq_refl *)
Qed.

每一步 tactic 对应项构造中的一步填充。exists 4 之后，4 已经固定在项中；reflexivity 填入了剩余的 eq_refl。Print Assumptions show_proof_demo. 应输出 Closed under the global context.，表明证明不依赖任何公理（仅使用归约规则）。

存在性与析构

证明中常见模式是从假设中析出存在性见证再加以使用：

1
2
3
4
5
6
7
Lemma use_existence : 
  (exists n : nat, n > 5) -> exists m : nat, m > 3.
Proof.
  intros [n Hn].   (* 从假设中提取见证 n 和 n > 5 的证明 *)
  exists n.
  lia.
Qed.

intros [n Hn] 是 destruct 的模式匹配简写，直接将 ∃ n, n > 5 分解为见证 n 和性质证明 Hn。与第05篇中 sigT 的 projT1/projT2 类比，Prop 层的存在性在析构时不产生可计算项，只能用于继续证明。

存在性与否定

¬ (∀ x, P x) 与 ∃ x, ¬ P x 在经典逻辑中等价，但在 Coq 的构造主义逻辑中，后者比前者更强——后者要求提供反例见证：

1
2
3
4
5
6
7
8
9
10
11
(* 这个方向在构造逻辑中成立 *)
Lemma exists_not_implies_not_forall :
  (exists n : nat, n <> 0) -> ~ (forall n : nat, n = 0).
Proof.
  intros [n Hn] Hall.
  apply Hn.
  apply Hall.
Qed.

(* 反方向需要经典公理 *)
(* 在纯构造逻辑中无法证明：~ (forall n, n = 0) -> exists n, n <> 0 *)

这一不对称性是构造主义数学的核心特征，第05篇在讨论依值类型时已提及类似区别。

综合模式：eexists + refine + 决策过程

实际证明工程中，这三者常结合使用：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
Require Import ZArith.
Open Scope Z_scope.

(* 整数域存在性：找满足不等式的整数 *)
Lemma integer_witness : exists z : Z, z^2 < 50 /\ z > 6.
Proof.
  eexists.
  refine (conj _ _).
  - (* 子目标 1：?z^2 < 50 *)
    (* 此处 ?z 还未确定，需通过另一目标约束 *)
    Fail lia.  (* 元变量未实例化时 lia 无法运行 *)
Abort.

(* 正确做法：先确定见证再证性质 *)
Lemma integer_witness_correct : exists z : Z, z^2 < 50 /\ z > 6.
Proof.
  exists 7.
  split.
  - (* 7^2 = 49 < 50 *)
    vm_compute. reflexivity.
  - lia.
Qed.

上面 Fail lia 的例子说明了 eexists 的局限：当两个子目标都依赖同一个未实例化元变量时，lia 无法在元变量仍自由时运行。正确策略是先给出见证，再分别验证各性质。

vm_compute 在此用于规约 7^2 这类具体计算，比 simpl 更高效（vm_compute 使用 Coq 虚拟机直接求值）。

小结

tactic 见证状态 典型场景
exists w 立即固定 见证已知，一步给出
eexists 延迟到元变量实例化 见证由后续 lia/omega 推导
econstructor 延迟，按构造子结构 归纳类型目标，构造子已知
refine 部分固定，洞待填 证明项结构复杂，需精细控制

存在性证明的核心是见证的构造，而非仅仅宣称存在。这与第05篇中依值类型"项即证明、类型即命题"的讨论一脉相承：∃ x, P x 的证明项携带了 x 的具体值，这一特性使 Coq 中的存在性证明天然具有可提取的计算内容。

练习

练习 1

证明以下命题，要求使用 eexists 加 lia 完成，不直接给出见证数值：

1
Lemma exercise1 : exists n : nat, n * 3 = 18 /\ n > 4.

练习 2

定义谓词 IsPrime : nat -> Prop（可简化为：大于 1 且只能被 1 和自身整除，前几个可以用 forall d, d > 1 -> d < n -> n mod d <> 0 近似），证明：

1
Lemma exercise2 : exists p : nat, p > 10 /\ IsPrime p.

并用 Show Proof. 在 exists 之后观察已构造的项结构。

练习 3

证明下列传递性引理，要求用模式匹配 intros [n Hn] 形式提取中间见证：

1
2
3
4
Lemma exercise3 : 
  (exists n : nat, n > 100) ->
  (forall m : nat, m > 100 -> exists k : nat, k = m + 1 /\ k > 100) ->
  exists k : nat, k > 101.

参考资料

  • Coq Reference Manual 8.19, §8.4 Existential quantifier tactics
  • Pierce et al., Software Foundations Vol.1, Chapter Logic
  • Bertot & Castéran, Interactive Theorem Proving and Program Development, Chapter 5
  • Coq Standard Library: Coq.Init.Logic, ex, sig, sigT 定义