Commit ef3214e0 authored by Ralf Jung's avatar Ralf Jung

change statement of inv-open lemmas such that they do not force the invariant,...

change statement of inv-open lemmas such that they do not force the invariant, and the 'inner step', to appear right next to each other
parent 563ed428
......@@ -72,15 +72,16 @@ Section auth.
step-indices. However, since A is timeless, that should not be
a restriction. *)
Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
`{!LocalUpdate Lv L} E P (Q : X iPropG Λ Σ) γ a :
`{!LocalUpdate Lv L} E P (Q : X iPropG Λ Σ) R γ a :
nclose N E
(auth_ctx γ auth_own γ a ( a', ▷φ (a a') -
FSA (E nclose N) (λ x, (Lv a (L aa')) ▷φ (L a a') (auth_own γ (L a) - Q x))))
FSA E Q.
R auth_ctx γ
R (auth_own γ a ( a', ▷φ (a a') -
FSA (E nclose N) (λ x, (Lv a (L aa')) ▷φ (L a a') (auth_own γ (L a) - Q x))))
R FSA E Q.
Proof.
rewrite /auth_ctx=>HN.
rewrite -inv_fsa; last eassumption.
apply sep_mono; first done. apply wand_intro_l.
rewrite /auth_ctx=>HN Hinv Hinner.
eapply inv_fsa; [eassumption..|]. rewrite Hinner=>{Hinner Hinv R}.
apply wand_intro_l.
rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
apply fsa_strip_pvs; first done. apply exist_elim=>a'.
rewrite (forall_elim a'). rewrite [(_ _)%I]comm.
......
......@@ -66,12 +66,14 @@ Proof. by rewrite always_always. Qed.
(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
E N P (Q : A iProp Λ Σ) :
E N P (Q : A iProp Λ Σ) R :
nclose N E
(inv N P (P - FSA (E nclose N) (λ a, P Q a))) FSA E Q.
R inv N P
R (P - FSA (E nclose N) (λ a, P Q a))
R FSA E Q.
Proof.
move=>HN.
rewrite /inv sep_exist_r. apply exist_elim=>i.
move=>HN Hinv Hinner. rewrite -[R](idemp ()%I) {1}Hinv Hinner =>{Hinv Hinner R}.
rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
rewrite -(fsa_trans3 E (E {[encode i]})) //; last by solve_elem_of+.
(* Add this to the local context, so that solve_elem_of finds it. *)
......@@ -87,16 +89,20 @@ Qed.
(* Derive the concrete forms for pvs and wp, because they are useful. *)
Lemma pvs_open_close E N P Q :
Lemma pvs_open_close E N P Q R :
nclose N E
(inv N P (P - pvs (E nclose N) (E nclose N) (P Q))) pvs E E Q.
Proof. move=>HN. by rewrite (inv_fsa pvs_fsa). Qed.
R inv N P
R (P - pvs (E nclose N) (E nclose N) (P Q))
R pvs E E Q.
Proof. move=>HN ? ?. apply: (inv_fsa pvs_fsa); eassumption. Qed.
Lemma wp_open_close E e N P (Q : val Λ iProp Λ Σ) :
Lemma wp_open_close E e N P (Q : val Λ iProp Λ Σ) R :
atomic e nclose N E
(inv N P (P - wp (E nclose N) e (λ v, P Q v))) wp E e Q.
R inv N P
R (P - wp (E nclose N) e (λ v, P Q v))
R wp E e Q.
Proof.
move=>He HN. by rewrite (inv_fsa (wp_fsa e _)). Qed.
move=>He HN ? ?. apply: (inv_fsa (wp_fsa e _)); eassumption. Qed.
Lemma inv_alloc N P : P pvs N N (inv N P).
Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
......
......@@ -92,8 +92,8 @@ Lemma vs_open_close N E P Q R :
Proof.
intros; apply (always_intro _ _), impl_intro_l.
rewrite always_and_sep_r assoc [(P _)%I]comm -assoc.
rewrite -(pvs_open_close E N) //. apply sep_mono; first done.
apply wand_intro_l.
apply: (pvs_open_close E N); [by eauto using sep_elim_l..|].
rewrite sep_elim_r. apply wand_intro_l.
(* Oh wow, this is annyoing... *)
rewrite assoc -always_and_sep_r'.
by rewrite /vs always_elim impl_elim_r.
......
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