coq - 如何在 Coq 中表达 "there exists a unique X"？

Question

我想知道是否有 简洁在 Coq 中存在一个独特的东西(即编写独特的存在量词)的写作方式？

例如，说存在一个 x英石。 2 + x = 4 :

Goal exists x, 2 + x = 4.

我怎么写存在一个 唯一 x具有相同的属性？

我知道我可以复制 s.t. 中的谓词像这样的部分:

Goal exists x, 2 + x = 4 /\ forall y, 2 + y = 4 -> y = x.

但总的来说，这是很多重复，有没有办法以某种方式编码一个新的量词，然后写:

Goal exists1, 2 + x = 4.

表达相同的目标？

Answer 1

Coq 已经提供了一个 exists!符号。例如:

Goal exists! x, 2 + x = 4.
Proof.
exists 2. split.
+ reflexivity.
+ intros. injection H; intro.
  symmetry; assumption.
Qed.