coq - 在 Coq 上使用 Coqelicot 进行偏微分

Question

我想部分区分需要 n 个参数的任意自然数 n 的函数。我希望只区分一次任意的论点，而不区分其他论点。

Require Import Reals.
Open Scope R_scope.

Definition myFunc (x y z:R) :R:=
 x^2 + y^3 + z^4.

我期待功能 3*(y^2)当我区分时 myFunc与 y。
我知道 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的参数名称。在递归中。
请告诉我如何部分区分具有任意数量参数的函数。

Answer 1

为您的功能 myFunc ，你可以这样写偏导数:

Definition pdiv2_myFunc (x y z : R) :=
 Derive (fun y => myFunc x y z) y.

然后，您可以证明它具有您对 x 的任何选择所期望的值(value)。 , 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我。