How do I write a summation on Coq?

Using Coq
,
1

I have just started getting acquainted with Coq and I would like to write this sum on it:

\sum_{p=1}^{n} \frac{\mathrm{d}^p}{\mathrm{d}x^p} f(x)

This is what I have tried:

Require Import Coquelicot.Coquelicot.

Require Import Coq.Sets.Finite_sets.

Require Import Coq.Reals.Reals.

Section test.

Local Open Scope R_scope.

Variable f : R -> R.

Definition f_p (m : nat)(x : R) := Derive_n f m x.

Local Open Scope nat_scope.

Definition summation_range (n : nat) := sum (fin_range n)(fun p => (Derive_n p f)).

The summation_range definition yields an error “The reference fin_range was not found
in the current environment”. Even though I have just imported the package Require Import Coq.Sets.Finite_sets., which should have fin_range on it (according to ChatGPT).

What is the proper way to write it?

2

ChatGTP outputs things that may look right, but it makes things up which may be completely false.

Just looking at lemmas like this one maybe something like this might work:

fun x => (sum_n (fun p => f_p p x) n)
1 Like
3

Since the sum is supposed to start at 1, sum_m_n (fun p => f_p p x) 1 n is presumably a better choice.