Stream: math-comp users

Topic: mathcomp analysis summation proof help


view this post on Zulip Dubravka Kutlesic (Nov 01 2021 at 19:49):

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.

view this post on Zulip Ana de Almeida Borges (Nov 01 2021 at 22:14):

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.

view this post on Zulip Ana de Almeida Borges (Nov 01 2021 at 22:19):

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.

view this post on Zulip Ana de Almeida Borges (Nov 01 2021 at 22:23):

(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.)

view this post on Zulip Notification Bot (Nov 02 2021 at 07:29):

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

view this post on Zulip Dubravka Kutlesic (Nov 02 2021 at 11:34):

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

view this post on Zulip Evgeniy Moiseenko (Nov 02 2021 at 12:49):

val i should convert i : 'I_n to nat

view this post on Zulip Evgeniy Moiseenko (Nov 02 2021 at 12:52):

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.

view this post on Zulip Ana de Almeida Borges (Nov 02 2021 at 13:40):

If you're getting confused by the implicit coercions, Set Printing Coercions. makes them explicit.

view this post on Zulip Ana de Almeida Borges (Nov 02 2021 at 14:02):

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.

view this post on Zulip Dubravka Kutlesic (Nov 08 2021 at 13:48):

[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

view this post on Zulip Ana de Almeida Borges (Nov 08 2021 at 14:48):

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.

view this post on Zulip Dubravka Kutlesic (Nov 10 2021 at 17:10):

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:

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.

view this post on Zulip Ana de Almeida Borges (Nov 10 2021 at 17:17):

MathComp's set is a library of finite sets of finite types. Rbar is not a finite set, so this won't work.

view this post on Zulip Ana de Almeida Borges (Nov 10 2021 at 17:18):

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

view this post on Zulip Karl Palmskog (Nov 10 2021 at 17:22):

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