如何重新排序Coq中的存在变量

Question

在某些情况下，在实例化一个存在项之前实例化另一个更容易。在这个人为的例子中，我希望首先设置c = 3，然后从中选择a = 1和b = 2。

Lemma three_nats : exists (a : nat) (b : nat) (c : nat),
a + b = c.
Proof.
eexists.
eexists.
exists 3.
(* Now what? *)

有没有办法先在c上使用简单的exists 3？

Answer 1

可以用它是enough来证明存在c，b，a使得a+b=c。

enough (exists c a b, a + b = c).

现在你有两个目标。首先，

exists c a b, a + b = c  -> exists a b c, a + b = c.

其次，

exists c a b, a + b = c.

顺便说一句，你可以像这样用firstorder快速完成第一部分的证明：

enough (exists c a b, a + b = c) by firstorder.

或者，如果你不想重复这个目标，就应用这个引理：

Lemma ex_swap {A B C} {P:A->B->C->Prop}: 
(exists c a b, P a b c) -> exists a b c, P a b c.
Proof. firstorder.  Qed.