Stream: Coq users

Topic: Sum of list excluding given index


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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" .

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2021 at 19:01):

Did you import ssrnat ?

view this post on Zulip Dubravka Kutlesic (Oct 26 2021 at 20:03):

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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2021 at 20:08):

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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 27 2021 at 11:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Oct 27 2021 at 12:14):

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

view this post on Zulip 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?

view this post on Zulip 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 *)

view this post on Zulip Enrico Tassi (Oct 27 2021 at 12:50):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:01):

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

view this post on Zulip 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