Сравнительно легко доказать следующее (Coq):
Goal forall A (P : A -> A -> Prop), (exists! xy, P (fst xy) (snd xy)) -> (exists! x, exists! y, P x y).
Вопрос, которым я озадачен: верно ли обратное? Формулировка exists x, exists y, ...
позволяет выбирать y
на основе того, что x
было выбрано на шаг назад, поэтому считается, что y
зависит от x
. Мне кажется (по крайней мере, я не могу себя убедить в обратном), что exists xy, ...
- существование пары (x, y)
иное: оно не позволяет выбирать y
на основе x
.
Забавный факт заключается в том, что я пытался доказать как Goal forall A (P : A -> A -> Prop), (exists! x, exists! y, P x y) -> ~ (exists! xy, P (fst xy) (snd xy)).
, так и его отрицание, и оба раза застрял с невозможностью построить требуемый объект или вывести False
.
Пожалуйста, помогите мне.
Обратное неверно. Вот контрпример:
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.
@Zazaeil Вы не можете опровергнуть результат для всех предикатов P. Например, P x y
может быть x = true /\ y = true
, и в этом случае верно обратное.
Спасибо. P.S. Довольно изящная тактика манипулирования. Я узнал несколько новых вещей.
Хорошо, но вы доказываете это для вполне определенного
P
использования сопоставимостиbool
широко AFAICS. Есть ли способ доказать то же самоеforall P
?