从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。 这个问题更详细地讨论了这个问题。