`∃! х, ∃! y, P (x, y)` означают `∃! xy, P (fst xy) (snd xy)`?
Сравнительно легко доказать следующее (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.
Пожалуйста, помогите мне.
Ответы 1
Обратное неверно. Вот контрпример:
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?