Wie ist "weniger als" für reelle Zahlen in Coq definiert?

Question

Ich frage mich nur, wie ist die „weniger als“ Beziehung für reelle Zahlen definiert.

Ich verstehe, dass für natürliche Zahlen (nat) können < rekursiv in Bezug auf eine Zahl festgelegt werden, dass die (1+) Nachfolger S einer anderen Zahl. Ich habe gehört, dass viele Dinge über reelle Zahlen in Coq axiomatisch sind und nicht berechnen.

Aber ich frage mich, ob es eine minimale Menge von Axiomen für reelle Zahlen in Coq ist basierend auf der anderen Eigenschaften/Beziehungen abgeleitet werden können. (Z Coq.Reals.RIneq hat es, dass Rplus_0_r : forall r, r + 0 = r. ein Axiom ist, ua)

Insbesondere Ich bin daran interessiert, ob die Beziehungen wie < oder <= können auf der Gleichheitsbeziehung definiert werden. Zum Beispiel kann ich das in herkömmlicher Mathematik vorstellen, da zwei Zahlen r1 r2:

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

Aber tue dies Halt in der konstruktiven Logik der Coq? Und kann ich diese verwenden, um zumindest tun einige Überlegungen über Ungleichheiten (statt Neuschreiben Axiome die ganze Zeit)?

Answer 1

Coq.Reals.RNeq hat es, dass Rplus_0_r: forall r, r + 0 = r. unter anderem ist ein Axiom,

Nitpick: Rplus_0_r kein Axiom ist aber Rplus_0_l ist. Sie können in Coq.Reals.Rdefinitions eine Liste von ihnen in dem Modul Coq.Reals.Raxioms und eine Liste der verwendeten Parameter erhalten.

Wie Sie sehen können "größer als (oder gleich)" und "kleiner als oder gleich" sind alle definiert als "weniger als", was eher postuliert als eingeführt wird unter Verwendung des Vorschlags, den Sie vorschlagen.

Es sieht aus wie Rlt zwar in der Art und Weise definiert werden könnten Sie vorschlagen: Die beiden Sätze sind beweisbar äquivalent wie unten gezeigt.

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. 

Allerdings würden Sie noch definieren müssen, was es bedeutet, „streng positiv“ für die s > 0 Bit zu sein Sinn zu machen und es ist nicht klar, dass Sie weniger Axiome am Ende haben würden (zB des Begriff streng positiv zu sein, sollte unter Addition, Multiplikation usw. geschlossen werden).

Answer 2

Tatsächlich ist die Coq.Real-Bibliothek ein bisschen schwach in dem Sinne, dass sie vollständig als Axiome spezifiziert ist, und zu einigen (kurzen) Punkten in der Vergangenheit war sie sogar inkonsistent.

Also die Definition von le ist ein bisschen "ad hoc" in dem Sinne, dass es aus der Sicht des Systems null Rechenwert, nur eine Konstante und ein paar Axiome trägt. Sie könnten auch das Axiom „x < x“ hinzufügen und Coq nichts, um es zu erkennen, tun könnte.

Es ist zeigen wert auf einige alternativen Konstruktionen des Reals für Coq: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

Es nur:

Meine Lieblinge klassische Konstruktion der in dem Vierfarbensatz von Georges Gonthier und B. Werner getan ist verwendet das ausgeschlossene mittlere Axiom (hauptsächlich um reelle Zahlen zu vergleichen), so dass das Vertrauen in seine Konsistenz sehr hoch ist.

Die bekannteste axiomfreie Charakterisierung der Realen ist das C-CORN-Projekt, http://corn.cs.ru.nl/, aber wir wissen, dass sich die konstruktive Analyse wesentlich von der üblichen unterscheidet.