Skip to content

Added [cmra_update_included] lemma

There is currently no way of weakening a fragment in the scope of the frame-preserving update of the authoritative RA (without breaking abstraction). It is thus proposed to add the rule:

Lemma auth_update_frag_included a b : b ≼ a → ◯ a ~~> ◯ b

One use of this is the instructive example of proving the following frame-preserving update for a simpler variant of the mono_nat RA:

(●MN n ⋅ ◯MN m) ~~> (●MN (n + x) ⋅ ◯MN (m + x))

In particular, this example follows from auth_update, max_nat_local_update, and auth_update_frag_included.

Note that the current version of mono_nat employs the pattern of keeping a copy of the persistent fragmental part within the authoritative abstraction, making this approach a bit less important.

I could however imagine other cases in which the lemma could be useful, although I fail to come up with them now.

EDIT:

Instead added the following lemma:

Lemma cmra_update_included x y : x ≼ y → y ~~> x

The originally intended lemma can be directly derived from this and have thus not been added, for consistency with remaining similar RA constructions.

Edited by Jonas Kastberg

Merge request reports

Loading