Commit 41feea65 authored by Ralf Jung's avatar Ralf Jung

show that atomic_wp masks have the opposite monotonicity compared to HT

parent 6cd681c3
Pipeline #20486 passed with stage
in 15 minutes and 38 seconds
......@@ -226,6 +226,7 @@ Section lemmas.
Local Existing Instance atomic_update_pre_mono.
(* Can't be in the section above as that fixes the parameters *)
Global Instance atomic_acc_ne Eo Ei n :
Proper (
pointwise_relation TA (dist n) ==>
......@@ -247,6 +248,18 @@ Section lemmas.
rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
Qed.
Lemma atomic_update_mask_weaken Eo1 Eo2 Ei α β Φ :
Eo1 Eo2
atomic_update Eo1 Ei α β Φ - atomic_update Eo2 Ei α β Φ.
Proof.
rewrite atomic_update_eq {2}/atomic_update_def /=.
iIntros (Heo) "HAU".
iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
iIntros "!# *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
iApply make_laterable_wand. iIntros "!#".
iApply atomic_acc_mask_weaken. done.
Qed.
(** The ellimination form: an atomic accessor *)
Lemma aupd_aacc Eo Ei α β Φ :
atomic_update Eo Ei α β Φ -
......
......@@ -99,6 +99,13 @@ Section lemmas.
Notation iProp := (iProp Σ).
Implicit Types (α : TA iProp) (β : TA TB iProp) (f : TA TB val Λ).
Lemma atomic_wp_mask_weaken e Eo1 Eo2 α β f :
Eo2 Eo1 atomic_wp e Eo1 α β f - atomic_wp e Eo2 α β f.
Proof.
iIntros (HEo) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
iApply atomic_update_mask_weaken; last done. done.
Qed.
(* Atomic triples imply sequential triples if the precondition is laterable. *)
Lemma atomic_wp_seq e Eo α β f {HL : .. x, Laterable (α x)} :
atomic_wp e Eo α β f -
......
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