在Coq上使用Coqelicot进行偏微分
在Coq上使用Coqelicot进行偏微分
提问于 2020-09-15 20:39:06
我想对任意自然数n的n个变元的函数进行部分微分，我希望对任意一个变元只微分一次，而不是对其他的。
Require Import Reals.
Open Scope R_scope.
Definition myFunc (x y z:R) :R:=
x^2 + y^3 + z^4.当我区分myFunc和y时，我期望函数为3*(y^2)。
我在Coquelicot认识partial_derive。
Definition partial_derive (m k : nat) (f : R → R → R) : R → R → R :=
fun x y ⇒ Derive_n (fun t ⇒ Derive_n (fun z ⇒ f t z) k y) m x.partial_derive可以部分区分f:R → R → R，但对于任意数量的参数是不可能的。
我考虑过使用依赖类型listR。
Inductive listR :nat -> Type:=
|RO : Euc 0
|Rn : forall {n}, R -> listR n -> listR (S n).
Notation "[ ]" := RO.
Notation "[ r1 , .. , r2 ]" := (Rn r1 .. ( Rn r2 RO ) .. ).
Infix ":::" := Rn (at level 60, right associativity).
Fixpoint partial_derive_nth {n} (k:nat) (f : listR n -> R) (e:listR n): listR n -> R:=k指定要区分的参数编号。我们不能像partial_derive一样定义partial_derive_nth，因为我们不能在递归中指定fun的参数名称。
请告诉我如何部分区分具有任意数目参数的函数。
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-09-17 15:55:26
对于你的函数myFunc，你可以这样写偏导数：
Definition pdiv2_myFunc (x y z : R) :=
Derive (fun y => myFunc x y z) y.然后，您可以证明对于x、y和z中的任何选项，它都具有您期望的值。多亏了Coquelicot中提供的策略，大多数证明都可以自动完成。
Lemma pdiv2_myFunc_value (x y z : R) :
pdiv2_myFunc x y z = 3 * y ^ 2.
Proof.
unfold pdiv2_myFunc, myFunc.
apply is_derive_unique.
auto_derive; auto; ring.
Qed.我有点惊讶，自动策略auto_derive不能处理Derive _ _ = _形式的目标，所以我必须自己应用定理is_derive_unique。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/63902038
复制相关文章
相似问题
腾讯云开发者
