## Stream: Coq users

### Topic: Sum of list excluding given index

#### Dubravka Kutlesic (Oct 26 2021 at 17:30):

Hello, I want to represent sum of real elements (in list l : R) excluding given index i . How can I do that? Thanks

#### Ana de Almeida Borges (Oct 26 2021 at 17:53):

If you wish to use the standard library, one option would be to write a function to drop the ith element of a list using firstn and skipn (see here) and another function to sum all the elements using fold_left (see here).

#### Ana de Almeida Borges (Oct 26 2021 at 17:55):

I actually don't know the standard library that well, there might be better ways.

#### Ana de Almeida Borges (Oct 26 2021 at 18:00):

MathComp's bigop does precisely this sort of thing, you can write something like \sum_(0 <= j < size s | j != i) (nth 0 s j), which reads as "the sum of the j-th elements of s, for j between 0 and the size of s such that j != i" .

#### Dubravka Kutlesic (Oct 26 2021 at 18:46):

Thanks! I tried it and I'm getting the following error:
The term "j" has type "nat" while it is expected to have type"Equality.sort ?T".
which i don't know how to resolve.
What can be a problem?

#### Emilio Jesús Gallego Arias (Oct 26 2021 at 19:01):

Did you import ssrnat ?

#### Dubravka Kutlesic (Oct 26 2021 at 20:03):

I didn't. Importing it solved my issue. Thanks!

#### Emilio Jesús Gallego Arias (Oct 26 2021 at 20:08):

You are welcome! Importing things in Coq do really changes a lot your setup, keep that in mind. When learning / experimenting you may want to do Require Import all_ssreflect etc... after YMMV; I like to have finer grained imports, but that's a bit of a personal choice.

#### Emilio Jesús Gallego Arias (Oct 26 2021 at 20:08):

In this case, importing ssrnat added the eqType instance for nat

#### Dubravka Kutlesic (Oct 27 2021 at 10:17):

I am still confused how to sum reals, in bigop is written that \sum is overloaded for R in ssralg, but i can't find it

#### Enrico Tassi (Oct 27 2021 at 11:17):

https://github.com/math-comp/math-comp/blob/9190ef76593482691dea25f40ab6ff0a1a908a7f/mathcomp/algebra/ssralg.v#L6127

#### Enrico Tassi (Oct 27 2021 at 11:19):

I think the word overloading is a bit misleading there. The "bigop notations" are redeclared in many scopes to get default values, eg \sum in nat_scope uses addn and 0, while in ring_scope it uses addr and 0%R.

#### Enrico Tassi (Oct 27 2021 at 11:21):

In any scope you can write \big[ <op> , <init> ]_( x <- <from> | <filter>) <f> but that is verbose, hence the various "instances" in notation scopes.

#### Ana de Almeida Borges (Oct 27 2021 at 12:14):

Nitpick: the notation is \big[ <op> / <init> ]_( x <- <from> | <filter>) <f>

#### Dubravka Kutlesic (Oct 27 2021 at 12:43):

Thanks! :) I am a Coq beginner, so I don't understand this notation. Could you provide me with an example with sum?

#### Enrico Tassi (Oct 27 2021 at 12:50):

From mathcomp Require Import all_ssreflect.
Check \big[addn/O]_(n <- [:: 1;2;3] | odd n) (n+1).
(* displays: \sum_(n <- [:: 1; 2; 3] | odd n) (n + 1) : nat *)


#### Enrico Tassi (Oct 27 2021 at 12:50):

\sum is just the iterated version (the "big" version) of addn

#### Dubravka Kutlesic (Oct 27 2021 at 13:03):

What do I need to include for something like this: Definition mySum (f : nat -> R) (n : nat) : R := \big[+%R/0%R]_(0 <= i < n) (f i).
I'm getting: The term "f i" has type "R" while it is expected to have type "GRing.Zmodule.sort ?V0". why does it even expect Zmodule?

#### Ana de Almeida Borges (Oct 27 2021 at 17:21):

%R can mean many different things depending on what you have imported. Edit: In mathcomp it refers to the ring scope, that's where GRing comes from.

This works:

From mathcomp Require Import all_ssreflect.
Require Import Reals.

Open Scope R_scope.

Definition mySum (f : nat -> R) (n : nat) : R :=
\big[Rplus/0]_(0 <= i < n) (f i).


#### Emilio Jesús Gallego Arias (Oct 28 2021 at 09:01):

Yeah the reason is that +%R is addition for an abelian group

#### Emilio Jesús Gallego Arias (Oct 28 2021 at 09:01):

So you need to use math-comp analysis for example which will provide an instance of the reals

Last updated: Jan 31 2023 at 14:03 UTC