Неявное определение предела функции в Coq

В Coq мы можем формализовать понятие предела функции, определенной на R, определив функцию lim типа (R -> R) -> R -> R -> Prop следующим образом:

Require Import Coq.Reals.Reals.
Open Scope R.

Definition lim (f : R -> R) (c : R) (L : R) :=
  forall (eps : R), 0 < eps -> exists (del : R), 0 < del /\
  (forall (x : R), 0 < R_dist x c < del -> R_dist (f x) L < eps).

Затем мы можем доказать, что предел уникален:

Theorem lim_unique (f : R -> R) (c : R) (L M : R) :
  lim f c L -> lim f c M -> L = M.

Однако в математике мы обычно пишем ограничения, используя знак равенства, например «lim x->c f(x) = L». Это работает из-за уникальности пределов, поэтому свойство = быть отношением эквивалентности совместимо с этим новым неявно определенным значением =, которое мы вводим в обозначении «lim x-> c f (x) = L».

Можно ли таким образом определить ограничения в Coq? Точнее, можем ли мы определить функцию lim2 типа (R -> R) -> R -> R, такую, что lim2 f c = L тогда и только тогда, когда lim f c L?


math definition coq real-number
person Ben    schedule 11.06.2017    source источник
comment
Конечно, вы можете, даже если вам нужно использовать для этого аксиому, но на самом деле это не имеет значения, поскольку Coq Reals фактически уже использует аксиому. Самый удобный способ — определить ограничения для работы над расширенной реальной линией, то есть R \cup {-inf, +inf} ; Я рекомендую вам взглянуть на библиотеку Coquelicot Coq и документы, в которых эта работа фактически выполняется. [Я мог бы опубликовать решение здесь, но это было бы просто копирование и вставка из этой библиотеки]   -  person ejgallego    schedule 11.06.2017
comment
См., в частности, ограничения и преемственность в coquelicot.saclay.inria.fr/html/Coquelicot. .Coquelicot.html   -  person ejgallego    schedule 11.06.2017
comment
@ejgallego Пожалуйста, опубликуйте! Это будет способствовать развитию экосистемы Coq и снизит входной барьер для всех!   -  person Anton Trunov    schedule 11.06.2017
comment
@ejgallego, так что в конечном итоге определение зависит от LimSup_seq, которое зависит от sig_proj1, которое зависит от sig. Хотя я не уверен, что понимаю, что делает sig. Определение говорит, что {x : T | P x} имеет тип Prop, но что означает, что этот объект является истинным? Означает ли это, что множество непусто? При чем тут единственность предела в этом определении?   -  person Ben    schedule 11.06.2017
comment
@Ben Возможно, этот вопрос может помочь с sig_proj1 и sig.   -  person Anton Trunov    schedule 11.06.2017
comment
{r : R | lim f r} обычно читается, так как существует r такое, что является пределом для f.   -  person ejgallego    schedule 12.06.2017
comment
@Ben, здесь немного больше пояснений о том, как вы переходите от своего первого определения предела к функциональному: грубо говоря, вы сначала проверяете, доказуемо ли exists L, lim f c L или нет. Это требует исключенного третьего. Предположим, что предел существует, тогда вы можете использовать принцип выбора, чтобы получить свидетеля, мы в порядке. Теперь во втором случае предела не существует, тогда мы возвращаем 0, или число пи, или любое другое произвольное значение! Нам все равно, поскольку функция имеет смысл только тогда, когда существует предел. На самом деле вы могли бы заставить функцию limit возвращать тип опции, но это делает ее использование более громоздким.   -  person ejgallego    schedule 12.06.2017