Lemmas for big ops commuting with updates
This MR features:
-
MonoidHomomorphism
instances for basic and fancy updates. - Lemmas that show that big ops commute with basic updates.
- Refactorings of the proofs of those lemmas for fancy updates, but using the
MonoidHomomorphism
infrastructure. - More consistent names for those lemmas for fancy updates, which are of the shape
big_sep{L,M,S,MS}_{bupd,fupd}
, and follow the convention for other such lemmas. - Consistency changes to file organization. Only lemmas about
bi
/sbi
are in thebig_op.v
file. The others are in the file where the construct is defined. Concretely, this means that theplainly
lemmas for bigops have moved to theplainly.v
file.