Skip to content

Alternative take at "better support for view shift with mismatching masks"

Robbert Krebbers requested to merge robbert/fupd_elim into master

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.
Edited by Ralf Jung

Merge request reports