Commit 955aa2d2 authored by Aleš Bizjak's avatar Aleš Bizjak

Add more examples from the lecture notes.

parent e146b872
......@@ -9,6 +9,14 @@ theories/barrier/example_joining_existentials.v
theories/lecture_notes/coq_intro_example_1.v
theories/lecture_notes/coq_intro_example_2.v
theories/lecture_notes/lists.v
theories/lecture_notes/lists_guarded.v
theories/lecture_notes/lock.v
theories/lecture_notes/lock_unary_spec.v
theories/lecture_notes/modular_incr.v
theories/lecture_notes/recursion_through_the_store.v
theories/lecture_notes/stack.v
theories/lecture_notes/ccounter.v
theories/spanning_tree/graph.v
theories/spanning_tree/mon.v
......
(* Counter with contributions. A specification derived from the modular
specification proved in modular_incr module. *)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth.
From iris_examples.lecture_notes Require Import modular_incr.
Class ccounterG Σ := CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
Definition ccounterΣ : gFunctors := #[GFunctor (frac_authR natR)].
Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ ccounterG Σ.
Proof. solve_inG. Qed.
Section ccounter.
Context `{!heapG Σ, !cntG Σ, !ccounterG Σ} (N : namespace).
Lemma ccounterRA_valid (m n : natR) (q : frac): (! m !{q} n) (n m)%nat.
Proof.
intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *)
by apply nat_included, (frac_auth_included_total q).
Qed.
Lemma ccounterRA_valid_full (m n : natR): (! m ! n) (n = m)%nat.
Proof.
by intros ?%frac_auth_agree.
Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (! m !{q} n) ~~> (! (S m) !{q} (S n)).
Proof.
apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
lia.
Qed.
Definition ccounter_inv (γ₁ γ₂ : gname): iProp Σ :=
( n, own γ₁ (! n) γ₂ ⤇½ (Z.of_nat n))%I.
Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (!{q} n) inv (N .@ "counter") (ccounter_inv γ₁ γ₂) Cnt N l γ₂)%I.
(** The main proofs. *)
Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) :
is_ccounter γ₁ γ₂ (q1 + q2) (n1 + n2)%nat is_ccounter γ₁ γ₂ q1 n1 is_ccounter γ₁ γ₂ q2 n2.
Proof.
apply uPred.equiv_spec; split; rewrite /is_ccounter frag_auth_op own_op.
- iIntros "[? #?]".
iFrame "#"; iFrame.
- iIntros "[[? #?] [? _]]".
iFrame "#"; iFrame.
Qed.
Lemma newcounter_contrib_spec (R : iProp Σ) m:
{{{ True }}}
newcounter #m
{{{ γ₁ γ₂ , RET #; is_ccounter γ₁ γ₂ 1 m%nat }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
wp_apply newcounter_spec; auto.
iIntros () "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
iMod (own_alloc (! m%nat ! m%nat)) as (γ₁) "[Hγ Hγ']"; first done.
iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
{ iNext. iExists _. by iFrame. }
iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
Qed.
Lemma incr_contrib_spec γ₁ γ₂ q n :
{{{ is_ccounter γ₁ γ₂ q n }}}
incr #
{{{ (y : Z), RET #y; is_ccounter γ₁ γ₂ q (S n) }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
iApply (incr_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ _, (own γ₁ (!{q} (S n))))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HOwnElem HP]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HOwnElem H2") as %->.
iMod (makeElem_update _ _ _ (k+1) with "HOwnElem H2") as "[HOwnElem H2]".
iMod (own_update_2 with "H1 HP") as "[H1 HP]".
{ apply ccounterRA_update. }
iMod ("HClose" with "[H1 H2]") as "_".
{ iNext; iExists (S k); iFrame.
rewrite Nat2Z.inj_succ Z.add_1_r //.
}
by iFrame.
- by iFrame.
- iNext.
iIntros (m) "[HCnt' Hown]".
iApply "HΦ". by iFrame.
Qed.
Lemma read_contrib_spec γ₁ γ₂ q n :
{{{ is_ccounter γ₁ γ₂ q n }}}
read #
{{{ (c : Z), RET #c; Z.of_nat n c is_ccounter γ₁ γ₂ q n }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ m, n m (own γ₁ (!{q} n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid.
iMod ("HClose" with "[H1 H2]") as "_".
{ iExists _; by iFrame. }
iFrame; iIntros "!>!%".
auto using inj_le.
- by iFrame.
- iIntros (i) "[_ [% HQ]]".
iApply "HΦ".
iSplit; first by iIntros "!%".
iFrame; iFrame "#".
Qed.
Lemma read_contrib_spec_1 γ₁ γ₂ n :
{{{ is_ccounter γ₁ γ₂ 1%Qp n }}} read #
{{{ RET #n; is_ccounter γ₁ γ₂ 1 n }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (! n))%I (λ m, Z.of_nat n = m (own γ₁ (! n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid_full; simplify_eq.
iMod ("HClose" with "[H1 H2]") as "_".
{ iExists _; by iFrame. }
iFrame; by iIntros "!>!%".
- by iFrame.
- iIntros (i) "[_ [% HQ]]".
simplify_eq. iApply "HΦ".
iFrame; iFrame "#".
Qed.
End ccounter.
\ No newline at end of file
(* In this file we explain how to do the "list examples" from the
Chapter on Separation Logic for Sequential Programs in the
Iris Lecture Notes *)
(* Contains definitions of the weakest precondition assertion, and its basic rules. *)
From iris.program_logic Require Export weakestpre.
(* Instantiation of Iris with the particular language. The notation file
contains many shorthand notations for the programming language constructs, and
the lang file contains the actual language syntax. *)
From iris.heap_lang Require Export notation lang.
(* Files related to the interactive proof mode. The first import includes the
general tactics of the proof mode. The second provides some more specialized
tactics particular to the instantiation of Iris to a particular programming
language. *)
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.
(* The following line makes Coq check that we do not use any admitted facts /
additional assumptions not in the statement of the theorems being proved. *)
Set Default Proof Using "Type".
(* ---------------------------------------------------------------------- *)
Section list_model.
(* This section contains the definition of our model of lists, i.e.,
definitions relating pointer data structures to our model, which is
simply mathematical sequences (Coq lists). *)
(* In order to do the proof we need to assume certain things about the
instantiation of Iris. The particular, even the heap is handled in an
analogous way as other ghost state. This line states that we assume the
Iris instantiation has sufficient structure to manipulate the heap, e.g.,
it allows us to use the points-to predicate. *)
Context `{!heapG Σ}.
Implicit Types l : loc.
(* The variable Σ has to do with what ghost state is available, and the type
of Iris propositions (written Prop in the lecture notes) depends on this Σ.
But since Σ is the same throughout the development we shall define
shorthand notation which hides it. *)
Notation iProp := (iProp Σ).
(* Here is the basic is_list representation predicate:
is_list hd xs holds if hd points to a linked list consisting of
the elements in the mathematical sequence (Coq list) xs.
*)
Fixpoint is_list (hd : val) (xs : list val) : iProp :=
match xs with
| [] => hd = NONEV
| x :: xs => l hd', hd = SOMEV #l l (x,hd') is_list hd' xs
end%I.
(* The following predicate
is_listP P hd xs
holds if hd points to a linked list consisting of the elements in xs and
each of those elements satisfy P.
*)
Fixpoint is_listP P (hd : val) (xs : list val) : iProp :=
match xs with
| [] => hd = NONEV
| x :: xs => l hd', hd = SOMEV #l l (x,hd') is_listP P hd' xs P x
end%I.
(* about_isList expresses how is_listP P hd xs can be seen as a combination of the
basic is_list predicate and the property that P holds for all the elements in xs.
*)
Lemma about_isList P hd xs :
is_listP P hd xs is_list hd xs [ list] x xs, P x.
Proof.
generalize dependent hd.
induction xs as [| x xs']; simpl; intros hd; iSplit.
- eauto.
- by iIntros "(? & _)".
- iDestruct 1 as (l hd') "(? & ? & H & ?)". rewrite IHxs'. iDestruct "H" as "(H_isListxs' & ?)".
iFrame. iExists l, hd'. iFrame.
- iDestruct 1 as "(H_isList & ? & H)". iDestruct "H_isList" as (l hd') "(? & ? & ?)".
iExists l, hd'. rewrite IHxs'. iFrame.
Qed.
(* The predicate
is_list_nat hd xs
holds if hd is a pointer to a linked list of numbers (integers).
*)
Fixpoint is_list_nat (hd : val) (xs : list Z) : iProp :=
match xs with
| [] => hd = NONEV
| x :: xs => l hd', hd = SOMEV #l l (#x,hd') is_list_nat hd' xs
end%I.
(* The reverse function on Coq lists is defined in the Coq library. *)
Definition reverse (l : list val) := List.rev l.
Definition inj {A B : Type} (f : A -> B) : Prop :=
forall (x y : A),
f x = f y -> x = y.
Lemma map_injective {A B : Type} :
forall xs ys (f : A -> B), inj f -> map f xs = map f ys
-> xs = ys.
Proof.
induction xs; intros ys f H_f H_map.
- symmetry in H_map. by apply map_eq_nil in H_map.
- destruct ys.
+ by apply map_eq_nil in H_map.
+ specialize (IHxs ys f). inversion H_map as [H_a].
rewrite -> IHxs; try done.
apply H_f in H_a. by rewrite H_a.
Qed.
End list_model.
(* ---------------------------------------------------------------------- *)
Section list_code.
(* This section contains the code of the list functions we specify *)
(* Function inc hd assumes all values in the linked list pointed to by hd
are numbers and increments them by 1, in-place *)
Definition inc : val :=
rec: "inc" "hd" :=
match: "hd" with
NONE => #()
| SOME "l" =>
let: "tmp1" := Fst !"l" in
let: "tmp2" := Snd !"l" in
"l" <- (("tmp1" + #1), "tmp2");;
"inc" "tmp2"
end.
(* Function app l l' appends linked list l' to end of linked list l *)
Definition app : val :=
rec: "app" "l" "l'" :=
match: "l" with
NONE => "l'"
| SOME "hd" =>
let: "tmp1" := !"hd" in
let: "tmp2" := "app" (Snd "tmp1") "l'" in
"hd" <- ((Fst "tmp1"), "tmp2");;
"l"
end.
(* Function rev l acc reverses all the pointers in linked list l and stiches
the accumulator argument acc at the end *)
Definition rev : val :=
rec: "rev" "l" "acc" :=
match: "l" with
NONE => "acc"
| SOME "p" =>
let: "h" := Fst !"p" in
let: "t" := Snd !"p" in
"p" <- ("h", "acc");;
"rev" "t" "l"
end.
(* Function len l returns the lenght of linked list l *)
Definition len : val :=
rec: "len" "l" :=
match: "l" with
NONE => #0
| SOME "p" =>
("len" (Snd !"p") + #1)
end.
(* Function foldr f a l is the usual fold right function for linked list l, with
base value a and combination function f *)
Definition foldr : val :=
rec: "foldr" "f" "a" "l" :=
match: "l" with
NONE => "a"
| SOME "p" =>
let: "hd" := Fst !"p" in
let: "t" := Snd !"p" in
"f" ("hd", ("foldr" "f" "a" "t"))
end.
(* sum_list l returns the sum of the list of numbers in linked list l,
implemented by call to foldr *)
Definition sum_list : val :=
rec: "sum_list" "l" :=
let: "f'" := (λ: "p", let: "x" := Fst "p" in
let: "y" := Snd "p" in
"x" + "y")
in
(foldr "f'" #0 "l").
Definition cons : val := (λ: "x" "xs",
let: "p" := ("x", "xs") in
SOME (Alloc("p"))).
Definition empty_list : val := NONEV.
(* filter prop l is the usual filter function on linked lists, prop is supposed
to be a function from values to booleans. Implemented using foldr. *)
Definition filter : val :=
rec: "filter" "prop" "l" :=
let: "f" := (λ: "p",
let: "x" := Fst "p" in
let: "xs" := Snd "p" in
if: ("prop" "x")
then (cons "x" "xs")
else "xs")
in (foldr "f" empty_list "l").
(* map_list f l is the usual map function on linked lists with f the function
to be mapped over the list l. Implemented using foldr. *)
Definition map_list : val :=
rec: "map_list" "f" "l" :=
let: "f'" := (λ: "p",
let: "x" := Fst "p" in
let: "xs" := Snd "p" in
(cons ("f" "x") "xs"))
in
(foldr "f'" empty_list "l").
(* incr l is another variant of the increment function on linked lists, implemented using map. *)
Definition incr : val :=
rec: "incr" "l" :=
map_list (λ: "n", "n" + #1)%I "l".
End list_code.
(* ---------------------------------------------------------------------- *)
Section list_spec.
(* This section contains the specifications and proofs for the list functions.
The specifications and proofs are explained in the Iris Lecture Notes
*)
Context `{!heapG Σ}.
Lemma inc_spec hd xs :
{{{ is_list_nat hd xs }}}
inc hd
{{{ w, RET w; w = #() is_list_nat hd (List.map Z.succ xs) }}}.
Proof.
iIntros (ϕ) "Hxs H".
iLöb as "IH" forall (hd xs ϕ). wp_rec. destruct xs as [|x xs]; iSimplifyEq.
- wp_match. iApply "H". done.
- iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)". iSimplifyEq.
wp_match. do 2 (wp_load; wp_proj; wp_let). wp_op.
wp_store. iApply ("IH" with "Hxs").
iNext. iIntros (w) "H'". iApply "H". iDestruct "H'" as "[Hw Hislist]".
iFrame. iExists l, hd'. iFrame. done.
Qed.
Lemma app_spec xs ys (l l' : val) :
{{{ is_list l xs is_list l' ys }}}
app l l'
{{{ v, RET v; is_list v (xs ++ ys) }}}.
Proof.
iIntros (ϕ) "[Hxs Hys] H".
iLöb as "IH" forall (l xs l' ys ϕ).
destruct xs as [| x xs']; iSimplifyEq.
- wp_rec. wp_let. wp_match. iApply "H". done.
- iDestruct "Hxs" as (l0 hd0) "(% & Hx & Hxs)". iSimplifyEq.
wp_rec. wp_let. wp_match. wp_load. wp_let. wp_proj. wp_bind (app _ _)%E.
iApply ("IH" with "Hxs Hys").
iNext. iIntros. wp_let. wp_proj. wp_store. iSimplifyEq. iApply "H".
iExists l0, v. iFrame. done.
Qed.
Lemma rev_spec vs us (l acc : val) :
{{{ is_list l vs is_list acc us }}}
rev l acc
{{{ w, RET w; is_list w (reverse vs ++ us) }}}.
Proof.
iIntros (ϕ) "[H1 H2] HL".
iInduction vs as [| v vs'] "IH" forall (acc l us).
- iSimplifyEq. wp_rec. wp_let. wp_match. iApply "HL". done.
- simpl. iDestruct "H1" as (l' t) "(% & H3 & H1)". wp_rec. wp_let.
rewrite -> H at 1. wp_match. do 2 (wp_load; wp_proj; wp_let).
wp_store. iSpecialize ("IH" $! l t ([v] ++ us)).
iApply ("IH" with "[H1] [H3 H2]").
+ done.
+ simpl. iExists l', acc. iFrame. done.
+ iNext. rewrite -> app_assoc. done.
Qed.
Lemma len_spec (l : val) xs :
{{{ is_list l xs }}}
len l
{{{ v, RET v; v = #(length xs) }}}.
Proof.
iIntros (ϕ) "Hl H".
iInduction xs as [| x xs'] "IH" forall (l ϕ); iSimplifyEq.
- wp_rec. wp_match. iApply "H". done.
- iDestruct "Hl" as (p hd') "(% & Hp & Hhd')". wp_rec. iSimplifyEq.
wp_match. wp_load. wp_proj. wp_bind (len hd')%I. iApply ("IH" with "[Hhd'] [Hp H]"); try done.
iNext. iIntros. iSimplifyEq. wp_op. iApply "H". iPureIntro. rewrite Zpos_P_of_succ_nat. done.
Qed.
(* The following specifications for foldr are non-trivial because the code is higher-order
and hence the specifications involved nested triples.
The specifications are explained in the Iris Lecture Notes. *)
Lemma foldr_spec_PI P I (f a hd : val) (e_f e_a e_hd : expr) (xs : list val)
`{Hef : !IntoVal e_f f} `{Hea : !IntoVal e_a a} `{Hehd : !IntoVal e_hd hd} :
{{{ ( (x a' : val) (ys : list val),
{{{ P x I ys a'}}}
e_f (x, a')
{{{r, RET r; I (x::ys) r }}})
is_list hd xs
([ list] x xs, P x)
I [] a
}}}
foldr e_f e_a e_hd
{{{
r, RET r; is_list hd xs
I xs r
}}}.
Proof.
apply of_to_val in Hef as <-.
apply of_to_val in Hea as <-.
apply of_to_val in Hehd as <-.
iIntros (ϕ) "(#H_f & H_isList & H_Px & H_Iempty) H_inv".
iInduction xs as [|x xs'] "IH" forall (ϕ a hd); wp_rec; do 2 wp_let; iSimplifyEq.
- wp_match. iApply "H_inv". eauto.
- iDestruct "H_isList" as (l hd') "[% [H_l H_isList]]".
iSimplifyEq.
wp_match. do 2 (wp_load; wp_proj; wp_let).
wp_bind (((foldr f) a) hd').
iDestruct "H_Px" as "(H_Px & H_Pxs')".
iApply ("IH" with "H_isList H_Pxs' H_Iempty [H_l H_Px H_inv]").
iNext. iIntros (r) "(H_isListxs' & H_Ixs')".
iApply ("H_f" with "[$H_Ixs' $H_Px] [H_inv H_isListxs' H_l]").
iNext. iIntros (r') "H_inv'". iApply "H_inv". iFrame.
iExists l, hd'. by iFrame.
Qed.
Lemma foldr_spec_PPI P I (f a hd : val ) (e_f e_a e_hd : expr) (xs : list val)
`{Hef : !IntoVal e_f f} `{Hea : !IntoVal e_a a} `{Hehd : !IntoVal e_hd hd} :
{{{ ( (x a' : val) (ys : list val),
{{{ P x I ys a'}}}
e_f (x, a')
{{{r, RET r; I (x::ys) r }}})
is_listP P hd xs
I [] a
}}}
foldr e_f e_a e_hd
{{{
r, RET r; is_listP (fun x => True) hd xs
I xs r
}}}.
Proof.
apply of_to_val in Hef as <-.
apply of_to_val in Hea as <-.
apply of_to_val in Hehd as <-.
iIntros (ϕ) "(#H_f & H_isList & H_Iempty) H_inv".
rewrite about_isList. iDestruct "H_isList" as "(H_isList & H_Pxs)".
iApply (foldr_spec_PI with "[-H_inv]").
- iFrame. by iFrame "H_f".
- iNext. iIntros (r) "(H_isList & H_Ixs)".
iApply "H_inv". iFrame. rewrite about_isList. iFrame. by rewrite big_sepL_forall.
Qed.
Lemma sum_spec (hd: val) (xs: list Z) :
{{{ is_list hd (map (fun (n : Z) => #n) xs)}}}
sum_list hd
{{{ v, RET v; v = # (fold_right Z.add 0 xs) }}}.
Proof.
iIntros (ϕ) "H_is_list H_later".
wp_rec. wp_let.
iApply (foldr_spec_PI
(fun x => ( (n : Z), x = #n)%I)
(fun xs' acc => ys,
acc = #(fold_right Z.add 0 ys)
xs' = map (fun (n : Z) => #n) ys
([ list] x xs', (n' : Z), x = #n'))%I
with "[$H_is_list] [H_later]").
- iSplitR.
+ iIntros (x a' ys). iAlways. iIntros (ϕ') "(H1 & H2) H3".
do 5 (wp_pure _).
iDestruct "H2" as (zs) "(% & % & H_list)".
iDestruct "H1" as (n2) "%". iSimplifyEq. wp_binop.
iApply "H3". iExists (n2::zs). repeat (iSplit; try done).
by iExists _.
+ iSplit.
* induction xs; iSimplifyEq; first done.
iSplit; [iExists a; done | apply IHxs].
* iExists []. eauto.
- iNext. iIntros (r) "(H1 & H2)".
iApply "H_later". iDestruct "H2" as (ys) "(% & % & H_list)".
iSimplifyEq. rewrite (map_injective xs ys (λ n : Z, #n)); try done.
unfold inj. intros x y H_xy. by inversion H_xy.
Qed.
Lemma filter_spec (hd p : val) (xs : list val) (P : val -> bool) :
{{{ is_list hd xs
( x : val ,
{{{ True }}}
p x
{{{r, RET r; r = #(P x) }}})
}}}
filter p hd
{{{ v, RET v; is_list hd xs
is_list v (List.filter P xs)
}}}.
Proof.
iIntros (ϕ) "[H_isList #H_p] H_ϕ".
do 3 (wp_pure _).
iApply (foldr_spec_PI (fun x => True)%I
(fun xs' acc => is_list acc (List.filter P xs'))%I
with "[$H_isList] [H_ϕ]").
- iSplitL.
+ iIntros "** !#" (ϕ'). iIntros "[_ H_isList] H_ϕ'".
repeat (wp_pure _). wp_bind (p x). iApply "H_p"; first done.
iNext. iIntros (r) "H". iSimplifyEq. destruct (P x); wp_if.
* unfold cons. repeat (wp_pure _). wp_alloc l. iApply "H_ϕ'".
iExists l, a'. by iFrame.
* by iApply "H_ϕ'".
+ iSplit; last done.
rewrite big_sepL_forall. eauto.
- iNext. iApply "H_ϕ".
Qed.
Lemma map_spec P Q (e_f e_hd : expr) (f hd : val) (xs : list val)
`{Hef : !IntoVal e_f f} `{Hehd : !IntoVal e_hd hd} :
{{{
is_list hd xs
( (x : val), {{{ P x }}}
e_f x
{{{r, RET r; Q x r}}})
[ list] x xs, P x
}}}
map_list e_f e_hd
{{{
r, RET r; (ys : list val), is_list r ys
([ list] p zip xs ys, Q (fst p) (snd p))
List.length ys = List.length xs
}}}.
Proof.
apply of_to_val in Hef as <-.
apply of_to_val in Hehd as <-.
iIntros (ϕ) "[H_is_list [#H1 H_P_xs]] H_ϕ".
do 3 (wp_pure _).
iApply (foldr_spec_PI
P
(fun xs acc => ys, (is_list acc ys)
([ list] p zip xs ys, Q (fst p) (snd p))
length xs = length ys)%I
with "[H_is_list H1 H_P_xs] [H_ϕ]").
- iSplitR "H_is_list H_P_xs".
+ iIntros (x a' ys). iAlways. iIntros (ϕ') "(H_Px & H_Q) H_ϕ'". repeat (wp_pure _).
wp_bind (f x). iApply ("H1" with "[H_Px][H_Q H_ϕ']"); try done.
iNext. iIntros (r) "H_Qr". repeat (wp_pure _). wp_alloc l. iApply "H_ϕ'".
iDestruct "H_Q" as (ys') "(H_is_list_ys' & H_Qys' & %)". iExists (r::ys').
iSplitR "H_Qr H_Qys'".
* unfold is_list. iExists l, a'. fold is_list. by iFrame.
* iSimplifyEq. iFrame. eauto.
+ iFrame. iExists []. iSplit; by simpl.
- iNext. iIntros (r) "H". iApply "H_ϕ". iDestruct "H" as "(_ & H_Q)".
iDestruct "H_Q" as (ys) "(H_isList & H_Q & %)". iExists ys. by iFrame.
Qed.
Lemma about_length {A : Type} (xs : list A) (n : nat) :
length xs = S n -> exists x xs', xs = x::xs'.
Proof.
intro H. induction xs as [| x xs' ].
- inversion H.
- by exists x, xs'.
Qed.
Lemma inc_with_map hd (xs : list Z) :
{{{ is_list hd (List.map (fun (n : Z) => #n) xs) }}}
incr hd
{{{ v, RET v; is_list v (List.map (fun (n : Z) => #n) (List.map Z.succ xs)) }}}.
Proof.
iIntros (ϕ) "H_isList H_ϕ".
wp_rec. iApply (map_spec
(fun x => ( (n : Z), x = #n)%I)
(fun x r => ( (n' : Z),
r = #(Z.succ n')
x = #n')%I)
with "[$H_isList] [H_ϕ]").
- iSplit. iIntros (x) "!#". iIntros (ϕ') "H1 H2". wp_let. iDestruct "H1" as (n) "H_x".
iSimplifyEq. wp_binop. iApply "H2". by iExists n.
rewrite big_sepL_fmap. rewrite big_sepL_forall. eauto.
- iNext. iIntros (r) "H". iApply "H_ϕ". iDestruct "H" as (ys) "(H_isList & H_post & H_length)".
iAssert (ys = (List.map (λ n : Z, #n) (List.map Z.succ xs)))%I with "[-H_isList]" as %->.
{ iInduction ys as [| y ys'] "IH" forall (xs); iDestruct "H_length" as %H.
- simpl. destruct xs. by simpl. inversion H.
- rewrite fmap_length in H. symmetry in H. simpl in H.
destruct (about_length _ _ H) as (x & xs' & ->). simpl.