proofmode.v 7.47 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.proofmode Require Import coq_tactics.
3
From iris.proofmode Require Export tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5 6
From iris.heap_lang Require Export wp_tactics heap.
Import uPred.

7
Ltac wp_strip_later ::= iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9

Section heap.
10
Context `{heapG Σ}.
11 12 13
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
14

15
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
16
  to_val e = Some v 
17
  (Δ  heap_ctx)  heapN  E 
18
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  ( l,  Δ'',
20
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
21
    (Δ''  Φ (LitV (LitLoc l)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
24
  intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
25
  apply and_intro; first done.
26
  rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

31
Lemma tac_wp_load Δ Δ' E i l q v Φ :
32
  (Δ  heap_ctx)  heapN  E 
33
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  envs_lookup i Δ' = Some (false, l {q} v)%I 
35
  (Δ'  Φ v) 
36
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Proof.
Ralf Jung's avatar
Ralf Jung committed
38
  intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
Ralf Jung's avatar
Ralf Jung committed
39
  apply and_intro; first done.
40
  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

44
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  to_val e = Some v' 
46
  (Δ  heap_ctx)  heapN  E 
47
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
50
  (Δ''  Φ (LitV LitUnit)) 
51
  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof.
Ralf Jung's avatar
Ralf Jung committed
53
  intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
Ralf Jung's avatar
Ralf Jung committed
54
  apply and_intro; first done.
55
  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

59
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  to_val e1 = Some v1  to_val e2 = Some v2 
61
  (Δ  heap_ctx)  heapN  E 
62
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
64
  (Δ'  Φ (LitV (LitBool false))) 
65
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
Ralf Jung's avatar
Ralf Jung committed
67
  intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
Ralf Jung's avatar
Ralf Jung committed
68
  apply and_intro; first done.
69
  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71 72
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

73
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  to_val e1 = Some v1  to_val e2 = Some v2 
75
  (Δ  heap_ctx)  heapN  E 
76
  IntoLaterEnvs Δ Δ' 
77
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
79
  (Δ''  Φ (LitV (LitBool true))) 
80
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof.
Ralf Jung's avatar
Ralf Jung committed
82
  intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
Ralf Jung's avatar
Ralf Jung committed
83
  apply and_intro; first done.
84
  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88 89
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
90
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
92
    wp_bind_core K; iApply lem; try iNext)
93
  | _ => fail "wp_apply: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96
  end.

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
97
  lazymatch goal with
98 99 100
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
101
         match eval hnf in e' with Alloc _ => wp_bind_core K end)
102
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
103
    eapply tac_wp_alloc with _ H _;
104 105 106
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_alloc:" e' "not a value"
      |iAssumption || fail "wp_alloc: cannot find heap_ctx"
107
      |solve_ndisj || fail "wp_alloc: cannot open heap invariant"
108 109 110 111 112
      |apply _
      |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
        eexists; split;
          [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
          |wp_finish]]
113
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  end.
115

116 117
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119

Tactic Notation "wp_load" :=
120
  lazymatch goal with
121 122 123
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
124
         match eval hnf in e' with Load _ => wp_bind_core K end)
125 126 127
      |fail 1 "wp_load: cannot find 'Load' in" e];
    eapply tac_wp_load;
      [iAssumption || fail "wp_load: cannot find heap_ctx"
128
      |solve_ndisj || fail "wp_load: cannot open heap invariant"
129 130
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
131
       iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
132
      |wp_finish]
133
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135 136
  end.

Tactic Notation "wp_store" :=
137
  lazymatch goal with
138 139 140
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
141
         match eval hnf in e' with Store _ _ => wp_bind_core K end)
142 143 144 145 146
      |fail 1 "wp_store: cannot find 'Store' in" e];
    eapply tac_wp_store;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_store:" e' "not a value"
      |iAssumption || fail "wp_store: cannot find heap_ctx"
147
      |solve_ndisj || fail "wp_store: cannot open heap invariant"
148 149 150 151
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
      |env_cbv; reflexivity
152
      |wp_finish]
153
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156
  end.

Tactic Notation "wp_cas_fail" :=
157
  lazymatch goal with
158 159 160
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
161
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
162 163 164 165 166 167 168
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    eapply tac_wp_cas_fail;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
169
      |solve_ndisj || fail "wp_cas_fail: cannot open heap invariant"
170 171 172 173 174
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
      |try congruence
      |wp_finish]
175
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177 178
  end.

Tactic Notation "wp_cas_suc" :=
179
  lazymatch goal with
180 181 182
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
183
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
184 185 186 187 188 189 190
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    eapply tac_wp_cas_suc;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
191
      |solve_ndisj || fail "wp_cas_suc: cannot open heap invariant"
192 193 194 195 196 197
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
      |try congruence
      |env_cbv; reflexivity
      |wp_finish]
198
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  end.