问题标签 [real-number]

我正在尝试用 Coq 为实数做简单的证明。例如，我想证明两个非负数的平均值也是非负数。

我的第一步是证明r1 + r2 >=0如下。

但是，我只能得到

在假设中。我无法将0 + 0H1 的 RHS 更改为0. 我尝试simpl in H1.了如图所示，它什么也没做。我知道实数不同于nat. 但是我应该如何简化这里的事情？

（注意：我是实数初学者。上面的代码可能很幼稚/效率低下。欢迎提出改进建议。）另外：

What I am looking for is an auto-like tactic that can prove simple equalities like:

So far, what I've tried manually is to use ring_simplify and field_simplify to prove equalities. Even this doesn't work out well (Coq 8.5b3). The example below works:

But it was necessary to use field_simplfy twice before reflexivity. The first field_simplfiy gives me:

which is not subject to reflexivity.

The example below does not work, field_simplify seems to do nothing on the goal, and therefore, reflexivity can't be used.

Again, is there an automatic way to achieve this, like an field_auto?

有没有办法自动证明简单的不等式1/2 >= 0？，即

ring我对or没有太多经验，field甚至在证明简单的等式方面也遇到了麻烦，例如1/2 = 2/4.

我正在寻找的是类似omega但适用于实数和不等式的东西。

我只是想知道如何为实数定义“小于”关系。

我知道对于自然数 ( nat)，<可以递归地定义为一个数字是另一个数字的 ( 1+) 后继S。我听说很多关于实数的事情在 Coq 中都是公理化的，不需要计算。

但我想知道 Coq 中是否有一组最小的实数公理，基于这些公理可以推导出其他属性/关系。（例如 Coq.Reals.RIneq有它Rplus_0_r : forall r, r + 0 = r.是一个公理，等等）

特别是，我对是否可以在相等关系之上定义诸如<或之类的关系感兴趣。<=例如，我可以想象在传统数学中，给定两个数字r1 r2：

但这在 Coq 的建设性逻辑中成立吗？我可以用它来至少对不等式进行一些推理（而不是一直重写公理）吗？

Reals在证明不等式和多项式方程等一般事实时，导入和类似的东西有什么区别Coq.Reals.{Rineq, R_sqrt, ...}？

我从搜索特定事实/定理开始，最终使用后者，但我看到其他人只使用Reals. 仅使用它更容易或更全面Reals吗？

怀疑它是遗留的东西，我试图导入，Coq.Reals但它似乎不存在（Coq 8.5 beta 3）。

我正在寻找一种在 Choco Solver 上对数学方程进行编码的方法。我看到有一种方法可以对约束进行编码，例如：

但我正在尝试编码类似

其中x和y是 int 变量，系数是实数。

Matlab中有任何函数可以在闭合区间内生成随机实数。我发现了一些东西，unifrnd()但它在开区间内生成数字。如果我使用unifrnd(x,y);我得到 (x,y) 间隔，而不是 [x,y]。

我正在用verilog写一个高斯噪声发生器，

当输出是逻辑向量（16位）时，代码工作正常

但我需要这段代码与另一个使用真实输入的块进行通信

我试过 $bitstoreal 函数，但它不起作用，输出总是 O

我所做的是在模块输入/输出声明中用输出真实 data_out1 替换输出 [16, 0] data_out1，并添加“assign data_out1 = $bitstoreal(data_out);” data_out 是来自其他模块的位向量

任何帮助

我需要在小数点之前的整数部分用前导零格式化一个实数。我知道如何用整数来实现这一点，但实数的语法让我无法理解。

这给了SNumber = ' 1.234'但我想要'01.234'。 Number始终为 0..99.999

我编写了一个简单的程序，将 pi 加载到 8087 中的寄存器堆栈的顶部，然后将该常量返回到一个短的实内存变量中。

shortReal 中存储的值是 40 49 0F DB hex。这转换为二进制的 0100000001001001111111011011。

第一位是 0，所以它是一个正数。有偏的指数部分转换为 1。

因此，实际数字如下所示：

1（隐含点）10010010000111111011011

1（隐含点）1 转换为 3. ，所以这是 PI 的正确整数部分，但我的理解在这一点之后就崩溃了。

现在剩下以下数字：

0010010000111111011011

001 可以转换为 1，这是正确的。但是，这意味着下一个数字将是 001，它又是 1，这是错误的，或者它可能是 0010，它等于 2，但这也是错误的。

你如何分离小数部分中的每个数字。