Commit a6bbb1ae authored by Dan Frumin's avatar Dan Frumin

Use set_solver in set_member_spec

parent 1d0a5447
......@@ -69,7 +69,6 @@ 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
......@@ -88,18 +87,15 @@ Section Sets_wp.
wp_case. wp_let. wp_proj.
destruct (decide (hd = x)); simplify_eq /=.
+ 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.
wp_if. assert (x ({[x]} (of_list tl : gset val))) by set_solver.
case_bool_decide; last by exfalso. by iApply "HPost".
+ 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. 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.
* case_bool_decide; last by set_solver. by iApply "HPost".
* case_bool_decide; first by set_solver. by iApply "HPost".
Admitted.
Lemma set_add_spec (x: val) (xs: val) (X: gset val):
......@@ -148,7 +144,7 @@ Section MutableSet_wp.
wp_lam. wp_let. wp_load. wp_let.
iApply (set_member_spec with "[$Hset //]").
iNext. iIntros (v).
iApply ("H" with "[Hset Hs]").
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