Commit d3412460 authored by Ralf Jung's avatar Ralf Jung
Browse files

prove generally applicable lemmas for non-mask-matching fancy updates

parent 55711e8e
Pipeline #8075 passed with stage
in 23 minutes and 43 seconds
......@@ -222,6 +222,25 @@ Section fupd_derived.
intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
(** 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).
intros ?. rewrite (fupd_mask_frame_r _ _ (E E1)); last set_solver.
assert (E = E1 E E1) as <-; last done.
apply union_difference_L. done.
Lemma fupd_mask_frame_diff 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).
intros ? HE. rewrite (fupd_mask_frame E); last 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.
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.
Supports Markdown
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