coq - 在 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

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

是的。在 Coq 中，除法是一个完全的、不受约束的函数:你可以将它应用于任何一对数字，包括一个零除数。如果您想承担 y <> 2 ，您需要将其作为明确的假设添加到您的引理中。

你可能会觉得这很可怕:我们怎么能被允许除以零呢？答案是没关系，只要你不试图争论 0 * (x / 0) = x . This question更详细地讨论这个问题。