Skip to content

Add generalized implication lemma for big_sepM

Simon Friis Vindum requested to merge simonfv/iris:big-op-impl into master

This MR adds a more general version of big_sepM_impl. The current big_sepM_impl requires the map in the assumption and conclusion to be exactly the same. The variant in this MR allows the maps to be different. They don't have to agree in their overlap and the domain of the map in the assumption can be both smaller or larger than the domain of the map in the conclusion.

The lemma big_sepM_impl_strong is the fully general lemma and big_sepM_impl_dom_subseteq is a variant that is easier to use when one knows that the map in the assumption is defined for at least as many keys as the map in the conclusion.

Note: Both the lemmas require Φ and Ψ to be affine since the map in the assumption may be larger and stuff from it may be thrown away. One can imagine variants of these lemmas where the initial map is only allowed to be smaller and where the affine requirement is lifted. For my use case I needed this more general variant though.

Note: This generalization makes sense for some of the other big_sep*_impl as well but I only needed it for big_sepM. If adding it for some of the others is not too much additional work then I can do that as well, but I would prefer not to 😅. Edit: See #431 for this.

Edited by Simon Friis Vindum

Merge request reports