Commit 67325634 authored by Ralf Jung's avatar Ralf Jung

more mask-related fancy update lemmas

parent d3412460
......@@ -224,23 +224,38 @@ Section fupd_derived.
Qed.
(** How to apply an arbitrary mask-changing view shift when having
an arbitrary mask. *)
Lemma fupd_mask_frame E E1 E2 P :
E1 E (|={E1,E2}=> P) - (|={E,E2 (E E1)}=> P).
Lemma fupd_mask_frame E E' E1 E2 P :
E1 E E' = E2 (E E1)
(|={E1,E2}=> P) - (|={E,E'}=> P).
Proof.
intros ?. rewrite (fupd_mask_frame_r _ _ (E E1)); last set_solver.
intros ? ->. rewrite (fupd_mask_frame_r _ _ (E E1)); last set_solver.
assert (E = E1 E E1) as <-; last done.
apply union_difference_L. done.
Qed.
Lemma fupd_mask_frame_diff E E1 E2 P :
Lemma fupd_mask_frame_diff_open E E1 E2 P :
(* E2 ⊆ E1 is needed bcause otherwise the [E ∖ E2] could remove
more invariants from E than it did from E1. *)
E2 E1 E1 E (|={E1,E1E2}=> P) - (|={E,EE2}=> P).
E1 E E2 E1 (|={E1,E1E2}=> P) - (|={E,EE2}=> P).
Proof.
intros ? HE. rewrite (fupd_mask_frame E); last done.
intros HE ?. rewrite (fupd_mask_frame E); [|done..].
assert (E1 E2 E E1 = E E2) as <-; last done.
apply (anti_symm ()); first set_solver.
rewrite {1}(union_difference_L _ _ HE). set_solver.
Qed.
Lemma fupd_mask_frame_diff_close E E1 E2 P :
(* E2 ⊆ E1 is needed bcause otherwise the [E ∖ E2] could remove
more invariants from E than it did from E1. *)
E1 E E2 E1 (|={E1E2,E1}=> P) - (|={EE2,E}=> P).
Proof.
intros HE ?. rewrite (fupd_mask_frame (E E2)); [|set_solver..].
assert (E = E1 E E2 (E1 E2)) as <-; last done.
apply (anti_symm ()); last set_solver.
rewrite {1}(union_difference_L _ _ HE). set_solver.
Qed.
Lemma fupd_mask_same E E1 P :
E = E1 (|={E}=> P) - (|={E,E1}=> P).
Proof. intros <-. done. Qed.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment