Commit ff6cc208 authored by Dan Frumin's avatar Dan Frumin

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

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