Блог

Я хочу повторно представить точное значение дифференциального исчисления в Coq, а не приближение.

Я определил, что индуктивный тип представляет собой дифференцирование действительного числа, как вы можете видеть ниже.

 Require Import Coq.Reals.Reals.

Inductive myR:=
| mR : R -> myR 
| Diff : myR -> myR.
  

Это не интересно.
Вы знаете лучший способ?

В стандартной библиотеке есть модуль Reals.Rderiv, который определяет производное отношение D_in так, что функция f : R -> R имеет производную d : R -> R в x0 , если предел (f(x) - f(x0)) / (x - x0) as x переходит в x0 равно d x0 (и все ограничено D подмножеством R домена).

Это в значительной степени стандартное определение, которое я изучил в своем первом курсе исчисления, и, в частности, использование предела гарантирует, что вы получите точную производную.

В Coquelicot , Derive определяется как

 Definition Derive (f : R → R) (x : R) := real (Lim (fun h ⇒ (f (x h) - f x)/h) 0).