Existe-t-il des travaux sur la création d'un cadre de théorie des nombres réels / probabilités dans COQ?

COQ est un prouveur de théorème interactif qui utilise le calcul des constructions inductives, c'est-à-dire qu'il s'appuie fortement sur les types inductifs. En utilisant celles-ci, les structures discrètes comme les nombres naturels, les nombres rationnels, les graphiques, les grammaires, la sémantique, etc. sont représentées de manière très concise.

Cependant, depuis que j'ai appris à aimer l'assistant de preuve, je me demandais s'il y avait des bibliothèques pour les structures innombrables, comme les nombres réels, les nombres complexes, les bornes de probabilité et autres. Je suis bien sûr conscient que l'on ne peut pas définir ces structures par induction (du moins pas pour autant que je sache), mais elles peuvent être définies de manière axiomatique, en utilisant par exemple l' approche axiomatique .

Existe-t-il des travaux qui fournissent des propriétés de base, ou même des limites probabilistes comme Chernoff lié ou union lié comme bibliothèque?

La bibliothèque standard de Coq a une section sur les nombres réels. Ce sont les nombres réels classiques, en utilisant la complétion Dedekind . Il y a aussi des résultats sur les nombres complexes, je suppose qu'il y a plusieurs bibliothèques, je connais celle-ci . Notez qu'il y a aussi beaucoup de résultats pour les nombres réels et complexes constructifs , C-CoRN est la référence.

Note latérale: vous pouvez également définir des nombres réels (calculables) par induction avec certaines des axiomatiques constructives, par exemple en utilisant des nombres rationnels des séquences de Cauchy ou une version constructive de la propriété de la borne inférieure. Je ne sais pas combien inductive que cela.

Je sais qu'il y a des gens qui travaillent sur les probabilités avec Coq. Malheureusement, je ne sais pas à quel point leurs travaux sont avancés. Je suppose qu'il n'y a probablement pas de résultat aussi précis concernant Chernoff lié ou lié à l'union. (Mais c'est juste une supposition)

Regarde ça! http://coq.io/opam/coq-markov.8.5.0.html . Une bibliothèque pour l'inégalité de Markov basée sur la théorie mathématique des probabilités.