The Coq mailing list

[Kiran Corbett Gopinathan <e0427802 AT u.nus.edu>]

Dear Coq Club,

I am working on a few proofs in ssreflect that rely on the bigop library, but have run into a block with regards to proving equality of bigop's when the indices are not equal or bijectively related - specifically, in my case I have a situation in which one summand of one of the summations corresponds to a varying number of summands in the other.

A full example would require too much context, but a simplified form of the problem I'm facing can be captured in the following way:

From mathcomp.ssreflect Require Import ssrnat bigop.

Fixpoint even (n: nat) : bool :=

  match n with

  | 0 => true

  | 1 => false

  | n'.+1 => negb (even n')

  end.

 

Lemma example: forall f, \sum_(0 <= i < 4) (2 * f (even i)) = \sum_(0 <= i < 8) (f (even i)).

Obviously this simple lemma can be proven in a number of ways, but I'm specifically interested in whether I could prove this by somehow relating each summand of the first summation to two in the second? (I've looked through the bigop documentation, but the ones on equality seem to be for the case in which indices have a one to one mapping between them (eq_big, eq_bigr etc.)).

Thank you.
-----
Kiran Gopinathan,
PhD Candidate, NUS,
Singapore