Commit ccd60df8 by Robbert Krebbers

### Some tweaks to `mset`.

```- Make use of the fact that https://gitlab.mpi-sws.org/FP/iris-coq/issues/184
has been fixed.
- Fix indentation.
- Always name hypotheses.
- Make use of `set_solver` to discharge set related stuff.
- Don't import stuff we don't need.```
parent 9a7e1e9c
 From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Import spin_lock assert par. From iris.algebra Require Import frac. From iris.base_logic.lib Require Import fractional. From iris.heap_lang Require Import assert. Section Sets. Fixpoint is_list (hd : val) (xs : list val) : Prop := match xs with | [] => hd = NONEV | x :: xs => ∃ hd', hd = SOMEV (x,hd') ∧ is_list hd' xs end. end. Definition is_set (hd : val) (X : gset val) : Prop := ∃ l : list val, is_list hd l ∧ NoDup l ∧ of_list l ≡ X. ∃ l : list val, is_list hd l ∧ NoDup l ∧ of_list l = X. Definition newset : val := λ: <>, NONEV. ... ... @@ -27,35 +23,28 @@ Section Sets. let: "y" := (Snd "p") in "member" "x" "y" end. Definition set_add : val := λ: "x" "xs", Definition set_add : val := λ: "x" "xs", if: set_member "x" "xs" then assert #false else SOME ("x", "xs"). End Sets. Section MutableSet. Definition is_set_mut `{heapG Σ} (v : val) (X : gset val) : iProp Σ := (∃ (l : loc) hd, ⌜ v = #l ⌝ ∗ l ↦ hd ∗ ⌜ is_set hd X ⌝)%I. Definition mset_create : val := λ: <>, ref (newset #()). Definition mset_member : val := λ: "x" "xs", Definition mset_member : val := λ: "x" "xs", let: "v" := ! "xs" in set_member "x" "v". Definition mset_add : val := λ: "x" "xs", Definition mset_add : val := λ: "x" "xs", let: "v" := ! "xs" in "xs" <- set_add "x" "v". Definition mset_clear : val := λ: "xs", Definition mset_clear : val := λ: "xs", "xs" <- newset #(). End MutableSet. Section Sets_wp. ... ... @@ -64,9 +53,8 @@ Section Sets_wp. Lemma set_newset_spec: {{{ True }}} newset #() {{{ v, RET v; ⌜is_set v ∅⌝ }}}. Proof. iIntros (Φ) "_ H". wp_lam. iApply "H". iExists []. iSimpl. iSplit. done. iSplit. iPureIntro. apply NoDup_nil_2. done. iIntros (Φ) "_ HΦ". wp_lam. iApply "HΦ". iExists []. simpl; eauto using NoDup_nil_2. Qed. Lemma set_member_spec (x: val) (xs: val) (X: gset val): ... ... @@ -74,52 +62,35 @@ Section Sets_wp. set_member x xs {{{ 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. 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. 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]. iIntros (Φ (l & Hl & _ & HX)) "HΦ". iRevert (Hl HX). iInduction l as [|hd tl] "IH" forall (xs X); simpl. - iIntros (-> <-) "/=". do 2 wp_lam. wp_case. wp_seq. rewrite bool_decide_false; last by set_solver. by iApply "HΦ". - iIntros ([hd' [-> Hl]] <-) "/=". do 2 wp_lam. wp_case. wp_let. wp_proj. wp_op. destruct (bool_decide_reflect (hd = x)) as [->|?]; wp_if. + rewrite bool_decide_true; last set_solver. by iApply "HΦ". + wp_proj. wp_let. iApply ("IH" \$! hd' (of_list tl) with "[HΦ] [//] [//]"). iNext; iIntros. case_bool_decide. * case_bool_decide; last by set_solver. by iApply "HPost". * case_bool_decide; first by set_solver. by iApply "HPost". Admitted. * rewrite bool_decide_true; last set_solver. by iApply "HΦ". * rewrite bool_decide_false; last set_solver. by iApply "HΦ". Qed. 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). 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. iIntros (Φ [Hset ?]) "HΦ". do 2 wp_lam. wp_bind (set_member x xs). iApply (set_member_spec _ _ X with "[//]"). iNext. iIntros "_". case_bool_decide; first by set_solver. wp_if. iApply "HΦ". iPureIntro. destruct Hset as (l & Hl & ? & <-). exists (x :: l). split_and!; [|constructor|]; set_solver. Qed. End Sets_wp. Section MutableSet_wp. Context `{heapG Σ}. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!