Alternative take at "better support for view shift with mismatching masks"
This is an alternative and more general take at !527 (closed). This MR generalizes the instance elim_modal_fupd_fupd
so that it can handle fancy updates with mismatching masks by implicitly using fupd_mask_frame_r
:
Global Instance elim_modal_fupd_fupd `{!BiFUpd PROP} φ p E1' E2' E1 E2 E3 P Q :
ElimFUpdChangeMask φ E1' E2' E1 E2 →
ElimModal φ p false
(={E1',E2'}=> P) P
(={E1,E3}=> Q) (={E2,E3}=> Q).
The class ElimFUpdChangeMask
factors our some typical cases (in all cases the resulting hypothesis is P
):
Hypothesis  Goal  Resulting goal  Sidecondition  Instance 

={E1,E2}=> P 
={E1,E3}=> Q 
={E2,E3}=> Q 
elim_fupd_change_mask_same_src 

={∅,E2}=> P 
={E1,E3}=> Q 
={E2 ∪ E1,E3}=> Q 
elim_fupd_change_mask_src_empty 

={E2,E2}=> P 
={E1,E3}=> Q 
={E1,E3}=> Q 
E2 ⊆ E1 
elim_fupd_change_mask_no_change 
={E2,∅}=> P 
={E1,E3}=> Q 
={E1 ∖ E2,E3}=> Q 
E2 ⊆ E1 
elim_fupd_change_mask_tgt_empty 
={E2,E2'}=> P 
={E1,E3}=> Q 
={E2' ∪ E1 ∖ E2,E3}=> Q 
E2 ⊆ E1 
elim_fupd_change_mask_default 
Contrary to !527 (closed), I think this MR matches up better with the usual behavior we have for eliminating modalities: it removes the modality from the hypothesis and changes the goal accordingly, while possibly generating a sidecondition.
In the future we could decide to extend ElimFUpdChangeMask
to have more sophisticated instances, e.g., for canceling out masks.
This MR furthermore includes the lemma fupd_intro_mask_adjust
from !527 (closed), which I think is very useful. This MR makes sure that the lemma is consistent with some other (new and existing) variants of the lemma:
Lemma fupd_mask_subseteq E1 E2 P :
E2 ⊆ E1 →
((={E2,E1}=> emp) ={E2}=∗ P) ={E1,E2}=∗ P.
Lemma fupd_intro_mask_subseteq E1 E2 P : (* [fupd_intro_mask_adjust] in !527 *)
E2 ⊆ E1 →
((={E2,E1}=> emp) ∗ P) ={E1,E2}=∗ P.
Lemma fupd_mask_eq E1 E2 P : E1 = E2 → (={E1}=> P) ={E1,E2}=∗ P. (* was [fupd_mask_same] *)
Lemma fupd_intro_mask_eq E1 E2 P : E1 = E2 → P ={E1,E2}=∗ P.