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.