The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Maybe you can use partition_big to split your sum in bits that
correspond to your mappping.


On 11/28/19 4:28 PM, Kiran Corbett Gopinathan wrote:
> Hi Laurent,
> 
> Apologies, my example wasn't quite clear enough to exactly capture the
> difficulty in my situation.
> 
> One problem is that my summation doesn't split quite as nicely as the
> one in the example, and the corresponding elements on each summand may
> be interleaved, ruling out the possibility of simply splitting the
> summation. Additionally, the size of the mapping between summands (2 in
> the example) is actually given by an expression on the index of the sum
> - i.e rather than 2 * f(even(i)), I have something like g(i) * f(even(i)).
> 
> 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.
> 
> Thanks,
> -----
> Kiran Gopinathan.
> ------------------------------------------------------------------------
> *From:* 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  on behalf
> of Laurent Thery 
> <Laurent.Thery AT inria.fr>
> *Sent:* 28 November 2019 21:17
> *To:* 
> coq-club AT inria.fr
>  
> <coq-club AT inria.fr>
> *Subject:* Re: [Coq-Club] BigOp equality over differing indices
>  
>         - External Email -
> 
> 
> 
> Hi,
> 
> I am not sure this will help you in your general problem.
> But in your particular example, you can split the sum to make
> the reindexing possible.
> 
> Lemma example: forall f, \sum_(0 <= i < 4) (2 * f (even i)) = \sum_(0 <=
> i < 8) (f (even i)).
> Proof.
> move=> f.
> rewrite [RHS](big_cat_nat _ _  _ (_ : 0 <= 4)) //=.
>  rewrite -[4]/(0 + 4) big_addn /= add0n.
> rewrite  [X in _ = _ + X](eq_bigr (fun i => f (even i))) => [|i _]; last
> first.
>   by rewrite addnC /=;  case: i => [|i]; rewrite  ?negbK.
> rewrite -big_split.
> by apply: eq_bigr => i _ ; rewrite /= mul2n addnn.
> Qed.
> 
> --
> Laurent
> 
> Ps : this 8.10 code