Как определяется "меньше чем" для действительных чисел в Coq?
Мне просто интересно, как отношения "меньше чем" определены для действительных чисел.
Я так понимаю для натуральных чисел (nat), < может быть определен рекурсивно с точки зрения одного числа, являющегося (1+) преемник S другого номера. Я слышал, что многие вещи о реальных числах в Coq аксиоматичны и не вычисляются.
Но мне интересно, существует ли минимальный набор аксиом для действительных чисел в Coq, на основе которого могут быть получены другие свойства / отношения. (например, Coq.Reals.RIneq имеет это, что Rplus_0_r : forall r, r + 0 = r. это аксиома, между прочим)
В частности меня интересует, есть ли такие отношения как < или же <= может быть определена поверх отношения равенства. Например, я могу представить, что в обычной математике, учитывая два числа r1 r2:
r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2.
Но верно ли это в конструктивной логике Coq? И могу ли я использовать это, чтобы хотя бы рассуждать о неравенствах (вместо того, чтобы постоянно переписывать аксиомы)?
2 ответа
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 Это имеет смысл, и совсем не ясно, что в итоге у вас будет меньше аксиом (например, понятие строгости положительного следует закрыть при сложении, умножении и т. д.).
Действительно, библиотека Coq.Real немного слаба в том смысле, что она полностью указана как аксиомы, и в некоторых (кратких) моментах в прошлом она была даже противоречивой.
Таким образом, определение le немного "ad hoc" в том смысле, что с точки зрения системы оно имеет нулевой вычислительный смысл, являясь лишь константой и несколькими аксиомами. Вы могли бы легко добавить аксиому "x Стоит указать на некоторые альтернативные конструкции Reals for Coq: Моя любимая классическая конструкция - это те, которые сделаны в теореме о четырех цветах Жоржем Гонтье и Б. Вернером: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/ Он использует только исключенную среднюю аксиому (в основном для сравнения действительных чисел), поэтому уверенность в ее согласованности очень высока. Самая известная характеристика аксиом без аксиом - это проект C-CORN, http://corn.cs.ru.nl/ но мы знаем, что конструктивный анализ значительно отличается от обычного.