proofmode.v 18.4 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
43
44
45
46
47
48
  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.
49
  rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
50
Qed.
51

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

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

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

93
94
95
96
97
98
99
100
101
102
103
104
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 _ _ _).
105
Tactic Notation "wp_match" := wp_case; wp_let.
106

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

Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
120
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
121
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
Robbert Krebbers's avatar
Robbert Krebbers committed
122
  end.
123
124
125
126
127
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
128

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

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

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

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

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

224
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  IntoVal e1 v1  AsVal e2 
226
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Ralf Jung's avatar
Ralf Jung committed
227
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1  vals_cas_compare_safe v v1 
228
229
  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
230
Proof.
Ralf Jung's avatar
Ralf Jung committed
231
  rewrite envs_entails_eq=> ???????.
232
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
233
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
235
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
236
237
Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
  IntoVal e1 v1  AsVal e2 
Ralf Jung's avatar
Ralf Jung committed
238
  envs_lookup i Δ = Some (false, l {q} v)%I  v  v1  vals_cas_compare_safe v v1 
239
240
241
  envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
242
243
244
  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.
245
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246

247
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
248
  IntoVal e1 v1  IntoVal e2 v2 
249
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Ralf Jung's avatar
Ralf Jung committed
250
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1  vals_cas_compare_safe v v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
252
253
  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
254
Proof.
Ralf Jung's avatar
Ralf Jung committed
255
  rewrite envs_entails_eq=> ????????; subst.
256
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
257
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
260
261
Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
  IntoVal e1 v1  IntoVal e2 v2 
Ralf Jung's avatar
Ralf Jung committed
262
  envs_lookup i Δ = Some (false, l  v)%I  v = v1  vals_cas_compare_safe v v1 
263
264
265
266
  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.
267
268
  rewrite envs_entails_eq. intros; subst.
  rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
269
270
271
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
272

Ralf Jung's avatar
Ralf Jung committed
273
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
274
  IntoVal e2 (LitV (LitInt i2)) 
275
  MaybeIntoLaterNEnvs 1 Δ Δ' 
276
277
  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
278
279
  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
280
Proof.
281
  rewrite envs_entails_eq=> ?????; subst.
Ralf Jung's avatar
Ralf Jung committed
282
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
283
284
285
  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.
286
287
288
289
290
291
292
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.
293
  rewrite envs_entails_eq=> ????; subst.
294
295
296
297
  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
298
299
300
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
301
302
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
303
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
304
      reshape_expr e ltac:(fun K e' =>
305
        wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
306
307
308
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
309
310
    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' =>
311
        twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
312
313
314
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
315
316
    | _ => fail "wp_apply: not a 'wp'"
    end).
Robbert Krebbers's avatar
Robbert Krebbers committed
317
318

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
319
320
321
  let finish _ :=
    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
322
        [pm_reflexivity || fail "wp_alloc:" H "not fresh"
323
        |wp_expr_simpl; try wp_value_head] in
324
  iStartProof;
325
  lazymatch goal with
326
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
327
    first
328
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
329
         eapply (tac_wp_alloc _ _ _ _ H K); [iSolveTC|..])
330
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
Ralf Jung's avatar
Ralf Jung committed
331
    [iSolveTC
332
333
334
335
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
336
         eapply (tac_twp_alloc _ _ _ H K); [iSolveTC|..])
337
338
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
    finish ()
339
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
340
  end.
341

342
343
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
345

Tactic Notation "wp_load" :=
346
347
348
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
349
  iStartProof;
350
  lazymatch goal with
351
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
352
    first
353
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
354
      |fail 1 "wp_load: cannot find 'Load' in" e];
Ralf Jung's avatar
Ralf Jung committed
355
    [iSolveTC
356
357
358
359
360
361
362
    |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 ()
363
    |wp_expr_simpl; try wp_value_head]
364
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
365
366
367
  end.

Tactic Notation "wp_store" :=
368
369
370
371
372
  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
373
  iStartProof;
374
  lazymatch goal with
375
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
376
    first
377
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
378
         eapply (tac_wp_store _ _ _ _ _ _ K); [iSolveTC|..])
379
      |fail 1 "wp_store: cannot find 'Store' in" e];
Ralf Jung's avatar
Ralf Jung committed
380
    [iSolveTC
381
    |solve_mapsto ()
382
    |pm_reflexivity
383
384
385
386
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
387
         eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
388
389
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
390
    |pm_reflexivity
391
    |finish ()]
392
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
393
394
395
  end.

Tactic Notation "wp_cas_fail" :=
396
397
398
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
399
  iStartProof;
400
  lazymatch goal with
401
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
402
    first
403
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
404
         eapply (tac_wp_cas_fail _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
405
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
406
    [iSolveTC
407
408
    |solve_mapsto ()
    |try congruence
409
    |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
410
411
412
413
    |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
414
         eapply (tac_twp_cas_fail _ _ _ _ K); [iSolveTC|iSolveTC|..])
415
416
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    [solve_mapsto ()
417
    |try congruence
418
    |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
419
    |wp_expr_simpl; try wp_value_head]
420
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
  end.

Tactic Notation "wp_cas_suc" :=
424
425
426
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
427
  iStartProof;
428
  lazymatch goal with
429
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
430
    first
431
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
432
         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
433
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
434
    [iSolveTC
435
436
    |solve_mapsto ()
    |try congruence
437
    |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
438
    |pm_reflexivity
439
440
441
442
    |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
443
         eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
444
445
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    [solve_mapsto ()
446
    |try congruence
447
    |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
448
    |pm_reflexivity
449
    |wp_expr_simpl; try wp_value_head]
450
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
451
  end.
452
453

Tactic Notation "wp_faa" :=
454
455
456
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
457
458
  iStartProof;
  lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
459
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
460
461
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
462
         eapply (tac_wp_faa _ _ _ _ _ _ K); [iSolveTC|..])
463
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
464
    [iSolveTC
465
    |solve_mapsto ()
466
    |pm_reflexivity
467
468
469
470
    |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
471
         eapply (tac_twp_faa _ _ _ _ _ K); [iSolveTC|..])
472
473
      |fail 1 "wp_faa: cannot find 'CAS' in" e];
    [solve_mapsto ()
474
    |pm_reflexivity
475
476
477
    |wp_expr_simpl; try wp_value_head]
  | _ => fail "wp_faa: not a 'wp'"
  end.