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

improving spec of set_member and mset_member using bool_decide (x in X)

parent e805705f
......@@ -69,55 +69,56 @@ Section Sets_wp.
iSplit. iPureIntro. apply NoDup_nil_2. done.
Qed.
(*(⌜v = #true⌝ ∧ ⌜x ∈ X⌝) ∨ (⌜v = #false⌝ ∧ ⌜x ∉ X⌝)*)
Lemma set_member_spec (x: val) (xs: val) (X: gset val):
{{{ is_set xs X }}}
set_member x xs
{{{ v, RET v;
(v = #true x X) (v = #false x X) }}}.
{{{ RET #(bool_decide (x X)); True }}}.
Proof.
iIntros (Φ) "% HPost".
unfold is_set in a.
destruct a as [l [HL [HDup HX]]].
iRevert (HL HX). iInduction l as [|hd tl] "IH" forall (xs X);
iIntros "% %"; simpl in a; subst; do 2 wp_lam.
- wp_case. wp_seq. iApply "HPost". iRight.
simplify_eq. done.
- wp_case. wp_seq.
rewrite of_list_nil in a0. apply leibniz_equiv in a0; subst.
case_bool_decide; first inversion H0. by iApply "HPost".
- destruct a as [hd' [HXs HL]].
rewrite of_list_cons in a0; simplify_eq /=.
wp_case. wp_let. wp_proj.
destruct (decide (hd = x)); simplify_eq /=.
+ assert (BinOp EqOp x x = #true) as ->. admit.
wp_if. iApply "HPost". iLeft. iSplit; first done.
iPureIntro. set_solver.
+ assert (BinOp EqOp x x = #true) as ->. admit.
wp_if. case_bool_decide. iApply "HPost". done.
destruct H0. by apply elem_of_union_l, elem_of_singleton_2.
+ assert (BinOp EqOp hd x = #false) as ->. admit.
wp_if. wp_proj. wp_let. apply NoDup_cons_12 in HDup.
iApply ("IH" $! _ hd' (of_list tl) with "[HPost]");
[| done| done].
iNext; iIntros; iApply "HPost";
destruct a; iPureIntro; destruct H0; set_solver.
iNext; iIntros. case_bool_decide.
* apply elem_of_union in H0. destruct H0.
** destruct n. by apply elem_of_singleton_1 in H0.
** case_bool_decide; by [iApply "HPost" | destruct H1].
* case_bool_decide; last by iApply "HPost".
apply not_elem_of_union in H0. destruct H0. by destruct H2.
Admitted.
Lemma set_add_spec (x: val) (xs: val) (X: gset val):
{{{ is_set xs X x X }}}
set_add x xs
{{{ v, RET v;
(is_set v ({[x]} X) )}}}.
{{{ v, RET v; (is_set v ({[x]} X) )}}}.
Proof.
iIntros (Φ) "[% %] HPost".
do 2 wp_lam.
wp_bind ((set_member x) xs).
iApply (set_member_spec _ _ X); first done.
iNext. iIntros (v) "[[% %]|[% %]]".
simplify_eq /=.
- by destruct H1.
- simplify_eq. wp_if. iApply "HPost".
destruct H0 as [l [HL [HD HX]]].
unfold is_set; simplify_eq.
iPureIntro. exists (x :: l).
split. simpl. exists xs. done.
split. apply NoDup_cons_2.
by apply not_elem_of_of_list in H1.
done. done.
iNext. iIntros (v). case_bool_decide; first by destruct H1.
wp_if. iApply "HPost".
destruct H0 as [l [HL [HD HX]]].
unfold is_set; simplify_eq.
iPureIntro. exists (x :: l).
split. simpl. exists xs. done.
split. apply NoDup_cons_2. by apply not_elem_of_of_list in H1.
done. done.
Qed.
End Sets_wp.
......@@ -140,15 +141,14 @@ Section MutableSet_wp.
Lemma mset_member_spec (x: val) (xs: val) (X: gset val):
{{{ is_set_mut xs X }}}
mset_member x xs
{{{ v, RET v; is_set_mut xs X
((v = #true x X) (v = #false x X)) }}}.
{{{ RET #(bool_decide (x X)); is_set_mut xs X }}}.
Proof.
iIntros (Φ) "Hmut H".
iDestruct "Hmut" as (s hd) "[% [Hs #Hset]]"; subst .
wp_lam. wp_let. wp_load. wp_let.
iApply (set_member_spec with "[$Hset //]").
iNext. iIntros (v) "%".
iApply ("H" $! _). iSplit; last done.
iNext. iIntros (v).
iApply ("H" with "[Hset Hs]").
iExists s, hd. eauto.
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