This is exactly what I have started to do. I have started to define a "duplicate lemma" for every property like the previous one, the preserves the resources. This is working, but it adds a certain amount of dull lemmas.
@jung To explain the usecase, it comes from the development of a reliable causal broadcast library in aneris. There are two operations: broadcast and deliver, which respectively broadcast a message to every other nodes, and try to deliver a previously broadcast message.
Here are the two of the resources used to specify these operations:
OwnGlobal h
: to describe the global set of the system. It means that the set of all broadcast messages is h
.OwnLocal i h
: to describe the local state of a node. It means that the set of messages broadcast or delivered by the node i
in h
.There is also an invariant called GlobalInvariant
.
Now, it is time to explain why I would need to introduce modalities without consuming resources. Indeed, there are several laws governing these resources telling that, if the global invariant is satisfied and if the user owns a resource OwnGlobal h
or OwnGlobal i h
, then the set of messages h
satisfies some properties. For example:
OwnLocal_local_ext n h E :
nclose RCB_InvName ⊆ E →
GlobalInv ⊢ OwnLocal n h ={E}=∗
⌜∀ e e', e ∈ h → e' ∈ h → e.(LE_vc) = e'.(LE_vc) → e = e'⌝.
This law tells us that for the user owns the resources OwnLocal i h
, then every messages sent at the same time (e.(LE_vc)
is the vector-clock time of the event e
) are equals.
Proving this law requires opening the global invariant GlobalInv
. This is why there is a view shift _ ={E}=∗ _
implied. Yet, the goal is a pure mathematical goal. Resources inside the invariants are not modifies.
More generally, there are several other laws governing these resources that requires opening an invariant to deduce properties satisfied by the global or local set of messages. This is why being able to introduce a modality with iMod
without consuming the resources would be useful.
Suppose that we want to eliminate a modality with the following fancy update with a pure conclusion:
l : R ={E}=∗ ⌜ H ⌝
Applying the tactic iMod (l with "[R1 ... Rn]") as "%H"
consumes the resources R1, ..., Rn. However, these hypotheses need not to be consumed. Yet, preserving them requires to explicitly use a lemma like fupd_plain_keep_l
or fupd_plain_keep_r
.
More generally, it would be useful that the tactic iMod
does not consume hypothesis when the right-hand P side of a fancy-update modality R ={E}=∗ P
is plain, like the tactic iDestruct
does when the right-hand side of an implication is persistent.