Julien Puydt (Aug 25 2021 at 20:02): 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.
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.
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 //=.
by rewrite doubleS addn0.
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 //=.
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.
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: Feb 08 2023 at 07:02 UTC