在COQ中创建实际数字/概率理论框架是否存在任何工作？

Question

coq 是使用归纳构造的计算的交互式定理谚语，即它在很大程度上依赖于电感类型。使用这些，诸如自然数，理性数字，图形，语法，语义等等离散结构非常简洁。

但是，由于我越来越喜欢证明助手，所以我想知道是否有无数结构的库，例如实数，复数数字，概率范围等。我当然知道，一个人不能归纳定义这些结构（至少据我所知），但是可以公理地定义它们，例如 公理方法.

是否有任何可提供基本属性，甚至提供概率界限的工作，例如Chernoff Bond Bond或Union Bonding作为图书馆？

Answer 1

这 标准库 COQ的一部分有关于实数的部分。这些是经典的实数，使用 Dedekind完成. 。关于复数的结果，我想有几个库，我碰巧知道 这个. 。请注意，还有很多结果 建设性 真实和复杂数字， c-corn 是参考。

旁注：你 可以 还可以用一些建设性的公理学来定义（可计算）实数，例如，使用凯奇序列中的有理数或某些最不可能结合的属性的建设性版本。我不确定这有多少归纳。

我知道有 一些 与COQ一起从事概率的人。不幸的是，我不确定他们的作品有多高。我的猜测是，Chernoff Bound或Union Bound可能没有这种具体结果。 （但这只是一个猜测）

Answer 2

看一下这个！ http://coq.io/opam/coq-markov.8.5.0.html. 。马尔可夫不平等的图书馆基于数学概率理论。