5

假设我们有这样的东西：

假设 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。

4

2 回答 2

4

我是否错误地认为这也应该暗示这一点y <> 2？

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

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

于 2017-12-06T12:51:49.370 回答
3

Coq 中的实数是公理定义的，即它们只是与类型相关的名称，没有附加到名称的定义。有基本数字（R0, R1）和对实数的运算（Rplus,Rmult等）不会被执行，即运算不是函数。从某种意义上说，人们只是通过像数据构造函数一样从这些操作中构造实数来构建实数（但我们不能对实数进行模式匹配）。

上面的意思是，eg1/0是一个有效的实数。这只是实数公理的前提，禁止一些涉及像这样的表达式的简化：我们不能像1/0 * 0to那样重写表达式1（尽管我们可以将它重写为0）。

这是我们如何证明我们不能y <> 2从像这样的表达式中推导出来的方法

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

因为我们可以使用“奇怪的”实数：

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.
于 2017-12-07T09:33:27.087 回答