Commit ab77927c authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 2be948e4 100c75d6
Pipeline #361 passed with stage
......@@ -68,13 +68,13 @@ Proof.
rewrite (own_update); (* FIXME: canonical structures are not working *)
last by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)).
rewrite pvs_frame_l; apply pvs_mono, sep_intro_True_r; eauto with I.
rewrite -later_intro /one_shot_inv -or_intro_r -(exist_intro n).
rewrite /one_shot_inv -or_intro_r -(exist_intro n).
solve_sep_entails.
+ rewrite sep_exist_l; apply exist_elim=>m.
eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
rewrite /= ?to_of_val; eauto with I ndisj; strip_later.
ecancel [l _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
rewrite -later_intro /one_shot_inv -or_intro_r -(exist_intro m).
rewrite /one_shot_inv -or_intro_r -(exist_intro m).
solve_sep_entails.
- apply: always_intro. wp_seq.
wp_focus (Load (%l))%I.
......@@ -92,7 +92,7 @@ Proof.
rewrite !sep_exist_l; apply exist_elim=> w.
eapply wp_load with (q:=1%Qp) (v:=w); eauto with I ndisj.
rewrite -later_intro; cancel [l w]%I.
rewrite -later_intro; apply wand_intro_l; rewrite -later_intro.
rewrite -later_intro; apply wand_intro_l.
trans (heap_ctx heapN inv N (one_shot_inv γ l) one_shot_inv γ l
(w = InjLV #0 ( n : Z, w = InjRV #n own γ (Shot (DecAgree n)))))%I.
{ cancel [heap_ctx heapN]. rewrite !sep_or_l; apply or_elim.
......@@ -130,7 +130,7 @@ Proof.
rewrite (True_intro (heap_ctx heapN)) left_id.
rewrite -own_op own_valid_l one_shot_validI Shot_op /= discrete_valid.
rewrite -assoc. apply const_elim_sep_l=> /dec_agree_op_inv [->].
rewrite dec_agree_idemp -later_intro. apply sep_intro_True_r.
rewrite dec_agree_idemp. apply sep_intro_True_r.
{ rewrite /one_shot_inv -or_intro_r -(exist_intro m). solve_sep_entails. }
wp_case; fold of_val. wp_let. rewrite -wp_assert'.
wp_op; by eauto using later_intro with I.
......
......@@ -55,12 +55,13 @@ Lemma inv_fsa_timeless {A} (fsa : FSA Λ Σ A)
`{!FrameShiftAssertion fsaV fsa} E N P `{!TimelessP P} Ψ R :
fsaV nclose N E
R inv N P
R (P - fsa (E nclose N) (λ a, P Ψ a))
R (P - fsa (E nclose N) (λ a, P Ψ a))
R fsa E Ψ.
Proof.
intros ??? HR. eapply inv_fsa, wand_intro_l; eauto.
trans (|={E N}=> P R)%I; first by rewrite pvs_timeless pvs_frame_r.
apply (fsa_strip_pvs _). by rewrite HR wand_elim_r.
apply (fsa_strip_pvs _). rewrite HR wand_elim_r.
apply: fsa_mono=> v. by rewrite -later_intro.
Qed.
(* Derive the concrete forms for pvs and wp, because they are useful. *)
......@@ -74,7 +75,7 @@ Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
Lemma pvs_inv_timeless E N P `{!TimelessP P} Q R :
nclose N E
R inv N P
R (P - |={E nclose N}=> ( P Q))
R (P - |={E nclose N}=> (P Q))
R (|={E}=> Q).
Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
......@@ -87,7 +88,7 @@ Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
atomic e nclose N E
R inv N P
R (P - WP e @ E nclose N {{ λ v, P Φ v }})
R (P - WP e @ E nclose N {{ λ v, P Φ v }})
R WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). 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