proofmode.v 8.71 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_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
9 10
  PureExec φ e1 e2 
  φ 
11
  IntoLaterNEnvs 1 Δ Δ' 
12 13
  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) 
  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
14
Proof.
15
  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
Dan Frumin's avatar
Dan Frumin committed
16
  rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
17
  by rewrite -ectx_lifting.wp_ectx_bind_inv.
18
Qed.
19

20
Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
21
  IntoVal e v 
22
  envs_entails Δ (Φ v)  envs_entails Δ (WP e @ E {{ Φ }}).
23 24 25
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
26

27
Tactic Notation "wp_pure" open_constr(efoc) :=
28 29
  iStartProof;
  lazymatch goal with
30
  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
31
    unify e' efoc;
32
    eapply (tac_wp_pure K);
33 34 35
    [simpl; apply _                 (* PureExec *)
    |try fast_done                  (* The pure condition for PureExec *)
    |apply _                        (* IntoLaters *)
36
    |simpl_subst; try wp_value_head (* new goal *)])
37 38
   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
  | _ => fail "wp_pure: not a 'wp'"
39 40
  end.

41 42 43 44 45 46 47 48 49 50 51 52
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 _ _ _).
53
Tactic Notation "wp_match" := wp_case; wp_let.
54

55 56 57
Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I 
  envs_entails Δ (WP fill K e @ E {{ Φ }}).
58 59
Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
63
  | _ => apply (tac_wp_bind K); simpl
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65
  end.

66 67 68
Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
69
  | |- envs_entails _ (wp ?E ?e ?Q) =>
70 71
    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
72 73 74 75
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Section heap.
77
Context `{heapG Σ}.
78 79 80
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
81

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

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

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

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

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

Tactic Notation "wp_apply" open_constr(lem) :=
152 153
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
154
    | |- envs_entails _ (wp ?E ?e ?Q) =>
155 156 157 158 159 160 161
      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
162 163

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

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

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

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

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

Tactic Notation "wp_cas_suc" :=
229
  iStartProof;
230
  lazymatch goal with
231
  | |- envs_entails _ (wp ?E ?e ?Q) =>
232
    first
233
      [reshape_expr e ltac:(fun K e' =>
234
         eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
235
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
236
    [apply _
237 238 239 240 241
    |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]
242
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
243
  end.