Partial differentiation using Coqelicot on Coq

Question

I want to partially differentiate functions which expects n arguments for arbitrary natural number n. I hope to differentiate arbitrary an argument only once and not the others.

Require Import Reals.
Open Scope R_scope.

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

I expect function 3*(y^2) when I differentiate myFunc with y.

I know partial_derive in 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 can partially differentiate f:R → R → R, but not possible for arbitrary number of arguments.

I thought about using dependent type 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 specifies argument number to differentiate. We can not define partial_derive_nth like partial_derive because we can not specify the name of arguments of fun in recursion.

Please tell me how to partially differentiate functions which has arbitrary number of arguments.

Answer 1

For your function myFunc, you can write the partial derivative like so:

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

You can then prove that it has the value you expect for any choice of x, y, and z. Most of the proof can be done automatically, thanks to the tactics provided in 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.

I am a bit surprised that the automatic tactic auto_derive does not handle a goal of the form Derive _ _ = _, so I have to apply theorem is_derive_unique myself.