Блог

Я хочу представить точное значение производной. Я могу рассчитать приближение, подобное этому.

 Require Import Coq.Reals.Reals.
Open Scope R_scope.

Definition QuadraticFunction (x:R) := x^2.

Definition differentiation (x:R)(I:R -> R):=
 let h := 0.000000001 in
 ((I (x h)) - (I x)) / h.
  

Но мы не можем вычислить точное значение производной на компьютере.
По этой причине я хочу каким-то образом представить точное значение с помощью индуктивного типа или других.

Я знаю D_in реалов.Rderiv, который возвращает Prop.

Мне нужна ваша помощь. Спасибо.

Мне нужно сделать четыре замечания

• Вам следует взглянуть на coquelicot, это библиотека расширений поверх Reals, которая лучше обрабатывает производные.

• В представлении действительных чисел нет индуктивного типа. Фактически, это часть теоретического фольклора, что действительные числа не могут быть представлены как индуктивный тип в том смысле, который мы обычно подразумеваем. В индуктивном типе вы обычно можете сравнить два элемента с помощью конечного вычисления. В действительных числах такое сравнение сталкивается с трудностью, заключающейся в том, что некоторые числа определяются процессом бесконечного уточнения. Одна из основ действительных чисел заключается в том, что набор является полным, что означает, что каждая последовательность Коши имеет предел. Это часто используется как способ определения новых действительных чисел.

• что значит вычислить число? Как вы вычисляете PI (отношение окружностей). Вы не можете вернуть 3.14, потому что это не точное значение. Итак, вам нужно сохранить PI в качестве результата. Но почему PI должно быть лучше, чем (4 * atan(1)) или lim(4 — 4/3 4/5 — 4/7 …)? Таким образом, вы не вычисляете действительные числа, как вы бы делали с карманными калькуляторами, потому что вам нужно сохранять точность. Лучшее, что вы можете сделать, это вернуть точное представление в виде рационального значения, когда действительное число рационально, «понятное символическое выражение» или интервальное приближение. Но интервальные аппроксимации не являются точными, и понятное символическое выражение является неоднозначной спецификацией. Как вы выбираете, какое выражение является наиболее понятным?

• Не существует функции, которая принимает произвольную функцию и возвращает ее производную в точке в виде действительного числа, потому что мы должны учитывать, что некоторые функции выводимы не везде. В Reals библиотеке есть функция, которая позволяет говорить о значении производной для производной функции. Это называется derive .

Вот скрипт, который выполняет весь процесс.

 Require Import Coq.Reals.Reals.

Require Import Coq.Reals.Reals.
 Open Scope R_scope.

Definition QuadraticFunction (x:R) := x^2.

Lemma derivable_qf : derivable QuadraticFunction.
Proof.
now repeat apply derivable_mu<
    (apply derivable_id || apply derivable_const).
Qed.

Definition QuadraticFunctionDerivative :=
  derive QuadraticFunction derivable_qf.
  

Теперь у вас есть имя для производной функции, и вы даже можете показать, что оно равно другой простой функции. Но является ли эта другая простая функция результатом вычисления производной, является субъективным. Вот пример, использующий только библиотеку Reals, но использование Coquelicot дало бы гораздо более краткий сценарий (поскольку вычисление производной может быть автоматизировано, заинтересованным читателям также следует взглянуть на ответ @larsr на тот же вопрос).

 Lemma QuadraticFunctionDerivativeSimple (x : R) :
  QuadraticFunctionDerivative x = 2 * x.
Proof.
unfold QuadraticFunctionDerivative, derive, QuadraticFunction; simpl.
rewrite derive_pt_eq.
replace (2 * x) with (1 * (x * 1)   x * (1 * 1   x * 0)) by ring.
apply (derivable_pt_lim_mult (fun x => x) (fun x => x * 1)).
  apply derivable_pt_lim_id.
apply (derivable_pt_lim_mult (fun x => x) (fun x => 1)).
  apply derivable_pt_lim_id.
apply derivable_pt_lim_const.
Qed.
  

Вероятно, это не лучший способ решения проблемы, но это тот, который я придумал, подумав о проблеме в течение нескольких минут.

Я рекомендую вдумчивый ответ @ Yves, а также хочу порекомендовать Coquelicot из-за его очень удобочитаемой формализации реального анализа.

У Коклико есть теорема для производной от (f x) ^ n , а в вашем случае f = id (функция идентификации) и n = 2 , поэтому, используя теорему Коклико, вы могли бы доказать свою лемму следующим образом:

 From Coquelicot Require Import Coquelicot.
Require Import Reals.
Open Scope R.

Goal  forall x, is_derive (fun x => x^2) x (2*x).
  intros x.
  evar (e:R). replace (2*x) with e.
  apply is_derive_pow.
  apply is_derive_id.
  unfold e, one. simpl. ring.
Qed.
  

Коклико отделяет доказательство того, что производная существует ( is_derive ), от функции ( Derive ), которая «вычисляет» производную, и имеет теорему, показывающую, что Derive дает правильный ответ , если производная существует.

 is_derive_unique: is_derive f x l -> Derive f x = l
  

Это значительно упрощает работу с производными в выражениях с rewrite тем, что использует формулировку в стандартной библиотеке. Просто выполните перезапись, и доказательства того, что производная действительно существует, окажутся побочными условиями.

(Обратите внимание, что я использовал evar s выше. Это полезно сделать, если вы хотите иметь возможность применять теорему, но выражения не «очевидно» (т. Е. вычислительно) равны Coq. Я по аналогичным причинам считаю полезным делать eapply is_derive_ext перезаписи внутри функции, над которой выполняется работа. Просто подсказка …)

Кроме того, у Coquelicot есть несколько полезных тактик, которые могут автоматизировать некоторые рассуждения. Например:

 Lemma Derive_x3_plus_cos x: Derive (fun x => x^3   cos x) x =  3*(x^2) - sin x.
  apply is_derive_unique.
  auto_derive; auto; ring.
Qed.