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

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

17
Tactic Notation "wp_expr_eval" tactic(t) :=
18
  try iStartProof;
19
20
  try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
       [t; reflexivity|]).
21

22
23
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
24

25
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
26
27
  PureExec φ e1 e2 
  φ 
28
  IntoLaterNEnvs 1 Δ Δ' 
29
30
  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) 
  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
31
Proof.
32
  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
33
34
35
36
37
38
39
40
41
  rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
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.
  rewrite /envs_entails=> ?? ->. rewrite -total_lifting.twp_pure_step //.
42
Qed.
43

44
Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
45
  IntoVal e v 
46
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ s; E {{ Φ }}).
47
Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
48
49
50
51
Lemma tac_twp_value `{heapG Σ} Δ s E Φ e v :
  IntoVal e v 
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. rewrite /envs_entails=> ? ->. by apply twp_value. Qed.
52

Robbert Krebbers's avatar
Robbert Krebbers committed
53
Ltac wp_value_head :=
54
  first [eapply tac_wp_value || eapply tac_twp_value];
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
    [apply _
    |iEval (lazy beta; simpl of_val)].
Robbert Krebbers's avatar
Robbert Krebbers committed
57

58
Tactic Notation "wp_pure" open_constr(efoc) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  iStartProof;
60
  lazymatch goal with
61
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
65
      eapply (tac_wp_pure _ _ _ _ (fill K e'));
Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
68
      [apply _                        (* PureExec *)
      |try fast_done                  (* The pure condition for PureExec *)
      |apply _                        (* IntoLaters *)
69
      |wp_expr_simpl_subst; try wp_value_head (* new goal *)
Robbert Krebbers's avatar
Robbert Krebbers committed
70
      ])
71
72
73
74
75
76
77
78
79
80
81
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
  | |- 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'));
      [apply _                        (* PureExec *)
      |try fast_done                  (* The pure condition for PureExec *)
      |wp_expr_simpl_subst; try wp_value_head (* new goal *)
      ])
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
82
  | _ => fail "wp_pure: not a 'wp'"
83
84
  end.

85
86
87
88
89
90
91
92
93
94
95
96
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 _ _ _).
97
Tactic Notation "wp_match" := wp_case; wp_let.
98

Ralf Jung's avatar
Ralf Jung committed
99
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
100
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
Ralf Jung's avatar
Ralf Jung committed
101
102
  envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I 
  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
103
Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
104
105
106
107
108
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 [{ Φ }]).
Proof. rewrite /envs_entails=> -> ->. by apply: twp_bind. Qed.
109

Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
113
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  end.
115
116
117
118
119
Ltac twp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|lazy beta]
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
120

121
122
123
Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
124
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
125
126
    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
127
128
129
  | |- 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
130
131
132
133
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Section heap.
135
Context `{heapG Σ}.
136
137
138
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
139

140
Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
141
  IntoVal e v 
142
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  ( l,  Δ'',
144
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
145
146
    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
147
Proof.
148
149
  rewrite /envs_entails=> ?? HΔ.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
150
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.
154
155
156
157
158
159
160
161
162
163
164
165
166
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.
  rewrite /envs_entails=> ? HΔ.
  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
167

168
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
169
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  envs_lookup i Δ' = Some (false, l {q} v)%I 
171
172
  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
173
Proof.
174
175
  rewrite /envs_entails=> ???.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
176
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
179
180
181
182
183
184
185
186
187
188
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.
  rewrite /envs_entails=> ??.
  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
189

190
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
191
  IntoVal e v' 
192
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
195
196
  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
197
Proof.
198
199
  rewrite /envs_entails=> ?????.
  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
200
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
203
204
205
206
207
208
209
210
211
212
213
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.
  intros. rewrite -twp_bind. eapply wand_apply; first by eapply twp_store.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
214

215
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
216
  IntoVal e1 v1  AsVal e2 
217
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
219
220
  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
221
Proof.
222
223
  rewrite /envs_entails=> ??????.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
224
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
226
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
227
228
229
230
231
232
233
234
235
Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
  IntoVal e1 v1  AsVal e2 
  envs_lookup i Δ = Some (false, l {q} v)%I  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.
  intros. rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_fail.
  rewrite envs_lookup_split //; simpl. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
236

237
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
238
  IntoVal e1 v1  IntoVal e2 v2 
239
  IntoLaterNEnvs 1 Δ Δ' 
240
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
241
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
242
243
  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
244
Proof.
245
246
  rewrite /envs_entails=> ???????; subst.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
247
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
250
251
252
253
254
255
256
257
258
259
260
Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
  IntoVal e1 v1  IntoVal e2 v2 
  envs_lookup i Δ = Some (false, l  v)%I  v = v1 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
  envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
  intros; subst. rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
261

Ralf Jung's avatar
Ralf Jung committed
262
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
263
264
265
266
  IntoVal e2 (LitV (LitInt i2)) 
  IntoLaterNEnvs 1 Δ Δ' 
  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
267
268
  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
269
270
Proof.
  rewrite /envs_entails=> ?????; subst.
Ralf Jung's avatar
Ralf Jung committed
271
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
272
273
274
  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.
275
276
277
278
279
280
281
282
283
284
285
286
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.
  rewrite /envs_entails=> ????; subst.
  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
287
288
289
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
290
291
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
292
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
293
      reshape_expr e ltac:(fun K e' =>
294
        wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
295
296
297
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
298
299
300
301
302
303
    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' =>
        twp_bind_core K; iApplyHyp H; wp_expr_simpl) ||
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
304
305
    | _ => fail "wp_apply: not a 'wp'"
    end).
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
308
309
310
311
312
  let finish _ :=
    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
        |wp_expr_simpl; try wp_value_head] in
313
  iStartProof;
314
  lazymatch goal with
315
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
316
    first
317
      [reshape_expr e ltac:(fun K e' =>
318
         eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
319
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
320
    [apply _
321
322
323
324
325
326
327
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
         eapply (tac_twp_alloc _ _ _ H K); [apply _|..])
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
    finish ()
328
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
329
  end.
330

331
332
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
334

Tactic Notation "wp_load" :=
335
336
337
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
338
  iStartProof;
339
  lazymatch goal with
340
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
341
    first
342
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
343
      |fail 1 "wp_load: cannot find 'Load' in" e];
344
    [apply _
345
346
347
348
349
350
351
    |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 ()
352
    |wp_expr_simpl; try wp_value_head]
353
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
356
  end.

Tactic Notation "wp_store" :=
357
358
359
360
361
  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
362
  iStartProof;
363
  lazymatch goal with
364
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
365
    first
366
      [reshape_expr e ltac:(fun K e' =>
367
         eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
368
      |fail 1 "wp_store: cannot find 'Store' in" e];
369
    [apply _
370
371
372
373
374
375
376
377
378
    |solve_mapsto ()
    |env_cbv; reflexivity
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
         eapply (tac_twp_store _ _ _ _ _ K); [apply _|..])
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
379
    |env_cbv; reflexivity
380
    |finish ()]
381
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
384
  end.

Tactic Notation "wp_cas_fail" :=
385
386
387
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
388
  iStartProof;
389
  lazymatch goal with
390
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
391
    first
392
      [reshape_expr e ltac:(fun K e' =>
393
         eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
394
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
395
    [apply _
396
397
398
399
400
401
402
403
404
    |solve_mapsto ()
    |try congruence
    |simpl; try wp_value_head]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
         eapply (tac_twp_cas_fail _ _ _ _ K); [apply _|apply _|..])
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    [solve_mapsto ()
405
    |try congruence
406
    |wp_expr_simpl; try wp_value_head]
407
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
408
409
410
  end.

Tactic Notation "wp_cas_suc" :=
411
412
413
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
414
  iStartProof;
415
  lazymatch goal with
416
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
417
    first
418
      [reshape_expr e ltac:(fun K e' =>
419
         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
420
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
421
    [apply _
422
423
424
425
426
427
428
429
430
431
    |solve_mapsto ()
    |try congruence
    |env_cbv; reflexivity
    |simpl; try wp_value_head]
  | |- envs_entails _ (twp ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
         eapply (tac_twp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    [solve_mapsto ()
432
433
    |try congruence
    |env_cbv; reflexivity
434
    |wp_expr_simpl; try wp_value_head]
435
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
436
  end.
437
438

Tactic Notation "wp_faa" :=
439
440
441
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
442
443
  iStartProof;
  lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
444
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
445
446
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
447
         eapply (tac_wp_faa _ _ _ _ _ _ K); [apply _|..])
448
449
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
    [apply _
450
451
452
453
454
455
456
457
458
    |solve_mapsto ()
    |env_cbv; reflexivity
    |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_faa _ _ _ _ _ K); [apply _|..])
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
    [solve_mapsto ()
459
460
461
462
    |env_cbv; reflexivity
    |wp_expr_simpl; try wp_value_head]
  | _ => fail "wp_faa: not a 'wp'"
  end.