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?

```
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
*)
```

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"`

).

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 //=.
by rewrite big_geq ?addn0 -addnn addnS // -addnn addSn.
Qed.
```

Thanks.

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

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.

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

Been reading the section about bigop in the mathcomp book.

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:

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