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 | Side-condition | 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 side-condition.
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.