Commit 3b81f7bf authored by Léon Gondelman's avatar Léon Gondelman

add wp_if_true wp_if_false rules

parent 90da10c1
......@@ -13,7 +13,7 @@ Section lifting.
awp (λ: <> <>, ve) R Φ.
Proof.
intros ?. rewrite -(of_to_val ve v); last done.
iIntros "HΦ". rewrite /awp.
iIntros "HΦ". rewrite /awp. wp_value_head.
iIntros (γ π env lk) "Hfl Hunfl".
do 2 wp_rec. by iFrame.
Qed.
......@@ -25,16 +25,10 @@ Section lifting.
awp (fill K e1) R Φ.
Proof.
iIntros (? Hφ) "Hawp".
rewrite /awp. iIntros (γ π env l) "#Hflock Hunfl".
replace ((fill K e1) env l) with (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]) e1); last first.
{ by rewrite fill_app. }
iApply (wp_bind (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]))).
wp_pure e1.
iSpecialize ("Hawp" with "Hflock Hunfl").
replace ((fill K e2) env l) with (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]) e2); last first.
{ by rewrite fill_app. }
rewrite (wp_bind_inv (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]))).
by iApply "Hawp".
rewrite /awp.
wp_pure _.
done.
Qed.
Lemma awp_ctx_bind (v1 v2 : val) (e1 e2 : expr) R Φ :
......@@ -57,4 +51,3 @@ Section lifting.
End lifting.
Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).
......@@ -39,9 +39,7 @@ Definition a_seq : val := λ: "env",
a_atomic_env (λ: "env", mset_clear "env") "env".
Definition a_sequence : val := λ: "e1" "e2",
a_bind (λ: <>,
a_bind (λ: <>, (a_bind (λ: "v", a_ret "v") "e2")) a_seq
) "e1".
a_bind (λ: <>, a_bind (λ: <>, "e2") a_seq) "e1".
Definition a_if : val := λ: "cnd" "e1" "e2",
a_bind (λ: "c", if: "c" then "e1" else "e2") "cnd".
......@@ -49,10 +47,10 @@ Definition a_if : val := λ: "cnd" "e1" "e2",
Definition a_while: val := λ: "cond" "body",
let: "rwhile" :=
rec: "while" "cnd" "bdy" :=
a_if "cnd"
(a_sequence "bdy"
(λ: "env" "l", ("while" "cnd" "bdy") "env" "l"))
(a_ret #())
λ: "env" "l",
(a_if "cnd"
(a_sequence "bdy" ("while" "cnd" "bdy"))
(a_ret #())) "env" "l"
in "rwhile" "cond" "body".
Section proofs.
......@@ -207,4 +205,26 @@ Section proofs.
- iApply "HΦ". iFrame.
Qed.
Lemma a_if_true_spec `{Timeless _ R} (e1 e2 : val) Φ :
awp e1 R Φ - awp (a_if (a_ret #true) e1 e2) R Φ.
Proof.
unfold a_if. iIntros "HΦ".
rewrite /a_ret.
repeat awp_pure _.
rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
repeat (wp_pure _).
by iApply ("HΦ" with "Hflock Hunfl").
Qed.
Lemma a_if_false_spec `{Timeless _ R} (e1 e2 : val) Φ :
awp e2 R Φ - awp (a_if (a_ret #false) e1 e2) R Φ.
Proof.
unfold a_if. iIntros "HΦ".
rewrite /a_ret.
repeat awp_pure _.
rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
repeat (wp_pure _).
by iApply ("HΦ" with "Hflock Hunfl").
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