如何爲Coq中的實數定義「小於」？

我理解，對於自然數（nat）<可以遞歸在爲另一數目的（1+）後繼S一個數來定義的。我聽說很多關於實數的事情在Coq中是公理的，並且不計算。

但我想知道在Coq中是否存在一個最小公理集合的實數，基於哪些其他屬性/關係可以派生出來。（例如有它Rplus_0_r : forall r, r + 0 = r.是一個公理，等等）

特別地，我對是否如<或<=的關係可以在平等關係的頂部限定。例如，我可以想像，在傳統的數學運算，給出了兩個數字r1 r2：

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

但在勒柯克的建設性的邏輯做到這一點不放？我能用這個來至少對不平等的一些推理（而不是總是重寫公理）嗎？

來源

2015-12-21 tinlyx

Coq.Reals.RIneq表示Rplus_0_r：forall r，r + 0 = r。是一個公理，等等

雞蛋裏挑骨頭：Rplus_0_r不是一個公理，但Rplus_0_l是。您可以在模塊Coq.Reals.Raxioms中獲得它們的列表以及在Coq.Reals.Rdefinitions中使用的參數列表。正如你所看到的「大於（或等於）」和「小於或等於」都是用「小於」來定義的，這是假設的，而不是用你提出的建議引入的。

它看起來像Rlt的確可以用你所建議的方式來定義：這兩個命題可以證明是等價的，如下所示。

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.

但是你仍然需要定義它的意思是「嚴格爲正」，爲s > 0位纔有意義，它不是完全清楚你有更少的公理到底（如概念嚴格肯定的應該在加法，乘法等情況下關閉）。

來源

2015-12-21 19:50:52 gallais

事實上，Coq.Real庫在它完全被指定爲公理的意義上有點弱，並且在過去的一些（簡短）點甚至是不一致的。

因此，從系統的角度來看，le的定義有點「特設」，它具有零計算意義，僅僅是一個常數和幾個公理。你可以加上公理「x < x」，Coq無法檢測到它。

值得指出的雷亞爾的勒柯克的一些替代結構：

我最喜歡的古典建築是一個由喬治斯·戈西爾和B.沃納在四個色定理做：http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

它只使用排除的中間公理（主要用於比較實數），因此對其一致性的信心非常高。

實數最有名的無公理描述是C-CORN項目http://corn.cs.ru.nl/，但我們知道建設性分析與通常的顯着不同。

來源

2016-01-28 01:08:20 ejgallego

如何爲Coq中的實數定義「小於」？

回答

相關問題