proofmode.v 11.1 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
9
10
11
12
13
(** wp-specific helper tactics *)
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
14

15
16
17
18
19
20
21
22
23
24
(* Solves side-conditions generated by the wp tactics *)
Ltac wp_done :=
  match goal with
  | |- Closed _ _ => solve_closed
  | |- is_Some (to_val _) => solve_to_val
  | |- to_val _ = Some _ => solve_to_val
  | |- language.to_val _ = Some _ => solve_to_val
  | _ => fast_done
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl.
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

Ltac wp_seq_head :=
  lazymatch goal with
  | |- _  wp ?E (Seq _ _) ?Q =>
    etrans; [|eapply wp_seq; wp_done]; iNext
  end.

Ltac wp_finish := intros_revert ltac:(
  rewrite /= ?to_of_val;
  try iNext;
  repeat lazymatch goal with
  | |- _  wp ?E (Seq _ _) ?Q =>
     etrans; [|eapply wp_seq; wp_done]; iNext
  | |- _  wp ?E _ ?Q => wp_value_head
  end).

Tactic Notation "wp_value" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
  | _ => fail "wp_value: not a wp"
  end.

Lemma of_val_unlock v e : of_val v = e  of_val (locked v) = e.
Proof. by unlock. Qed.

(* Applied to goals that are equalities of expressions. Will try to unlock the
   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.

Tactic Notation "wp_rec" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(*      match eval hnf in e1 with Rec _ _ _ => *)
    wp_bind_core K; etrans;
      [|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
  | _ => fail "wp_rec: not a 'wp'"
  end.

Tactic Notation "wp_lam" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with App ?e1 _ =>
(*    match eval hnf in e1 with Rec BAnon _ _ => *)
    wp_bind_core K; etrans;
      [|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
  | _ => fail "wp_lam: not a 'wp'"
  end.

Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_let.

Tactic Notation "wp_op" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    lazymatch eval hnf in e' with
    | BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
    | BinOp EqOp _ _ =>
       wp_bind_core K; eapply wp_eq; [wp_done|wp_done|wp_finish|wp_finish]
    | BinOp _ _ _ =>
       wp_bind_core K; etrans;
         [|eapply wp_bin_op; [wp_done|wp_done|try fast_done]]; wp_finish
    | UnOp _ _ =>
       wp_bind_core K; etrans;
         [|eapply wp_un_op; [wp_done|try fast_done]]; wp_finish
    end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
  | _ => fail "wp_op: not a 'wp'"
  end.

Tactic Notation "wp_proj" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
    | Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
    end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
  | _ => fail "wp_proj: not a 'wp'"
  end.

Tactic Notation "wp_if" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | If _ _ _ =>
      wp_bind_core K;
      etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
    end) || fail "wp_if: cannot find 'If' in" e
  | _ => fail "wp_if: not a 'wp'"
  end.

Tactic Notation "wp_match" :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Case _ _ _ =>
      wp_bind_core K;
      etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
      simpl_subst; wp_finish
    end) || fail "wp_match: cannot find 'Match' in" e
  | _ => fail "wp_match: not a 'wp'"
  end.

Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match e' with
    | efoc => unify e' efoc; wp_bind_core K
    end) || fail "wp_bind: cannot find" efoc "in" e
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Section heap.
152
Context `{heapG Σ}.
153
154
155
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
156

157
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
158
  to_val e = Some v 
159
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  ( l,  Δ'',
161
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
162
    (Δ''  Φ (LitV (LitLoc l)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
165
166
  intros ?? HΔ. eapply wand_apply; first exact: wp_alloc.
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
169
170
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

171
Lemma tac_wp_load Δ Δ' E i l q v Φ :
172
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  envs_lookup i Δ' = Some (false, l {q} v)%I 
174
  (Δ'  Φ v) 
175
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Proof.
177
  intros. eapply wand_apply; first exact: wp_load.
178
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
181
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

182
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
183
  to_val e = Some v' 
184
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
187
  (Δ''  Φ (LitV LitUnit)) 
188
  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
Proof.
190
  intros. eapply wand_apply; first by eapply wp_store.
191
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

195
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
196
  to_val e1 = Some v1  to_val e2 = Some v2 
197
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
198
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
199
  (Δ'  Φ (LitV (LitBool false))) 
200
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Proof.
202
  intros. eapply wand_apply; first exact: wp_cas_fail.
203
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
206
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

207
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
208
  to_val e1 = Some v1  to_val e2 = Some v2 
209
  IntoLaterNEnvs 1 Δ Δ' 
210
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
212
  (Δ''  Φ (LitV (LitBool true))) 
213
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Proof.
215
  intros; subst. eapply wand_apply; first exact: wp_cas_suc.
216
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
219
220
221
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
222
223
224
225
226
227
228
229
230
231
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
    | |- _  wp ?E ?e ?Q =>
      reshape_expr e ltac:(fun K e' =>
        wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
      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
232
233

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
234
  iStartProof;
235
  lazymatch goal with
236
237
238
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
239
         match eval hnf in e' with Alloc _ => wp_bind_core K end)
240
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
241
    eapply tac_wp_alloc with _ H _;
242
243
244
245
246
247
248
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_alloc:" e' "not a value"
      |apply _
      |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
        eexists; split;
          [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
          |wp_finish]]
249
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
250
  end.
251

252
253
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255

Tactic Notation "wp_load" :=
256
  iStartProof;
257
  lazymatch goal with
258
259
260
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
261
         match eval hnf in e' with Load _ => wp_bind_core K end)
262
263
      |fail 1 "wp_load: cannot find 'Load' in" e];
    eapply tac_wp_load;
264
      [apply _
265
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
266
       iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
267
      |wp_finish]
268
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
  end.

Tactic Notation "wp_store" :=
272
  iStartProof;
273
  lazymatch goal with
274
275
276
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
277
         match eval hnf in e' with Store _ _ => wp_bind_core K end)
278
279
280
281
282
283
284
285
      |fail 1 "wp_store: cannot find 'Store' in" e];
    eapply tac_wp_store;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_store:" e' "not a value"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
      |env_cbv; reflexivity
286
      |wp_finish]
287
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
288
289
290
  end.

Tactic Notation "wp_cas_fail" :=
291
  iStartProof;
292
  lazymatch goal with
293
294
295
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
296
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
297
298
299
300
301
302
303
304
305
306
307
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    eapply tac_wp_cas_fail;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
      |try congruence
      |wp_finish]
308
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
309
310
311
  end.

Tactic Notation "wp_cas_suc" :=
312
  iStartProof;
313
  lazymatch goal with
314
315
316
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
317
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
318
319
320
321
322
323
324
325
326
327
328
329
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    eapply tac_wp_cas_suc;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
      |try congruence
      |env_cbv; reflexivity
      |wp_finish]
330
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
331
  end.