Commit 55f0efa1 authored by Robbert Krebbers's avatar Robbert Krebbers

Nits.

parent 11719e83
......@@ -114,12 +114,12 @@ Section a_wp_rules.
Qed.
(* Use [IntoVal] everywhere *)
Lemma awp_bind (f e : expr) fv R Φ :
IntoVal f fv
awp e R (λ ev, awp (fv ev) R Φ) -
Lemma awp_bind (f e : expr) R Φ :
AsVal f
awp e R (λ ev, awp (f ev) R Φ) -
awp (a_bind f e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
......
......@@ -37,11 +37,11 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
Definition a_seq : val := λ: <>,
a_atomic_env (λ: "env", mset_clear "env").
Definition a_seq_bind : val := λ: "e1" "e2",
a_bind (λ: "x", a_seq #();;; "e2" "x") "e1".
Definition a_seq_bind : val := λ: "f" "x",
a_bind (λ: "a", a_seq #();;; "f" "a") "x".
Notation "e1 ;;;; e2" :=
(a_seq_bind e1 (λ: <>, e2))%E (at level 80, right associativity).
(a_seq_bind (λ: <>, e2) e1)%E (at level 80, right associativity).
Definition a_if : val := λ: "cnd" "e1" "e2",
a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd".
......@@ -53,7 +53,7 @@ Definition a_while: val :=
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma a_seq_spec R Φ :
Lemma a_seq_spec R Φ :
U (Φ #()) -
awp (a_seq #()) R Φ.
Proof.
......@@ -85,14 +85,13 @@ Section proofs.
{ rewrite -bi.big_sepM_insert_override; eauto. }
Qed.
Lemma a_sequence_spec R Φ (e1 e2 : expr) :
AsVal e2
awp e1 R (λ v, U (awp (e2 v) R Φ)) -
awp (a_seq_bind e1 e2) R Φ.
Lemma a_sequence_spec R Φ (f e : expr) :
AsVal f
awp e R (λ v, U (awp (f v) R Φ)) -
awp (a_seq_bind f e) R Φ.
Proof.
iIntros ([v2 <-%of_to_val]) "H".
awp_apply (a_wp_awp with "H"); iIntros (v) "H".
rewrite /a_seq_bind /=. do 2 awp_lam.
iIntros ([fv <-%of_to_val]) "H". rewrite /a_seq_bind /=. awp_lam.
awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
awp_lam. iApply awp_bind. iApply a_seq_spec.
iModIntro. by awp_lam.
......@@ -100,7 +99,7 @@ Section proofs.
Lemma a_load_spec R Φ Ψ e :
awp e R (λ v, l : loc, v = #l Ψ l) -
( (l : loc), Ψ l - ( v, l U v (l U v - Φ v))) -
( l : loc, Ψ l - v, l U v (l U v - Φ v)) -
awp (a_load e) R Φ.
Proof.
iIntros "H HΦ". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
......@@ -258,13 +257,13 @@ Section proofs.
Qed.
Lemma a_while_spec (cnd bdy : val) R Φ :
awp (a_if (cnd #()) (bdy ;;;; (a_while cnd bdy))) R Φ -
awp (a_if (cnd #()) (bdy ;;;; a_while cnd bdy)) R Φ -
awp (a_while cnd bdy) R Φ.
Proof.
iIntros "HAWP".
rewrite {2}/a_while.
awp_lam. awp_lam.
rewrite /a_while.
iApply "HAWP".
Qed.
Proof.
iIntros "HAWP".
rewrite {2}/a_while.
awp_lam. awp_lam.
rewrite /a_while.
iApply "HAWP".
Qed.
End proofs.
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