proofmode.v 6.14 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap.
Import uPred.

Ltac strip_later ::= iNext.

Section heap.
Context {Σ : gFunctors} `{heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val  iPropG heap_lang Σ.
Implicit Types Δ : envs (iResR heap_lang (globalF Σ)).

Global Instance sep_destruct_mapsto l q v :
  SepDestruct false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.

Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
  to_val e = Some v  
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  ( l,  Δ'',
24
25
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
    Δ''  Φ (LitV (LitLoc l))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
33
34
35
36
37
38
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
  intros ???? HΔ; eapply wp_alloc; eauto.
  rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

Lemma tac_wp_load Δ Δ' N E i l q v Φ :
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l {q} v)%I 
  Δ'  Φ v 
39
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
44
45
46
47
48
49
50
51
Proof.
  intros. eapply wp_load; eauto.
  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
  to_val e = Some v' 
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
52
  Δ''  Φ (LitV LitUnit)  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
56
57
58
59
60
61
62
63
64
Proof.
  intros. eapply wp_store; eauto.
  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
  Δ'  Φ (LitV (LitBool false)) 
65
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
68
69
70
71
72
73
74
75
76
77
Proof.
  intros. eapply wp_cas_fail; eauto.
  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v1)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
78
  Δ''  Φ (LitV (LitBool true))  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Proof.
  intros. eapply wp_cas_suc; eauto.
  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind K; iApply lem; try iNext)
  end.

Tactic Notation "wp_apply" open_constr(lem) constr(Hs) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind K; iApply lem Hs; try iNext)
  end.

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Alloc ?e =>
       wp_bind K; eapply tac_wp_alloc with _ _ H _;
         [wp_done || fail 2 "wp_alloc:" e "not a value"
         |iAssumption || fail 2 "wp_alloc: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |intros l; eexists; split;
           [env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
           |wp_finish]]
    end)
  end.
Tactic Notation "wp_alloc" ident(l) := let H := iFresh in wp_alloc l as H.

Tactic Notation "wp_load" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
119
    | Load (Lit (LitLoc ?l)) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
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
       wp_bind K; eapply tac_wp_load;
         [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
         |wp_finish]
    end)
  end.

Tactic Notation "wp_store" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Store ?l ?e =>
       wp_bind K; eapply tac_wp_store;
         [wp_done || fail 2 "wp_store:" e "not a value"
         |iAssumption || fail 2 "wp_store: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_store: cannot find" l "↦ ?"
         |env_cbv; reflexivity
         |wp_finish]
    end)
  end.

Tactic Notation "wp_cas_fail" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
149
    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
       wp_bind K; eapply tac_wp_cas_fail;
         [wp_done || fail 2 "wp_cas_fail:" e1 "not a value"
         |wp_done || fail 2 "wp_cas_fail:" e2 "not a value"
         |iAssumption || fail 2 "wp_cas_fail: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
         |try discriminate
         |wp_finish]
    end)
  end.

Tactic Notation "wp_cas_suc" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
166
    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
169
170
171
172
173
174
175
176
177
       wp_bind K; eapply tac_wp_cas_suc;
         [wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
         |wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
         |iAssumption || fail 2 "wp_cas_suc: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
         |env_cbv; reflexivity
         |wp_finish]
    end)
  end.