ModelSep.v 23.4 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
(** 

This file formalizes "Separation Logic", as described in 
Arthur Charguéraud's lecture notes.

We formalize heap predicates, properties of heap entailment,
define the interpretation of triples, and derive the reasoning
rules in the form of lemmas.

Two interpretation of triples are considered: a basic version,
and a refined version that allows for discarding arbitrary
heap predicates. The former version is useful to ensure full recollection
of all allocated data in languages with explicit deallocation,
white the latter version is required for the analysis of programs 
with implicit garbage collection.

Author: Arthur Charguéraud.
License: MIT.

*)

charguer's avatar
charguer committed
22
Set Implicit Arguments.
charguer's avatar
charguer committed
23
Require Import LibCore Shared ModelLambda.
charguer's avatar
charguer committed
24
Open Scope state_scope.
charguer's avatar
charguer committed
25

charguer's avatar
charguer committed
26 27
Ltac auto_star ::= jauto.

charguer's avatar
charguer committed
28 29 30 31 32

(********************************************************************)
(* ** Heaps *)

(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
33
(* ** Definition of heaps *)
charguer's avatar
charguer committed
34

charguer's avatar
charguer committed
35
(** Data type for heaps *)
charguer's avatar
charguer committed
36

charguer's avatar
charguer committed
37
Definition heap : Type := (state)%type.
charguer's avatar
charguer committed
38

charguer's avatar
charguer committed
39 40 41 42 43 44 45 46 47 48 49
(** Notation for empty and union *)

Notation "'heap_empty'" := state_empty : heap_scope.

Notation "h1 \u h2" := (state_union h1 h2)
   (at level 51, right associativity) : heap_scope.


(*------------------------------------------------------------------*)
(* ** Definition of heap predicates *)

charguer's avatar
charguer committed
50 51 52 53
(** [hprop] is the type of predicates on heaps *)

Definition hprop := heap -> Prop.

charguer's avatar
charguer committed
54 55 56
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.

charguer's avatar
charguer committed
57 58
(** Empty heap *)

charguer's avatar
charguer committed
59
Definition hprop_empty : hprop := 
charguer's avatar
charguer committed
60
  fun h => h = state_empty.
charguer's avatar
charguer committed
61

charguer's avatar
charguer committed
62 63
(** Lifting of predicates *)

charguer's avatar
charguer committed
64
Definition hprop_pure (H:Prop) : hprop :=
charguer's avatar
charguer committed
65
  fun h => h = state_empty /\ H.
charguer's avatar
charguer committed
66

charguer's avatar
charguer committed
67 68
(** Singleton heap *)

charguer's avatar
charguer committed
69
Definition hprop_single (l:loc) (v:val) : hprop := 
charguer's avatar
charguer committed
70 71 72 73
  fun h => h = state_single l v.

(** Heap union *)

charguer's avatar
charguer committed
74
Definition hprop_star (H1 H2 : hprop) : hprop := 
charguer's avatar
charguer committed
75 76
  fun h => exists h1 h2, H1 h1 
                      /\ H2 h2 
charguer's avatar
charguer committed
77 78
                      /\ (\# h1 h2)
                      /\ h = h1 \+ h2.
charguer's avatar
charguer committed
79 80 81

(** Lifting of existentials *)

charguer's avatar
charguer committed
82
Definition hprop_exists A (Hof : A -> hprop) : hprop := 
charguer's avatar
charguer committed
83 84 85 86
  fun h => exists x, Hof x h.

(** Garbage collection predicate: [Hexists H, H]. *)

charguer's avatar
charguer committed
87 88 89
Definition hprop_gc : hprop := 
  hprop_exists (fun H => H).

charguer's avatar
charguer committed
90
Global Opaque hprop_empty hprop_pure hprop_single 
charguer's avatar
charguer committed
91
              hprop_star hprop_exists hprop_gc. 
charguer's avatar
charguer committed
92 93 94 95 96


(*------------------------------------------------------------------*)
(* ** Notation for heap predicates *)

charguer's avatar
charguer committed
97
Notation "\[]" := (hprop_empty) 
charguer's avatar
charguer committed
98 99
  (at level 0) : heap_scope.

charguer's avatar
charguer committed
100
Notation "\[ L ]" := (hprop_pure L) 
charguer's avatar
charguer committed
101 102
  (at level 0, L at level 99) : heap_scope.

charguer's avatar
charguer committed
103 104 105 106
Notation "r '~~>' v" := (hprop_single r v)
  (at level 32, no associativity) : heap_scope.

Notation "H1 '\*' H2" := (hprop_star H1 H2)
charguer's avatar
charguer committed
107 108
  (at level 41, right associativity) : heap_scope.

charguer's avatar
charguer committed
109
Notation "Q \*+ H" := (fun x => hprop_star (Q x) H)
charguer's avatar
charguer committed
110
  (at level 40) : heap_scope.
charguer's avatar
charguer committed
111

charguer's avatar
charguer committed
112
Notation "'Hexists' x1 , H" := (hprop_exists (fun x1 => H))
charguer's avatar
charguer committed
113
  (at level 39, x1 ident, H at level 50) : heap_scope.
charguer's avatar
charguer committed
114
Notation "'Hexists' x1 : T1 , H" := (hprop_exists (fun x1:T1 => H))
charguer's avatar
charguer committed
115
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
charguer's avatar
charguer committed
116
Notation "'Hexists' ( x1 : T1 ) , H" := (hprop_exists (fun x1:T1 => H))
charguer's avatar
charguer committed
117 118
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.

charguer's avatar
charguer committed
119
Notation "\GC" := (hprop_gc) : heap_scope. 
charguer's avatar
charguer committed
120

charguer's avatar
charguer committed
121 122 123 124
Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.

charguer's avatar
charguer committed
125 126

(********************************************************************)
charguer's avatar
charguer committed
127
(* ** Properties *)
charguer's avatar
charguer committed
128

charguer's avatar
charguer committed
129
(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
130 131 132 133 134 135 136 137 138 139 140 141
(* ** Tactic for automation *)

Hint Extern 1 (_ = _ :> heap) => state_eq.

Tactic Notation "state_disjoint_pre" :=
  subst; rew_disjoint; jauto_set.

Hint Extern 1 (\# _ _) => state_disjoint_pre.


(*------------------------------------------------------------------*)
(* ** Properties of [hprop] *)
charguer's avatar
charguer committed
142

charguer's avatar
charguer committed
143 144
Global Instance hprop_inhab : Inhab hprop.
Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
charguer's avatar
charguer committed
145

charguer's avatar
charguer committed
146
Section HeapProp.
charguer's avatar
charguer committed
147
Transparent hprop_empty hprop_pure hprop_single hprop_star hprop_gc.
charguer's avatar
charguer committed
148

charguer's avatar
charguer committed
149
Lemma hprop_empty_prove : 
charguer's avatar
charguer committed
150
  \[] state_empty.
charguer's avatar
charguer committed
151 152
Proof using. hnfs~. Qed.

charguer's avatar
charguer committed
153
Lemma hprop_empty_inv : forall h,
charguer's avatar
charguer committed
154
  \[] h -> h = state_empty.
charguer's avatar
charguer committed
155
Proof using. auto. Qed.
charguer's avatar
charguer committed
156

charguer's avatar
charguer committed
157
Lemma hprop_pure_prove : forall (P:Prop),
charguer's avatar
charguer committed
158
  P -> 
charguer's avatar
charguer committed
159
  \[P] state_empty.
charguer's avatar
charguer committed
160
Proof using. intros. hnfs~. Qed.
charguer's avatar
charguer committed
161

charguer's avatar
charguer committed
162
Lemma hprop_pure_inv : forall h (P:Prop),
charguer's avatar
charguer committed
163
  \[P] h -> 
charguer's avatar
charguer committed
164
  h = state_empty /\ P.
charguer's avatar
charguer committed
165
Proof using. intros. auto. Qed.
charguer's avatar
charguer committed
166

charguer's avatar
charguer committed
167 168 169 170 171 172 173 174 175 176 177 178
Lemma hprop_gc_prove : forall h, 
  \GC h.
Proof using. intros. exists~ (=h). Qed.

Lemma hprop_gc_merge : 
  \GC \* \GC = \GC.
Proof using.
  unfold hprop. extens. intros h. iff (h1&h2&M1&M2&D&U) M.
  { apply hprop_gc_prove. }
  { exists h heap_empty. splits~. apply hprop_gc_prove. }
Qed.

charguer's avatar
charguer committed
179 180
Lemma hprop_star_comm : forall H1 H2,
   H1 \* H2 = H2 \* H1.
charguer's avatar
charguer committed
181
Proof using. 
charguer's avatar
charguer committed
182
  intros H1 H2. unfold hprop, hprop_star. extens. intros h.
charguer's avatar
charguer committed
183 184
  iff (h1&h2&M1&M2&D&U); 
    rewrite~ state_union_comm_disjoint in U; exists* h2 h1. 
charguer's avatar
charguer committed
185 186
Qed.

charguer's avatar
charguer committed
187 188
Lemma hprop_star_empty_l : forall H,
   \[] \* H = H.
charguer's avatar
charguer committed
189
Proof using.
charguer's avatar
charguer committed
190
  intro. unfold hprop, hprop_star. extens. intros h.
charguer's avatar
charguer committed
191
  iff (h1&h2&M1&M2&D&U) M. 
charguer's avatar
charguer committed
192
  hnf in M1. subst h1 h. rewrite~ state_union_empty_l.
charguer's avatar
charguer committed
193
  exists state_empty h. hint hprop_empty_prove. auto.
charguer's avatar
charguer committed
194 195
Qed.

charguer's avatar
charguer committed
196 197
Lemma hprop_star_empty_r : forall H, 
  H \* \[] = H.
charguer's avatar
charguer committed
198 199
Proof using.
  apply neutral_r_from_comm_neutral_l.
charguer's avatar
charguer committed
200
  applys hprop_star_comm. applys hprop_star_empty_l.
charguer's avatar
charguer committed
201 202
Qed.

charguer's avatar
charguer committed
203
Lemma hprop_star_assoc : forall H1 H2 H3,
charguer's avatar
charguer committed
204
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
charguer's avatar
charguer committed
205
Proof using. 
charguer's avatar
charguer committed
206 207
  intros H1 H2 H3. unfold hprop, hprop_star. extens. intros h. split.
  { intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
charguer's avatar
charguer committed
208 209
    exists h1 (h2 \+ h3). splits~.
    { exists h2 h3. splits*. } }
charguer's avatar
charguer committed
210
  { intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
charguer's avatar
charguer committed
211 212 213
    exists (h1 \+ h2) h3. splits~.
    { exists h1 h2. splits*. } }
Qed. 
charguer's avatar
charguer committed
214

charguer's avatar
charguer committed
215 216
Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
  (hprop_single l v1) \* (hprop_single l v2) ==> \[False].
charguer's avatar
charguer committed
217
Proof using.
charguer's avatar
charguer committed
218 219
  intros. unfold hprop_single. intros h (h1&h2&E1&E2&D&E). false.
  subst. applys* state_single_same_loc_disjoint.
charguer's avatar
charguer committed
220 221
Qed.

charguer's avatar
charguer committed
222
Lemma hprop_star_prop_elim : forall (P:Prop) H h,
charguer's avatar
charguer committed
223 224
  (\[P] \* H) h -> P /\ H h.
Proof using.
charguer's avatar
charguer committed
225
  introv (?&?&N&?&?&?). destruct N. subst. rewrite~ state_union_empty_l.
charguer's avatar
charguer committed
226 227
Qed.

charguer's avatar
charguer committed
228 229 230
(*------------------------------------------------------------------*)
(* ** Properties of [himpl] *)

charguer's avatar
charguer committed
231 232 233 234 235 236 237 238 239 240
(** 

Note that [P ==> Q] is a notation from [pred_le P Q], defined as
[forall x, P x -> Q x].

Note that [P ===> Q] is a notation from [rel_le P Q], defined as
[forall x y, P x y -> Q x y].

*)

charguer's avatar
charguer committed
241 242 243 244
Lemma himpl_forward : forall H1 H2 h,
  (H1 ==> H2) -> (H1 h) -> (H2 h).
Proof using. auto. Qed.

charguer's avatar
charguer committed
245 246 247 248 249 250 251 252 253 254 255 256
Lemma himpl_refl : forall H,
  H ==> H.
Proof using. intros h. auto. Qed.

Lemma himpl_trans : forall H1 H2 H3,
  (H1 ==> H2) -> (H2 ==> H3) -> (H1 ==> H3).
Proof using. introv M1 M2. intros h H1h. eauto. Qed.

Lemma himpl_antisym : forall H1 H2,
  (H1 ==> H2) -> (H2 ==> H1) -> (H1 = H2).
Proof using. introv M1 M2. applys prop_ext_1. intros h. iff*. Qed.

charguer's avatar
charguer committed
257 258 259 260 261
Lemma himpl_cancel_l : forall H1 H1' H2,
  H1 ==> H1' -> (H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

Lemma himpl_cancel_r : forall H1 H2 H2',
charguer's avatar
charguer committed
262 263 264 265
  H2 ==> H2' -> (H1 \* H2) ==> (H1 \* H2').
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

Lemma himpl_extract_prop : forall (P:Prop) H H',
charguer's avatar
charguer committed
266
  (P -> H ==> H') -> (\[P] \* H) ==> H'.
charguer's avatar
charguer committed
267
Proof using. introv W Hh. lets (?&?): hprop_star_prop_elim Hh. applys* W. Qed.
charguer's avatar
charguer committed
268

charguer's avatar
charguer committed
269 270 271 272 273 274 275
Lemma himpl_extract_exists : forall A H (J:A->hprop),
  (forall x, J x ==> H) -> (hprop_exists J) ==> H.
Proof using. introv W. intros h (x&Hh). applys* W. Qed.

Lemma himpl_inst_prop : forall (P:Prop) H H',
  P -> H ==> H' -> H ==> (\[P] \* H').
Proof using.
charguer's avatar
charguer committed
276
  introv HP W. intros h Hh. exists state_empty h.
charguer's avatar
charguer committed
277
  splits*. applys* hprop_pure_prove.
charguer's avatar
charguer committed
278 279 280
Qed.

Lemma himpl_inst_exists : forall A (x:A) H J,
charguer's avatar
charguer committed
281
  (H ==> J x) -> H ==> (hprop_exists J).
charguer's avatar
charguer committed
282 283
Proof using. introv W h. exists x. apply~ W. Qed.

charguer's avatar
charguer committed
284
Lemma himpl_remove_gc : forall H H',
charguer's avatar
charguer committed
285 286 287
  H ==> H' ->
  H ==> H' \* \GC.
Proof using.
charguer's avatar
charguer committed
288
  introv M. intros h Hh. exists h state_empty. splits*.
charguer's avatar
charguer committed
289
  exists \[]. applys hprop_empty_prove.
charguer's avatar
charguer committed
290 291
Qed.

charguer's avatar
charguer committed
292
End HeapProp.
charguer's avatar
charguer committed
293

charguer's avatar
charguer committed
294
Hint Resolve hprop_empty_prove hprop_pure_prove hprop_gc_prove.
charguer's avatar
charguer committed
295 296


charguer's avatar
charguer committed
297

charguer's avatar
charguer committed
298 299

(********************************************************************)
charguer's avatar
charguer committed
300
(********************************************************************)
charguer's avatar
charguer committed
301 302 303 304
(********************************************************************)
(** * Rules without GC *)

Module TripleWithoutGC.
charguer's avatar
charguer committed
305

charguer's avatar
charguer committed
306

charguer's avatar
charguer committed
307 308
(*------------------------------------------------------------------*)
(** Definition of triples *)
charguer's avatar
charguer committed
309

charguer's avatar
charguer committed
310
Definition triple t H Q :=
charguer's avatar
charguer committed
311 312 313 314 315 316 317 318
  forall h1 h2, 
  \# h1 h2 -> 
  H h1 -> 
  exists h1' v, 
       \# h1' h2 
    /\ red (h1 \u h2) t (h1' \u h2) v
    /\ Q v h1'.

charguer's avatar
charguer committed
319

charguer's avatar
charguer committed
320
(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
321
(** Structural rules *)
charguer's avatar
charguer committed
322

charguer's avatar
charguer committed
323 324
Definition heap_union_empty_r := state_union_empty_r.

charguer's avatar
charguer committed
325 326
Lemma rule_extract_prop : forall t (P:Prop) H Q,
  (P -> triple t H Q) ->
charguer's avatar
charguer committed
327
  triple t (H \* \[P]) Q.
charguer's avatar
charguer committed
328
Proof using. 
charguer's avatar
charguer committed
329 330
  introv M. intros h1 h2 D (h21&h22&N1&(HE&HP)&N3&N4).
  subst h22 h1. rewrite heap_union_empty_r. applys* M. 
charguer's avatar
charguer committed
331 332
Qed.

charguer's avatar
charguer committed
333
Lemma rule_extract_exists : forall t A (J:A->hprop) Q,
charguer's avatar
charguer committed
334
  (forall x, triple t (J x) Q) ->
charguer's avatar
charguer committed
335
  triple t (hprop_exists J) Q.
charguer's avatar
charguer committed
336
Proof using. introv M D (x&Jx). applys* M. Qed.
charguer's avatar
charguer committed
337

charguer's avatar
charguer committed
338 339
Lemma rule_consequence : forall t H' Q' H Q,
  H ==> H' ->
charguer's avatar
charguer committed
340
  triple t H' Q' ->
charguer's avatar
charguer committed
341
  Q' ===> Q ->
charguer's avatar
charguer committed
342 343
  triple t H Q.
Proof using. 
charguer's avatar
charguer committed
344 345 346 347
  introv MH M MQ. intros h1 h2 D P1. 
  lets P1': (rm MH) (rm P1). 
  forwards~ (h1'&v&(N1&N2&N3)): (rm M) h2 (rm P1'). 
  exists h1' v. splits~. applys~ MQ.
charguer's avatar
charguer committed
348 349
Qed.

charguer's avatar
charguer committed
350
Lemma rule_frame : forall t H Q H',
charguer's avatar
charguer committed
351 352 353
  triple t H Q ->
  triple t (H \* H') (Q \*+ H').
Proof using. 
charguer's avatar
charguer committed
354 355 356 357 358
  introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D12a&E12).
  lets~ (h1'a&v&Da&Ra&Qa): M h1a (h1b \u h2).
  subst h1. exists (h1'a \u h1b) v. splits~.
  { state_red. }
  { exists~ h1'a h1b. }
charguer's avatar
charguer committed
359 360
Qed.

charguer's avatar
charguer committed
361 362

(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
363
(** Term rules *)
charguer's avatar
charguer committed
364

charguer's avatar
charguer committed
365 366 367 368
Lemma rule_val : forall v H Q,
  H ==> Q v ->
  triple (trm_val v) H Q.
Proof using.
charguer's avatar
charguer committed
369 370
  introv M D H1. exists h1 v. splits~.
  { applys red_val. }
charguer's avatar
charguer committed
371
Qed.
charguer's avatar
charguer committed
372

charguer's avatar
charguer committed
373
Lemma rule_if : forall v t1 t2 H Q,
charguer's avatar
charguer committed
374 375 376
  triple (If v = val_int 0 then t2 else t1) H Q ->
  triple (trm_if v t1 t2) H Q.
Proof using.
charguer's avatar
charguer committed
377 378
  introv M D H1. forwards (h1'&v'&Da&Ra&Qa): M D H1.
  exists h1' v'. splits~.
charguer's avatar
charguer committed
379 380
  { applys~ red_if. }
Qed.
charguer's avatar
charguer committed
381

charguer's avatar
charguer committed
382
Lemma rule_let : forall x t1 t2 H Q Q1,
charguer's avatar
charguer committed
383 384 385 386 387
  triple t1 H Q1 ->
  (forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
  triple (trm_let x t1 t2) H Q.
Proof using.
  introv M1 M2. intros h1 h2 D1 H1.
charguer's avatar
charguer committed
388 389 390 391
  lets (h1'&v1&Da&Ra&Qa): M1 D1 H1.
  forwards~ (h1''&v2&Db&Rb&Qb): M2 v1 h1' h2.
  exists h1'' v2. splits~.
  { applys red_let Ra. state_red. }
charguer's avatar
charguer committed
392
Qed.
charguer's avatar
charguer committed
393

charguer's avatar
charguer committed
394 395 396 397
Lemma rule_let_val : forall x v1 t2 H Q,
  (forall (X:val), X = v1 -> triple (subst_trm x X t2) H Q) ->
  triple (trm_let x (trm_val v1) t2) H Q.
Proof using. 
charguer's avatar
charguer committed
398 399 400
  introv M. forwards~ M': M.
  applys_eq~ (>> rule_let H (fun x => H \* \[x = v1])) 2.
  { applys rule_val. rewrite hprop_star_comm. applys~ himpl_inst_prop. }
charguer's avatar
charguer committed
401
  { intros X. applys rule_extract_prop. applys M. }
charguer's avatar
charguer committed
402
Qed.
charguer's avatar
charguer committed
403

charguer's avatar
charguer committed
404
Lemma rule_app : forall f x F V t1 H Q,
charguer's avatar
charguer committed
405 406 407 408 409
  F = (val_fix f x t1) ->
  triple (subst_trm f F (subst_trm x V t1)) H Q ->
  triple (trm_app F V) H Q.
Proof using.
  introv EF M. subst F. intros h1 h2 D1 H1.
charguer's avatar
charguer committed
410 411
  lets (h1'a&ra&Da&Ra&Qa): M D1 H1.
  exists h1'a ra. splits~. 
charguer's avatar
charguer committed
412 413 414
  { applys~ red_app. }
Qed.

charguer's avatar
charguer committed
415
Lemma rule_let_fix : forall f x t1 t2 H Q,
charguer's avatar
charguer committed
416
  (forall (F:val), 
charguer's avatar
charguer committed
417 418
    (forall X H' Q', 
      triple (subst_trm f F (subst_trm x X t1)) H' Q' ->
charguer's avatar
charguer committed
419
      triple (trm_app F X) H' Q') ->
charguer's avatar
charguer committed
420
    triple (subst_trm f F t2) H Q) ->
charguer's avatar
charguer committed
421
  triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
charguer's avatar
charguer committed
422
Proof using.
charguer's avatar
charguer committed
423
  introv M. applys rule_let_val. intros F EF. 
charguer's avatar
charguer committed
424
  applys (rm M). clears H Q. intros X H Q. applys~ rule_app.
charguer's avatar
charguer committed
425
Qed.
charguer's avatar
charguer committed
426

charguer's avatar
charguer committed
427
Lemma rule_new : forall v,
charguer's avatar
charguer committed
428
  triple (prim_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
charguer's avatar
charguer committed
429
Proof using.
charguer's avatar
charguer committed
430 431 432 433 434 435 436
  intros. intros h1 h2 _ P1.
  lets E: hprop_empty_inv P1. subst h1.
  lets (l&Dl): (state_disjoint_new h2 v).
  sets h1': (state_single l v).
  exists h1' (val_loc l). splits~.
  { rew_state. applys~ red_new. }
  { exists l. applys~ himpl_inst_prop (l ~~> v). split~. }
charguer's avatar
charguer committed
437
Qed.
charguer's avatar
charguer committed
438

charguer's avatar
charguer committed
439
Lemma rule_get : forall v l,
charguer's avatar
charguer committed
440
  triple (prim_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
charguer's avatar
charguer committed
441
Proof using.
charguer's avatar
charguer committed
442 443 444
  intros. intros h1 h2 D P1. exists h1 v. splits~.
  { rew_state. applys red_get. applys~ state_union_single_read. }
  { exists~ heap_empty h1. }
charguer's avatar
charguer committed
445
Qed.
charguer's avatar
charguer committed
446

charguer's avatar
charguer committed
447
Lemma rule_set : forall l v w,
charguer's avatar
charguer committed
448
  triple (prim_set (val_pair (val_loc l) w)) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
charguer's avatar
charguer committed
449
Proof using.
charguer's avatar
charguer committed
450 451 452 453 454 455
  intros. intros h1 h2 D P1.
  sets h1': (state_single l w).
  exists h1' val_unit. splits~.
  { applys state_disjoint_single_set v. rewrite~ <- P1. }
  { rew_state. applys~ red_set. applys~ state_union_single_write v w. }
  { applys~ himpl_inst_prop (l ~~> w). split~. }
charguer's avatar
charguer committed
456
Qed.
charguer's avatar
charguer committed
457

charguer's avatar
charguer committed
458

charguer's avatar
charguer committed
459 460 461 462 463 464 465 466 467 468 469 470 471 472
End TripleWithoutGC.




(********************************************************************)
(********************************************************************)
(********************************************************************)
(** * Rules with GC *)

Module TripleWithGC.

(*------------------------------------------------------------------*)
(* ** Definition of [on_sub] *)
charguer's avatar
charguer committed
473

charguer's avatar
charguer committed
474
Definition on_sub H := (H \* \GC).
charguer's avatar
charguer committed
475

charguer's avatar
charguer committed
476 477 478 479
Lemma on_sub_base : forall H h,
  H h -> 
  on_sub H h.
Proof using. intros H h M. exists~ h heap_empty. Qed.
charguer's avatar
charguer committed
480

charguer's avatar
charguer committed
481 482 483 484 485 486 487
Lemma on_sub_gc : forall H h,
  on_sub (H \* \GC) h ->
  on_sub H h.
Proof using.
  introv M. unfolds on_sub. applys himpl_forward (rm M).
  rewrite hprop_star_assoc. rewrite~ hprop_gc_merge.
Qed.
charguer's avatar
charguer committed
488

charguer's avatar
charguer committed
489 490 491 492 493 494 495 496
Lemma on_sub_union_r : forall H h1 h2,
  on_sub H h1 ->
  \# h1 h2 ->
  on_sub H (h1 \u h2).
Proof using.
  introv M D. unfolds on_sub. rewrite <- hprop_gc_merge.
  rewrite <- hprop_star_assoc. exists~ h1 h2.
Qed.
charguer's avatar
charguer committed
497

charguer's avatar
charguer committed
498 499 500 501 502 503 504 505 506 507 508 509
Lemma on_sub_union : forall H1 H2 h1 h2,
  on_sub H1 h1 ->
  H2 h2 ->
  \# h1 h2 ->
  on_sub (H1 \* H2) (h1 \u h2).
Proof using.
  introv M P2 D. unfolds on_sub. 
  rewrite hprop_star_assoc.
  rewrite (@hprop_star_comm H2 \GC).
  rewrite <- hprop_star_assoc.
  exists~ h1 h2. 
Qed.
charguer's avatar
charguer committed
510

charguer's avatar
charguer committed
511 512 513 514 515 516 517 518
Lemma on_sub_weaken : forall Q Q' v h,
  on_sub (Q v) h ->
  Q ===> Q' ->
  on_sub (Q' v) h.
Proof using.
  introv M W. unfolds on_sub. applys himpl_forward (rm M).
  applys~ himpl_cancel_l. 
Qed.
charguer's avatar
charguer committed
519 520


charguer's avatar
charguer committed
521 522 523 524 525 526 527 528 529 530 531
(*------------------------------------------------------------------*)
(** Definition of triples *)

Definition triple t H Q :=
  forall h1 h2, 
  \# h1 h2 -> 
  H h1 -> 
  exists h1' v, 
       \# h1' h2 
    /\ red (h1 \u h2) t (h1' \u h2) v
    /\ on_sub (Q v) h1'.
charguer's avatar
charguer committed
532 533


charguer's avatar
charguer committed
534 535
(*------------------------------------------------------------------*)
(** Structural rules *)
charguer's avatar
charguer committed
536

charguer's avatar
charguer committed
537 538 539 540 541 542 543 544 545
Definition heap_union_empty_r := state_union_empty_r.

Lemma rule_extract_prop : forall t (P:Prop) H Q,
  (P -> triple t H Q) ->
  triple t (H \* \[P]) Q.
Proof using. 
  introv M. intros h1 h2 D (h21&h22&N1&(HE&HP)&N3&N4).
  subst h22 h1. rewrite heap_union_empty_r. applys* M. 
Qed.
charguer's avatar
charguer committed
546

charguer's avatar
charguer committed
547
Lemma rule_extract_exists : forall t (A:Type) (J:A->hprop) Q,
charguer's avatar
charguer committed
548 549 550
  (forall x, triple t (J x) Q) ->
  triple t (hprop_exists J) Q.
Proof using. introv M D (x&Jx). applys* M. Qed.
charguer's avatar
charguer committed
551

charguer's avatar
charguer committed
552 553 554 555 556 557 558 559 560 561 562
Lemma rule_consequence : forall t H' Q' H Q,
  H ==> H' ->
  triple t H' Q' ->
  Q' ===> Q ->
  triple t H Q.
Proof using. 
  introv MH M MQ. intros h1 h2 D P1. 
  lets P1': (rm MH) (rm P1). 
  forwards~ (h1'&v&(N1&N2&N3)): (rm M) h2 (rm P1'). 
  exists h1' v. splits~. { applys~ on_sub_weaken Q'. }
Qed.
charguer's avatar
charguer committed
563

charguer's avatar
charguer committed
564 565 566 567 568 569 570 571 572 573
Lemma rule_frame : forall t H Q H',
  triple t H Q ->
  triple t (H \* H') (Q \*+ H').
Proof using. 
  introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D12a&E12).
  lets~ (h1'a&v&Da&Ra&Qa): M h1a (h1b \u h2).
  subst h1. exists (h1'a \u h1b) v. splits~.
  { state_red. }
  { applys~ on_sub_union. }
Qed.
charguer's avatar
charguer committed
574

charguer's avatar
charguer committed
575 576 577 578 579 580 581 582
Lemma rule_gc_post : forall t H Q,
  triple t H (Q \*+ \GC) ->
  triple t H Q.
Proof using.
  introv M. intros h1 h2 D P1. 
  forwards* (h1'&v&(N1&N2&N3)): (rm M) h1 h2.
  exists h1' v. splits~. { applys~ on_sub_gc. }
Qed.
charguer's avatar
charguer committed
583

charguer's avatar
charguer committed
584 585 586 587 588 589
Lemma rule_gc_pre : forall t H Q,
  triple t H Q ->
  triple t (H \* \GC) Q.
Proof using.
  introv M. applys rule_gc_post. applys~ rule_frame.
Qed.
charguer's avatar
charguer committed
590 591


charguer's avatar
charguer committed
592 593
(*------------------------------------------------------------------*)
(** Term rules *)
charguer's avatar
charguer committed
594

charguer's avatar
charguer committed
595 596 597 598 599 600 601 602
Lemma rule_val : forall v H Q,
  H ==> Q v ->
  triple (trm_val v) H Q.
Proof using.
  introv M D H1. exists h1 v. splits~.
  { applys red_val. }
  { applys~ on_sub_base. }
Qed.
charguer's avatar
charguer committed
603

charguer's avatar
charguer committed
604 605 606 607 608 609 610 611
Lemma rule_if : forall v t1 t2 H Q,
  triple (If v = val_int 0 then t2 else t1) H Q ->
  triple (trm_if v t1 t2) H Q.
Proof using.
  introv M D H1. forwards (h1'&v'&Da&Ra&Qa): M D H1.
  exists h1' v'. splits~.
  { applys~ red_if. }
Qed.
charguer's avatar
charguer committed
612

charguer's avatar
charguer committed
613 614 615 616 617 618 619 620 621 622 623 624 625
Lemma rule_let : forall x t1 t2 H Q Q1,
  triple t1 H Q1 ->
  (forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
  triple (trm_let x t1 t2) H Q.
Proof using.
  introv M1 M2. intros h1 h2 D1 H1.
  lets (h1'&v1&Da&Ra&Qa): M1 D1 H1.
  lets (h1'a&h1'b&N1&N2&N3&N4): (rm Qa).
  forwards~ (h1''&v2&Db&Rb&Qb): M2 v1 h1'a (h1'b \u h2).
  exists (h1'' \u h1'b) v2. splits~.
  { applys red_let Ra. state_red. }
  { applys~ on_sub_union_r. }
Qed.
charguer's avatar
charguer committed
626

charguer's avatar
charguer committed
627 628 629 630 631 632 633 634 635
Lemma rule_let_val : forall x v1 t2 H Q,
  (forall (X:val), X = v1 -> triple (subst_trm x X t2) H Q) ->
  triple (trm_let x (trm_val v1) t2) H Q.
Proof using. 
  introv M. forwards~ M': M.
  applys_eq~ (>> rule_let H (fun x => H \* \[x = v1])) 2.
  { applys rule_val. rewrite hprop_star_comm. applys~ himpl_inst_prop. }
  { intros X. applys rule_extract_prop. applys M. }
Qed.
charguer's avatar
charguer committed
636

charguer's avatar
charguer committed
637 638 639 640 641 642 643 644 645 646
Lemma rule_app : forall f x F V t1 H Q,
  F = (val_fix f x t1) ->
  triple (subst_trm f F (subst_trm x V t1)) H Q ->
  triple (trm_app F V) H Q.
Proof using.
  introv EF M. subst F. intros h1 h2 D1 H1.
  lets (h1'a&ra&Da&Ra&Qa): M D1 H1.
  exists h1'a ra. splits~. 
  { applys~ red_app. }
Qed.
charguer's avatar
charguer committed
647

charguer's avatar
charguer committed
648 649 650 651 652 653 654 655 656 657 658
Lemma rule_let_fix : forall f x t1 t2 H Q,
  (forall (F:val), 
    (forall X H' Q', 
      triple (subst_trm f F (subst_trm x X t1)) H' Q' ->
      triple (trm_app F X) H' Q') ->
    triple (subst_trm f F t2) H Q) ->
  triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
Proof using.
  introv M. applys rule_let_val. intros F EF. 
  applys (rm M). clears H Q. intros X H Q. applys~ rule_app.
Qed.
charguer's avatar
charguer committed
659

charguer's avatar
charguer committed
660
Lemma rule_new : forall v,
charguer's avatar
charguer committed
661
  triple (prim_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
charguer's avatar
charguer committed
662 663 664 665 666 667 668 669 670 671
Proof using.
  intros. intros h1 h2 _ P1.
  lets E: hprop_empty_inv P1. subst h1.
  lets (l&Dl): (state_disjoint_new h2 v).
  sets h1': (state_single l v).
  exists h1' (val_loc l). splits~.
  { rew_state. applys~ red_new. }
  { applys~ on_sub_base. exists l. 
    applys~ himpl_inst_prop (l ~~> v). split~. }
Qed.
charguer's avatar
charguer committed
672

charguer's avatar
charguer committed
673
Lemma rule_get : forall v l,
charguer's avatar
charguer committed
674
  triple (prim_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
charguer's avatar
charguer committed
675 676 677 678 679
Proof using.
  intros. intros h1 h2 D P1. exists h1 v. splits~.
  { rew_state. applys red_get. applys~ state_union_single_read. }
  { exists h1 heap_empty. splits~. { exists~ heap_empty h1. } }
Qed.
charguer's avatar
charguer committed
680

charguer's avatar
charguer committed
681
Lemma rule_set : forall l v w, (* todo: changer order of arguments *)
charguer's avatar
charguer committed
682
  triple (prim_set (val_pair (val_loc l) w)) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
charguer's avatar
charguer committed
683 684 685 686 687 688 689 690
Proof using.
  intros. intros h1 h2 D P1.
  sets h1': (state_single l w).
  exists h1' val_unit. splits~.
  { applys state_disjoint_single_set v. rewrite~ <- P1. }
  { rew_state. applys~ red_set. applys~ state_union_single_write v w. }
  { applys~ on_sub_base. applys~ himpl_inst_prop (l ~~> w). split~. }
Qed.
charguer's avatar
charguer committed
691

charguer's avatar
charguer committed
692
End TripleWithGC.
charguer's avatar
charguer committed
693

charguer's avatar
charguer committed
694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730




(********************************************************************)
(********************************************************************)
(********************************************************************)
(** * Triples with lifting *)

Module TripleWithGCAndLifting.

Import TripleWithGC.
Generalizable Variables A B.


Definition func := val.


Class Enc (A:Type) := 
  make_Enc { enc : A -> val }.

Instance Enc_int : Enc int. 
Proof using. constructor. applys val_int. Defined.

Instance Enc_func : Enc func. 
Proof using. constructor. applys (fun x:func => x). Defined.


Definition Subst_trm (x:var) `{Enc A} (X:A) (t:trm) : trm :=
  subst_trm x (enc X) t.

Definition PostEnc `{Enc A} (Q:A->hprop) : val->hprop :=
  fun v => Hexists V, \[v = enc V] \* Q V.

Definition Triple (t:trm) (H:hprop) `{EA:Enc A} (Q:A->hprop) :=
  triple t H (PostEnc Q).

charguer's avatar
charguer committed
731
Lemma Rule_val : forall A `{EA:Enc A} (V:A) v H (Q:A->hprop),
charguer's avatar
charguer committed
732 733 734 735 736 737 738 739 740 741
  v = enc V ->
  H ==> Q V ->
  Triple (trm_val v) H Q.
Proof using.
  introv E M. applys rule_val.
  unfold PostEnc. subst.
  applys himpl_inst_exists V.
  applys~ himpl_inst_prop.
Qed.

charguer's avatar
charguer committed
742
Lemma Rule_if : forall (V:int) v t1 t2 H A `{EA:Enc A} (Q:A->hprop),
charguer's avatar
charguer committed
743 744 745 746 747 748 749 750 751
  v = enc V ->
  Triple (If V = 0 then t2 else t1) H Q ->
  Triple (trm_if v t1 t2) H Q.
Proof using.
  introv E M. applys rule_if. subst. 
  applys_eq (rm M) 3. tests: (V = 0); simpl; case_if~.
Qed.

Lemma Rule_let : forall x t1 t2 H,
charguer's avatar
charguer committed
752
  forall A `{EA:Enc A} (Q:A->hprop) A1 `{EA1:Enc A1} (Q1:A1->hprop),
charguer's avatar
charguer committed
753 754 755 756 757 758 759 760 761 762 763 764 765
  Triple t1 H Q1 ->
  (forall (X:A1), Triple (Subst_trm x X t2) (Q1 X) Q) ->
  Triple (trm_let x t1 t2) H Q.
Proof using.
  introv M1 M2. applys rule_let M1.
  intros v. unfold PostEnc.
  applys rule_extract_exists. intros V.
  rewrite hprop_star_comm. applys rule_extract_prop.
  introv E. subst. applys M2.
(* TODO: why notation for hprop_exists shows hexists? *)
Qed.


charguer's avatar
charguer committed
766
Lemma Rule_let_val_enc : forall A1 `{Enc A1} (V1:A1) x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
charguer's avatar
charguer committed
767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817
  v1 = enc V1 ->
  (forall X, X = V1 -> Triple (Subst_trm x X t2) H Q) ->
  Triple (trm_let x (trm_val v1) t2) H Q.
Proof using.
  introv E M. applys rule_let_val. intros X EX. subst. applys~ M.
Qed.

(*
Lemma Rule_let_val : forall x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
  (forall `{Enc A1} (X:A1), v1 = enc X -> Triple (Subst_trm x X t2) H Q) ->
  Triple (trm_let x (trm_val v1) t2) H Q.
 => true by exploiting the fact that every value is the encoding of another.
*)

Lemma Rule_app : forall f x (F:func) V t1 H A `{EA:Enc A} (Q:A->hprop),
  F = (val_fix f x t1) ->
  Triple (subst_trm f F (subst_trm x V t1)) H Q ->
  Triple (trm_app F V) H Q.
Proof using.
  introv EF M. applys* rule_app.
Qed.

Lemma enc_val_fix_eq : forall F f x t1,
  F = val_fix f x t1 ->
  enc F = F.
Proof using. intros. subst~. Qed.

Lemma Rule_let_fix : forall f x t1 t2 H A `{EA:Enc A} (Q:A->hprop),
  (forall (F:func), 
    (forall `{EA1:Enc A1} `{EA2:Enc A2} (X:A1) H' (Q':A2->hprop), 
      Triple (Subst_trm f F (Subst_trm x X t1)) H' Q' ->
      Triple (trm_app F (enc X)) H' Q') ->
    Triple (Subst_trm f F t2) H Q) ->
  Triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
Proof using.
  introv M. applys (@Rule_let_val_enc _ _ (val_fix f x t1)).
  { symmetry. applys* enc_val_fix_eq. }
  intros F EF. applys (rm M). clears H Q.
  intros A2 EA2 A3 EA3 X H Q M.
  applys~ Rule_app EF.
Qed.

Definition hprop_single_enc `{EA:Enc A} r V := 
  hprop_single r (enc V).

Notation "r '~~~>' V" := (hprop_single_enc r V)
  (at level 32, no associativity) : heap_scope.

Instance Enc_loc : Enc loc. 
Proof using. constructor. applys val_loc. Defined.

charguer's avatar
charguer committed
818
Lemma Rule_new : forall A `{EA:Enc A} (V:A) v,
charguer's avatar
charguer committed
819
  v = enc V ->
charguer's avatar
charguer committed
820
  Triple (prim_new v) \[] (fun l => l ~~~> V).
charguer's avatar
charguer committed
821 822 823 824
Proof using.
  introv E. applys_eq rule_new 1. subst~. 
Qed.

charguer's avatar
charguer committed
825
Lemma Rule_get : forall A `{EA:Enc A} (V:A) l,
charguer's avatar
charguer committed
826
  Triple (prim_get (val_loc l)) (l ~~~> V) (fun x => \[x = V] \* (l ~~~> V)).
charguer's avatar
charguer committed
827 828 829 830 831 832 833 834 835 836 837 838 839
Proof using.
  introv. applys rule_consequence. { auto. } { applys rule_get. }
  { intros v. unfold PostEnc. 
    applys himpl_extract_prop. intro_subst.
    applys himpl_inst_exists V.
    applys~ himpl_inst_prop.
    applys~ himpl_inst_prop. }
Qed.


Instance Enc_unit : Enc unit. 
Proof using. constructor. applys (fun x:unit => val_unit). Defined.

charguer's avatar
charguer committed
840
Lemma Rule_set : forall A1 A2 `{EA1:Enc A1} (V1:A1) `{EA2:Enc A2} (V2:A2) l v2,
charguer's avatar
charguer committed
841
  v2 = enc V2 ->
charguer's avatar
charguer committed
842
  Triple (prim_set (val_pair (val_loc l) v2)) (l ~~~> V1) (fun (r:unit) => l ~~~> V2).
charguer's avatar
charguer committed
843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861
Proof using.
  introv E. applys rule_consequence. { auto. } { applys rule_set. }
  { subst. intros v. unfold PostEnc. 
    applys himpl_extract_prop. intro_subst.
    applys himpl_inst_exists tt.
    applys~ himpl_inst_prop. }
Qed.

End TripleWithGCAndLifting.