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

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

18
Tactic Notation "wp_expr_eval" tactic(t) :=
19
  iStartProof;
20
21
22
23
24
25
26
27
28
  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.
29

30
31
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
32

33
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
34
35
  PureExec φ e1 e2 
  φ 
36
  MaybeIntoLaterNEnvs 1 Δ Δ' 
37
38
  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) 
  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
39
Proof.
40
  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
41
42
  rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
43

44
45
46
47
48
49
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
  PureExec φ e1 e2 
  φ 
  envs_entails Δ (WP e2 @ s; E [{ Φ }]) 
  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
Proof.
50
  rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
51
Qed.
52

53
Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
54
  IntoVal e v 
55
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ s; E {{ Φ }}).
56
Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
57
58
59
Lemma tac_twp_value `{heapG Σ} Δ s E Φ e v :
  IntoVal e v 
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ s; E [{ Φ }]).
60
Proof. rewrite envs_entails_eq=> ? ->. by apply twp_value. Qed.
61

Robbert Krebbers's avatar
Robbert Krebbers committed
62
Ltac wp_value_head :=
63
  first [eapply tac_wp_value || eapply tac_twp_value];
Ralf Jung's avatar
Ralf Jung committed
64
    [iSolveTC
65
    |reduction.pm_prettify; iEval (simpl of_val)].
Robbert Krebbers's avatar
Robbert Krebbers committed
66

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

94
95
96
97
98
99
100
101
102
103
104
105
Tactic Notation "wp_if" := wp_pure (If _ _ _).
Tactic Notation "wp_if_true" := wp_pure (If (Lit (LitBool true)) _ _).
Tactic Notation "wp_if_false" := wp_pure (If (Lit (LitBool false)) _ _).
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_rec" := wp_pure (App _ _).
Tactic Notation "wp_lam" := wp_rec.
Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_lam.
Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
106
Tactic Notation "wp_match" := wp_case; wp_let.
107

Ralf Jung's avatar
Ralf Jung committed
108
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
109
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
Ralf Jung's avatar
Ralf Jung committed
110
111
  envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I 
  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
112
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
113
114
115
116
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 *)
  envs_entails Δ (WP e @ s; E [{ v, WP f (of_val v) @ s; E [{ Φ }] }])%I 
  envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
117
Proof. rewrite envs_entails_eq=> -> ->. by apply: twp_bind. Qed.
118

Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
121
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
122
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify]
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  end.
124
125
126
Ltac twp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
127
  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|reduction.pm_prettify]
128
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
129

130
131
132
Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
133
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
134
135
    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
136
137
138
  | |- 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
139
140
141
142
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Section heap.
144
Context `{heapG Σ}.
145
146
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Implicit Types Δ : envs (uPredI (iResUR Σ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
148

149
Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
150
  IntoVal e v 
151
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  ( l,  Δ'',
153
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
154
155
    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (Alloc e) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Proof.
157
  rewrite envs_entails_eq=> ?? HΔ.
158
  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
159
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
162
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.
163
164
165
166
167
168
169
Lemma tac_twp_alloc Δ s E j K e v Φ :
  IntoVal e v 
  ( l,  Δ',
    envs_app false (Esnoc Enil j (l  v)) Δ = Some Δ' 
    envs_entails Δ' (WP fill K (Lit (LitLoc l)) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (Alloc e) @ s; E [{ Φ }]).
Proof.
170
  rewrite envs_entails_eq=> ? HΔ.
171
172
173
174
175
  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
176

177
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
178
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  envs_lookup i Δ' = Some (false, l {q} v)%I 
180
181
  envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Proof.
183
  rewrite envs_entails_eq=> ???.
184
  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
185
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
188
189
190
191
192
Lemma tac_twp_load Δ s E i K l q v Φ :
  envs_lookup i Δ = Some (false, l {q} v)%I 
  envs_entails Δ (WP fill K (of_val v) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E [{ Φ }]).
Proof.
193
  rewrite envs_entails_eq=> ??.
194
195
196
197
  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
198

199
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
200
  IntoVal e v' 
201
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
204
205
  envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
206
Proof.
207
  rewrite envs_entails_eq=> ?????.
208
  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
209
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
212
213
214
215
216
217
218
Lemma tac_twp_store Δ Δ' s E i K l v e v' Φ :
  IntoVal e v' 
  envs_lookup i Δ = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ = Some Δ' 
  envs_entails Δ' (WP fill K (Lit LitUnit) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E [{ Φ }]).
Proof.
219
220
  rewrite envs_entails_eq. intros. rewrite -twp_bind.
  eapply wand_apply; first by eapply twp_store.
221
222
223
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
224

225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
  IntoVal e1 v1  IntoVal e2 v2 
  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 
  (v = v1  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})) 
  (v  v1  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_eq=> ?????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
  - 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.
    { eapply wp_cas_fail; eauto. by eexists. }
    rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
    apply later_mono, sep_mono_r. apply wand_mono; auto.
Qed.
Lemma tac_twp_cas Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
  IntoVal e1 v1  IntoVal e2 v2 
  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 
  (v = v1  envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }])) 
  (v  v1  envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_eq=> ????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
  - 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.
    { eapply twp_cas_fail; eauto. by eexists. }
    rewrite /= {1}envs_lookup_split //; simpl.
    apply sep_mono_r. apply wand_mono; auto.
Qed.

263
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
264
  IntoVal e1 v1  AsVal e2 
265
  MaybeIntoLaterNEnvs 1 Δ Δ' 
266
267
  envs_lookup i Δ' = Some (false, l {q} v)%I 
  v  v1  vals_cas_compare_safe v v1 
268
269
  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
270
Proof.
Ralf Jung's avatar
Ralf Jung committed
271
  rewrite envs_entails_eq=> ???????.
272
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
273
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
276
277
Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
  IntoVal e1 v1  AsVal e2 
278
279
  envs_lookup i Δ = Some (false, l {q} v)%I 
  v  v1  vals_cas_compare_safe v v1 
280
281
282
  envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
283
284
285
  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.
286
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
287

288
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
289
  IntoVal e1 v1  IntoVal e2 v2 
290
  MaybeIntoLaterNEnvs 1 Δ Δ' 
291
  envs_lookup i Δ' = Some (false, l  v)%I 
Robbert Krebbers's avatar
Robbert Krebbers committed
292
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
293
  v = v1  val_is_unboxed v 
294
295
  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Proof.
Ralf Jung's avatar
Ralf Jung committed
297
  rewrite envs_entails_eq=> ????????; subst.
298
299
  rewrite -wp_bind. eapply wand_apply.
  { eapply wp_cas_suc; eauto. by left. }
300
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
303
304
Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
  IntoVal e1 v1  IntoVal e2 v2 
305
  envs_lookup i Δ = Some (false, l  v)%I 
306
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
307
  v = v1  val_is_unboxed v 
308
309
310
  envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
311
  rewrite envs_entails_eq. intros; subst.
312
313
  rewrite -twp_bind. eapply wand_apply.
  { eapply twp_cas_suc; eauto. by left. }
314
315
316
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
317

Ralf Jung's avatar
Ralf Jung committed
318
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
319
  IntoVal e2 (LitV (LitInt i2)) 
320
  MaybeIntoLaterNEnvs 1 Δ Δ' 
321
322
  envs_lookup i Δ' = Some (false, l  LitV (LitInt i1))%I 
  envs_simple_replace i false (Esnoc Enil i (l  LitV (LitInt (i1 + i2)))) Δ' = Some Δ'' 
Ralf Jung's avatar
Ralf Jung committed
323
324
  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
325
Proof.
326
  rewrite envs_entails_eq=> ?????; subst.
Ralf Jung's avatar
Ralf Jung committed
327
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
328
329
330
  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.
331
332
333
334
335
336
337
Lemma tac_twp_faa Δ Δ' s E i K l i1 e2 i2 Φ :
  IntoVal e2 (LitV (LitInt i2)) 
  envs_lookup i Δ = Some (false, l  LitV (LitInt i1))%I 
  envs_simple_replace i false (Esnoc Enil i (l  LitV (LitInt (i1 + i2)))) Δ = Some Δ' 
  envs_entails Δ' (WP fill K (Lit (LitInt i1)) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E [{ Φ }]).
Proof.
338
  rewrite envs_entails_eq=> ????; subst.
339
340
341
342
  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ i1 _ i2).
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
345
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
346
347
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
348
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
349
      reshape_expr e ltac:(fun K e' =>
350
        wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
351
352
353
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
354
355
    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' =>
356
        twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
357
358
359
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
360
361
    | _ => fail "wp_apply: not a 'wp'"
    end).
Robbert Krebbers's avatar
Robbert Krebbers committed
362
363

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
364
  let Htmp := iFresh in
365
366
367
  let finish _ :=
    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
368
        [pm_reflexivity || fail "wp_alloc:" H "not fresh"
369
        |iDestructHyp Htmp as H; wp_expr_simpl; try wp_value_head] in
370
  iStartProof;
371
  lazymatch goal with
372
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
373
    first
374
      [reshape_expr e ltac:(fun K e' =>
375
         eapply (tac_wp_alloc _ _ _ _ Htmp K); [iSolveTC|..])
376
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
Ralf Jung's avatar
Ralf Jung committed
377
    [iSolveTC
378
379
380
381
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
382
         eapply (tac_twp_alloc _ _ _ Htmp K); [iSolveTC|..])
383
384
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
    finish ()
385
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
386
  end.
387

388
Tactic Notation "wp_alloc" ident(l) :=
389
  wp_alloc l as "?".
Robbert Krebbers's avatar
Robbert Krebbers committed
390
391

Tactic Notation "wp_load" :=
392
393
394
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
395
  iStartProof;
396
  lazymatch goal with
397
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
398
    first
399
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
400
      |fail 1 "wp_load: cannot find 'Load' in" e];
Ralf Jung's avatar
Ralf Jung committed
401
    [iSolveTC
402
403
404
405
406
407
408
    |solve_mapsto ()
    |wp_expr_simpl; try wp_value_head]
  | |- 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 ()
409
    |wp_expr_simpl; try wp_value_head]
410
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
411
412
413
  end.

Tactic Notation "wp_store" :=
414
415
416
417
418
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
  let finish _ :=
    wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head] in
419
  iStartProof;
420
  lazymatch goal with
421
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
422
    first
423
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
424
         eapply (tac_wp_store _ _ _ _ _ _ K); [iSolveTC|..])
425
      |fail 1 "wp_store: cannot find 'Store' in" e];
Ralf Jung's avatar
Ralf Jung committed
426
    [iSolveTC
427
    |solve_mapsto ()
428
    |pm_reflexivity
429
430
431
432
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
433
         eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
434
435
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
436
    |pm_reflexivity
437
    |finish ()]
438
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
  end.

441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
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
  iStartProof;
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
         eapply (tac_wp_cas _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
      |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 *)
    |intros H1; wp_expr_simpl; try wp_value_head
    |intros H2; wp_expr_simpl; try wp_value_head]
  | |- envs_entails _ (twp ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
         eapply (tac_twp_cas _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
      |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 *)
    |intros H1; wp_expr_simpl; try wp_value_head
    |intros H2; wp_expr_simpl; try wp_value_head]
  | _ => fail "wp_cas: not a 'wp'"
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
471
Tactic Notation "wp_cas_fail" :=
472
473
474
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
475
  iStartProof;
476
  lazymatch goal with
477
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
478
    first
479
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
480
         eapply (tac_wp_cas_fail _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
481
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
482
    [iSolveTC
483
484
    |solve_mapsto ()
    |try congruence
485
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
486
487
488
489
    |simpl; try wp_value_head]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
490
         eapply (tac_twp_cas_fail _ _ _ _ K); [iSolveTC|iSolveTC|..])
491
492
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    [solve_mapsto ()
493
    |try congruence
494
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
495
    |wp_expr_simpl; try wp_value_head]
496
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
497
498
499
  end.

Tactic Notation "wp_cas_suc" :=
500
501
502
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
503
  iStartProof;
504
  lazymatch goal with
505
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
506
    first
507
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
508
         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
509
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
510
    [iSolveTC
511
    |solve_mapsto ()
512
    |pm_reflexivity
513
514
    |try congruence
    |try fast_done (* vals_cas_compare_safe *)
515
516
517
518
    |simpl; try wp_value_head]
  | |- envs_entails _ (twp ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
519
         eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
520
521
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    [solve_mapsto ()
522
    |pm_reflexivity
523
524
    |try congruence
    |try fast_done (* vals_cas_compare_safe *)
525
    |wp_expr_simpl; try wp_value_head]
526
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
527
  end.
528
529

Tactic Notation "wp_faa" :=
530
531
532
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
533
534
  iStartProof;
  lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
535
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
536
537
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
538
         eapply (tac_wp_faa _ _ _ _ _ _ K); [iSolveTC|..])
539
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
540
    [iSolveTC
541
    |solve_mapsto ()
542
    |pm_reflexivity
543
544
545
546
    |wp_expr_simpl; try wp_value_head]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
547
         eapply (tac_twp_faa _ _ _ _ _ K); [iSolveTC|..])
548
549
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
    [solve_mapsto ()
550
    |pm_reflexivity
551
552
553
    |wp_expr_simpl; try wp_value_head]
  | _ => fail "wp_faa: not a 'wp'"
  end.