W jaki sposób zdefiniowano "mniej niż" dla liczb rzeczywistych w Coq?

Question

Zastanawiam się, jak definiuje się "mniej niż" dla liczb rzeczywistych.

I zrozumieć, że dla liczb naturalnych (nat) < można zdefiniować rekurencyjnie w zakresie jednego numeru będących (1+) następca S innej liczby. Słyszałem, że wiele rzeczy o liczbach rzeczywistych jest aksjomatycznych w Coq i nie są obliczane.

Ale zastanawiam się, czy istnieje minimalny zestaw aksjomatów dla liczb rzeczywistych w Coq, na podstawie którego można uzyskać inne właściwości/relacje. (Np Coq.Reals.RIneq głosi, że Rplus_0_r : forall r, r + 0 = r. jest aksjomatem, między innymi)

W szczególności jestem zainteresowany, czy związki takie jak < lub <= mogą być definiowane w górnej części relacji równości. Na przykład, można sobie wyobrazić, że w konwencjonalnym matematyki, podane dwa numery r1 r2:

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

Ale czy to trzymać w konstruktywną logiką Coq? Czy mogę tego użyć, aby przynajmniej przeprowadzić jakieś rozumowanie na temat nierówności (zamiast przepisywania aksjomatów przez cały czas)?

Answer 1

Coq.Reals.RIneq ma to, że Rplus_0_r: forall r, r + 0 = r. Jest to aksjomat, m.in.

nitpick: Rplus_0_r nie jest aksjomatem ale Rplus_0_l jest. Możesz uzyskać ich listę w module Coq.Reals.Raxioms oraz listę parametrów używanych w Coq.Reals.Rdefinitions.

Jak widać "większy niż (lub równy)" i "mniejszy niż lub równy" wszystkie są zdefiniowane w terminach "mniej niż", co jest postulowane, a nie wprowadzane przy użyciu zaproponowanej propozycji.

Wygląda na to, że Rlt może być zdefiniowany w sposób, który sugerujesz: dwie propozycje są w przybliżeniu równoważne, jak pokazano poniżej.

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. 

Jednak będzie trzeba jeszcze zdefiniować, co to znaczy być „ściśle pozytywny” dla s > 0 odrobiną sensu i nie jest wcale oczywiste, że chcesz mieć mniej aksjomaty w końcu (na przykład pojęcie bycia ściśle pozytywnym powinno zostać zamknięte przy dodawaniu, mnożeniu itp.).

Answer 2

Rzeczywiście, biblioteka Coq.Real jest nieco słaba w tym sensie, że jest całkowicie określona jako aksjomaty, a w niektórych (krótkich) punktach w przeszłości była nawet niespójna.

Definicja le jest więc nieco "ad hoc" w tym sensie, że z punktu widzenia systemu niesie zero zerowego znaczenia obliczeniowego, będąc jedynie stałą i kilkoma aksjomatami. Możesz dodać aksjomat "x < x", a Coq nie może zrobić nic, aby to wykryć.

Warto zwrócić do niektórych alternatywnych konstrukcji liczb rzeczywistych dla Coq:

Mój ulubiony klasyczny konstrukcja jest zrobione w jednym z czterech kolorów twierdzenia Georges Gonthier i B. Werner: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

To tylko wykorzystuje wykluczony aksjomat środkowy (głównie w celu porównania liczb rzeczywistych), więc pewność jego spójności jest bardzo wysoka.

Najbardziej znaną aksjologiczną charakterystyką reali jest projekt C-CORN, http://corn.cs.ru.nl/, ale zdajemy sobie sprawę, że analiza konstruktywna znacznie różni się od zwykłej.