如何解决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).
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。