proofmode.v 9.02 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
(* Solves side-conditions generated specifically by wp_pure *)
Ltac wp_pure_done :=
29
  split_and?; wp_done.
30

31
32
33
Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
  PureExec φ e1 e2 
  φ 
34
  IntoLaterNEnvs 1 Δ Δ' 
35
36
37
  (Δ'  WP fill K e2 @ E {{ Φ }}) 
  (Δ  WP fill K e1 @ E {{ Φ }}).
Proof.
38
  intros ??? HΔ'. rewrite into_laterN_env_sound /=.
Dan Frumin's avatar
Dan Frumin committed
39
  rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
40
  by rewrite -ectx_lifting.wp_ectx_bind_inv.
41
Qed.
42

43
Tactic Notation "wp_pure" open_constr(efoc) :=
44
45
46
  iStartProof;
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
47
    unify e' efoc;
48
    eapply (tac_wp_pure K);
49
    [unlock; simpl; apply _   (* PureExec *)
50
    |wp_pure_done             (* The pure condition for PureExec *)
51
    |apply _                  (* IntoLaters *)
52
    |simpl_subst; try wp_value_head (* new goal *)])
53
54
   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
  | _ => fail "wp_pure: not a 'wp'"
55
56
  end.

57
58
59
60
61
62
63
64
65
66
67
68
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 _ _ _).
69
Tactic Notation "wp_match" := wp_case; wp_let.
70
71
72
73
74
75
76
77
78
79
80
81

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
82
Section heap.
83
Context `{heapG Σ}.
84
85
86
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
87

88
Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
89
  to_val e = Some v 
90
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  ( l,  Δ'',
92
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
93
94
    (Δ''  WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) 
  Δ  WP fill K (Alloc e) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Proof.
96
  intros ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
97
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
100
101
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

102
Lemma tac_wp_load Δ Δ' E i K l q v Φ :
103
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  envs_lookup i Δ' = Some (false, l {q} v)%I 
105
106
  (Δ'  WP fill K (of_val v) @ E {{ Φ }}) 
  Δ  WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Proof.
108
  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
109
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

113
Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  to_val e = Some v' 
115
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
118
119
  (Δ''  WP fill K (Lit LitUnit) @ E {{ Φ }}) 
  Δ  WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Proof.
121
  intros. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
122
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
125
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

126
Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  to_val e1 = Some v1  to_val e2 = Some v2 
128
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
130
131
  (Δ'  WP fill K (Lit (LitBool false)) @ E {{ Φ }}) 
  Δ  WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof.
133
  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
134
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

138
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
139
  to_val e1 = Some v1  to_val e2 = Some v2 
140
  IntoLaterNEnvs 1 Δ Δ' 
141
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
143
144
  (Δ''  WP fill K (Lit (LitBool true)) @ E {{ Φ }}) 
  Δ  WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
  intros; subst. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
147
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
151
152
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
153
154
155
156
157
158
159
160
161
162
  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
163
164

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
165
  iStartProof;
166
  lazymatch goal with
167
168
  | |- _  wp ?E ?e ?Q =>
    first
169
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ H K))
170
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
171
172
173
174
175
176
177
    [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"
        |simpl; try wp_value_head]]
178
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  end.
180

181
182
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
184

Tactic Notation "wp_load" :=
185
  iStartProof;
186
  lazymatch goal with
187
188
  | |- _  wp ?E ?e ?Q =>
    first
189
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
190
      |fail 1 "wp_load: cannot find 'Load' in" e];
191
192
193
194
    [apply _
    |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
     iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
    |simpl; try wp_value_head]
195
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
  end.

Tactic Notation "wp_store" :=
199
  iStartProof;
200
  lazymatch goal with
201
202
  | |- _  wp ?E ?e ?Q =>
    first
203
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ K))
204
      |fail 1 "wp_store: cannot find 'Store' in" e];
205
206
207
208
209
210
211
    [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
    |simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
212
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
  end.

Tactic Notation "wp_cas_fail" :=
216
  iStartProof;
217
  lazymatch goal with
218
219
  | |- _  wp ?E ?e ?Q =>
    first
220
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ K))
221
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
222
223
224
225
226
227
228
229
230
    [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
    |simpl; try wp_value_head]
231
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
234
  end.

Tactic Notation "wp_cas_suc" :=
235
  iStartProof;
236
  lazymatch goal with
237
238
  | |- _  wp ?E ?e ?Q =>
    first
239
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ K))
240
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
241
242
243
244
245
246
247
248
249
250
    [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
    |simpl; try wp_value_head]
251
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
252
  end.