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

If you wish to use the standard library, one option would be to write a function to drop the `i`

th element of a list using `firstn`

and `skipn`

(see here) and another function to sum all the elements using `fold_left`

(see here).

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

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" .

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?

Did you import `ssrnat`

?

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

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.

In this case, importing `ssrnat`

added the eqType instance for nat

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

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.

In any scope you can write `\big[ <op> , <init> ]_( x <- <from> | <filter>) <f>`

but that is verbose, hence the various "instances" in notation scopes.

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

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

```
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 *)
```

`\sum`

is just the iterated version (the "big" version) of `addn`

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?

`%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).
```

Yeah the reason is that `+%R`

is addition for an abelian group

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

Last updated: Sep 25 2023 at 12:01 UTC