proofmode.v 6.45 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.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.heap_lang Require Export wp_tactics lifting.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
Import uPred.

7
Ltac wp_strip_later ::= iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9

Section heap.
10
Context `{heapG Σ}.
11
12
13
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
14

15
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
16
  to_val e = Some v 
17
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
18
  ( l,  Δ'',
19
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
20
    (Δ''  Φ (LitV (LitLoc l)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
23
24
  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
25
26
27
28
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

29
Lemma tac_wp_load Δ Δ' E i l q v Φ :
30
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  envs_lookup i Δ' = Some (false, l {q} v)%I 
32
  (Δ'  Φ v) 
33
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Proof.
35
  intros. eapply wand_apply; first exact: wp_load.
36
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
39
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

40
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  to_val e = Some v' 
42
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
45
  (Δ''  Φ (LitV LitUnit)) 
46
  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Proof.
48
  intros. eapply wand_apply; first by eapply wp_store.
49
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
52
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

53
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  to_val e1 = Some v1  to_val e2 = Some v2 
55
  IntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
57
  (Δ'  Φ (LitV (LitBool false))) 
58
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof.
60
  intros. eapply wand_apply; first exact: wp_cas_fail.
61
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

65
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  to_val e1 = Some v1  to_val e2 = Some v2 
67
  IntoLaterNEnvs 1 Δ Δ' 
68
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
70
  (Δ''  Φ (LitV (LitBool true))) 
71
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  intros; subst. eapply wand_apply; first exact: wp_cas_suc.
74
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
78
79
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
80
  iStartProof;
81
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
83
    wp_bind_core K; iApply lem; try iNext)
84
  | _ => fail "wp_apply: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
87
  end.

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
88
  iStartProof;
89
  lazymatch goal with
90
91
92
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
93
         match eval hnf in e' with Alloc _ => wp_bind_core K end)
94
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
95
    eapply tac_wp_alloc with _ H _;
96
97
98
99
100
101
102
      [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]]
103
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  end.
105

106
107
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109

Tactic Notation "wp_load" :=
110
  iStartProof;
111
  lazymatch goal with
112
113
114
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
115
         match eval hnf in e' with Load _ => wp_bind_core K end)
116
117
      |fail 1 "wp_load: cannot find 'Load' in" e];
    eapply tac_wp_load;
118
      [apply _
119
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
120
       iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
121
      |wp_finish]
122
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
125
  end.

Tactic Notation "wp_store" :=
126
  iStartProof;
127
  lazymatch goal with
128
129
130
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
131
         match eval hnf in e' with Store _ _ => wp_bind_core K end)
132
133
134
135
136
137
138
139
      |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
140
      |wp_finish]
141
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
  end.

Tactic Notation "wp_cas_fail" :=
145
  iStartProof;
146
  lazymatch goal with
147
148
149
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
150
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
151
152
153
154
155
156
157
158
159
160
161
      |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]
162
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
  end.

Tactic Notation "wp_cas_suc" :=
166
  iStartProof;
167
  lazymatch goal with
168
169
170
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
171
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
172
173
174
175
176
177
178
179
180
181
182
183
      |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]
184
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
185
  end.