Skip to content

Lemmas for big ops commuting with updates

Robbert Krebbers requested to merge robbert/big_op_commute into master

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 the big_op.v file. The others are in the file where the construct is defined. Concretely, this means that the plainly lemmas for bigops have moved to the plainly.v file.
Edited by Robbert Krebbers

Merge request reports