proofmode.v 17.8 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'), e = e'') 
10
  envs_entails Δ (WP e' @ s; E {{ Φ }})  envs_entails Δ (WP e @ s; E {{ Φ }}).
11
Proof. by intros ->. Qed.
12
Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
13
  ( (e'':=e'), e = e'') 
14 15
  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 19 20 21 22 23 24 25 26 27
  iStartProof;
  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.
28

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

32
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
33 34
  PureExec φ e1 e2 
  φ 
35
  MaybeIntoLaterNEnvs 1 Δ Δ' 
36 37
  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) 
  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
38
Proof.
39
  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
40 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.
  rewrite /envs_entails=> ?? ->. rewrite -total_lifting.twp_pure_step //.
49
Qed.
50

51
Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
52
  IntoVal e v 
53
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ s; E {{ Φ }}).
54
Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
55 56 57 58
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.
59

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
315 316 317 318 319
  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
320
  iStartProof;
321
  lazymatch goal with
322
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
323
    first
324
      [reshape_expr e ltac:(fun K e' =>
325
         eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
326
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
327
    [apply _
328 329 330 331 332 333 334
    |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 ()
335
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  end.
337

338 339
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341

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

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

Tactic Notation "wp_cas_fail" :=
392 393 394
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_fail: 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' =>
400
         eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
401
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
402
    [apply _
403 404 405 406 407 408 409 410 411
    |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 ()
412
    |try congruence
413
    |wp_expr_simpl; try wp_value_head]
414
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416 417
  end.

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

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