My question is two-stage.

First, I couldn't find a lemma to split a sum between the terms where a predicate is true, versus the ones where it's false ; say the terms where the index variable is even and the terms where it's not even (then something like eq_bigl should allow turning not even to odd ).

But in fact, what prompted the first part was that I would like to be able to cut a \sum_(0 <= i < n.*2.+1) F i to \sum_(0 <= i < n.+1) F i.*2 + \sum_(0 <= i < n) F (i.*2.+1). At some point I wondered if partition_big could be of some use, but it's getting way too hairy for such a simple thing.

Maybe you want `bigID`

?

For the first, you want to apply the typical map step

with `reindex`

and `big_split`

I agree the setup is annoying

Oh, reindex only works for finite types, so you may want to define your own lemma, or maybe just use big_cat_nat

Some ideas maybe here

```
Lemma foo n F : \sum_(0 <= i < n.*2.+1) F i = \sum_(0 <= i < n.+1) F i.*2 + \sum_(0 <= i < n) F (i.*2.+1).
Proof.
have h_lb : 0 <= n.+1 by [].
have h_ub : n.+1 <= n.*2.+1 by admit.
have -> /= := big_cat_nat _ _ _ h_lb h_ub.
have -> := big_addn 0 n.*2.+1 n.+1.
```

Emilio Jesús Gallego Arias said:

Maybe you want

`bigID`

?

Ah! I hadn't found it! Indeed it almost looks like it - except I don't see how to turn a \sum_() F to a \sum_(|) F.

\sum_() is just \sum_( | xtrue) where `xtrue`

is the true predicate

Coq hides it by default

Emilio Jesús Gallego Arias said:

Oh, reindex only works for finite types, so you may want to define your own lemma, or maybe just use big_cat_nat

Hmmm... I don't think big_cat_nat will do the trick: even and odds are intertwined, and as far as I understand, big_cat_nat can only cut on adjacent segments.

Indeed, I was just brainstorming. For bigID, your case is immediate:

```
Lemma foo n F : \sum_(0 <= i < n.*2.+1) F i =
\sum_(0 <= i < n.*2.+1 | odd i) F i +
\sum_(0 <= i < n.*2.+1 | ~~ odd i) F i.
Proof. exact: (bigID odd). Qed.
```

Emilio Jesús Gallego Arias said:

Indeed, I was just brainstorming. For bigID, your case is immediate:

`Lemma foo n F : \sum_(0 <= i < n.*2.+1) F i = \sum_(0 <= i < n.*2.+1 | odd i) F i + \sum_(0 <= i < n.*2.+1 | ~~ odd i) F i. Proof. exact: (bigID odd). Qed.`

I had to use Nat.odd (or Nat.even), but yes, bigID does manage to cut the sum -- that does the trick for the first part of my question!

Julien Puydt said:

But in fact, what prompted the first part was that I would like to be able to cut a \sum_(0 <= i < n.

2.+1) F i to \sum_(0 <= i < n.+1) F i.2 + \sum_(0 <= i < n) F (i.*2.+1). At some point I wondered if partition_big could be of some use, but it's getting way too hairy for such a simple thing.

Here is what I came up with ; extremely inelegant:

```
Lemma simple_even: forall n, Nat.even n.*2 = true.
Proof.
by elim.
Qed.
Lemma simple_odd: forall n, Nat.even n.*2.+1 = false.
Proof.
by elim.
Qed.
Lemma sum_even: forall F n, \sum_(0 <= i < n.*2.+1 | Nat.even i) F i
= \sum_(0 <= i < n.+1) F i.*2.
Proof.
move=> F.
elim=> [ | n Hn].
by rewrite unlock.
rewrite doubleS.
rewrite big_mkcond.
rewrite [in LHS]big_nat_recr //=.
rewrite simple_even.
rewrite -big_mkcond /=.
rewrite big_mkcond /=.
rewrite [in LHS]big_nat_recr //.
rewrite simple_odd.
rewrite -big_mkcond /=.
rewrite Hn.
rewrite [in RHS]big_nat_recr //=.
by rewrite doubleS addn0.
Qed.
```

I lack the courage to dig into sum_odd tonight...

For this case, induction seems to be simpler than splitting and reindexing.

```
Lemma sum_even_odd n F :
\sum_(0 <= i < n.*2.+1) F i = \sum_(0 <= i < n.+1) F i.*2 + \sum_(0 <= i < n) F i.*2.+1.
Proof.
elim: n => [|n IHn]; first by rewrite !big_nat1 big_nil addn0.
rewrite doubleS 2?big_nat_recr //= IHn.
rewrite [X in _ = _ + X]big_nat_recr // [in RHS]big_nat_recr //=.
by rewrite [RHS]addnAC addnA.
Qed.
```

Indeed, if you are open to use induction, you can do a bit simpler:

```
Lemma sum_even F n :
\sum_(0 <= i < n) F i.*2 = \sum_(0 <= i < n.*2 | ~~ odd i) F i.
Proof.
rewrite (big_mkcond [pred x | ~~ odd x]) /=.
elim: n => [|n ihn]; first by rewrite !big_nil.
by rewrite doubleS !big_nat_recr //= ihn odd_double addn0.
Qed.
Lemma sum_odd F n :
\sum_(0 <= i < n) F i.*2.+1 = \sum_(0 <= i < n.*2 | odd i) F i.
Proof.
rewrite (big_mkcond odd) /=.
elim: n => [|n ihn]; first by rewrite !big_nil.
by rewrite doubleS !big_nat_recr //= ihn odd_double addn0.
Qed.
```

Or as Mitsuharu does, a bit simpler:

```
Lemma sum_even_odd n F :
\sum_(0 <= i < n.*2) F i = \sum_(0 <= i < n) F i.*2 + \sum_(0 <= i < n) F i.*2.+1.
Proof.
elim: n => [|n ihn]; first by rewrite !big_nil.
by rewrite doubleS !big_nat_recr //= ihn addnACA addnA.
Qed.
```

For the other lemma, I prefer to state it as:

```
Lemma sum_even_oddS n F :
\sum_(0 <= i < n.*2.+1) F i = \sum_(0 <= i < n.+1) F i.*2 + \sum_(0 <= i < n) F i.*2.+1.
Proof. by rewrite !big_nat_recr //= sum_even_odd addnAC. Qed.
```

Emilio Jesús Gallego Arias said:

For the other lemma, I prefer to state it as:

`Lemma sum_even_oddS n F : \sum_(0 <= i < n.*2.+1) F i = \sum_(0 <= i < n.+1) F i.*2 + \sum_(0 <= i < n) F i.*2.+1. Proof. by rewrite !big_nat_recr //= sum_even_odd addnAC. Qed.`

Why do you prefer that formulation in particular?

I was wondering why ssrnat.v had an odd predicate with a nice odd_double lemma, but no even predicate.

Julien Puydt said:

Why do you prefer that formulation in particular?

Because it is strictly more general than the other lemma.

I was wondering why ssrnat.v had an odd predicate with a nice odd_double lemma, but no even predicate.

No point on defining even x := ~~ odd x , it just adds naming overhead IMHO.

Last updated: Jul 15 2024 at 20:02 UTC