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 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
64
    |reduction.pm_prettify; iEval (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|reduction.pm_prettify]
Robbert Krebbers's avatar
Robbert Krebbers committed
122
  end.
123 124 125
Ltac twp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
126
  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|reduction.pm_prettify]
127
  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 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
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.

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

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

Ralf Jung's avatar
Ralf Jung committed
317
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
318
  IntoVal e2 (LitV (LitInt i2)) 
319
  MaybeIntoLaterNEnvs 1 Δ Δ' 
320 321
  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
322 323
  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
324
Proof.
325
  rewrite envs_entails_eq=> ?????; subst.
Ralf Jung's avatar
Ralf Jung committed
326
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
327 328 329
  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.
330 331 332 333 334 335 336
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.
337
  rewrite envs_entails_eq=> ????; subst.
338 339 340 341
  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
342 343 344
End heap.

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

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

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

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

Tactic Notation "wp_store" :=
413 414 415 416 417
  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
418
  iStartProof;
419
  lazymatch goal with
420
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
421
    first
422
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
423
         eapply (tac_wp_store _ _ _ _ _ _ K); [iSolveTC|..])
424
      |fail 1 "wp_store: cannot find 'Store' in" e];
Ralf Jung's avatar
Ralf Jung committed
425
    [iSolveTC
426
    |solve_mapsto ()
427
    |pm_reflexivity
428 429 430 431
    |finish ()]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
432
         eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
433 434
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
435
    |pm_reflexivity
436
    |finish ()]
437
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
438 439
  end.

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

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

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