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
ith element of a list using
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
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
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.
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: Jan 31 2023 at 14:03 UTC