Commit b8d083f2 authored by Ralf Jung's avatar Ralf Jung

explain why the open inv-creation does not imply the other variants

parent b03f7081
......@@ -62,7 +62,7 @@ Section proofs.
(*** Allocation rules. *)
(** The "strong" variants permit any infinite [I], and choosing [P] is delayed
until after [γ] was chosen. *)
until after [γ] was chosen.*)
Lemma cinv_alloc_strong (I : gname Prop) E N :
pred_infinite I
(|={E}=> γ, I γ cinv_own γ 1 P, P ={E}= cinv N γ P)%I.
......@@ -73,7 +73,8 @@ Section proofs.
Qed.
(** The "open" variants create the invariant in the open state, and delay
having to prove [P]. *)
having to prove [P].
These do not imply the other variants because of the extra assumption [↑N ⊆ E]. *)
Lemma cinv_alloc_strong_open (I : gname Prop) E N :
pred_infinite I
N E
......
......@@ -56,6 +56,7 @@ Section inv.
do 2 iModIntro. iExists i. auto.
Qed.
(* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
Lemma own_inv_alloc_open N E P :
N E (|={E, E∖↑N}=> own_inv N P (P ={E∖↑N, E}= True))%I.
Proof.
......
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