The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Kiran,

Kiran Corbett Gopinathan 
<e0427802 AT u.nus.edu>
 writes:

> Now, in my case, I can prove there exists a mapping between the
> summands of each summation - for each element in one sum, I can find
> g(i) distinct unique elements in the other sum, but I'm not sure how
> to manipulate the goal such that applying this mapping is possible.

I guess you could take inspiration from `partition_big` or `big_flatten`
as to partition your indexes into what you want, then you can apply the
lemma relating each element with their set in the other side; for example:

Lemma example f :
  \sum_(i <- [:: 0; 1; 2; 3])         (2 * f (even i)) =
  \sum_(i <- [:: 0; 1; 2; 3; 4; 5; 6; 7]) (f (even i)).
Proof.
pose dflt := reshape [::2;2;2;2] [:: 0; 1; 2; 3; 4; 5; 6; 7].
have -> /= := @big_flatten _ _ addn_monoid _ dflt xpredT.
rewrite (big_nth 0) (big_nth [::]) {}/dflt /=; apply: eq_bigr => i _.

will get you down to the shape:

  2 * f (even (nth 0 [:: 0; 1; 2; 3] i)) =
  \sum_(j <- nth [::] [:: [:: 0; 1]; [:: 2; 3]; [:: 4; 5]; [:: 6; 7]] i)  f 
(even j)

which you can prove as a more general lemma.

Kind regards,
E.