## Stream: math-comp users

### Topic: Splitting bigop on a predicate, and even/odd expansion

#### Julien Puydt (Aug 25 2021 at 20:02):

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.

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:05):

Maybe you want bigID ?

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:06):

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

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:07):

with reindex

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:09):

and big_split

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:13):

I agree the setup is annoying

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:17):

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

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:23):

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.


#### Julien Puydt (Aug 25 2021 at 20:24):

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.

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:25):

\sum_() is just \sum_( | xtrue) where xtrue is the true predicate

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:25):

Coq hides it by default

#### Julien Puydt (Aug 25 2021 at 20:25):

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.

#### Emilio Jesús Gallego Arias (Aug 25 2021 at 20:28):

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.


#### Julien Puydt (Aug 25 2021 at 20:32):

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 (Aug 25 2021 at 21:14):

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 //=.
Qed.


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

#### YAMAMOTO Mitsuharu (Aug 25 2021 at 23:47):

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 //=.
Qed.


#### Emilio Jesús Gallego Arias (Aug 26 2021 at 00:23):

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


#### Emilio Jesús Gallego Arias (Aug 26 2021 at 09:52):

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.


#### Julien Puydt (Aug 26 2021 at 11:27):

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.

#### Emilio Jesús Gallego Arias (Aug 26 2021 at 13:44):

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