¿Existe algún trabajo en la creación de un número real / Probabilidad marco de la Teoría de COQ?

Question

COQ es un demostrador de teoremas interactiva que utiliza el cálculo de construcciones inductivas, es decir, que depende en gran medida de los tipos inductivos. El uso de los, estructuras discretas como números naturales, números racionales, gráficos, gramáticas, semántica etc., están muy concisa representaba.

Sin embargo, ya que crecí a como el asistente prueba, me preguntaba si hay bibliotecas para estructuras incontables, como números reales, números complejos, límites de probabilidad y tal. Por supuesto, soy consciente de que no se puede definir estas estructuras inductivamente (al menos no por lo que yo sé), pero se puede definir axiomáticamente, utilizando por ejemplo el enfoque axiomático .

¿Hay alguna obra que proporciona propiedades básicas, o incluso los límites probabilísticos como Chernoff unido o unión obligado como una biblioteca?

Answer 1

La biblioteca estándar de Coq tiene una sección sobre los números reales. Estos son los números reales clásicos, utilizando el Dedekind finalización . También hay resultados acerca de los números complejos, supongo que hay varias bibliotecas, me he enterado de éste . Tenga en cuenta que también hay una gran cantidad de resultados para constructiva los números reales y complejos, C-Corn es la referencia.

Nota al margen: que podría también definir (computable) números reales inductivamente con algunos de los axiomas constructivas, por ejemplo usando números racionales de las secuencias de Cauchy o alguna versión constructiva de los menos del límite superior, propiedad. No estoy seguro de cuánto inductiva que esta.

Sé que hay algunos las personas que trabajan en las probabilidades con Coq. Por desgracia, no estoy seguro de lo avanzado que las obras de ellos. Mi conjetura es que no es probable que tal resultado específico sobre Chernoff ligado o unión obligado. (Pero es sólo una suposición)

Answer 2

Mira esto! http://coq.io/opam/coq-markov.8.5.0. html . Una biblioteca para la desigualdad de Markov basa en la teoría de la probabilidad matemática.