在Coq中如何调整存在量词变量的实例化顺序？

Coq 默认的 exists 策略会按从左到右的顺序依次实例化存在量词，要跳过前两个量词直接实例化第三个量词 c，可以用以下几种方法：

方法1：使用enough策略（标准Coq无额外依赖） #

通过enough提前锚定c的取值，绕开按顺序实例化的限制：

Lemma three_nats : exists (a : nat) (b : nat) (c : nat),
  a + b = c.
Proof.
  enough (exists a b, a + b = 3) as [a [b H]].
  - (* 将已得到的a、b、3回填到原目标 *)
    exists a, b, 3. exact H.
  - (* 仅需证明存在a、b满足a+b=3，直接实例化即可 *)
    exists 1, 2. reflexivity.
Qed.

方法2：使用Ssreflect扩展的exists策略（写法最简洁） #

如果你的项目引入了ssreflect库，可以直接按变量名指定要实例化的存在量词：

From Coq Require Import ssreflect.

Lemma three_nats : exists (a : nat) (b : nat) (c : nat),
  a + b = c.
Proof.
  exists (c := 3). (* 直接跳过a、b，先实例化c为3 *)
  exists 1, 2. reflexivity.
Qed.

方法3：用instantiate给存在变量赋值 #

你示例中用到的eexists会为前两个量词创建未确定的存在变量?a、?b，实例化c为3后，可以直接用instantiate给前面的存在变量赋值：

Lemma three_nats : exists (a : nat) (b : nat) (c : nat),
  a + b = c.
Proof.
  eexists. (* 创建存在变量?a : nat *)
  eexists. (* 创建存在变量?b : nat *)
  exists 3. (* 实例化c=3，当前目标为 ?a + ?b = 3 *)
  instantiate (1 := 1). (* 给?a赋值1 *)
  instantiate (1 := 2). (* 给?b赋值2 *)
  reflexivity.
Qed.

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