# How do I write a summation on Coq?

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?

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

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.