## Stream: math-comp users

### Topic: proof involving \sum

#### Julin Shaji (Oct 23 2023 at 10:35):

I was trying to read about bigop from the mathcomp book and wished to try one of the proofs, but couldn't:

Lemma sum_odd_n (n: nat): \sum_(0 <= i < n.*2 | odd i) i = n^2.
Proof.
rewrite unlock.
(*
1 subgoal

n : nat

========================= (1 / 1)

reducebig 0 (index_iota 0 n.*2) (fun i : nat => BigBody i addn (odd i) i) =
n ^ 2
*)


With unlock, I just tried what was done for the proof of n=3 as shown in the book:

Lemma sum_odd_3: \sum_(0 <= i < 3.*2 | odd i) i = 3^2.
Proof.
by rewrite unlock /=.
Qed.


I guess I should start with elim instead? For induction?

#### Julin Shaji (Oct 23 2023 at 10:37):

Lemma sum_odd_n (n: nat): \sum_(0 <= i < n.*2 | odd i) i = n^2.
Proof.
elim: n.
by rewrite unlock /=.
rewrite unlock /=.
(*
1 subgoal

========================= (1 / 1)

forall n : nat,
reducebig 0 (index_iota 0 n.*2) (fun i : nat => BigBody i addn (odd i) i) =
n ^ 2 ->
1 +
reducebig 0 (iota 2 (n.*2)%Nrec) (fun i : nat => BigBody i addn (odd i) i) =
n.+1 ^ 2
*)


#### Pierre Roux (Oct 23 2023 at 10:44):

The proof of the book seems to proceed by computation (/=) because it applies on concrete values. If you want to perform an induction, you can indeed elim: n or use one of the induction principles specialised on bigop (c.f., Search bigop "_ind" and Search bigop "_rec").

#### Pierre Jouvelot (Oct 23 2023 at 13:03):

A simple proof using induction, via elim, can run as follows (I'm sure one can be more succinct, but this gives an idea of one way to proceed):

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma sum_odd_n (n: nat) : \sum_(0 <= i < n.*2 | odd i) i = n^2.
Proof.
elim: n => [//=|n IH]; first by rewrite double0 -mulnn muln0 big_geq.
rewrite (@big_cat_nat _ _ _ n.*2) //=; last by rewrite -!addnn leq_add.
rewrite IH -!mulnn mulSnr mulnSr -addnA.
congr (_ + _).
rewrite big_ltn_cond ?ifF ?odd_double //.
rewrite big_ltn_cond /ifT ?oddS ?odd_double //=.
Qed.


#### Julin Shaji (Oct 23 2023 at 17:04):

Thanks.

Is it that there are other ways which are more preferred than explicit induction?

#### Pierre Jouvelot (Oct 23 2023 at 17:33):

In my somewhat limited experience, it's either this or you find an existing lemma (or combination of lemmas) in the mathcomp library that can be applied to your problem. As mentioned by @Pierre Roux, there are also more general induction principles that can be sometimes used, depending on the datatypes you're working on. Of course, you need to have the general idea of the proof in your head or on paper before digging into Coq.

I found also quite useful to spend time reading the HTML mathcomp documentation files (e.g., ssrnat.html or bigop.html) and the comments there to get a feel for how this quite extensive library is structured and what's available (it's ok to not understand everything right away :wink: ). Looking at the actual proofs for all these lemmas is also illuminating.

#### Julin Shaji (Oct 25 2023 at 14:51):

Yeah, one needs practice to get familiar with mathcomp way of doing proofs I guess.

#### Julin Shaji (Oct 25 2023 at 14:52):

Pierre Jouvelot said:

how this quite extensive library is structured and what's available

Am trying to get to know what's available. Still haven't got the hang of knowing what to search for. :sweat_smile:

#### Pierre Jouvelot (Oct 25 2023 at 19:21):

Personally, I basically used a lot of ssreflect <blah> in google when I started. In addition to the two documentation files I mentioned before, I think it's quite necessary to go through seq.v (for lists) and ssrbool.v (for booleans) to get a feel of what's already there. But of course, there is whole lot more :smile:

Last updated: Jul 23 2024 at 20:01 UTC