Ssreflect Users Discussion List

[Vincent Siles <>]

2011/5/30 Georges Gonthier <>:
>  For situation 1, I assume by "0" you meant idx. In this case the big1 
> lemma does exactly what you want; perhaps you should browse the bigop 
> documentation to get a better idea of the available lemmas.

I did, but I got confused with the notations (and understood *%M for a
particular operator, not the op of the monoid).. silly me

>  In situation 2, and more generally, you can rewrite under a \big, what you 
> can't do (unless you turn to the "experimental" setoid rewriting), is 
> rewrite a subterm that contains a bound variable, such as the bigop index. 
> In this case it is best to use the transitivity tactic to state the reduce 
> \big form you want to use, then use eq_bigr (or possibly eq_big) to prove 
> the simplification. This will give a cleaner, more declarative proof 
> script, which won't necessarily be very much longer (because once you've 
> given the intermediate term you can rewrite from both ends, and use congr 
> to remove identical context).

Thank you for the clarification, since I may have wanted the
"experimental" rewrite. I'll try with transitivity then.

Cheers,
Vincent