问题标签 [real-number]

我们使用 FPU 解决汇编语言中的实数问题。通常我们使用C语言或准备好的函数来编写输入输出代码。例如：

如何在不使用现成函数的情况下用汇编语言输入和输出实数？

假设我们有这样的东西：

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

我正在尝试检查字符串变量的值是否为双倍。

我已经看到了这个现有的问题（检查变量是否为双精度数据类型），它的答案很好，但我有一个不同的问题。

从我上面的代码中，当 ValueToTest 为“-∞”时，我在变量 Test 中得到的输出为“-Infinity”，并且该方法返回 true。

当 ValueToTest 为“NaN”时，我得到的输出为“NaN”。

它们是 C# 中的“-∞”和“NaN”双值吗？

还有一种方法可以只检查实数（https://en.wikipedia.org/wiki/Real_number）并排除无穷大和 NaN 吗？

我想在定义的 Reals 上使用 ssreflect 的引理Coq.Reals.Raxioms。我怎么做？

例如，我希望能够直接在类型变量上使用定义的add、mul等操作，并直接在 Coq 实数上应用。ssralg.GRing.RingRdefintions.RNum.real_closed_axiom

是否有必要证明从 eqType、choice、zmodule 等到 ClosedReals 的所有结构？如果是这样，之前一定有人这样做过，但我一直无法找到它。我可以使用其他一些开发吗？

如果不是这样，那么通过公理来做到这一点的正确方法是什么？是否必须添加额外的强制和Canonical结构语句。

我想找到垂直渐近线：

f=(3x^3 + 17x^2 + 6x + 1)/(2x^3 - x + 3)

所以我想找到 (2x^3 - x + 3) 的根，所以我写道：

输出是：

所以现在输出中唯一有意义的数字是-1.289，复数没有任何意义。

我的问题是：我怎样才能只选择实数所以输出显示：

我只是想从一个 BYTE 数组中获取一个 8 BYTE REAL 浮点数，该数组是我之前从文件内容生成的，作为浮点数。

目前我知道 8 BYTE Real 与 double 相同。因此，必须在逻辑上可以读出 8 个字节并将它们直接分配给变量。不幸的是，它不像我想象的那样工作。

举例说明：

My Byte Array Array 用于控制文件中存储的 HEX 值的输出。

从输出中的文件返回正确的十六进制值

wsprintf 必须使用它，因为我使用 API 工作并依赖 whitecharbuffer。

到目前为止，我已经尝试了以下方法：

输出：

另一个尝试：

输出：

页面的正确结果：http: //www.binaryconvert.com/result_double.html?hexadecimal=C1D6D420937EE766

但必须出来-1,532002893982。逗号计算不正确。

为什么我会得到错误的双数，我该怎么做才能得到结果 -1,532001 而不是 -1532001869,982873 ？

编辑：我从@ Gerhardh 试试这个

输出：

第一行有字节交换

我有同样的结果。

我想知道 Coq 是否将实数定义为 Cauchy 序列或 Dedekind 切割，所以我检查了 Coq.Reals.Raxioms 和......这两个都没有。实数及其运算（如Parameters 和Axioms）被公理化。为什么会这样？

此外，实数紧密依赖于子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上界。将Axiom completeness这些子集编码为Props。

我的印象是这些Props 仅形成实数的可定义子集。那么 Coq 是否只能访问可定义的实数？这个 Coq 到底是什么R？解析数字？代数数？算术数字？

如果，正如我所怀疑的那样，Coq 只有实数的可数子集（因为只有可数的多个Props），那就是实数的无穷小部分。它是否适合深入利用 ZFC 实数结构的理论，例如分形、混沌理论或勒贝格测度？

编辑

这是 Dedekind 切割对实数的天真构造。

编辑

这是 Coq 中R不可数的证明。我真的不知道该怎么想，因为Props 在 Coq 之外显然是可数的。正如 Arthur Azevedo De Amorim 所暗示的，这可能是Skolem 悖论的一种表现。R我想说的是，和之间的双射nat不能用 Coq 编写。可能出于与不可能在 Coq 中编写 Coq 解释器类似的原因。

我收到错误：

我现在正在研究 MyComplex 类，如 3.1 所示：http: //www.ntu.edu.sg/home/ehchua/programming/java/J3f_OOPExercises.html#zz-2

这是相关的代码的一部分：

我试图进行测试，当我运行它们时，我遇到的错误是向上的，这是我的测试代码的一部分：

在我正在工作的应用程序中，一些数字从长（18 位）转换并保存为浮点/双精度。这些数字类似于参考/ID，但不用于计算。最近我注意到存储为浮点/双精度的数据存在一些差异。我试图了解这种行为是否是由于浮点数称为有效数字，也许是对相同的简单解释。

我基于以下程序的问题是

1. 输出 no : 5 显示一个非常大的数字（小数点前 39 位）作为浮点的最大值。为什么 float 不能准确显示 7 位以上的内容。这是因为它只支持 6-7 位有效数字。
2. 输出 no : 10 显示一个非常大的数字作为 double 的最大值。那么为什么 double 无法准确显示 16 位以上的任何内容。这是因为它只支持 15 位有效数字。
3. 有效数字的真正含义是什么？这是否意味着该数字之后的任何数字无论是在小数点之前还是之后都无法准确表示？

注意：在我对这个主题进行研究之后，我现在明白浮点数本质上是不准确的，不应该用于表示需要准确表示的事物。我仍然对上述行为和有效数字感到有些困惑。

上述程序的输出

1. 50000000115 的浮点值为：49,999,998,976.000000。预期输出为 50000000115.000000
2. 50000000116 的浮点值为：49,999,998,976.000000。预期输出为 50000000116.000000

3. 50000000117 的浮点值为：49,999,998,976.000000。预期输出为 50000000117.000000

4. 2175863596593954381 的浮点值为：2,175,863,554,941,386,750.000000。预期产量为 2175863596593954381.000 000

5. Float.MAX_VALUE: 340,282,346,638,528,860,000,000,000,000,000,000,000.000000

6. 50000000115 的双倍值是：50,000,000,115.000000

7. 50000000116 的双倍值是：50,000,000,116.000000

8. 50000000117 的双倍值是：50,000,000,117.000000

9. 2175863596593954381 的双精度值为：2,175,863,596,593,954,300.000000。预期输出为 2175863596593954381.0 00000

10. Double.MAX_VALUE: 179,769,313,486,231,570,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,00 0,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,00 0,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,00 0,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000.000000

11. 数字的浮点值给出了预期的结果，直到 7 位，即 12345678 是：12,345,678.000000

12. 数字的浮点值给出了预期的结果，直到 7 位，即 11111111 是：11,111,111.000000
13. 数字的双值给出预期结果，直到 16 位，即 1122334455667788 是：1,122,334,455,667,788.000000
14. 数字的双值给出预期结果，直到 16 位，即 1111222233334444 是：1,111,222,233,334,444.000000

我是 Coq 的新手，我的主要兴趣是使用它来解决简单的实际分析问题。在第一个练习中，我设法证明 x^2+2x 趋于 0，而 x 趋于 0。请参见下面的代码。

这看起来很笨拙，我会对任何关于如何缩短这个证明的一般反馈或提高其可读性的良好实践感兴趣。然而，我的主要问题是，是否有任何 Coq 策略可以自动执行涉及实数的简单任务，field并且lra更好。

可能的示例 1： 是否有任何策略来证明来自 的函数的身份Rbasic_fun，例如绝对值？例如，我的一半证明致力于证明 |x*x|+|2*x|=|x| |x|+2 |x| ！

可能的示例 2：是否有任何策略可以自动使用来自 的引理，Rineq例如Rlt_le、和？也就是说，人类证明创建者用来“链接”一系列不等式的引理。Rle_transRplus_le_compat_rRmult_le_compat_r