Recovery of implicit information from existential numbers in Coq

Question

Suppose we have something like this:

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

If someone formulates this in an obvious way: forall x : R, (exists y, ((y + 1) * / (y - 2)) = x) -> x <> 1 , you will very soon encounter a problem.

There is an assumption about the existence of y such that ((y + 1) * / (y - 2)) = x) . Am I mistaken in believing that this should also mean that y <> 2 ? Is there a way to recover this information in Coq?

Undoubtedly, if such a y exists, then this is not so. 2. How to restore this information in Coq - do I need to explicitly assume it (that is, there is no way to restore it through an existential instance?).

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 .

Answer 1

Am I mistaken in believing that this should also mean that y <> 2 ?

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

You may find this scary: how do we allow something to divide by zero? The answer is that it does not matter if you are not trying to claim that 0 * (x / 0) = x . This question discusses the problem in more detail.

Answer 2

Real numbers in Coq are determined axiomatically, i.e. these are just names associated with types, there are no definitions associated with names. There are basic numbers ( R0 , R1 ) and operations on actions ( Rplus , Rmult , etc.) that are not performed, that is, operations are not functions. In a sense, it simply builds real numbers, creating them from these operations, as with data constructors (but we cannot match patterns by reals).

The foregoing means that, for example, 1/0 is a real real number. This is simply a premise of the axioms for real numbers, which prohibits some of the simplifications associated with such expressions: we cannot rewrite expressions like 1/0 * 0 - 1 (although we can rewrite it to 0 ).

Here's how we can show that we cannot deduce y <> 2 from an expression like

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

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

 From Coq Require Import Reals. Open Scope R. Goal ~ (forall xy : 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.