如何在 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.

How can I reorder existential variables in Coq?