问题标签 [real-number]

我想比较x并c忽略c.

这是 Coq 标准库中定义的完整性公理。

假设我添加

这是必需的吗？（即它是否遵循其他）一致性是否有任何问题？另外，为什么这不是标准库中的定义（我猜这部分是主观的）。

因此，举个例子，我有一个实数，比如说 17.4578，但我想用帕斯卡显示它，点后只有两位数字，所以它是 17.45。我在我的程序中写了什么？

导入 Reals 库

如何定义诸如 3.14 或 10.1 之类的常量并将它们用于函数定义或计算？

我在 mathcomp/SSreflect 上安装了 Coquelicot。

即使我还没有掌握标准 Coq，我也想用它进行非常基本的实际分析。

这是我的第一个引理：

is_derive f x0 f'是一个 Coquelicot Prop，它声明了 function 的导数f at x0 is f'。

auto_derive由于Coquelicot 提供的策略，我已经证明了这个引理。

如果我想让我的手有点脏，这是我没有的尝试auto_derive：

现在我被这个悬而未决的判断困住了：

我该如何解决？

编辑：

如果我打电话ring，我会得到：

如果我展开一个，我会得到：

我不太确定 Java 时期的正确正则表达式是什么。以下是我的一些尝试。可悲的是，它们都意味着任何角色。

但我想要的是实际的“。” 性格本身。有人有想法吗？

我实际上要做的是为非负实数（允许小数）写出正则表达式。所以可能性是：12.2, 3.7, 2., 0.3, .89, 19

最后一行应该打印 false 但无论如何打印 true。我认为我的正则表达式是错误的。

我目前正在从事一个 ML 小型项目并学习如何使用它，但这里有一些我面临的问题，但在网上找不到任何来源。

我想要一个函数来返回列表的最后一个数字，这是一个实数列表。我写了一个代码来返回一个单元素实数列表，但我希望它是一个实数而不是一个列表。这是我的代码：

我想

将有助于获得真实数字，但它只会给我一个错误：

谢谢！

在 Coq 中，我们可以通过定义如下lim类型的函数来形式化定义在 R 上的函数极限的概念：(R -> R) -> R -> R -> Prop

然后我们可以证明极限是唯一的：

但是在数学中，我们通常使用等号来写限制，例如“lim x->cf(x) = L”。这是因为限制的唯一性，所以 = 是等价关系的性质与我们在符号“lim x->cf(x) = L”中引入的 = 的这个新的隐式定义的含义兼容。

是否可以在 Coq 中以这种方式定义限制？更具体地说，我们可以定义一个函数lim2类型(R -> R) -> R -> R，使得lim2 f c = L当且仅当lim f c L？

我用python写了这个函数：

如果我写float(x)或有什么区别int(x)吗？或者+ 1在某些情况下部分有用吗？

编辑：is_number_like将True在传递字符串时返回 - 这是我不想成为的。我想要一个函数，只要将False类似文本的值作为参数传递，它就会返回。有办法吗？

也许：

会更好？

或者可能：

我想编写一个模块，它可以接受任何表现良好的数字类型，它代表一维实数（例如SimpleITK.sitkUInt8数字类型numpy.int32等等......）。

恐怕可能有库，在转换为 int 或 float 时不会出错。例如我可以想象这样的情况：

这可能吗，我应该担心这种情况吗？

并且所有设计良好的实数类型都将转换为float没有错误吗？

附言。我已经读过这个： 如何检查字符串是否为数字（浮点数）？

我在读一本书（CSAPP）。书中写道——

浮点加法满足以下单调性属性：
if a>=bthen(x + a) >= (x+b)对于任何值a，b并且x除了NaN. 无符号或二进制补码加法不遵守实数（和整数）加法的这一特性。

浮点如何服从它？
为什么无符号或二进制补码加法不遵守它？