Comment "inférieur à" est-il défini pour les nombres réels dans Coq?

Question

Je me demande simplement comment est définie la relation «inférieur à» pour les nombres réels.

Je comprends que pour les nombres naturels (nat), < peut être défini de manière récursive en termes d'un nombre étant le successeur (1+) S d'un autre numéro. J'ai entendu dire que beaucoup de choses sur les nombres réels sont axiomatiques dans Coq et ne calculent pas. Mais je me demande s'il existe un ensemble minimum d'axiomes pour les nombres réels dans Coq sur la base duquel d'autres propriétés/relations peuvent être dérivées. (Par exemple Coq.Reals.RIneq a ce que Rplus_0_r : forall r, r + 0 = r. est un axiome, entre autres)

En particulier, je suis intéressé à savoir si les relations telles que < ou <= peuvent être définies au-dessus de la relation d'égalité. Par exemple, je peux imaginer que dans les mathématiques classiques, compte tenu de deux nombres r1 r2:

r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2. 

Mais cette attente dans la logique constructive de Coq? Et puis-je utiliser cela pour au moins faire un raisonnement sur les inégalités (au lieu de réécrire des axiomes tout le temps)?

Answer 1

Coq.Reals.RIneq veut que Rplus_0_r: pour tout r, r + 0 = r. est un axiome, entre autres

pinailler: Rplus_0_r n'est pas un axiome, mais Rplus_0_l est. Vous pouvez en obtenir une liste dans le module Coq.Reals.Raxioms et une liste des paramètres utilisés dans Coq.Reals.Rdefinitions. Comme vous pouvez le voir, «supérieur à (ou égal)» et «inférieur ou égal» sont tous définis en termes de «inférieur à», ce qui est postulé plutôt qu'introduit en utilisant la proposition que vous suggérez.

On dirait que Rlt pourrait en effet être défini de la manière que vous suggérez: les deux propositions sont prouvablement équivalentes comme indiqué ci-dessous.

Require Import Reals. 
Require Import Psatz. 
Open Scope R_scope. 

Goal forall (r1 r2 : R), r1 < r2 <-> exists s, s > 0 /\ r1 + s = r2. 
Proof. 
intros r1 r2; split. 
- intros H; exists (r2 - r1); split; [lra | ring]. 
- intros [s [s_pos eq]]; lra. 
Qed. 

Cependant, vous aurez encore besoin de définir ce que signifie être « strictement positif » pour le bit s > 0 pour donner un sens et ce n'est pas du tout clair que vous auriez moins axiomes à la fin (par exemple, la notion d'être strictement positif devrait être fermé sous addition, multiplication, etc.).

Answer 2

En effet, la bibliothèque Coq.Real est un peu faible dans le sens où elle est totalement spécifiée comme axiomes, et à certains points (brefs) dans le passé, elle était même inconsistante. Donc la définition de le est un peu "ad hoc" en ce sens que du point de vue du système il porte une signification computationnelle nulle, étant juste une constante et quelques axiomes. Vous pourriez bien ajouter l'axiome "x < x" et Coq ne pouvait rien faire pour le détecter.

Il convient de souligner certaines constructions alternatives des Reals pour Coq:

Ma construction classique préférée est celle faite dans les quatre couleurs théorème de Georges Gonthier et B. Werner: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

Il ne utilise l'axiome moyen exclu (principalement pour comparer les nombres réels) de sorte que la confiance dans sa cohérence est très élevée.

La caractérisation sans axiomes la plus connue des réels est le projet C-CORN, http://corn.cs.ru.nl/ mais nous savons que l'analyse constructive diffère significativement de l'analyse habituelle.