Recovering implicit information from existentials in Coq

Question

Suppose we have something like this:

Suppose x is a real number. Show that if there is a real number y such that (y + 1) / (y - 2) = x, then x <> 1".

If one formulates it in an obvious way: forall x : R, (exists y, ((y + 1) * / (y - 2)) = x) -> x <> 1, one runs into an issue very soon.

We have an assumption of existence of y such that ((y + 1) * / (y - 2)) = x). Am I wrong to assume that this should also imply that y <> 2? Is there a way to recover this information in Coq?

Surely, if such y exists, then it is not 2. How does one recover this information in Coq - do I need to explicitly assume it (that is, there is no way to recover it by existential instantiation somehow?).

Of course, destruct H as [y] just gives us ((y + 1) * / (y - 2)) = x) for y : R, but now we don't know y <> 2.

Mccain

Answer 1

Am I wrong to assume that this should also imply that y <> 2?

Yes. In Coq, division is a total, unconstrained function: you can apply it to any pair of numbers, including a zero divisor. If you want to assume y <> 2, you need to add that as an explicit assumption to your lemma.

You may find this scary: how could we be allowed to divide something by zero? The answer is that it doesn't matter, as long as you do not try to argue that 0 * (x / 0) = x. This question discusses the issue in more detail.

Gird

Answer 2

The real numbers in Coq are defined axiomatically, i.e. they are just names associated with types, there are no definitions attached to the names. There are basic numbers (R0, R1) and operations on reals (Rplus, Rmult, etc.) which do not get executed, i.e. operations are not functions. In a sense one just builds real numbers by constructing them out of those operations just like with data constructors (but we cannot pattern-match on reals).

The above means that, e.g. 1/0 is a valid real number. It's just the premises of the axioms for real numbers prohibit some simplifications involving expressions like that: we cannot rewrite expressions like 1/0 * 0 to 1 (though, we can rewrite it to 0).

Here is how we can show that we cannot derive y <> 2 from an expression like

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

because we are allowed to use "strange" real numbers:

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.

Ferriage