proofmode.v 22.2 KB
Newer Older
1
From iris.program_logic Require Export weakestpre total_weakestpre.
2
From iris.program_logic Require Import atomic.
3
From iris.proofmode Require Import coq_tactics reduction.
4
From iris.proofmode Require Export tactics.
5
From iris.heap_lang Require Export tactics lifting.
6
From iris.heap_lang Require Import notation.
7
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
Import uPred.

10
Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
11
  ( (e'':=e'), e = e'') 
12
  envs_entails Δ (WP e' @ s; E {{ Φ }})  envs_entails Δ (WP e @ s; E {{ Φ }}).
13
Proof. by intros ->. Qed.
14
Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
15
  ( (e'':=e'), e = e'') 
16 17
  envs_entails Δ (WP e' @ s; E [{ Φ }])  envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.
18

19
Tactic Notation "wp_expr_eval" tactic(t) :=
20
  iStartProof;
21 22 23 24 25 26 27 28 29
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
    eapply tac_wp_expr_eval;
      [let x := fresh in intros x; t; unfold x; reflexivity|]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    eapply tac_twp_expr_eval;
      [let x := fresh in intros x; t; unfold x; reflexivity|]
  | _ => fail "wp_expr_eval: not a 'wp'"
  end.
30

31 32
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 
33
  φ 
34
  MaybeIntoLaterNEnvs n Δ Δ' 
35 36
  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) 
  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
37
Proof.
38
  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
39 40
  rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
41 42
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 
43 44 45 46
  φ 
  envs_entails Δ (WP e2 @ s; E [{ Φ }]) 
  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
Proof.
47
  rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
48
Qed.
49

50 51 52 53 54 55
Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
  envs_entails Δ (Φ v)  envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
  envs_entails Δ (Φ v)  envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
56

57 58
Ltac wp_expr_simpl := wp_expr_eval simpl.

Robbert Krebbers's avatar
Robbert Krebbers committed
59
Ltac wp_value_head :=
60 61 62 63 64 65 66
  first [eapply tac_wp_value || eapply tac_twp_value].

Ltac wp_finish :=
  wp_expr_simpl;      (* simplify occurences of subst/fill *)
  try wp_value_head;  (* in case we have reached a value, get rid of the WP *)
  pm_prettify.        (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
                         λs caused by wp_value *)
Robbert Krebbers's avatar
Robbert Krebbers committed
67

68
Tactic Notation "wp_pure" open_constr(efoc) :=
69 70
  iStartProof;
  lazymatch goal with
71
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
75
      eapply (tac_wp_pure _ _ _ _ (fill K e'));
Ralf Jung's avatar
Ralf Jung committed
76
      [iSolveTC                       (* PureExec *)
Robbert Krebbers's avatar
Robbert Krebbers committed
77
      |try fast_done                  (* The pure condition for PureExec *)
Ralf Jung's avatar
Ralf Jung committed
78
      |iSolveTC                       (* IntoLaters *)
79
      |wp_finish                      (* new goal *)
Robbert Krebbers's avatar
Robbert Krebbers committed
80
      ])
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
82 83 84 85 86
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
      eapply (tac_twp_pure _ _ _ (fill K e'));
Ralf Jung's avatar
Ralf Jung committed
87
      [iSolveTC                       (* PureExec *)
88
      |try fast_done                  (* The pure condition for PureExec *)
89
      |wp_finish                      (* new goal *)
90
      ])
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
92
  | _ => fail "wp_pure: not a 'wp'"
93 94
  end.

95 96 97 98 99
(* TODO: do this in one go, without [repeat]. *)
Ltac wp_pures :=
  iStartProof;
  repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
                             magically spawns. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114

(* The handling of beta-reductions with wp_rec needs special care in
  order to allow it to unlock locked `RecV` values: We first put
  `AsRecV_recv_locked` in the current environment so that it can be
  used as an instance by the typeclass resolution system, then we
  perform the reduction, and finally we clear this new hypothesis.

  The reason is that we do not want impure wp_ tactics to unfold
  locked terms, while we want them to execute arbitrary pure steps. *)
Tactic Notation "wp_rec" :=
  let H := fresh in
  assert (H := AsRecV_recv_locked);
  wp_pure (App _ _);
  clear H.

115
Tactic Notation "wp_if" := wp_pure (If _ _ _).
116 117
Tactic Notation "wp_if_true" := wp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "wp_if_false" := wp_pure (If (LitV (LitBool false)) _ _).
118 119 120 121
Tactic Notation "wp_unop" := wp_pure (UnOp _ _).
Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
Tactic Notation "wp_op" := wp_unop || wp_binop.
Tactic Notation "wp_lam" := wp_rec.
122 123
Tactic Notation "wp_let" := wp_pure (Rec BAnon (BNamed _) _); wp_lam.
Tactic Notation "wp_seq" := wp_pure (Rec BAnon BAnon _); wp_lam.
124 125
Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
126 127 128 129
Tactic Notation "wp_match" := wp_case; wp_pure (Rec _ _ _); wp_lam.
Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "wp_pair" := wp_pure (Pair _ _).
Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
130

Ralf Jung's avatar
Ralf Jung committed
131
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
132
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
133
  envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I 
Ralf Jung's avatar
Ralf Jung committed
134
  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
135
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
136 137
Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
138
  envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I 
139
  envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
140
Proof. rewrite envs_entails_eq=> -> ->. by apply: twp_bind. Qed.
141

Robbert Krebbers's avatar
Robbert Krebbers committed
142 143 144
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
145
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify]
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  end.
147 148 149
Ltac twp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
150
  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|reduction.pm_prettify]
151
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
152

153 154 155
Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
156
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
157 158
    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
159 160 161
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
162 163 164 165
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Section heap.
167
Context `{heapG Σ}.
168 169
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Implicit Types Δ : envs (uPredI (iResUR Σ)).
171 172
Implicit Types v : val.
Implicit Types z : Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
173

174
Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
175
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  ( l,  Δ'',
177
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
178 179
    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (Alloc v) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Proof.
181
  rewrite envs_entails_eq=> ? HΔ.
182
  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
183
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185 186
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.
187
Lemma tac_twp_alloc Δ s E j K v Φ :
188 189
  ( l,  Δ',
    envs_app false (Esnoc Enil j (l  v)) Δ = Some Δ' 
190 191
    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (Alloc v) @ s; E [{ Φ }]).
192
Proof.
193
  rewrite envs_entails_eq=> HΔ.
194 195 196 197 198
  rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
  rewrite left_id. apply forall_intro=> l.
  destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
199

200
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
201
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
202
  envs_lookup i Δ' = Some (false, l {q} v)%I 
203 204
  envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Proof.
206
  rewrite envs_entails_eq=> ???.
207
  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
208
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
211 212
Lemma tac_twp_load Δ s E i K l q v Φ :
  envs_lookup i Δ = Some (false, l {q} v)%I 
213 214
  envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
215
Proof.
216
  rewrite envs_entails_eq=> ??.
217 218 219 220
  rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
  rewrite envs_lookup_split //; simpl.
  by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v v' Φ :
223
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
224 225
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
226 227
  envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
228
Proof.
229
  rewrite envs_entails_eq=> ????.
230
  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
231
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
234
Lemma tac_twp_store Δ Δ' s E i K l v v' Φ :
235 236
  envs_lookup i Δ = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ = Some Δ' 
237 238
  envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (Store (LitV l) v') @ s; E [{ Φ }]).
239
Proof.
240 241
  rewrite envs_entails_eq. intros. rewrite -twp_bind.
  eapply wand_apply; first by eapply twp_store.
242 243 244
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
245

246
Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
247 248 249 250
  MaybeIntoLaterNEnvs 1 Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
  vals_cas_compare_safe v v1 
251 252 253
  (v = v1  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) 
  (v  v1  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
254
Proof.
255
  rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
256 257 258 259
  - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
    rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
    apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -wp_bind. eapply wand_apply.
260
    { eapply wp_cas_fail; eauto. }
261 262 263
    rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
    apply later_mono, sep_mono_r. apply wand_mono; auto.
Qed.
264
Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
265 266 267
  envs_lookup i Δ = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
  vals_cas_compare_safe v v1 
268 269 270
  (v = v1  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) 
  (v  v1  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
271
Proof.
272
  rewrite envs_entails_eq=> ??? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
273 274 275 276
  - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
    rewrite /= {1}envs_simple_replace_sound //; simpl.
    apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -twp_bind. eapply wand_apply.
277
    { eapply twp_cas_fail; eauto. }
278 279 280 281
    rewrite /= {1}envs_lookup_split //; simpl.
    apply sep_mono_r. apply wand_mono; auto.
Qed.

282
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
283
  MaybeIntoLaterNEnvs 1 Δ Δ' 
284 285
  envs_lookup i Δ' = Some (false, l {q} v)%I 
  v  v1  vals_cas_compare_safe v v1 
286 287
  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
288
Proof.
289
  rewrite envs_entails_eq=> ?????.
290
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
291
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
292 293
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
294
Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
295 296
  envs_lookup i Δ = Some (false, l {q} v)%I 
  v  v1  vals_cas_compare_safe v v1 
297 298
  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
299
Proof.
300 301 302
  rewrite envs_entails_eq. intros. rewrite -twp_bind.
  eapply wand_apply; first exact: twp_cas_fail.
  rewrite envs_lookup_split //=. by do 2 f_equiv.
303
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304

305
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
306
  MaybeIntoLaterNEnvs 1 Δ Δ' 
307
  envs_lookup i Δ' = Some (false, l  v)%I 
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
309
  v = v1  val_is_unboxed v 
310 311
  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
312
Proof.
313
  rewrite envs_entails_eq=> ??????; subst.
314 315
  rewrite -wp_bind. eapply wand_apply.
  { eapply wp_cas_suc; eauto. by left. }
316
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
317 318
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
319
Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
320
  envs_lookup i Δ = Some (false, l  v)%I 
321
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
322
  v = v1  val_is_unboxed v 
323 324
  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
325
Proof.
326
  rewrite envs_entails_eq=>?????; subst.
327 328
  rewrite -twp_bind. eapply wand_apply.
  { eapply twp_cas_suc; eauto. by left. }
329 330 331
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
332

333
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
334
  MaybeIntoLaterNEnvs 1 Δ Δ' 
335 336 337 338
  envs_lookup i Δ' = Some (false, l  LitV z1)%I 
  envs_simple_replace i false (Esnoc Enil i (l  LitV (z1 + z2))) Δ' = Some Δ'' 
  envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
339
Proof.
340 341
  rewrite envs_entails_eq=> ????.
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
342 343 344
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
345 346 347 348 349
Lemma tac_twp_faa Δ Δ' s E i K l z1 z2 Φ :
  envs_lookup i Δ = Some (false, l  LitV z1)%I 
  envs_simple_replace i false (Esnoc Enil i (l  LitV (z1 + z2))) Δ = Some Δ' 
  envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
350
Proof.
351 352
  rewrite envs_entails_eq=> ???.
  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
353 354 355
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
356 357
End heap.

358
Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
359
  wp_pures;
360 361
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
362
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
363
      reshape_expr e ltac:(fun K e' =>
364
        wp_bind_core K; tac H) ||
365 366 367
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
368 369
    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' =>
370
        twp_bind_core K; tac H) ||
371 372 373
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
374 375
    | _ => fail "wp_apply: not a 'wp'"
    end).
376 377
Tactic Notation "wp_apply" open_constr(lem) :=
  wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
378 379 380 381 382 383
(** Tactic tailored for atomic triples: the first, simple one just runs iAuIntro
on the goal, as atomic triples always have an atomic update as their premise.
The second one additionaly does some framing: it gets rid of `Hs` from the
context, which is intended to be the non-laterable assertions that iAuIntro
would choke on.  You get them all back in the continuation of the atomic
operation. *)
384
Tactic Notation "awp_apply" open_constr(lem) :=
385
  wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
386
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
387
  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; last iAuIntro]).
Robbert Krebbers's avatar
Robbert Krebbers committed
388 389

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
390
  let Htmp := iFresh in
391 392 393
  let finish _ :=
    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
394
        [pm_reflexivity || fail "wp_alloc:" H "not fresh"
395
        |iDestructHyp Htmp as H; wp_finish] in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
396
  wp_pures;
397
  lazymatch goal with
398
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
399
    first
400
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
401
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
Ralf Jung's avatar
Ralf Jung committed
402
    [iSolveTC
403 404 405
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
406
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
407 408
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
    finish ()
409
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  end.
411

412
Tactic Notation "wp_alloc" ident(l) :=
413
  wp_alloc l as "?".
Robbert Krebbers's avatar
Robbert Krebbers committed
414 415

Tactic Notation "wp_load" :=
416 417 418
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
419
  wp_pures;
420
  lazymatch goal with
421
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
422
    first
423
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
424
      |fail 1 "wp_load: cannot find 'Load' in" e];
Ralf Jung's avatar
Ralf Jung committed
425
    [iSolveTC
426
    |solve_mapsto ()
427
    |wp_finish]
428 429 430 431 432
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K))
      |fail 1 "wp_load: cannot find 'Load' in" e];
    [solve_mapsto ()
433
    |wp_finish]
434
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
435 436 437
  end.

Tactic Notation "wp_store" :=
438 439 440
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
441
  wp_pures;
442
  lazymatch goal with
443
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
444
    first
445
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K))
446
      |fail 1 "wp_store: cannot find 'Store' in" e];
Ralf Jung's avatar
Ralf Jung committed
447
    [iSolveTC
448
    |solve_mapsto ()
449
    |pm_reflexivity
450
    |first [wp_seq|wp_finish]]
451 452
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
453
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ _ K))
454 455
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
456
    |pm_reflexivity
457
    |first [wp_seq|wp_finish]]
458
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
459 460
  end.

461 462 463 464
Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
465
  wp_pures;
466 467 468
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
    first
469
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas _ _ _ _ _ _ K))
470 471 472 473 474
      |fail 1 "wp_cas: cannot find 'CAS' in" e];
    [iSolveTC
    |solve_mapsto ()
    |pm_reflexivity
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
475 476
    |intros H1; wp_finish
    |intros H2; wp_finish]
477 478
  | |- envs_entails _ (twp ?E ?e ?Q) =>
    first
479
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas _ _ _ _ _ K))
480 481 482 483
      |fail 1 "wp_cas: cannot find 'CAS' in" e];
    [solve_mapsto ()
    |pm_reflexivity
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
484 485
    |intros H1; wp_finish
    |intros H2; wp_finish]
486 487 488
  | _ => fail "wp_cas: not a 'wp'"
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
489
Tactic Notation "wp_cas_fail" :=
490 491 492
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
493
  wp_pures;
494
  lazymatch goal with
495
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
496
    first
497
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ _ K))
498
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
499
    [iSolveTC
500 501
    |solve_mapsto ()
    |try congruence
502
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
503
    |wp_finish]
504 505
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
506
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
507 508
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    [solve_mapsto ()
509
    |try congruence
510
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
511
    |wp_finish]
512
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
513 514 515
  end.

Tactic Notation "wp_cas_suc" :=
516 517 518
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
519
  wp_pures;
520
  lazymatch goal with
521
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
522
    first
523
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ _ K))
524
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
525
    [iSolveTC
526
    |solve_mapsto ()
527
    |pm_reflexivity
528 529
    |try congruence
    |try fast_done (* vals_cas_compare_safe *)
530
    |wp_finish]
Robbert Krebbers's avatar
Robbert Krebbers committed
531
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
532
    first
533
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
534 535
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    [solve_mapsto ()
536
    |pm_reflexivity
537 538
    |try congruence
    |try fast_done (* vals_cas_compare_safe *)
539
    |wp_finish]
540
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
541
  end.
542 543

Tactic Notation "wp_faa" :=
544 545 546
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
547
  wp_pures;
548
  lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
549
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
550
    first
551
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))
552
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
553
    [iSolveTC
554
    |solve_mapsto ()
555
    |pm_reflexivity
556
    |wp_finish]
557 558
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
559
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K))
560 561
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
    [solve_mapsto ()
562
    |pm_reflexivity
563
    |wp_finish]
564 565
  | _ => fail "wp_faa: not a 'wp'"
  end.