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
.
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.