From f5e2db760e42570bb412e1a93b32cb1b796a3d4f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Jul 2019 19:40:26 +0200
Subject: [PATCH] Make the `list` stuff simpler since we don't really use
`val_encode` anymore.
---
_CoqProject | 1 -
{theories/utils => experimental}/encodable.v | 0
.../producer_consumer.v | 9 +-
theories/channel/channel.v | 4 +-
theories/examples/mapper.v | 17 +-
theories/examples/sort.v | 32 +--
theories/examples/sort_client.v | 16 +-
theories/examples/sort_elem_client.v | 10 +-
theories/utils/list.v | 222 ++++++------------
9 files changed, 117 insertions(+), 194 deletions(-)
rename {theories/utils => experimental}/encodable.v (100%)
rename {theories/examples => experimental}/producer_consumer.v (95%)
diff --git a/_CoqProject b/_CoqProject
index 0116ae5..7961f39 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,6 @@
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/utils/auth_excl.v
-theories/utils/encodable.v
theories/utils/list.v
theories/utils/compare.v
theories/utils/spin_lock.v
diff --git a/theories/utils/encodable.v b/experimental/encodable.v
similarity index 100%
rename from theories/utils/encodable.v
rename to experimental/encodable.v
diff --git a/theories/examples/producer_consumer.v b/experimental/producer_consumer.v
similarity index 95%
rename from theories/examples/producer_consumer.v
rename to experimental/producer_consumer.v
index e0efb05..ed3d4d8 100644
--- a/theories/examples/producer_consumer.v
+++ b/experimental/producer_consumer.v
@@ -4,10 +4,8 @@ From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
From osiris.utils Require Import list compare spin_lock.
-Definition qnew : val := λ: <>, #().
Definition qenqueue : val := λ: "q" "v", #().
Definition qdequeue : val := λ: "q", #().
-Definition qis_empty : val := λ: "q", #().
Definition enq := true.
Definition deq := false.
@@ -23,10 +21,11 @@ Definition pd_loop : val :=
if: "cc" ≤ #0 then #() else
if: recv "c" then (* enq/deq *)
if: recv "c" then (* cont/stop *)
- "go" (qenqueue "q" (recv "c")) "pc" "cc" "c"
+ let: "x" := recv "x" in
+ "go" (qenqueue "q" "x") "pc" "cc" "c"
else "go" "q" ("pc"-#1) "cc" "c"
else
- if: (qis_empty "q") then
+ if: lisnil "q" then
if: "pc" ≤ #0 then
send "c" #stop;;
"go" "q" "pc" ("cc"-#1) "c"
@@ -40,7 +39,7 @@ Definition pd_loop : val :=
"go" (Fst "qv") "pc" "cc" "c".
Definition new_pd : val := λ: "pc" "cc",
- let: "q" := qnew #() in
+ let: "q" := lnil #() in
let: "c" := start_chan (λ: "c", pd_loop "q" "pc" "cc" "c") in
let: "l" := new_lock #() in
("c", "l").
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index a6acf89..c2e7096 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -56,7 +56,7 @@ Section channel.
Context `{!heapG Σ, !chanG Σ} (N : namespace).
Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
- (∃ l' : loc, ⌜l = #l'⌠∧ l' ↦ val_encode xs)%I.
+ (∃ l' : loc, ⌜l = #l'⌠∧ l' ↦ llist xs)%I.
Record chan_name := Chan_name {
chan_lock_name : gname;
@@ -139,7 +139,7 @@ Section channel.
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
wp_load.
- wp_apply (lsnoc_spec (A:=val))=> //; iIntros (_).
+ wp_apply (lsnoc_spec with "[//]"); iIntros (_).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
diff --git a/theories/examples/mapper.v b/theories/examples/mapper.v
index 411d385..c3b3c96 100644
--- a/theories/examples/mapper.v
+++ b/theories/examples/mapper.v
@@ -140,8 +140,8 @@ Section mapper.
c ↣ mapper_protocol n (X_send : gmultiset A) @ N ∗
([∗ list] x;v ∈ xs;vs, IA x v) ∗ ([∗ list] x;w ∈ xs_recv;ws, IB (f x) w)
}}}
- mapper_service_loop #n c (val_encode vs) (val_encode ws)
- {{{ ys ws, RET (val_encode ws);
+ mapper_service_loop #n c (llist vs) (llist ws)
+ {{{ ys ws, RET (llist ws);
⌜ys ≡ₚ f <$> elements X_send ++ xs⌠∗
[∗ list] y;w ∈ ys ++ (f <$> xs_recv);ws, IB y w
}}}.
@@ -152,20 +152,20 @@ Section mapper.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []); simpl. rewrite big_sepL2_fmap_l. auto. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
- - wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+ - wp_apply (lisnil_spec with "[//]"); iIntros (_).
destruct vs as [|v vs], xs as [|x xs]; csimpl; try done; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" with "[] Hc [//] [$] HΦ"). iPureIntro; naive_solver.
+ iDestruct "HIA" as "[HIAx HIA]". wp_select.
- wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lhead_spec with "[//]"); iIntros (_).
wp_send with "[$HIAx]".
- wp_apply (ltail_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (ltail_spec with "[//]"); iIntros (_).
wp_apply ("IH" with "[] Hc HIA HIB"); first done.
iIntros (ys ws').
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton -!assoc_L.
iApply "HΦ".
- wp_recv (x w) as (HH) "HIBfx".
- wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lcons_spec with "[//]"); iIntros (_).
wp_apply ("IH" $! _ _ _ _ _ (_ :: _) with "[] Hc HIA [HIBfx HIB]"); first done.
{ simpl; iFrame. }
iIntros (ys ws'); iDestruct 1 as (Hys) "HIB"; simplify_eq/=.
@@ -182,9 +182,8 @@ Section mapper.
0 < n →
(∀ x v, {{{ IA x v }}} ff v {{{ w, RET w; IB (f x) w }}}) -∗
{{{ [∗ list] x;v ∈ xs;vs, IA x v }}}
- mapper_service #n ff (val_encode vs)
- {{{ ys ws, RET (val_encode ws); ⌜ys ≡ₚ f <$> xs⌠∗
- [∗ list] y;w ∈ ys;ws, IB y w }}}.
+ mapper_service #n ff (llist vs)
+ {{{ ys ws, RET (llist ws); ⌜ys ≡ₚ f <$> xs⌠∗ [∗ list] y;w ∈ ys;ws, IB y w }}}.
Proof.
iIntros (?) "#Hf !>"; iIntros (Φ) "HI HΦ". wp_lam; wp_pures.
wp_apply (new_lock_spec N with "[//]"); iIntros (lk) "[Hu Hlk]".
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index ce043c8..99f16b1 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -43,42 +43,42 @@ Section sort.
`{!RelDecision R, !Total R} (cmp : val),
MSG cmp {{ cmp_spec I R cmp }};
<!> (xs : list A) (l : loc) (vs : list val),
- MSG #l {{ l ↦ val_encode vs ∗ [∗ list] x;v ∈ xs;vs, I x v }};
+ MSG #l {{ l ↦ llist vs ∗ [∗ list] x;v ∈ xs;vs, I x v }};
<?> (xs' : list A) (vs' : list val),
MSG #() {{ ⌜ Sorted R xs' ⌠∗ ⌜ xs' ≡ₚ xs ⌠∗
- l ↦ val_encode vs' ∗ [∗ list] x;v ∈ xs';vs', I x v }};
+ l ↦ llist vs' ∗ [∗ list] x;v ∈ xs';vs', I x v }};
END)%proto.
Lemma lmerge_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
`{!RelDecision R, !Total R} (cmp : val) xs1 xs2 vs1 vs2 :
cmp_spec I R cmp -∗
{{{ ([∗ list] x;v ∈ xs1;vs1, I x v) ∗ ([∗ list] x;v ∈ xs2;vs2, I x v) }}}
- lmerge cmp (val_encode vs1) (val_encode vs2)
- {{{ ws, RET val_encode ws; [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
+ lmerge cmp (llist vs1) (llist vs2)
+ {{{ ws, RET llist ws; [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
Proof.
iIntros "#Hcmp" (Ψ) "!> [HI1 HI2] HΨ". iLöb as "IH" forall (xs1 xs2 vs1 vs2 Ψ).
- wp_lam. wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+ wp_lam. wp_apply (lisnil_spec with "[//]"); iIntros (_).
destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; done || wp_pures.
{ iApply "HΨ". by rewrite list_merge_nil_l. }
- wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lisnil_spec with "[//]"); iIntros (_).
destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; done || wp_pures.
{ iApply "HΨ". iFrame. }
- wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
- wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lhead_spec with "[//]"); iIntros (_).
+ wp_apply (lhead_spec with "[//]"); iIntros (_).
iDestruct "HI1" as "[HI1 HI1']"; iDestruct "HI2" as "[HI2 HI2']".
wp_apply ("Hcmp" with "[$HI1 $HI2]"); iIntros "[HI1 HI2]".
case_bool_decide; wp_pures.
- rewrite decide_True //.
- wp_apply (ltail_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (ltail_spec with "[//]"); iIntros (_).
wp_apply ("IH" $! _ (x2 :: _) with "HI1'[HI2 HI2']"); [simpl; iFrame|].
iIntros (ws) "HI".
- wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lcons_spec with "[//]"); iIntros (_).
iApply "HΨ". iFrame.
- rewrite decide_False //.
- wp_apply (ltail_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (ltail_spec with "[//]"); iIntros (_).
wp_apply ("IH" $! (x1 :: _) with "[HI1 HI1'] HI2'"); [simpl; iFrame|].
iIntros (ws) "HI".
- wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lcons_spec with "[//]"); iIntros (_).
iApply "HΨ". iFrame.
Qed.
@@ -91,13 +91,13 @@ Section sort.
wp_lam.
wp_recv (A I R ?? cmp) as "#Hcmp".
wp_recv (xs l vs) as "[Hl HI]".
- wp_load. wp_apply (llength_spec (A:=val) with "[//]"); iIntros (_).
+ wp_load. wp_apply (llength_spec with "[//]"); iIntros (_).
iDestruct (big_sepL2_length with "HI") as %<-.
wp_op; case_bool_decide as Hlen; wp_if.
{ assert (Sorted R xs).
{ destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
wp_send with "[$Hl $HI]"; first by auto. by iApply "HΨ". }
- wp_load. wp_apply (lsplit_spec (A:=val) with "[//]"); iIntros (vs1 vs2 <-).
+ wp_load. wp_apply (lsplit_spec with "[//]"); iIntros (vs1 vs2 ->).
wp_alloc l1 as "Hl1"; wp_alloc l2 as "Hl2".
iDestruct (big_sepL2_app_inv_r with "HI") as (xs1 xs2 ->) "[HI1 HI2]".
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (cy) "Hcy".
@@ -125,10 +125,10 @@ Section sort.
Lemma sort_client_spec {A} (I : A → val → iProp Σ) R
`{!RelDecision R, !Total R} cmp l (vs : list val) (xs : list A) :
cmp_spec I R cmp -∗
- {{{ l ↦ val_encode vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
+ {{{ l ↦ llist vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
sort_client cmp #l
{{{ ys ws, RET #(); ⌜Sorted R ys⌠∗ ⌜ys ≡ₚ xs⌠∗
- l ↦ val_encode ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
+ l ↦ llist ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
diff --git a/theories/examples/sort_client.v b/theories/examples/sort_client.v
index e52de6d..49416b6 100644
--- a/theories/examples/sort_client.v
+++ b/theories/examples/sort_client.v
@@ -7,27 +7,21 @@ From osiris.examples Require Import sort.
Section sort_client.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
- Local Arguments val_encode _ _ !_ /.
-
Lemma sort_client_le_spec l (xs : list Z) :
- {{{ l ↦ val_encode xs }}}
+ {{{ l ↦ llist (LitV ∘ LitInt <$> xs) }}}
sort_client cmpZ #l
- {{{ ys, RET #(); ⌜Sorted (≤) ys⌠∗ ⌜ ys ≡ₚ xs⌠∗ l ↦ val_encode ys }}}.
+ {{{ ys, RET #(); ⌜Sorted (≤) ys⌠∗ ⌜ ys ≡ₚ xs⌠∗ l ↦ llist (LitV ∘ LitInt <$> ys) }}}.
Proof.
- assert (∀ zs : list Z, val_encode zs = val_encode (LitV ∘ LitInt <$> zs)) as Henc.
- { intros zs. induction zs; f_equal/=; auto with f_equal. }
iIntros (Φ) "Hl HΦ".
iApply (sort_client_spec N IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
{ iApply cmpZ_spec. }
- { rewrite -Henc. iFrame "Hl".
- iInduction xs as [|x xs] "IH"; csimpl; first by iFrame.
- by iFrame "IH". }
+ { iFrame "Hl". iInduction xs as [|x xs] "IH"; csimpl; by iFrame "#". }
iIntros "!>" (ys ws) "(?&?&?&HI)".
iAssert ⌜ ws = (LitV ∘ LitInt) <$> ys âŒ%I with "[HI]" as %->.
{ iInduction ys as [|y ys] "IH" forall (ws);
- destruct ws as [|w ws]; csimpl; try done.
+ destruct ws as [|w ws]; csimpl; try done.
iDestruct "HI" as "[-> HI2]".
by iDestruct ("IH" with "HI2") as %->. }
- rewrite -Henc. iApply ("HΦ" $! ys with "[$]").
+ iApply ("HΦ" $! ys with "[$]").
Qed.
End sort_client.
diff --git a/theories/examples/sort_elem_client.v b/theories/examples/sort_elem_client.v
index 28f384c..073f59e 100644
--- a/theories/examples/sort_elem_client.v
+++ b/theories/examples/sort_elem_client.v
@@ -31,7 +31,7 @@ Section sort_elem_client.
Lemma send_all_spec c p xs' xs vs :
{{{ c ↣ sort_elem_head_protocol I R xs' <++> p @ N ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
- send_all c (val_encode vs)
+ send_all c (llist vs)
{{{ RET #(); c ↣ sort_elem_tail_protocol I R (xs' ++ xs) [] <++> p @ N }}}.
Proof.
iIntros (Φ) "[Hc HI] HΦ".
@@ -46,7 +46,7 @@ Section sort_elem_client.
Sorted R ys' →
{{{ c ↣ sort_elem_tail_protocol I R xs ys' <++> p @ N }}}
recv_all c
- {{{ ys ws, RET (val_encode ws);
+ {{{ ys ws, RET (llist ws);
⌜Sorted R (ys' ++ ys)⌠∗ ⌜ys' ++ ys ≡ₚ xs⌠∗
c ↣ p @ N ∗ [∗ list] y;w ∈ ys;ws, I y w
}}}.
@@ -57,7 +57,7 @@ Section sort_elem_client.
- wp_recv (y v) as (Htl) "HIxv".
wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
iIntros (ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "[Hc HI]".
- wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
+ wp_apply (lcons_spec with "[//]"); iIntros (_).
iApply ("HΦ" $! (y :: ys)). simpl; iFrame; auto.
- wp_apply (lnil_spec with "[//]"); iIntros (_).
iApply ("HΦ" $! [] []); rewrite /= right_id_L; by iFrame.
@@ -66,8 +66,8 @@ Section sort_elem_client.
Lemma sort_client_spec cmp vs xs :
cmp_spec I R cmp -∗
{{{ [∗ list] x;v ∈ xs;vs, I x v }}}
- sort_elem_client cmp (val_encode vs)
- {{{ ys ws, RET (val_encode ws); ⌜Sorted R ys⌠∗ ⌜ys ≡ₚ xs⌠∗
+ sort_elem_client cmp (llist vs)
+ {{{ ys ws, RET (llist ws); ⌜Sorted R ys⌠∗ ⌜ys ≡ₚ xs⌠∗
[∗ list] y;w ∈ ys;ws, I y w }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "HI HΦ". wp_lam.
diff --git a/theories/utils/list.v b/theories/utils/list.v
index 4d0702e..1767faa 100644
--- a/theories/utils/list.v
+++ b/theories/utils/list.v
@@ -1,15 +1,13 @@
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.
-From osiris.utils Require Export encodable.
(** Immutable ML-style functional lists *)
-Instance list_val_enc `{ValEnc A} : ValEnc (list A) :=
- fix go xs :=
- let _ : ValEnc _ := @go in
- match xs with
- | [] => val_encode None
- | x :: xs => val_encode (Some (x,xs))
- end.
+Fixpoint llist (vs : list val) : val :=
+ match vs with
+ | [] => NONEV
+ | v :: vs => SOMEV (v,llist vs)
+ end%V.
+Arguments llist : simpl never.
Definition lnil : val := λ: <>, NONEV.
Definition lcons : val := λ: "x" "l", SOME ("x", "l").
@@ -49,15 +47,6 @@ Definition lreplicate : val :=
if: "n" = #0 then lnil #() else
let: "l" := "go" ("n" - #1) "x" in lcons "x" "l".
-Definition llist_member : val :=
- rec: "go" "x" "l" :=
- match: "l" with
- NONE => #false
- | SOME "p" =>
- if: Fst "p" = "x" then #true
- else let: "l" := (Snd "p") in "go" "x" "l"
- end.
-
Definition llength : val :=
rec: "go" "l" :=
match: "l" with
@@ -97,195 +86,138 @@ Definition lsplit : val :=
λ: "l", lsplit_at "l" ((llength "l") `quot` #2).
Section lists.
-Context `{heapG Σ} `{ValEncDec A}.
+Context `{heapG Σ}.
Implicit Types i : nat.
-Implicit Types x : A.
-Implicit Types xs : list A.
+Implicit Types v : val.
+Implicit Types vs : list val.
Lemma lnil_spec :
- {{{ True }}} lnil #() {{{ RET val_encode []; True }}}.
+ {{{ True }}} lnil #() {{{ RET llist []; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
-Lemma lcons_spec x xs :
- {{{ True }}}
- lcons (val_encode x) (val_encode xs)
- {{{ RET val_encode (x :: xs); True }}}.
+Lemma lcons_spec v vs :
+ {{{ True }}} lcons v (llist vs) {{{ RET llist (v :: vs); True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-Lemma lisnil_spec xs:
+Lemma lisnil_spec vs:
{{{ True }}}
- lisnil (val_encode xs)
- {{{ RET #(if xs is [] then true else false); True }}}.
-Proof. iIntros (Φ _) "HΦ". wp_lam. destruct xs; wp_pures; by iApply "HΦ". Qed.
+ lisnil (llist vs)
+ {{{ RET #(if vs is [] then true else false); True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. destruct vs; wp_pures; by iApply "HΦ". Qed.
-Lemma lhead_spec x xs:
- {{{ True }}} lhead (val_encode (x::xs)) {{{ RET val_encode x; True }}}.
+Lemma lhead_spec v vs :
+ {{{ True }}} lhead (llist (v :: vs)) {{{ RET v; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-Lemma ltail_spec x xs :
- {{{ True }}} ltail (val_encode (x::xs)) {{{ RET val_encode xs; True }}}.
+Lemma ltail_spec v vs :
+ {{{ True }}} ltail (llist (v :: vs)) {{{ RET llist vs; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-Lemma llookup_spec i xs x:
- xs !! i = Some x →
- {{{ True }}}
- llookup #i (val_encode xs)
- {{{ RET val_encode x; True }}}.
+Lemma llookup_spec i vs v :
+ vs !! i = Some v →
+ {{{ True }}} llookup #i (llist vs) {{{ RET v; True }}}.
Proof.
- iIntros (Hi Φ Hl) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (i Hi Hl);
+ iIntros (Hi Φ _) "HΦ".
+ iInduction vs as [|v' vs] "IH" forall (i Hi);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
wp_lam. wp_pures.
- wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
+ wp_apply (ltail_spec with "[//]"); iIntros (_). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
-Lemma linsert_spec i xs x :
- is_Some (xs !! i) →
- {{{ True }}}
- linsert #i (val_encode x) (val_encode xs)
- {{{ RET val_encode (<[i:=x]>xs); True }}}.
+Lemma linsert_spec i vs v :
+ is_Some (vs !! i) →
+ {{{ True }}} linsert #i v (llist vs) {{{ RET llist (<[i:=v]>vs); True }}}.
Proof.
- iIntros ([w Hi] Φ Hl) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
+ iIntros ([w Hi] Φ _) "HΦ".
+ iInduction vs as [|v' vs] "IH" forall (i Hi Φ);
destruct i as [|i]=> //; simplify_eq/=.
- { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (?).
+ { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"); iIntros (_).
wp_let. by iApply (lcons_spec with "[//]"). }
wp_lam; wp_pures.
- wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
+ wp_apply (ltail_spec with "[//]"); iIntros (_). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
- wp_apply ("IH" with "[//] [//]"). iIntros (?). wp_let.
+ wp_apply ("IH" with "[//]"); iIntros (_).
wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]").
Qed.
-(*
-Lemma llist_member_spec `{EqDecision A} (xs : list A) (x : A) :
- {{{ True }}}
- llist_member (val_encode x) (val_encode xs)
- {{{ RET #(bool_decide (x ∈ xs)); True }}}.
-Proof.
- iIntros (Φ Hl) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=.
- { wp_lam; wp_pures. by iApply "HΦ". }
- wp_lam; wp_pures.
- destruct (bool_decide_reflect (val_encode x' = val_encode x)); simplify_eq/=; wp_if.
- { rewrite (bool_decide_true (_ ∈ _ :: _)); last by left. by iApply "HΦ". }
- wp_proj. wp_let. iApply ("IH" with "[//]").
- destruct (bool_decide_reflect (x ∈ xs)).
- - by rewrite bool_decide_true; last by right.
- - by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
-Qed.
-*)
-
-Lemma lreplicate_spec i x :
- {{{ True }}}
- lreplicate #i (val_encode x)
- {{{ RET val_encode (replicate i x); True }}}.
+Lemma lreplicate_spec i v :
+ {{{ True }}} lreplicate #i v {{{ RET llist (replicate i v); True }}}.
Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
- { wp_lam; wp_pures.
- iApply (lnil_spec with "[//]"). iApply "HΦ". }
+ { wp_lam; wp_pures. iApply (lnil_spec with "[//]"); auto. }
wp_lam; wp_pures.
rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
- wp_apply "IH"; iIntros (Hl). wp_let. by iApply (lcons_spec with "[//]").
+ wp_apply "IH"; iIntros (_). wp_let. by iApply (lcons_spec with "[//]").
Qed.
-Lemma llength_spec xs :
- {{{ True }}} llength (val_encode xs) {{{ RET #(length xs); True }}}.
+Lemma llength_spec vs :
+ {{{ True }}} llength (llist vs) {{{ RET #(length vs); True }}}.
Proof.
- iIntros (Φ Hl) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (Hl Φ); simplify_eq/=.
+ iIntros (Φ _) "HΦ".
+ iInduction vs as [|v' vs] "IH" forall (Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". }
wp_lam. wp_match. wp_proj.
- wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
+ wp_apply "IH"; iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
-Lemma lsnoc_spec xs x :
- {{{ True }}}
- lsnoc (val_encode xs) (val_encode x)
- {{{ RET (val_encode (xs++[x])); True }}}.
+Lemma lsnoc_spec vs v :
+ {{{ True }}} lsnoc (llist vs) v {{{ RET (llist (vs ++ [v])); True }}}.
Proof.
iIntros (Φ _) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (Φ).
+ iInduction vs as [|v' vs] "IH" forall (Φ).
{ wp_rec. wp_pures. wp_lam. wp_pures. by iApply "HΦ". }
- wp_rec.
- wp_apply "IH"=> //.
- iIntros (_). by wp_apply lcons_spec=> //.
+ wp_rec. wp_apply "IH"; iIntros (_). by wp_apply lcons_spec=> //.
Qed.
-Lemma ltake_spec xs (n:Z) :
- {{{ True }}}
- ltake (val_encode xs) #n
- {{{ RET val_encode (take (Z.to_nat n) xs); True }}}.
+Lemma ltake_spec vs (n : nat) :
+ {{{ True }}} ltake (llist vs) #n {{{ RET llist (take n vs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (n Φ).
- - wp_rec. wp_pures. destruct (bool_decide (n ≤ 0)); wp_pures;
- rewrite take_nil; by iApply "HΦ".
+ iInduction vs as [|x' vs] "IH" forall (n Φ).
- wp_rec. wp_pures.
- destruct (decide (n ≤ 0)).
- + rewrite bool_decide_true=> //. wp_pures.
- rewrite Z_to_nat_nonpos=> //.
- rewrite firstn_O. by iApply "HΦ".
- + rewrite bool_decide_false=> //.
- wp_apply ("IH"); iIntros (_).
- wp_apply (lcons_spec)=> //; iIntros (_).
- rewrite -firstn_cons.
- rewrite -Z2Nat.inj_succ; last lia.
- rewrite Z.succ_pred.
- by iApply "HΦ".
+ destruct (bool_decide (n ≤ 0)); wp_pures; rewrite take_nil; by iApply "HΦ".
+ - wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
+ rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
+ wp_apply "IH"; iIntros (_).
+ wp_apply (lcons_spec with "[//]"); iIntros (_). by iApply "HΦ".
Qed.
-Lemma ldrop_spec xs (n:Z) :
- {{{ True }}}
- ldrop (val_encode xs) #n
- {{{ RET val_encode (drop (Z.to_nat n) xs); True }}}.
+Lemma ldrop_spec vs (n : nat) :
+ {{{ True }}} ldrop (llist vs) #n {{{ RET llist (drop n vs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
- iInduction xs as [|x' xs] "IH" forall (n Φ).
- - wp_rec.
- wp_pures. destruct (bool_decide (n ≤ 0)); wp_pures;
- rewrite drop_nil; by iApply "HΦ".
+ iInduction vs as [|x' vs] "IH" forall (n Φ).
- wp_rec. wp_pures.
- destruct (decide (n ≤ 0)).
- + rewrite bool_decide_true=> //. wp_pures.
- rewrite Z_to_nat_nonpos=> //. rewrite drop_0.
- by iApply "HΦ".
- + rewrite bool_decide_false=> //.
- wp_apply "IH"; iIntros (_).
- rewrite -{1}(Z.succ_pred n) Z2Nat.inj_succ /= -Z.sub_1_r; last lia.
- by iApply "HΦ".
+ destruct (bool_decide (n ≤ 0)); wp_pures; rewrite drop_nil; by iApply "HΦ".
+ - wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
+ rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
+ wp_apply "IH"; iIntros (_). by iApply "HΦ".
Qed.
-Lemma lsplit_at_spec xs n :
+Lemma lsplit_at_spec vs (n : nat) :
{{{ True }}}
- lsplit_at (val_encode (xs)) #n
- {{{ RET val_encode (val_encode (take (Z.to_nat n) xs),
- val_encode (drop (Z.to_nat n) xs)); True }}}.
+ lsplit_at (llist vs) #n
+ {{{ RET (llist (take n vs), llist (drop n vs)); True }}}.
Proof.
- iIntros (Φ _) "HΦ".
- wp_lam.
- wp_apply (ldrop_spec)=> //; iIntros (_).
- wp_apply (ltake_spec)=> //; iIntros (_).
- wp_pures.
- by iApply "HΦ".
+ iIntros (Φ _) "HΦ". wp_lam.
+ wp_apply (ldrop_spec with "[//]"); iIntros (_).
+ wp_apply (ltake_spec with "[//]"); iIntros (_).
+ wp_pures. by iApply "HΦ".
Qed.
-Lemma lsplit_spec xs :
+Lemma lsplit_spec vs :
{{{ True }}}
- lsplit (val_encode xs)
- {{{ ys zs, RET (val_encode ys, val_encode zs); ⌜ ys++zs = xs ⌠}}}.
+ lsplit (llist vs)
+ {{{ ws1 ws2, RET (llist ws1, llist ws2); ⌜ vs = ws1 ++ ws2 ⌠}}}.
Proof.
- iIntros (Φ _) "HΦ".
- wp_lam.
- wp_apply (llength_spec)=>//; iIntros (_).
- wp_apply (lsplit_at_spec)=>//; iIntros (_).
- wp_pures.
- iApply "HΦ".
- iPureIntro.
- apply take_drop.
+ iIntros (Φ _) "HΦ". wp_lam.
+ wp_apply (llength_spec with "[//]"); iIntros (_). wp_pures.
+ rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
+ wp_apply (lsplit_at_spec with "[//]"); iIntros (_).
+ iApply "HΦ". by rewrite take_drop.
Qed.
End lists.
--
GitLab