Coqの実数に対して「より小さい」定義方法は？

Question

私は実数のために定義された関係「未満」であるか疑問に思って。

Iは自然数（nat）ため、<は別の番号の（1+）後継Sであるつの番号の点で再帰的に定義することができることを理解します。実数についての多くのことがCoqでは公理であり、計算しないと聞きました。

しかし、私は他のプロパティ/関係が導出することができるに基づいてCoqので実数のための公理の最小セットがあるかどうかを疑問に思って。特に

（例えば​​がRplus_0_r : forall r, r + 0 = r.は、とりわけ、公理であること、それを持っている）、私は、<又は<=ような関係が平等関係の上に定義することができるかどうかに興味があります。

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

しかし、コックの建設的なロジックで、このホールドを行います。たとえば、私は従来の数学では、二つの数r1 r2を与えられたことを想像できますか？そして、これを使って、少なくとも公理を書き直すのではなく、不等式についての何らかの推論をすることができますか？

Answer 1

Coq.Reals.RIneqには、Rplus_0_r：forall r、r + 0 = rがあります。 Rplus_0_r公理ではなくRplus_0_lは次のとおりです。中でも公理は、

Nitpickです。あなたはモジュールCoq.Reals.RaxiomsとCoq.Reals.Rdefinitionsで使用されるパラメータのリストにそれらのリストを取得することができます。

あなたが「以下」「より大きい（または等しい）」と見ることができるように、すべての面で定義されている仮定ではなく、あなたが提案する提案を使用して導入された「より少ないです」。

Rltは確かにあなたがお勧めの方法で定義することができように見えます：以下のように2つの命題は証明可能同等です。

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ビットのために、「厳密に正」であることの意味を定義する必要があり、それはあなたが最後に少数の公理を持っているだろうとは全く明らかではないのですが（例えば概念厳密に正であることは、加えて、乗算などによって）閉じなければならない。

Answer 2

確かに、Coq.Realライブラリは公理として完全に指定されているという意味で少し弱く、過去のいくつかの（簡潔な）点では矛盾していました。

のでルの定義は、システムの観点から、それだけで定数といくつかの公理であること、ゼロの計算の意味を運ぶという意味でビット「アドホック」です。あなたは公理 "x < x"を追加することができ、Coqはそれを検出するために何もできません。

それはコックのためにレアルのいくつかの代替構造を指している価値がある：

私のお気に入りの古典的な建設がジョージズ・ゴンサーとB.ヴェルナーによって4色定理で行うものです：http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

それだけ（主に実数を比較するために）除外された中間公理を使用するので、その一貫性に対する信頼性は非常に高い。

実例の最も知られていない公理化されていない特徴付けは、C-CORNプロジェクトhttp://corn.cs.ru.nl/ですが、建設的な分析は通常のものと大きく異なります。