问题

以下是翻译好的部分：

可以相对容易地证明以下内容（Coq）：

目标 forall A（P：A->A->Prop），（存在！xy，P（fst xy）（snd xy））->（存在！x，存在！y，P x y）。

问题我感到困惑的是：反向是否成立？存在x，存在y，...的表述允许基于一步前选择的x来选择y，因此y允许依赖于x。在我看来（至少，我无法使自己相信否定），存在xy，... - 一对(x, y)的存在是不同的：它不允许基于x选择y。

有趣的事实是，我尝试证明Goal forall A（P：A->A->Prop），（存在！x，存在！y，P x y）-> ~（存在！xy，P（fst xy）（snd xy））。及其否定，并且两次都陷入无法构造所需对象或推导False的困境。

请帮助我。

<details>
<summary>英文:</summary>

It is comparatively easy to prove the following (Coq):

Goal forall A (P : A -> A -> Prop), (exists! xy, P (fst xy) (snd xy)) -> (exists! x, exists! y, P x y).

The question I am puzzled with: does the reverse hold? The `exists x, exists y, ...` formulation allows `y` to be chosen based on what `x` got selected one step back, so `y` is admitted to be __dependent upon `x`__. It seems to me (at least, I am not able to convince myself otherwise) that `exists xy, ...` - a pair `(x, y)` existence is different: it does not allow `y` to be chosen based on `x`. 

The fun fact is that I tried to prove both `Goal forall A (P : A -> A -> Prop), (exists! x, exists! y, P x y) -> ~ (exists! xy, P (fst xy) (snd xy)).` and it's negation and both times got stuck with not being able to construct a required object or derive `False`.

Please, help me out.

</details>


# 答案1
**得分**: 1

以下是代码的翻译部分：

The converse does not hold. Here is a counterexample:

``` Definition P (x y : bool) : Prop :=
  x = true -> y = true.

Lemma l1 : exists! x, exists! y, P x y.
Proof.
exists true.
split.
- exists true. split; [easy|].
  now intros y ->.
- intros x' (y & Py & unique_y).
  destruct x'; trivial.
  assert (contra: P false (negb y)).
  { intros; easy. }
  specialize (unique_y (negb y) contra).
  now destruct y.
Qed.

Lemma l2: ~ (exists! xy, P (fst xy) (snd xy)).
Proof.
intros ([x y] & Pxy & unique_xy); simpl in *.
assert (contra: P (negb x) true).
{ intros ?. reflexivity. }
specialize (unique_xy (negb x, true) contra).
injection unique_xy as contra' _.
now destruct x.

Definition P (x y : bool) : Prop :=
  x = true -> y = true.

Lemma l1 : exists! x, exists! y, P x y.
Proof.
exists true.
split.
- exists true. split; [easy|].
  now intros y ->.
- intros x' (y & Py & unique_y).
  destruct x'; trivial.
  assert (contra : P false (negb y)).
  { intros; easy. }
  specialize (unique_y (negb y) contra).
  now destruct y.
Qed.

Lemma l2 : ~ (exists! xy, P (fst xy) (snd xy)).
Proof.
intros ([x y] & Pxy & unique_xy); simpl in *.
assert (contra : P (negb x) true).
{ intros ?. reflexivity. }
specialize (unique_xy (negb x, true) contra).
injection unique_xy as contra' _.
now destruct x.
Qed.