Commit 30a88b10 authored by Ralf Jung's avatar Ralf Jung

add list_reverse example

parent b598e0d5
Pipeline #2271 failed with stage
...@@ -106,6 +106,7 @@ tests/one_shot.v ...@@ -106,6 +106,7 @@ tests/one_shot.v
tests/joining_existentials.v tests/joining_existentials.v
tests/proofmode.v tests/proofmode.v
tests/barrier_client.v tests/barrier_client.v
proofmode/coq_tactics.v proofmode/coq_tactics.v
proofmode/pviewshifts.v proofmode/pviewshifts.v
proofmode/environments.v proofmode/environments.v
(** Correctness of in-place list reversal *)
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.
Section list_reverse.
Context `{!heapG Σ} (heapN : namespace).
Notation iProp := (iPropG heap_lang Σ).
Implicit Types l : loc.
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
Definition rev : val :=
rec: "rev" "hd" "acc" :=
match: "hd" with
NONE => "acc"
| SOME "l" =>
let: "tmp1" := Fst !"l" in
let: "tmp2" := Snd !"l" in
"l" <- ("tmp1", "acc");;
"rev" "tmp2" "hd"
Global Opaque rev.
Lemma rev_acc_wp hd acc xs ys (Φ : val iProp) :
heap_ctx heapN is_list hd xs is_list acc ys
( w, is_list w (reverse xs ++ ys) - Φ w)
WP rev hd acc {{ Φ }}.
iIntros "(#Hh & Hxs & Hys & HΦ)".
iLöb (hd acc xs ys Φ) as "IH". wp_rec; wp_let.
destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. }
iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Lemma rev_wp hd xs (Φ : val iProp) :
heap_ctx heapN is_list hd xs ( w, is_list w (reverse xs) - Φ w)
WP rev hd (InjL #()) {{ Φ }}.
iIntros "(#Hh & Hxs & HΦ)".
iApply (rev_acc_wp hd NONEV xs []); iFrame "Hh Hxs".
iSplit; first done. iIntros (w). rewrite right_id_L. iApply "HΦ".
End list_reverse.
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