Existe algum trabalho para criar uma Estrutura de Teoria de Número Real / Probabilidade no COQ?

O COQ é um provador de teoremas interativo que usa o cálculo de construções indutivas, ou seja, depende muito de tipos indutivos. Usando isso, estruturas discretas como números naturais, números racionais, gráficos, gramáticas, semânticas etc. são representadas de forma muito concisa.

No entanto, como passei a gostar do assistente de provas, fiquei pensando se existem bibliotecas para estruturas incontáveis, como números reais, números complexos, limites de probabilidade e outros. É claro que sei que não se pode definir indutivamente essas estruturas (pelo menos não tanto quanto eu sei), mas elas podem ser definidas axiomaticamente, usando, por exemplo, a abordagem axiomática .

Existe algum trabalho que forneça propriedades básicas, ou mesmo limites probabilísticos, como Chernoff bound ou union bound como uma biblioteca?

A biblioteca padrão da Coq possui uma seção sobre números reais. Estes são os números reais clássicos, usando a conclusão do Dedekind . Também existem resultados sobre números complexos, suponho que existam várias bibliotecas, conheço esta . Observe que também há muitos resultados para números construtivos reais e complexos, o C-CoRN é a referência.

Nota lateral: você também pode definir números reais (computáveis) indutivamente com alguns dos axiomatics construtivos, por exemplo, usando números racionais das seqüências de Cauchy ou alguma versão construtiva da propriedade com limite mínimo superior. Não tenho certeza de quanto isso é indutivo.

Eu sei que existem algumas pessoas trabalhando em probabilidades com o Coq. Infelizmente, não tenho certeza de quão avançados são seus trabalhos. Meu palpite é que provavelmente não há resultado específico sobre o limite de Chernoff ou o limite de união. (Mas é apenas um palpite)

Veja isso! http://coq.io/opam/coq-markov.8.5.0.html . Uma biblioteca para a desigualdade de Markov baseada na teoria da probabilidade matemática.