如何在Coq中表达"存在独特的X"？

Question

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

例如,要说存在一个xst 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.