proofmode.v 6.6 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
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
28
29
  intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
  apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
32
33
34
35
36
37
38
39
  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 
40
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Proof.
Ralf Jung's avatar
Ralf Jung committed
42
  intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
48
49
50
51
52
  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 Δ'' 
53
  Δ''  Φ (LitV LitUnit)  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Proof.
55
  intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
58
59
60
61
62
63
64
65
  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)) 
66
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Proof.
68
  intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
72
73
74
75
76
77
78
  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 Δ'' 
79
  Δ''  Φ (LitV (LitBool true))  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Proof.
81
  intros. rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
84
85
86
87
88
89
90
  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)
91
  | _ => fail "wp_apply: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
  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]]
107
108
    end) || fail "wp_alloc: cannot find 'Alloc' in" e
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  end.
110
111
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
114
115
116

Tactic Notation "wp_load" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
117
    | Load (Lit (LitLoc ?l)) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
120
121
122
123
       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]
124
125
    end) || fail "wp_load: cannot find 'Load' in" e
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
  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]
141
142
    end) || fail "wp_store: cannot find 'Store' in" e
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
146
147
148
  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 ?l ?e1 ?e2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
155
156
157
158
       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]
159
160
    end) || fail "wp_cas_fail: cannot find 'CAS' in" e
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
164
165
166
  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
167
    | CAS ?l ?e1 ?e2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
171
172
173
174
175
176
       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]
177
178
    end) || fail "wp_cas_suc: cannot find 'CAS' in" e
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  end.