list_reverse.v 1.61 KB
Newer Older
1
(** Correctness of in-place list reversal *)
2
From iris.proofmode Require Export tactics.
3
From iris.program_logic Require Export total_weakestpre weakestpre.
4
From iris.heap_lang Require Export lang.
5
From iris.heap_lang Require Import proofmode notation.
6
Set Default Proof Using "Type".
7

8
9
Unset Mangle Names.

10
Section list_reverse.
11
Context `{!heapG Σ}.
12
13
Implicit Types l : loc.

14
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
15
  match xs with
Ralf Jung's avatar
Ralf Jung committed
16
17
  | [] => hd = NONEV
  | x :: xs =>  l hd', hd = SOMEV #l  l  (x,hd')  is_list hd' xs
18
19
20
21
22
23
24
25
26
27
28
29
30
  end%I.

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"
    end.

31
Lemma rev_acc_wp hd acc xs ys :
32
  [[{ is_list hd xs  is_list acc ys }]]
33
    rev hd acc
34
  [[{ w, RET w; is_list w (reverse xs ++ ys) }]].
35
Proof.
36
  iIntros (Φ) "[Hxs Hys] HΦ". Show.
37
38
  iInduction xs as [|x xs] "IH" forall (hd acc ys Φ);
    iSimplifyEq; wp_rec; wp_let.
39
  - Show. wp_match. by iApply "HΦ".
40
  - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
41
    wp_load. wp_load. wp_store.
42
    iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
43
    { iExists l, acc; by iFrame. }
44
    iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
45
46
Qed.

47
Lemma rev_wp hd xs :
48
  [[{ is_list hd xs }]] rev hd NONEV [[{ w, RET w; is_list w (reverse xs) }]].
49
Proof.
50
51
  iIntros (Φ) "Hxs HΦ".
  iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
52
  iIntros (w). rewrite right_id_L. iApply "HΦ".
53
54
Qed.
End list_reverse.