如何解决在Coq上使用Coqelicot进行偏微分
我想部分区分那些期望n个参数代表任意自然数n的函数。我希望仅将任意一个论点区分开，而不是其他。
Require Import Reals.
Open Scope R_scope.
Definition myFunc (x y z:R) :R:=
x^2 + y^3 + z^4.
用y区分3*(y^2)时，我期望函数myFunc。
我在partial_derive中认识Coquelicot。
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的参数名称。
请告诉我如何部分区分具有任意数量参数的函数。
解决方法
对于函数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。
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。