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: Sep 25 2023 at 12:01 UTC