Commit 8d8b842a authored by Dan Frumin's avatar Dan Frumin Committed by Robbert Krebbers

Port list.v and mset.v to the latest version of Iris

parent 8cf789c6
......@@ -67,15 +67,18 @@ Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma lcons_spec hd vs v :
{{{ is_list hd vs }}} lcons v hd {{{ hd', RET hd'; is_list hd' (v :: vs) }}}.
Proof. iIntros (Φ ?) "HΦ". do 2 wp_lam. iApply "HΦ". simpl; eauto. Qed.
Proof.
iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
iApply "HΦ". simpl; eauto.
Qed.
Lemma lhead_spec hd vs v :
{{{ is_list hd (v :: vs) }}} lhead hd {{{ RET v; True }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". repeat wp_pure _. by iApply "HΦ". Qed.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ltail_spec hd vs v :
{{{ is_list hd (v :: vs) }}} ltail hd {{{ hd', RET hd'; is_list hd' vs }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". repeat wp_pure _. by iApply "HΦ". Qed.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i hd vs v :
vs !! i = Some v
......@@ -83,8 +86,8 @@ Lemma llookup_spec i hd vs v :
Proof.
iIntros (Hi Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl); destruct i as [|i]=> //; simplify_eq/=.
{ do 2 wp_lam. wp_op; wp_if. by iApply (lhead_spec with "[//]"). }
do 2 wp_lam. wp_op; case_bool_decide=> [//|]. wp_if.
{ wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
wp_lam. wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
......@@ -95,9 +98,9 @@ Lemma linsert_spec i hd vs v :
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ); destruct i as [|i]=> //; simplify_eq/=.
{ do 3 wp_lam. wp_op; wp_if. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
wp_let. by iApply (lcons_spec with "[//]"). }
do 3 wp_lam. wp_op; case_bool_decide=> [//|]. wp_if.
wp_lam; wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
......@@ -110,9 +113,9 @@ Lemma llist_member_spec hd vs v :
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
{ do 2 wp_lam. wp_match. by iApply "HΦ". }
destruct Hl as (hd'&->&?). do 2 wp_lam. wp_match. wp_proj.
wp_op. destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
{ rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". }
wp_proj. wp_let. iApply ("IH" with "[//]"). destruct (bool_decide_reflect (v vs)).
- by rewrite bool_decide_true; last by right.
......@@ -123,10 +126,10 @@ Lemma lreplicate_spec i v :
{{{ True }}} lreplicate #i v {{{ hd, RET hd; is_list hd (replicate i v) }}}.
Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
{ do 2 wp_lam. wp_op; case_bool_decide=> //=; wp_if.
{ wp_lam; wp_pures.
iApply (lnil_spec with "[//]"). iApply "HΦ". }
do 2 wp_lam; wp_op; case_bool_decide=> [//|]; wp_if.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_lam; wp_pures.
rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed.
......
......@@ -39,7 +39,7 @@ Section mset.
{{{ RET #(bool_decide (v X)); is_mset x X }}}.
Proof.
iIntros (<- Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
do 2 wp_lam. wp_load. wp_let.
wp_lam; wp_pures. wp_load. wp_let.
wp_apply (llist_member_spec with "[//]"). iIntros "_".
rewrite (bool_decide_iff _ (v vs)); last set_solver.
iApply "HΦ". iExists l, hd, vs; auto.
......@@ -53,7 +53,7 @@ Section mset.
{{{ RET #(); is_mset x ({[v]} X) }}}.
Proof.
iIntros (<- Φ ?) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
do 2 wp_lam. wp_load. wp_lam. wp_apply wp_assert.
wp_lam. wp_pures. wp_load. wp_let. wp_apply wp_assert.
wp_apply (llist_member_spec with "[//]"); iIntros "_".
rewrite bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
......
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