Coq上的微积分

问题描述

我想代表Coq上的微积分的确切值，而不是近似值。

我定义了归纳类型，代表实数的微分，如下所示。

Require Import Coq.Reals.Reals.

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

这没意思。 你知道更好的方法吗？

解决方法

在标准库中，模块Reals.Rderiv定义了导数关系D_in，即函数f : R -> R在{{1}处具有导数d : R -> R }，如果x0到(f(x) - f(x0)) / (x - x0)的限制为x（并且所有内容都限于x0的域d x0子集）。

这几乎是我在第一个微积分课程中学到的标准定义，特别是，采用极限可以确保您获得精确的导数。

,

在Coquelicot中，Derive is defined为

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