proofmode.v 9.59 KB
Newer Older
1
From iris.program_logic Require Export 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
12
Proof. by intros ->. Qed.

13
Ltac wp_expr_eval t :=
14
  try iStartProof;
15
  try (eapply tac_wp_expr_eval; [t; reflexivity|]).
16

17
18
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
19

20
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
21
22
  PureExec φ e1 e2 
  φ 
23
  IntoLaterNEnvs 1 Δ Δ' 
24
25
  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) 
  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
26
Proof.
27
  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
28
  rewrite HΔ' -wp_pure_step_later //.
29
Qed.
30

31
Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
32
  IntoVal e v 
33
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ s; E {{ Φ }}).
34
35
36
Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.

Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
Tactic Notation "wp_pure" open_constr(efoc) :=
39
40
  iStartProof;
  lazymatch goal with
41
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
45
      eapply (tac_wp_pure _ _ _ _ (fill K e'));
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
      [apply _                        (* PureExec *)
      |try fast_done                  (* The pure condition for PureExec *)
      |apply _                        (* IntoLaters *)
49
      |wp_expr_simpl_subst; try wp_value_head (* new goal *)
Robbert Krebbers's avatar
Robbert Krebbers committed
50
      ])
51
52
   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
  | _ => fail "wp_pure: not a 'wp'"
53
54
  end.

55
56
57
58
59
60
61
62
63
64
65
66
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 _ _ _).
67
Tactic Notation "wp_match" := wp_case; wp_let.
68

69
<<<<<<< HEAD
70
71
72
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
  envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I 
  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
73
Proof. rewrite /envs_entails=> ->. by apply: wp_bind. Qed.
74
=======
75
76
77
Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e f :
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
  envs_entails Δ (WP e @ E {{ v, WP f (of_val v) @ E {{ Φ }} }})%I 
78
  envs_entails Δ (WP fill K e @ E {{ Φ }}).
79
Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
80
>>>>>>> master
81

Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
84
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
85
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
  end.

88
89
90
Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
91
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
92
93
    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
94
95
96
97
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Section heap.
99
Context `{heapG Σ}.
100
101
102
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
103

104
Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
105
  IntoVal e v 
106
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  ( l,  Δ'',
108
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
109
110
    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
111
Proof.
112
113
  rewrite /envs_entails=> ?? HΔ.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
114
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
117
118
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

119
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
120
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  envs_lookup i Δ' = Some (false, l {q} v)%I 
122
123
  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
124
Proof.
125
126
  rewrite /envs_entails=> ???.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
127
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

131
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
132
  IntoVal e v' 
133
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
136
137
  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
138
Proof.
139
140
  rewrite /envs_entails=> ?????.
  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
141
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

145
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  IntoVal e1 v1  AsVal e2 
147
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
148
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
149
150
  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
151
Proof.
152
153
  rewrite /envs_entails=> ??????.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
154
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

158
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
159
  IntoVal e1 v1  IntoVal e2 v2 
160
  IntoLaterNEnvs 1 Δ Δ' 
161
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
162
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
163
164
  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
165
Proof.
166
167
  rewrite /envs_entails=> ???????; subst.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
168
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
172
173
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
174
175
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
176
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
177
      reshape_expr e ltac:(fun K e' =>
178
        wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
179
180
181
182
183
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
    | _ => fail "wp_apply: not a 'wp'"
    end).
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
186
  iStartProof;
187
  lazymatch goal with
188
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
189
    first
190
      [reshape_expr e ltac:(fun K e' =>
191
         eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
192
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
193
    [apply _
194
195
196
    |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
197
        |wp_expr_simpl; try wp_value_head]]
198
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  end.
200

201
202
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204

Tactic Notation "wp_load" :=
205
  iStartProof;
206
  lazymatch goal with
207
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
208
    first
209
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
210
      |fail 1 "wp_load: cannot find 'Load' in" e];
211
212
213
    [apply _
    |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
     iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
214
    |wp_expr_simpl; try wp_value_head]
215
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
  end.

Tactic Notation "wp_store" :=
219
  iStartProof;
220
  lazymatch goal with
221
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
222
    first
223
      [reshape_expr e ltac:(fun K e' =>
224
         eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
225
      |fail 1 "wp_store: cannot find 'Store' in" e];
226
    [apply _
227
228
229
    |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
     iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
    |env_cbv; reflexivity
230
    |wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
231
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
234
  end.

Tactic Notation "wp_cas_fail" :=
235
  iStartProof;
236
  lazymatch goal with
237
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
238
    first
239
      [reshape_expr e ltac:(fun K e' =>
240
         eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
241
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
242
    [apply _
243
244
245
    |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
     iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
    |try congruence
246
    |wp_expr_simpl; try wp_value_head]
247
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
250
  end.

Tactic Notation "wp_cas_suc" :=
251
  iStartProof;
252
  lazymatch goal with
253
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
254
    first
255
      [reshape_expr e ltac:(fun K e' =>
256
         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
257
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
258
    [apply _
259
260
261
262
    |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
     iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
    |try congruence
    |env_cbv; reflexivity
263
    |wp_expr_simpl; try wp_value_head]
264
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  end.