Hello, how can I prove the following?

Require Import Coq.Reals.Reals.

From mathcomp Require Import all_ssreflect ssralg ssrnum Rstruct reals.

Local Open Scope ring_scope.

(* for all i: (f_i + sum f_j over j!=i) = sum f_j over all j *)

Lemma adding_and_excluding_index (n : nat) (f : nat -> R) (i : 'I_n) :

f i + \sum_(j < n | j != i) f j = \sum_(j < n) f j.

There's a lemma that's basically exactly that, we just need to make it clear that the goal has the expected form. There is probably a better solution, but this one should work.

```
Lemma adding_and_excluding_index (n : nat) (f : nat -> R) (i : 'I_n) :
f i + \sum_(j < n | j != i) f j = \sum_(j < n) f j.
Proof.
rewrite -[\sum_(j < n | j != i) _]/(\sum_(j < n | predT j && (j != i)) _).
by rewrite -bigD1.
Qed.
```

Alright, this one is much better:

```
Lemma adding_and_excluding_index (n : nat) (f : nat -> R) (i : 'I_n) :
f i + \sum_(j < n | j != i) f j = \sum_(j < n) f j.
Proof.
by rewrite -(bigD1 i (P := predT)).
Qed.
```

(You may be wondering: how did she find this lemma? And unfortunately the answer is that I browsed the source of bigop until I found it. `Search`

is famously bad with `bigop`

, but there *are* a lot of useful lemmas, so I was fairly certain there would be something to prove your goal in a couple of steps at most.)

This topic was moved here from #Coq users > mathcomp analysis summation proof help by Karl Palmskog

Thanks a lot! Could you tell me how can I transform (i : 'I_n) to (i : nat)?

`val i`

should convert `i : 'I_n`

to ```
nat
```

Usually one doesn't need to explicitly convert `'I_n`

to `nat`

, because there is an implicit coercion `nat_of_ord`

.

So you could just put `i : 'I_n`

in the context where term of type `nat`

is expected.

If you're getting confused by the implicit coercions, `Set Printing Coercions.`

makes them explicit.

If you have `i : 'I_n`

and want a `nat`

*and* want to remember that this natural number is less than `n`

, just destruct `i`

, which will give you `i' : nat`

and a proof of `i' < n`

. If you just want the `nat`

then `val`

is fine.

[Quoting…]

Can this be generalized to Rbar (f: nat -> Rbar)? I was reading the library and I didn't find something that can help me

Do you mean the `adding_and_excluding_index`

lemma? The basic structure is the same. The only important thing is that the operation forms a commutative monoid (and Coq knows through `Monoid.com_law`

).

```
Print Monoid.com_law.
Record com_law (T : Type) (idm : T) : Type := ComLaw
{ com_operator : Monoid.law idm; _ : commutative com_operator }
Print Monoid.law.
Record law (T : Type) (idm : T) : Type := Law
{ operator : T -> T -> T;
_ : associative operator;
_ : left_id idm operator;
_ : right_id idm operator }
```

Thus if this is not in MathComp already, you need to prove that the addition over `Rbar`

is associative, has zero as a left and right id, and is commutative. Once you have all of these lemmas, you package them inside something of type `Monoid.com_law`

, which ends up being just addition over `Rbar`

with a bunch of proven properties about it, and then you can apply `bigD1`

.

There might be a less clunky way of doing it, perhaps someone more knowledgeable can give better advice.

Thank you very much for your answer! :)

Yes, I meant for that lemma.

Actually my use-case is that f maps to positives from Rbar, so lemma is correct, but it's not correct for Rbar in general.

Should I do the following then:

- define Rbar+
- prove that Rbar+ is associative, commutative, and has zero as left and right id
- package them inside of something of type Monoid.com_law.

In that case, how should I define Rbar+? I was thinking to use set from mathcomp, but I am getting the error

```
Found type "Rbar" where "Finite.sort ?T" was expected.
```

MathComp's `set`

is a library of finite sets of finite types. `Rbar`

is not a finite set, so this won't work.

I would suggest following the spirit of `'I_n`

: define `Rbar+`

as a (dependent) pair with an element of `Rbar`

and a proof that this element is positive

Edit: here is an untested snipet illustrating the idea:

```
Record Rbarp := mkRbarp {
Rbar_of_Rbarp :> Rbar;
_ : 0 <= Rbar_of_Rbarp
}.
Canonical Rbarp_subType := [subType for Rbar_of_Rbarp].
```

Reals can be put in "classical sets" from MathComp analysis, as was recently flagged up in another topic: https://github.com/math-comp/analysis/blob/master/theories/classical_sets.v

Last updated: Jul 15 2024 at 20:02 UTC