Commit bb028004 authored by Léon Gondelman's avatar Léon Gondelman

add a_sequence_spec

parent 5b46218d
......@@ -88,6 +88,15 @@ Section proofs.
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_sequence_spec R (v1 v2: val) Φ :
awp v1 R (λ _, U (awp v2 R Φ)) - awp (a_sequence v1 v2) R Φ.
Proof.
iIntros "HΦ". do 2 awp_lam. iApply awp_bind.
iApply (awp_wand _ (λ _, U (awp v2 R Φ))%I _ _ with "[HΦ]"); first done.
iIntros (v) "H". awp_lam. iApply awp_bind. iApply a_seq_spec.
iUnlock. by awp_pure _.
Qed.
Lemma a_load_spec R (l : loc) (v : val) Φ :
l U v -
(l U v - Φ v) -
......
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