proofmode.v 10.4 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

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.


58
59
60
(* Solves side-conditions generated specifically by wp_pure *)
Ltac wp_pure_done :=
  split_and?;
61
  lazymatch goal with
62
63
  | |- of_val _ = _ => solve_of_val_unlock
  | _ => wp_done
64
65
  end.

66
67
68
69
70
71
72
73
74
75
76
Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
  IntoLaterNEnvs 1 Δ Δ' 
  PureExec φ e1 e2 
  φ 
  (Δ'  WP fill K e2 @ E {{ Φ }}) 
  (Δ  WP fill K e1 @ E {{ Φ }}).
Proof.
  intros ??? HΔ'.
  rewrite into_laterN_env_sound /=.
  rewrite HΔ' -wp_pure' //.
Qed.
77

78
Tactic Notation "wp_pure" open_constr(efoc) :=
79
80
81
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
82
83
84
85
86
87
88
89
90
91
    let e'' := eval hnf in e' in
    unify e'' efoc;
    wp_bind_core K;
    eapply (tac_wp_pure []);
    [apply _                  (* IntoLaters *)
    |unlock; simpl; apply _   (* PureExec *)
    |wp_pure_done             (* The pure condition for PureExec *)
    |simpl_subst; wp_finish   (* new goal *)])
   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
  | _ => fail "wp_pure: not a 'wp'"
92
93
  end.

94
95
96
97
98
99
100
101
102
103
104
105
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 _ _ _).
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
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
130
Section heap.
131
Context `{heapG Σ}.
132
133
134
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
135

136
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
137
  to_val e = Some v 
138
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
139
  ( l,  Δ'',
140
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
141
    (Δ''  Φ (LitV (LitLoc l)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
144
145
  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
146
147
148
149
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

150
Lemma tac_wp_load Δ Δ' E i l q v Φ :
151
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  envs_lookup i Δ' = Some (false, l {q} v)%I 
153
  (Δ'  Φ v) 
154
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Proof.
156
  intros. eapply wand_apply; first exact: wp_load.
157
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

161
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
162
  to_val e = Some v' 
163
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
166
  (Δ''  Φ (LitV LitUnit)) 
167
  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Proof.
169
  intros. eapply wand_apply; first by eapply wp_store.
170
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
173
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

174
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  to_val e1 = Some v1  to_val e2 = Some v2 
176
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
178
  (Δ'  Φ (LitV (LitBool false))) 
179
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Proof.
181
  intros. eapply wand_apply; first exact: wp_cas_fail.
182
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
185
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

186
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  to_val e1 = Some v1  to_val e2 = Some v2 
188
  IntoLaterNEnvs 1 Δ Δ' 
189
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
191
  (Δ''  Φ (LitV (LitBool true))) 
192
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Proof.
194
  intros; subst. eapply wand_apply; first exact: wp_cas_suc.
195
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
199
200
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
201
202
203
204
205
206
207
208
209
210
  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
211
212

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
213
  iStartProof;
214
  lazymatch goal with
215
216
217
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
218
         match eval hnf in e' with Alloc _ => wp_bind_core K end)
219
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
220
    eapply tac_wp_alloc with _ H _;
221
222
223
224
225
226
227
      [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]]
228
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
229
  end.
230

231
232
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234

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

Tactic Notation "wp_store" :=
251
  iStartProof;
252
  lazymatch goal with
253
254
255
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
256
         match eval hnf in e' with Store _ _ => wp_bind_core K end)
257
258
259
260
261
262
263
264
      |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
265
      |wp_finish]
266
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
267
268
269
  end.

Tactic Notation "wp_cas_fail" :=
270
  iStartProof;
271
  lazymatch goal with
272
273
274
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
275
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
276
277
278
279
280
281
282
283
284
285
286
      |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]
287
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
288
289
290
  end.

Tactic Notation "wp_cas_suc" :=
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
308
      |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]
309
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
310
  end.