如何解决Coq的导数的精确值
我想代表微分的精确值。 我可以这样计算一个近似值。
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.
但是,我们无法在计算机上计算导数的确切值。 因此,我想用归纳类型或其他方式表示确切的值。
我知道Reals.Rderiv的D_in,它返回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_mult;
(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,因为它对Real Analysis的可读性很强。
Coquelicot有一个(f x) ^ n
导数的定理,在您的情况下f = id
(恒等函数)和n = 2
,所以使用Coquelicot定理,您可以证明自己的引理:
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.
Coquelicot将导数存在(is_derive
)的证明与“计算”导数的函数(Derive
)分开,并且有一个定理表明Derive
提供正确的答案如果衍生物存在。
is_derive_unique: is_derive f x l -> Derive f x = l
与标准库中的公式相比,使用rewrite
处理表达式中的导数要容易得多。只要重写一下,导数确实存在的证明就变成了附带条件。
(请注意,我在上面使用了evar
。如果您希望能够应用定理,但表达式“显然”(即在计算上)不等于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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。