Восстановление неявной информации из существующих в Coq

Question

Предположим, у нас есть что-то вроде этого:

Предположим, что x - действительное число. Покажите, что если существует действительное число y такое, что (y + 1) / (y - 2) = x, то x <> 1".

Если сформулировать это очевидным образом: forall x : R, (exists y, ((y + 1) * / (y - 2)) = x) -> x <> 1, человек сталкивается с проблемой очень скоро.

У нас есть предположение о существовании y такой, что ((y + 1) * / (y - 2)) = x), Я ошибаюсь, если предположить, что это также должно означать, что y <> 2? Есть ли способ восстановить эту информацию в Coq?

Конечно, если такой y существует, а не 2. Как можно восстановить эту информацию в Coq - нужно ли мне явно предполагать ее (то есть, нет способа восстановить ее путем экзистенциальной реализации как-то?).

Конечно, destruct H as [y] просто дает нам ((y + 1) * / (y - 2)) = x) за y : R, но сейчас мы не знаем y <> 2,

Answer 1

Я ошибаюсь, если предположить, что это также должно означать, что y <> 2?

Да. В Coq деление является полной неограниченной функцией: вы можете применить ее к любой паре чисел, включая делитель нуля. Если вы хотите предположить, y <> 2Вы должны добавить это как явное предположение к своей лемме.

Вы можете найти это страшным: как мы можем позволить делить что-то на ноль? Ответ в том, что это не имеет значения, если вы не пытаетесь утверждать, что 0 * (x / 0) = x, Этот вопрос обсуждает проблему более подробно.

Answer 2

Вещественные числа в Coq определены аксиоматически, то есть они являются просто именами, связанными с типами, к именам нет определений. Есть основные цифры (R0, R1) и операции с реалами (Rplus, Rmultи т. д.), которые не выполняются, т.е. операции не являются функциями. В некотором смысле можно просто построить действительные числа, построив их из этих операций, точно так же, как с помощью конструкторов данных (но мы не можем сопоставить шаблон с реалами).

Вышеуказанное означает, что, например, 1/0 является действительным действительным числом. Это просто аксиомы для действительных чисел, запрещающие некоторые упрощения, включающие такие выражения: мы не можем переписать такие выражения, как 1/0 * 0 в 1 (хотя, мы можем переписать его 0).

Вот как мы можем показать, что мы не можем вывести y <> 2 из выражения как

(y + 1) / (y - 2) = x

потому что нам разрешено использовать "странные" действительные числа:

From Coq Require Import Reals.
Open Scope R.

Goal ~ (forall x y : R, (y + 1) / (y - 2) = x -> y <> 2).
  unfold "_ - _"; intros contra; specialize (contra ((2+1)/0) 2).
  rewrite Rplus_opp_r in contra.
  intuition.
Qed.