CFHeaps.v 90.3 KB
Newer Older
charguer's avatar
init  
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
Require Export LibCore Shared LibMonoid LibMap LibSet.
charguer's avatar
init  
charguer committed
3 4 5


(********************************************************************)
charguer's avatar
charguer committed
6
(* ** States *)
charguer's avatar
init  
charguer committed
7 8 9 10 11 12

(*------------------------------------------------------------------*)
(* ** Representation of values packed with their type *)

(** Representation of heap items *)

13 14
Record dynamic := dyn {
  dyn_type : Type;
charguer's avatar
init  
charguer committed
15 16
  dyn_value : dyn_type }.

charguer's avatar
charguer committed
17
Arguments dyn {dyn_type}.
charguer's avatar
init  
charguer committed
18 19

Lemma dyn_inj : forall A (x y : A),
20
  dyn x = dyn y -> x = y.
charguer's avatar
new_gc  
charguer committed
21
Proof using. introv H. inverts~ H. Qed.
charguer's avatar
init  
charguer committed
22 23 24

Lemma dyn_inj_type : forall A1 A2 (x1:A1) (x2:A2),
  dyn x1 = dyn x2 -> A1 = A2.
charguer's avatar
new_gc  
charguer committed
25
Proof using. introv H. inverts~ H. Qed.
charguer's avatar
init  
charguer committed
26

27
Lemma dyn_eta : forall d,
charguer's avatar
init  
charguer committed
28
  d = dyn (dyn_value d).
charguer's avatar
new_gc  
charguer committed
29
Proof using. intros. destruct~ d. Qed.
charguer's avatar
init  
charguer committed
30 31 32 33 34 35 36 37 38 39 40 41 42


(*------------------------------------------------------------------*)
(* ** Representation of partial functions *)

(** Type of partial functions from A to B *)

Definition pfun (A B : Type) :=
  A -> option B.

(** Finite domain of a partial function *)

Definition pfun_finite (A B : Type) (f : pfun A B) :=
charguer's avatar
charguer committed
43
  exists (L : list A), forall x, f x <> None -> mem x L.
charguer's avatar
init  
charguer committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61

(** Disjointness of domain of two partial functions *)

Definition pfun_disjoint (A B : Type) (f1 f2 : pfun A B) :=
  forall x, f1 x = None \/ f2 x = None.

(** Disjoint union of two partial functions *)

Definition pfun_union (A B : Type) (f1 f2 : pfun A B) :=
  fun x => match f1 x with
           | Some y => Some y
           | None => f2 x
           end.

(** Finiteness of union *)

Lemma pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B),
  pfun_finite f1 -> pfun_finite f2 -> pfun_finite (pfun_union f1 f2).
charguer's avatar
new_gc  
charguer committed
62
Proof using.
charguer's avatar
init  
charguer committed
63
  introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M.
64
  specializes F1 x. specializes F2 x. unfold pfun_union in M.
charguer's avatar
charguer committed
65
  rewrite mem_app_eq. destruct~ (f1 x).
charguer's avatar
init  
charguer committed
66 67 68 69 70 71
Qed.

(** Symmetry of disjointness *)

Lemma pfun_disjoint_sym : forall (A B : Type),
  sym (@pfun_disjoint A B).
charguer's avatar
new_gc  
charguer committed
72
Proof using.
charguer's avatar
init  
charguer committed
73 74 75 76 77
  introv H. unfolds pfun_disjoint. intros z. specializes H z. intuition.
Qed.

(** Commutativity of disjoint union *)

charguer's avatar
charguer committed
78
Tactic Notation "cases" constr(E) :=  (* TODO: move *)
charguer's avatar
init  
charguer committed
79 80 81
  let H := fresh "Eq" in cases E as H.

Lemma pfun_union_comm : forall (A B : Type) (f1 f2 : pfun A B),
82
  pfun_disjoint f1 f2 ->
charguer's avatar
init  
charguer committed
83
  pfun_union f1 f2 = pfun_union f2 f1.
84
Proof using.
charguer's avatar
init  
charguer committed
85
  introv H. extens. intros x. unfolds pfun_disjoint, pfun_union.
86
  specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false.
charguer's avatar
init  
charguer committed
87 88 89
Qed.

(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
90 91
(* ** Representation of states *)

92
Section State.
charguer's avatar
init  
charguer committed
93 94 95 96 97 98 99 100 101 102 103

(** Representation of locations *)

Definition loc : Type := nat.

Global Opaque loc.

(** The null location *)

Definition null : loc := 0%nat.

charguer's avatar
charguer committed
104 105 106 107 108 109 110
(** Representation of the field of an in-memory object;
    For a record, the field is the field index;
    For an array, the field is the cell index. *)

Definition field : Type := nat.

(** Representation of the address of a memory cell,
Armaël Guéneau's avatar
Armaël Guéneau committed
111
    as a pair of the location at which the object
charguer's avatar
charguer committed
112 113 114 115
    is allocated and the field within this object. *)

Definition address : Type := (loc * field)%type.

charguer's avatar
init  
charguer committed
116 117
(** Representation of heaps *)

charguer's avatar
charguer committed
118
Inductive state : Type := state_of {
charguer's avatar
charguer committed
119
  state_data :> pfun address dynamic;
charguer's avatar
charguer committed
120
  state_finite : pfun_finite state_data }.
charguer's avatar
init  
charguer committed
121

charguer's avatar
charguer committed
122
Arguments state_of : clear implicits.
charguer's avatar
init  
charguer committed
123

charguer's avatar
charguer committed
124
(** Proving states equals *)
charguer's avatar
init  
charguer committed
125

charguer's avatar
charguer committed
126
Lemma state_eq : forall f1 f2 F1 F2,
charguer's avatar
init  
charguer committed
127
  (forall x, f1 x = f2 x) ->
charguer's avatar
charguer committed
128
  state_of f1 F1 = state_of f2 F2.
charguer's avatar
new_gc  
charguer committed
129
Proof using.
130
  introv H. asserts: (f1 = f2). extens~. subst.
charguer's avatar
init  
charguer committed
131 132 133
  fequals. (* note: involves proof irrelevance *)
Qed.

charguer's avatar
charguer committed
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
(** Disjoint states *)

Definition state_disjoint (h1 h2 : state) : Prop :=
  pfun_disjoint h1 h2.

Notation "\# h1 h2" := (state_disjoint h1 h2)
  (at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope.
Local Open Scope state_scope.

(** Union of states *)

Program Definition state_union (h1 h2 : state) : state :=
  state_of (pfun_union h1 h2) _.
Next Obligation. destruct h1. destruct h2. apply~ pfun_union_finite. Qed.

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

(** Empty state *)

Program Definition state_empty : state :=
charguer's avatar
charguer committed
155 156
  state_of (fun a => None) _.
Next Obligation. exists (@nil address). auto_false. Qed.
charguer's avatar
charguer committed
157 158 159

(** Singleton state *)

charguer's avatar
charguer committed
160 161
Program Definition state_single (l:loc) (f:field) A (v:A) : state :=
  state_of (fun a' => If a' = (l,f) then Some (dyn v) else None) _.
charguer's avatar
charguer committed
162
Next Obligation.
charguer's avatar
charguer committed
163
  exists ((l,f)::nil). intros. case_if. subst~.
charguer's avatar
charguer committed
164 165 166 167 168 169 170 171 172
Qed.

(*------------------------------------------------------------------*)
(* ** Properties on states *)

(** Disjointness *)

Lemma state_disjoint_sym : forall h1 h2,
  state_disjoint h1 h2 -> state_disjoint h2 h1.
charguer's avatar
new_gc  
charguer committed
173
Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed.
charguer's avatar
charguer committed
174 175 176

Lemma state_disjoint_comm : forall h1 h2,
  \# h1 h2 = \# h2 h1.
177
Proof using. lets: state_disjoint_sym. extens*. Qed.
charguer's avatar
charguer committed
178 179 180

Lemma state_disjoint_empty_l : forall h,
  state_disjoint state_empty h.
charguer's avatar
new_gc  
charguer committed
181
Proof using. intros [f F] x. simple~. Qed.
charguer's avatar
charguer committed
182 183 184

Lemma state_disjoint_empty_r : forall h,
  state_disjoint h state_empty.
charguer's avatar
new_gc  
charguer committed
185
Proof using. intros [f F] x. simple~. Qed.
charguer's avatar
charguer committed
186 187 188 189 190 191

Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r.

Lemma state_disjoint_union_eq_r : forall h1 h2 h3,
  state_disjoint h1 (state_union h2 h3) =
  (state_disjoint h1 h2 /\ state_disjoint h1 h3).
charguer's avatar
new_gc  
charguer committed
192
Proof using.
charguer's avatar
charguer committed
193 194 195
  intros [f1 F1] [f2 F2] [f3 F3].
  unfolds state_disjoint, state_union. simpls.
  unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2].
Armaël Guéneau's avatar
Armaël Guéneau committed
196
  split; intros x; specializes M x;
charguer's avatar
charguer committed
197
   destruct (f2 x); destruct M; auto_false.
198
  intros x. specializes M1 x. specializes M2 x.
charguer's avatar
charguer committed
199
   destruct (f2 x); destruct M1; auto_false.
charguer's avatar
charguer committed
200 201 202 203 204
Qed.

Lemma state_disjoint_union_eq_l : forall h1 h2 h3,
  state_disjoint (state_union h2 h3) h1 =
  (state_disjoint h1 h2 /\ state_disjoint h1 h3).
charguer's avatar
new_gc  
charguer committed
205
Proof using.
206
  intros. rewrite state_disjoint_comm.
charguer's avatar
charguer committed
207 208 209 210 211 212 213 214 215 216 217 218
  apply state_disjoint_union_eq_r.
Qed.

Definition state_disjoint_3 h1 h2 h3 :=
  state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3.

Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3)
  (at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity)
  : state_scope.

Lemma state_disjoint_3_unfold : forall h1 h2 h3,
  \# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
charguer's avatar
new_gc  
charguer committed
219
Proof using. auto. Qed.
charguer's avatar
charguer committed
220 221 222 223 224

(** Union *)

Lemma state_union_neutral_l : forall h,
  state_union state_empty h = h.
225
Proof using.
charguer's avatar
charguer committed
226 227 228 229 230 231
  intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
  apply~ state_eq.
Qed.

Lemma state_union_neutral_r : forall h,
  state_union h state_empty = h.
232
Proof using.
charguer's avatar
charguer committed
233 234 235 236 237 238 239
  intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
  apply state_eq. intros x. destruct~ (f x).
Qed.

Lemma state_union_comm : forall h1 h2,
  state_disjoint h1 h2 ->
  state_union h1 h2 = state_union h2 h1.
charguer's avatar
new_gc  
charguer committed
240
Proof using.
charguer's avatar
charguer committed
241 242 243 244
  intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl.
  intros. rewrite~ pfun_union_comm.
Qed.

245
Lemma state_union_assoc :
charguer's avatar
charguer committed
246
  LibOperation.assoc state_union.
charguer's avatar
new_gc  
charguer committed
247
Proof using.
charguer's avatar
charguer committed
248 249 250 251 252 253 254 255 256 257
  intros [f1 F1] [f2 F2] [f3 F3]. unfolds state_union. simpls.
  apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x).
Qed.

End State.

(** Hints and tactics *)

Hint Resolve state_union_neutral_l state_union_neutral_r.

258
Hint Rewrite
charguer's avatar
charguer committed
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
  state_disjoint_union_eq_l
  state_disjoint_union_eq_r
  state_disjoint_3_unfold : rew_disjoint.

Tactic Notation "rew_disjoint" :=
  autorewrite with rew_disjoint in *.
Tactic Notation "rew_disjoint" "*" :=
  rew_disjoint; auto_star.



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

(*------------------------------------------------------------------*)
(* ** Representation of heaps *)

(** Representation of credits *)

278
Definition credits_type : Type := int.
charguer's avatar
charguer committed
279 280 281

(** Zero and one credits *)

282 283
Definition credits_zero : credits_type := 0.
Definition credits_one : credits_type := 1.
charguer's avatar
charguer committed
284 285 286 287 288

(** Representation of heaps *)

Definition heap : Type := (state * credits_type)%type.

289 290 291 292 293 294 295 296
(** Projections *)

Definition heap_state (h:heap) : state :=
  match h with (m,_) => m end.

Definition heap_credits (h:heap) : credits_type :=
  match h with (_,c) => c end.

charguer's avatar
charguer committed
297 298 299 300 301 302
(** Predicate over pairs *)

Definition prod_st A B (v:A*B) (P:A->Prop) (Q:B->Prop) := (* todo move to TLC *)
  let (x,y) := v in P x /\ Q y.

Definition prod_st2 A B (P:binary A) (Q:binary B) (v1 v2:A*B) := (* todo move to TLC *)
303 304
  let (x1,y1) := v1 in
  let (x2,y2) := v2 in
charguer's avatar
charguer committed
305 306 307
  P x1 x2 /\ Q y1 y2.

Definition prod_func A B (F:A->A->A) (G:B->B->B) (v1 v2:A*B) := (* todo move to TLC *)
308 309
  let (x1,y1) := v1 in
  let (x2,y2) := v2 in
charguer's avatar
charguer committed
310 311
  (F x1 x2, G y1 y2).

charguer's avatar
init  
charguer committed
312 313 314
(** Disjoint heaps *)

Definition heap_disjoint (h1 h2 : heap) : Prop :=
charguer's avatar
charguer committed
315
  prod_st2 state_disjoint (fun _ _ => True) h1 h2. (* todo: name (fun _ _ => True) *)
charguer's avatar
init  
charguer committed
316 317 318 319 320 321

Notation "\# h1 h2" := (heap_disjoint h1 h2)
  (at level 40, h1 at level 0, h2 at level 0, no associativity).

(** Union of heaps *)

charguer's avatar
charguer committed
322
Definition heap_union (h1 h2 : heap) : heap :=
323
  prod_func state_union (fun a b => (a + b)) h1 h2.
charguer's avatar
init  
charguer committed
324 325 326 327 328 329

Notation "h1 \+ h2" := (heap_union h1 h2)
   (at level 51, right associativity).

(** Empty heap *)

charguer's avatar
charguer committed
330
Definition heap_empty : heap :=
331
  (state_empty, 0).
charguer's avatar
init  
charguer committed
332

333 334 335 336
(** Affine heaps *)

Definition heap_affine (h: heap) : Prop :=
  0 <= heap_credits h.
charguer's avatar
init  
charguer committed
337 338 339 340 341 342 343 344

(*------------------------------------------------------------------*)
(* ** Properties on heaps *)

(** Disjointness *)

Lemma heap_disjoint_sym : forall h1 h2,
  heap_disjoint h1 h2 -> heap_disjoint h2 h1.
charguer's avatar
new_gc  
charguer committed
345
Proof using.
charguer's avatar
charguer committed
346 347 348
  intros [m1 n1] [m2 n2] H. simpls.
  hint state_disjoint_sym. autos*.
Qed.
charguer's avatar
init  
charguer committed
349 350 351

Lemma heap_disjoint_comm : forall h1 h2,
  \# h1 h2 = \# h2 h1.
352
Proof using.
charguer's avatar
charguer committed
353 354
  intros [m1 n1] [m2 n2]. simpls.
  hint state_disjoint_sym. extens*.
355
Qed.
charguer's avatar
init  
charguer committed
356 357 358

Lemma heap_disjoint_empty_l : forall h,
  heap_disjoint heap_empty h.
charguer's avatar
new_gc  
charguer committed
359
Proof using. intros [m n]. hint state_disjoint_empty_l. simple*. Qed.
charguer's avatar
init  
charguer committed
360 361 362

Lemma heap_disjoint_empty_r : forall h,
  heap_disjoint h heap_empty.
charguer's avatar
new_gc  
charguer committed
363
Proof using. intros [m n]. hint state_disjoint_empty_r. simple*. Qed.
charguer's avatar
init  
charguer committed
364 365 366 367 368 369

Hint Resolve heap_disjoint_sym heap_disjoint_empty_l heap_disjoint_empty_r.

Lemma heap_disjoint_union_eq_r : forall h1 h2 h3,
  heap_disjoint h1 (heap_union h2 h3) =
  (heap_disjoint h1 h2 /\ heap_disjoint h1 h3).
charguer's avatar
new_gc  
charguer committed
370
Proof using.
charguer's avatar
charguer committed
371
  intros [m1 n1] [m2 n2] [m3 n3].
charguer's avatar
init  
charguer committed
372
  unfolds heap_disjoint, heap_union. simpls.
charguer's avatar
charguer committed
373
  rewrite state_disjoint_union_eq_r. extens*.
charguer's avatar
init  
charguer committed
374 375 376 377 378
Qed.

Lemma heap_disjoint_union_eq_l : forall h1 h2 h3,
  heap_disjoint (heap_union h2 h3) h1 =
  (heap_disjoint h1 h2 /\ heap_disjoint h1 h3).
charguer's avatar
new_gc  
charguer committed
379
Proof using.
380
  intros. rewrite heap_disjoint_comm.
charguer's avatar
init  
charguer committed
381 382 383 384 385 386 387 388 389 390 391
  apply heap_disjoint_union_eq_r.
Qed.

Definition heap_disjoint_3 h1 h2 h3 :=
  heap_disjoint h1 h2 /\ heap_disjoint h2 h3 /\ heap_disjoint h1 h3.

Notation "\# h1 h2 h3" := (heap_disjoint_3 h1 h2 h3)
  (at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity).

Lemma heap_disjoint_3_unfold : forall h1 h2 h3,
  \# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
charguer's avatar
new_gc  
charguer committed
392
Proof using. auto. Qed.
charguer's avatar
init  
charguer committed
393 394 395 396 397

(** Union *)

Lemma heap_union_neutral_l : forall h,
  heap_union heap_empty h = h.
398
Proof using.
charguer's avatar
charguer committed
399 400
  intros [m n]. unfold heap_union, heap_empty. simpl.
  fequals. apply~ state_union_neutral_l.
charguer's avatar
init  
charguer committed
401 402 403 404
Qed.

Lemma heap_union_neutral_r : forall h,
  heap_union h heap_empty = h.
405
Proof using.
charguer's avatar
charguer committed
406 407
  intros [m n]. unfold heap_union, heap_empty. simpl.
  fequals. apply~ state_union_neutral_r. math.
charguer's avatar
init  
charguer committed
408 409 410 411 412
Qed.

Lemma heap_union_comm : forall h1 h2,
  heap_disjoint h1 h2 ->
  heap_union h1 h2 = heap_union h2 h1.
charguer's avatar
new_gc  
charguer committed
413
Proof using.
charguer's avatar
charguer committed
414 415 416
  intros [m1 n1] [m2 n2] H. simpls. fequals.
  applys* state_union_comm.
  math.
charguer's avatar
init  
charguer committed
417 418
Qed.

419
Lemma heap_union_assoc :
charguer's avatar
init  
charguer committed
420
  LibOperation.assoc heap_union.
charguer's avatar
new_gc  
charguer committed
421
Proof using.
charguer's avatar
charguer committed
422 423
  intros [m1 n1] [m2 n2] [m3 n3]. unfolds heap_union. simpls.
  fequals. applys state_union_assoc. math.
charguer's avatar
init  
charguer committed
424 425
Qed.

426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449
(** Affine *)

Lemma heap_affine_empty :
  heap_affine heap_empty.
Proof.
  unfold heap_affine, heap_empty. simpl.
  math.
Qed.

Lemma heap_affine_union : forall h1 h2,
  heap_affine h1 ->
  heap_affine h2 ->
  heap_affine (h1 \+ h2).
Proof.
  intros (m1 & c1) (m2 & c2) HA1 HA2.
  unfold heap_affine, heap_union, prod_func in *. simpl in *.
  math.
Qed.

Lemma heap_affine_credits : forall c,
  0 <= c ->
  heap_affine (state_empty, c).
Proof. auto. Qed.

450 451 452
Lemma heap_affine_single : forall l f A (v:A),
  heap_affine (state_single l f v, 0).
Proof. intros. unfold heap_affine. simpl. math. Qed.
453

charguer's avatar
init  
charguer committed
454 455 456 457
(** Hints and tactics *)

Hint Resolve heap_union_neutral_l heap_union_neutral_r.

458
Hint Rewrite
charguer's avatar
init  
charguer committed
459 460 461 462 463 464 465 466 467 468
  heap_disjoint_union_eq_l
  heap_disjoint_union_eq_r
  heap_disjoint_3_unfold : rew_disjoint.

Tactic Notation "rew_disjoint" :=
  autorewrite with rew_disjoint in *.
Tactic Notation "rew_disjoint" "*" :=
  rew_disjoint; auto_star.


charguer's avatar
charguer committed
469

charguer's avatar
init  
charguer committed
470 471 472 473 474 475 476 477 478 479 480 481
(********************************************************************)
(* ** Predicate on Heaps *)

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

(** [hprop] is the type of predicates on heaps *)

Definition hprop := heap -> Prop.

(** Empty heap *)

482
Definition heap_is_empty : hprop :=
charguer's avatar
init  
charguer committed
483 484 485 486
  fun h => h = heap_empty.

(** Singleton heap *)

charguer's avatar
charguer committed
487 488
Definition heap_is_single (l:loc) (f:field) A (v:A) : hprop :=
  fun h => let (m,n) := h in m = state_single l f v /\ l <> null /\ n = 0%nat.
charguer's avatar
charguer committed
489

charguer's avatar
init  
charguer committed
490 491
(** Heap union *)

492 493 494 495
Definition heap_is_star (H1 H2 : hprop) : hprop :=
  fun h => exists h1 h2, H1 h1
                      /\ H2 h2
                      /\ heap_disjoint h1 h2
charguer's avatar
init  
charguer committed
496 497
                      /\ h = heap_union h1 h2.

498 499 500 501 502
(** Affine heap predicates *)

Definition affine (H : hprop) : Prop :=
  forall h, H h -> heap_affine h.

charguer's avatar
init  
charguer committed
503 504
(** Lifting of existentials *)

505
Definition heap_is_pack A (Hof : A -> hprop) : hprop :=
charguer's avatar
init  
charguer committed
506 507 508 509 510 511 512
  fun h => exists x, Hof x h.

(** Lifting of predicates *)

Definition heap_is_empty_st (H:Prop) : hprop :=
  fun h => h = heap_empty /\ H.

513
(** Garbage collection predicate: equivalent to [Hexists H, H \* \[affine H]]. *)
charguer's avatar
cp  
charguer committed
514

515
Definition heap_is_gc : hprop :=
516
  fun h => heap_affine h /\ exists H, H h.
charguer's avatar
cp  
charguer committed
517

charguer's avatar
credits  
charguer committed
518 519
(** Credits *)

520 521
Definition heap_is_credits (x:int) : hprop :=
  fun h => let (m,x') := h in m = state_empty /\ x' = x.
charguer's avatar
credits  
charguer committed
522

523
Opaque heap_union state_single heap_is_star heap_is_pack
524
  heap_is_gc heap_is_credits heap_affine affine.
charguer's avatar
init  
charguer committed
525

charguer's avatar
charguer committed
526 527 528
(** Hprop is inhabited *)

Instance hprop_inhab : Inhab hprop.
charguer's avatar
charguer committed
529
Proof using. intros. apply (Inhab_of_val heap_is_empty). Qed.
charguer's avatar
charguer committed
530

charguer's avatar
init  
charguer committed
531 532 533 534

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

535
Notation "\[]" := (heap_is_empty)
charguer's avatar
init  
charguer committed
536 537 538 539 540 541
  (at level 0) : heap_scope.

Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.

542
Notation "\[ L ]" := (heap_is_empty_st L)
charguer's avatar
init  
charguer committed
543 544 545 546 547
  (at level 0, L at level 99) : heap_scope.

Notation "H1 '\*' H2" := (heap_is_star H1 H2)
  (at level 41, right associativity) : heap_scope.

548
Notation "\GC" := (heap_is_gc) : heap_scope.
charguer's avatar
cp  
charguer committed
549

550
Notation "'\$' x" := (heap_is_credits x)
charguer's avatar
credits  
charguer committed
551 552
  (at level 40, format "\$ x") : heap_scope.

charguer's avatar
init  
charguer committed
553 554 555 556 557 558
Notation "'Hexists' x1 , H" := (heap_is_pack (fun x1 => H))
  (at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
  (at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
559
Notation "'Hexists' x1 x2 x3 x4 , H" :=
charguer's avatar
init  
charguer committed
560 561
  (Hexists x1, Hexists x2, Hexists x3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50) : heap_scope.
562
Notation "'Hexists' x1 x2 x3 x4 x5 , H" :=
charguer's avatar
init  
charguer committed
563 564 565 566 567 568 569
  (Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.

Notation "'Hexists' x1 : T1 , H" := (heap_is_pack (fun x1:T1 => H))
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
570
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) , H" :=
charguer's avatar
init  
charguer committed
571 572
  (Hexists x1:T1, Hexists x2:T2, H)
  (at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
573
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) , H" :=
charguer's avatar
init  
charguer committed
574 575
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
576
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) , H" :=
charguer's avatar
init  
charguer committed
577 578
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
579
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) ( x5 : T5 ) , H" :=
charguer's avatar
init  
charguer committed
580 581 582
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, Hexists x5:T5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

583
Notation "'Hexists' ( x1 x2 : T ) , H" :=
charguer's avatar
init  
charguer committed
584 585
  (Hexists x1:T, Hexists x2:T, H)
  (at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
586
Notation "'Hexists' ( x1 x2 x3 : T ) , H" :=
charguer's avatar
init  
charguer committed
587 588
  (Hexists x1:T, Hexists x2:T, Hexists x3:T, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
589
Notation "'Hexists' ( x1 x2 x3 x4 : T ) , H" :=
charguer's avatar
init  
charguer committed
590 591
  (Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
592
Notation "'Hexists' ( x1 x2 x3 x4 x5 : T ) , H" :=
charguer's avatar
init  
charguer committed
593 594 595
  (Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, Hexists x5:T, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

596
Notation "'Hexists' ( x1 : T1 ) x2 , H" :=
charguer's avatar
init  
charguer committed
597 598
  (Hexists x1:T1, Hexists x2, H)
  (at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
599
Notation "'Hexists' ( x1 : T1 ) x2 x3 , H" :=
charguer's avatar
init  
charguer committed
600 601
  (Hexists x1:T1, Hexists x2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
602
Notation "'Hexists' ( x1 : T1 ) x2 x3 x4 , H" :=
charguer's avatar
init  
charguer committed
603 604
  (Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
605
Notation "'Hexists' ( x1 : T1 ) x2 x3 x4 x5 , H" :=
charguer's avatar
init  
charguer committed
606 607 608
  (Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

609
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 , H" :=
charguer's avatar
init  
charguer committed
610 611
  (Hexists x1:T1, Hexists x2:T2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
612
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 , H" :=
charguer's avatar
init  
charguer committed
613 614
  (Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
615
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 x5 , H" :=
charguer's avatar
init  
charguer committed
616 617 618
  (Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

619
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 , H" :=
charguer's avatar
init  
charguer committed
620 621
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
622
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 x5 , H" :=
charguer's avatar
init  
charguer committed
623 624 625 626 627 628 629 630
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.


Notation "Q \*+ H" :=
  (fun x => heap_is_star (Q x) H)
  (at level 40) : heap_scope.

charguer's avatar
charguer committed
631
Notation "# H" := (fun (_:unit) => (H:hprop))
charguer's avatar
init  
charguer committed
632 633
  (at level 39, H at level 99) : heap_scope.

charguer's avatar
charguer committed
634 635 636
Notation "\[= v ]" := (fun x => \[x = v])
  (at level 0) : heap_scope.

charguer's avatar
charguer committed
637
Notation "P ==+> Q" := (pred_incl P%h (heap_is_star P Q))
charguer's avatar
cp  
charguer committed
638
  (at level 55, only parsing) : heap_scope.
charguer's avatar
charguer committed
639
(* TODO: notation PRE P '/' ==> KEEP '/' POST Q *)
charguer's avatar
init  
charguer committed
640

charguer's avatar
cp  
charguer committed
641
(* DEPRECATED
642
Notation "'hkeep' P '==>' Q" := (pred_le P%h (Q \* P))
charguer's avatar
cp  
charguer committed
643 644
  (at level 55, P at level 0, right associativity) : heap_scope.
*)
charguer's avatar
init  
charguer committed
645

charguer's avatar
charguer committed
646

charguer's avatar
init  
charguer committed
647
(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
648
(* ** Properties of heap empty *)
charguer's avatar
init  
charguer committed
649

650
Lemma heap_is_empty_prove :
charguer's avatar
charguer committed
651
  \[] heap_empty.
charguer's avatar
new_gc  
charguer committed
652
Proof using. hnfs~. Qed.
charguer's avatar
init  
charguer committed
653 654

Lemma heap_is_empty_st_prove : forall (P:Prop),
charguer's avatar
charguer committed
655
  P -> \[P] heap_empty.
charguer's avatar
new_gc  
charguer committed
656
Proof using. intros. hnfs~. Qed.
charguer's avatar
init  
charguer committed
657 658 659

Hint Resolve heap_is_empty_prove heap_is_empty_st_prove.

charguer's avatar
charguer committed
660

charguer's avatar
charguer committed
661 662 663
(*------------------------------------------------------------------*)
(* ** Properties of heap single *)

charguer's avatar
charguer committed
664 665
Lemma heap_is_single_null : forall (l:loc) (f:field) A (v:A) h,
  heap_is_single l f v h -> l <> null.
charguer's avatar
new_gc  
charguer committed
666
Proof using. intros. destruct h as [m n]. unfolds* heap_is_single. Qed.
charguer's avatar
init  
charguer committed
667

charguer's avatar
charguer committed
668 669
Lemma heap_is_single_null_eq_false : forall A (v:A) (f:field),
  heap_is_single null f v = \[False].
charguer's avatar
new_gc  
charguer committed
670
Proof using.
charguer's avatar
init  
charguer committed
671
  intros. unfold heap_is_single.
charguer's avatar
charguer committed
672 673
  unfold hprop. extens. intros [m n].
  unfold heap_is_empty_st. autos*.
charguer's avatar
init  
charguer committed
674 675
Qed.

charguer's avatar
charguer committed
676 677
Lemma heap_is_single_null_to_false : forall A (v:A) (f:field),
  heap_is_single null f v ==> \[False].
678
Proof using. introv Hh. forwards*: heap_is_single_null. Qed.
charguer's avatar
init  
charguer committed
679

680
Global Opaque heap_is_empty_st heap_is_single.
charguer's avatar
init  
charguer committed
681

charguer's avatar
charguer committed
682

charguer's avatar
init  
charguer committed
683
(*------------------------------------------------------------------*)
charguer's avatar
charguer committed
684
(* ** Properties of [star] and [pack] *)
charguer's avatar
init  
charguer committed
685 686 687 688

Section Star.
Transparent heap_is_star heap_union.

689 690
Lemma star_comm : comm heap_is_star.
Proof using.
charguer's avatar
init  
charguer committed
691 692 693 694
  intros H1 H2. unfold hprop, heap_is_star. extens. intros h.
  iff (h1&h2&M1&M2&D&U); rewrite~ heap_union_comm in U; exists* h2 h1.
Qed.

charguer's avatar
charguer committed
695
Lemma star_neutral_l : neutral_l heap_is_star \[].
charguer's avatar
new_gc  
charguer committed
696
Proof using.
charguer's avatar
init  
charguer committed
697
  intros H. unfold hprop, heap_is_star. extens. intros h.
698
  iff (h1&h2&M1&M2&D&U) M.
charguer's avatar
init  
charguer committed
699
  hnf in M1. subst h1 h. rewrite~ heap_union_neutral_l.
700
  exists heap_empty h. splits~.
charguer's avatar
init  
charguer committed
701 702
Qed.

charguer's avatar
charguer committed
703
Lemma star_neutral_r : neutral_r heap_is_star \[].
charguer's avatar
new_gc  
charguer committed
704
Proof using.
charguer's avatar
charguer committed
705
  apply neutral_r_of_comm_neutral_l.
charguer's avatar
init  
charguer committed
706 707 708
  apply star_comm. apply star_neutral_l.
Qed.

709 710
Lemma star_assoc : LibOperation.assoc heap_is_star.
Proof using.
charguer's avatar
init  
charguer committed
711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728
  intros H1 H2 H3. unfold hprop, heap_is_star. extens. intros h. split.
  intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
   exists (heap_union h1 h2) h3. rewrite heap_disjoint_union_eq_r in D.
   splits.
    exists h1 h2. splits*.
    auto.
    rewrite* heap_disjoint_union_eq_l.
    rewrite~ <- heap_union_assoc.
  intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
   exists h1 (heap_union h2 h3). rewrite heap_disjoint_union_eq_l in D.
   splits.
    auto.
    exists h2 h3. splits*.
    rewrite* heap_disjoint_union_eq_r.
    rewrite~ heap_union_assoc.
Qed. (* later: exploit symmetry in the proof *)

Lemma star_comm_assoc : comm_assoc heap_is_star.
Armaël Guéneau's avatar
Armaël Guéneau committed
729 730
Proof using.
  apply comm_assoc_of_comm_and_assoc. apply star_comm. apply star_assoc.
charguer's avatar
charguer committed
731
Qed.
charguer's avatar
init  
charguer committed
732 733

Lemma starpost_neutral : forall B (Q:B->hprop),
charguer's avatar
charguer committed
734
  Q \*+ \[] = Q.
charguer's avatar
charguer committed
735
Proof using. extens. intros. (* unfold starpost. *) rewrite* star_neutral_r. Qed.
charguer's avatar
init  
charguer committed
736 737 738

Lemma star_cancel : forall H1 H2 H2',
  H2 ==> H2' -> H1 \* H2 ==> H1 \* H2'.
charguer's avatar
new_gc  
charguer committed
739
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
charguer's avatar
init  
charguer committed
740

charguer's avatar
charguer committed
741 742
Lemma star_is_single_same_loc : forall (l:loc) A (v1 v2:A) (f:field),
  (heap_is_single l f v1) \* (heap_is_single l f v2) ==> \[False].
charguer's avatar
charguer committed
743 744 745
Proof using.
  Transparent heap_is_single state_single.
  intros. intros h ((m1&n1)&(m2&n2)&(E1&?&?)&(E2&?&?)&(D&?)&E).
746
  unfolds heap_disjoint, state_disjoint, prod_st2, pfun_disjoint.
charguer's avatar
charguer committed
747
  specializes D (l,f). rewrite E1, E2 in D.
charguer's avatar
charguer committed
748 749 750
  unfold state_single in D. simpls. case_if. destruct D; tryfalse.
Qed.

charguer's avatar
init  
charguer committed
751
Lemma heap_star_prop_elim : forall (P:Prop) H h,
charguer's avatar
charguer committed
752
  (\[P] \* H) h -> P /\ H h.
charguer's avatar
new_gc  
charguer committed
753
Proof using.
charguer's avatar
init  
charguer committed
754 755 756 757
  introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_neutral_l.
Qed.

Lemma heap_extract_prop : forall (P:Prop) H H',
charguer's avatar
charguer committed
758
  (P -> H ==> H') -> (\[P] \* H) ==> H'.
charguer's avatar
new_gc  
charguer committed
759
Proof using. introv W Hh. applys_to Hh heap_star_prop_elim. autos*. Qed.
charguer's avatar
init  
charguer committed
760 761 762

Lemma heap_weaken_pack : forall A (x:A) H J,
  H ==> J x -> H ==> (heap_is_pack J).
charguer's avatar
new_gc  
charguer committed
763
Proof using. introv W h. exists x. apply~ W. Qed.
charguer's avatar
init  
charguer committed
764

charguer's avatar
charguer committed
765

charguer's avatar
init  
charguer committed
766 767 768 769 770 771
End Star.


(*------------------------------------------------------------------*)
(* ** Separation Logic monoid *)

charguer's avatar
charguer committed
772
Definition sep_monoid := monoid_make heap_is_star heap_is_empty.
charguer's avatar
init  
charguer committed
773

charguer's avatar
charguer committed
774
Global Instance Monoid_sep : Monoid sep_monoid.
charguer's avatar
new_gc  
charguer committed
775
Proof using.
charguer's avatar
init  
charguer committed
776 777 778 779 780 781
  constructor; simpl.
  apply star_assoc.
  apply star_neutral_l.
  apply star_neutral_r.
Qed.

charguer's avatar
charguer committed
782
Global Instance Comm_monoid_sep : Comm_monoid sep_monoid.
charguer's avatar
charguer committed
783 784
Proof using.
  constructor; simpl.
charguer's avatar
charguer committed
785
  applys Monoid_sep.
charguer's avatar
charguer committed
786 787 788
  apply star_comm.
Qed.

charguer's avatar
init  
charguer committed
789 790 791 792

(*------------------------------------------------------------------*)
(* ** Normalization of [star] *)

793
Hint Rewrite
charguer's avatar
init  
charguer committed
794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818
  star_neutral_l star_neutral_r starpost_neutral : rew_heap.
Hint Rewrite <- star_assoc : rew_heap.

Tactic Notation "rew_heap" :=
  autorewrite with rew_heap.
Tactic Notation "rew_heap" "in" "*" :=
  autorewrite with rew_heap in *.
Tactic Notation "rew_heap" "in" hyp(H) :=
  autorewrite with rew_heap in H.

Tactic Notation "rew_heap" "~" :=
  rew_heap; auto_tilde.
Tactic Notation "rew_heap" "~" "in" "*" :=
  rew_heap in *; auto_tilde.
Tactic Notation "rew_heap" "~" "in" hyp(H) :=
  rew_heap in H; auto_tilde.

Tactic Notation "rew_heap" "*" :=
  rew_heap; auto_star.
Tactic Notation "rew_heap" "*" "in" "*" :=
  rew_heap in *; auto_star.
Tactic Notation "rew_heap" "*" "in" hyp(H) :=
  rew_heap in H; auto_star.


charguer's avatar
credits  
charguer committed
819 820 821 822
(*------------------------------------------------------------------*)
(* ** Properties of heap credits *)

Section Credits.
823
Transparent heap_is_credits
charguer's avatar
credits  
charguer committed
824 825 826
  heap_is_empty heap_is_empty_st heap_is_star heap_union heap_disjoint.

Definition pay_one H H' :=
827
  H ==> \$ 1 \* H'.
charguer's avatar
credits  
charguer committed
828

829
Lemma credits_zero_eq : \$ 0 = \[].
charguer's avatar
new_gc  
charguer committed
830
Proof using.
831
  unfold heap_is_credits, heap_is_empty, heap_empty.
charguer's avatar
charguer committed
832
  applys pred_ext_1. intros [m n]. iff [M1 M2] M.  (* todo: extens should work *)
charguer's avatar
credits  
charguer committed
833 834 835 836
    subst*.
    inverts* M.
Qed.

837 838
Lemma credits_split_eq : forall (n m : int),
  \$ (n+m) = \$ n \* \$ m.
charguer's avatar
new_gc  
charguer committed
839
Proof using.
840
  intros c1 c2. unfold heap_is_credits, heap_is_star, heap_union, heap_disjoint.
charguer's avatar
charguer committed
841
  applys pred_ext_1. intros [m n]. (* todo: extens should work *)
charguer's avatar
credits  
charguer committed
842 843 844 845 846 847 848
  iff [M1 M2] ([m1 n1]&[m2 n2]&(M1&E1)&(M2&E2)&M3&M4).
    exists (state_empty,c1) (state_empty,c2). simpl. splits*.
      autos* state_disjoint_empty_l.
      subst. rewrite* state_union_neutral_l.
    inverts M4. subst*.
Qed.

Armaël Guéneau's avatar
Armaël Guéneau committed
849
(* Used by xgc_credit *)
850 851
Lemma credits_le_rest : forall (n m : int), (* todo: move later, inverse hyp *)
  n <= m -> exists H', affine H' /\ \$ m ==> \$ n \* H'.
charguer's avatar
new_gc  
charguer committed
852
Proof using.
853 854 855 856 857 858
  introv M. exists (\$ (m - n)). rewrite <- credits_split_eq.
  math_rewrite (n + (m-n) = m).
  splits~.
  Local Transparent affine. unfold affine, heap_is_credits.
  intros (? & ?) (? & ?); subst. apply heap_affine_credits.
  math.
charguer's avatar
credits  
charguer committed
859 860
Qed.

861 862
Lemma credits_join_eq : forall x y,
  \$ x \* \$ y = \$(x+y).
charguer's avatar
new_gc  
charguer committed
863
Proof using.
864 865 866 867 868 869 870 871 872 873 874 875 876 877
  introv. unfold heap_is_credits.
  applys pred_ext_1. intros h. splits.
  { intros ([m1 c1] & [m2 c2] & ([? ?] & [? ?] & [[? ?] ?])).
    subst. unfold heap_union. simpl.
    rewrite state_union_neutral_r. splits~. }
  { destruct h as [m c]. intros (? & ?). subst.
    unfold heap_is_star.
    exists (state_empty, x) (state_empty, y).
    splits~.
    { unfold heap_disjoint. simpl.
      splits~. apply state_disjoint_empty_l. }
    { unfold heap_union. simpl.
      rewrite~ state_union_neutral_r. } }
 Qed.
charguer's avatar
credits  
charguer committed
878

879 880
Lemma credits_join_eq_rest : forall x y (H:hprop),
  \$ x \* \$ y \* H = \$(x+y) \* H.
charguer's avatar
new_gc  
charguer committed
881
Proof using.
882
  introv. rewrite star_assoc. rewrite~ credits_join_eq.
charguer's avatar
credits  
charguer committed
883 884 885 886 887 888 889 890 891 892
Qed.

End Credits.


(*------------------------------------------------------------------*)
(* ** Tactics for credits *)

(** Tactic [credits_split] converts [\$(x+y) \* ...] into [\$x \* \$y \* ...] *)

893
Hint Rewrite credits_split_eq : credits_split_rew.
charguer's avatar
credits  
charguer committed
894 895 896 897 898 899 900 901

Ltac credits_split :=
  autorewrite with credits_split_rew.

(** Tactic [credits_join] converts [\$x \* ... \* \$y] into [\$(x+y) \* ...] *)

Lemma credits_swap : forall x (H:hprop),
  H \* (\$ x) = (\$ x) \* H.
charguer's avatar
charguer committed
902
Proof using. intros. rewrite~ star_comm. Qed.
charguer's avatar
credits  
charguer committed
903

charguer's avatar
charguer committed
904

charguer's avatar
credits  
charguer committed
905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924
Ltac credits_join_in H :=
  match H with
  | \$ ?x \* \$ ?y => rewrite (@credits_join_eq x y)
  | \$ ?x \* \$ ?y \* ?H' => rewrite (@credits_join_eq_rest x y H')
  | _ \* ?H' => credits_join_in H'
  end.

Ltac credits_join_left_step tt :=
  match goal with |- ?HL ==> ?HR => credits_join_in HL end.

Ltac credits_join_left_repeat tt :=
  repeat (credits_join_left_step tt).

Ltac credits_join_pre_step tt :=
  match goal with |- ?R ?H ?Q => credits_join_in H end.

Ltac credits_join_pre_repeat tt :=
  repeat (credits_join_pre_step tt).

Ltac credits_join_core :=
925
  match goal with
charguer's avatar
charguer committed
926
  | |- ?HL ==> ?HR => credits_join_left_repeat tt
927
  | |- _ => credits_join_pre_repeat tt
charguer's avatar
credits  
charguer committed
928 929 930 931 932
  end.

Tactic Notation "credits_join" :=
  credits_join_core.

charguer's avatar
charguer committed
933 934
(** Tactic [skip_credits] eliminates credits.
    Use this tactic only for development purposes *)
charguer's avatar
credits  
charguer committed
935

charguer's avatar
charguer committed
936
Axiom skip_credits : forall x, \$ x = \[]. (* only used by "skip_credits" tactic *)
charguer's avatar
credits  
charguer committed
937 938 939

Hint Rewrite skip_credits : rew_skip_credits.

940
Ltac skip_credits_core :=
charguer's avatar
credits  
charguer committed
941 942
  autorewrite with rew_skip_credits.

943
Tactic Notation "skip_credits" :=
charguer's avatar
credits  
charguer committed
944 945 946 947
  skip_credits_core.



charguer's avatar
init  
charguer committed
948 949 950 951 952
(********************************************************************)
  (* ** Specification predicates for values *)

(** Type of post-conditions on values of type B *)

953
Notation "'~~' B" := (hprop->(B->hprop)->Prop)
charguer's avatar
init  
charguer committed
954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970
  (at level 8, only parsing) : type_scope.

(** Type for imperative data structures *)

Definition htype A a := A -> a -> hprop.

(** Label for imperative data structures *)

Definition hdata (A:Type) (S:A->hprop) (x:A) : hprop :=
  S x.

Notation "'~>' S" := (hdata S)
  (at level 32, no associativity) : heap_scope. (* _advanced *)

Notation "x '~>' S" := (hdata S x)
  (at level 33, no associativity) : heap_scope.

971 972
Hint Transparent hdata : affine.

973
(** Specification of pure functions:
charguer's avatar
charguer committed
974
    [pure F P] is equivalent to [F [] (fun x => [P x])] *)
charguer's avatar
init  
charguer committed
975

976
Definition pure B (R:~~B) :=
charguer's avatar
charguer committed
977
  fun P => R \[] (fun r => \[P r]).
charguer's avatar
init  
charguer committed
978

979
(** Specification of functions that keep their input:
charguer's avatar
init  
charguer committed
980 981 982
    [keep F H Q] is equivalent to [F H (Q \*+ H)] *)

Notation "'keep' R H Q" :=
charguer's avatar
charguer committed
983
  (R H%h (Q \*+ H)) (at level 25, R at level 0, H at level 0, Q at level 0).
charguer's avatar
init  
charguer committed
984 985 986 987 988

(* Note: tactics need to be updated if a definition is used instead of notation
   Definition keep B (R:~~B) := fun H Q => R H (Q \*+ H). *)


charguer's avatar
charguer committed
989 990 991 992 993 994 995 996 997 998 999 1000 1001

(********************************************************************)
(* ** Special cases for hdata *)

(*------------------------------------------------------------------*)
(* ** Heapdata *)

(** [Heapdata G] captures the fact that the heap predicate [G]
    captures some real piece of the heap, hence if [x ~> G X]
    and [y ~> G Y] are in disjoint union then [x] and [y] must
    be different values *)

Class Heapdata a A (G:htype A a) := {
1002 1003
  heapdata : forall x y X Y,
    x ~> G X \* y ~> G Y ==>
charguer's avatar
charguer committed
1004 1005 1006 1007 1008 1009 1010 1011
    x ~> G X \* y ~> G Y \* \[x <> y] }.


(*------------------------------------------------------------------*)
(* ** Id *)

(** [x ~> Id X] holds when [x] is equal to [X] in the empty heap *)

1012
Definition Id {A:Type} (X:A) (x:A) :=
charguer's avatar
charguer committed
1013
  \[ X = x ].
1014

charguer's avatar
charguer committed
1015 1016 1017 1018 1019 1020 1021
(*------------------------------------------------------------------*)
(* ** Any *)

(** [x ~> Any tt] describes the fact that x points towards something
    whose value is not relevant. In other words, the model is unit.
    Note: [[True]] is used in place of [[]] to avoid confusing tactics. *)

1022
Definition Any {A:Type} (X:unit) (x:A) :=
charguer's avatar
charguer committed
1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033
  \[True].


(*------------------------------------------------------------------*)
(* ** Groups *)

Definition Group a A (G:htype A a) (M:map a A) :=
     fold sep_monoid (fun x X => x ~> G X) M
  \* \[LibMap.finite M].


1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084
(*------------------------------------------------------------------*)
(* ** Properties of [affine] *)

Section Affine.
Transparent affine.

Lemma affine_empty :
  affine \[].
Proof.
  unfold affine, heap_is_empty. intros; subst.
  apply heap_affine_empty.
Qed.

Lemma affine_star : forall H1 H2,
  affine H1 ->
  affine H2 ->
  affine (H1 \* H2).
Proof.
  Transparent heap_is_star.
  introv HA1 HA2. unfold affine, heap_is_star in *.
  intros h (? & ? & ? & ? & ? & ?). subst.
  apply~ heap_affine_union.
Qed.

Lemma affine_credits : forall c,
  0 <= c ->
  affine (\$ c).
Proof.
  Transparent heap_is_credits.
  introv N. unfold affine, heap_is_credits.
  intros (m & c'). intros (? & ?). subst.
  apply~ heap_affine_credits.
Qed.

Lemma affine_empty_st : forall P,
  affine \[P].
Proof.
  Transparent heap_is_empty_st.
  introv. unfold affine, heap_is_empty_st.
  introv (? & ?); subst.
  apply heap_affine_empty.
Qed.

Lemma affine_gc :
  affine \GC.
Proof.
  Transparent heap_is_gc.
  unfold affine, heap_is_gc.
  tauto.
Qed.

1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101
Lemma affine_single : forall l f A (v:A),
  affine (heap_is_single l f v).
Proof.
  Transparent heap_is_single.
  intros. unfold affine, heap_is_single.
  intros (m & c). intros (? & ? & ?). subst.
  apply heap_affine_single.
Qed.

Lemma affine_pack : forall A (J : A -> hprop),
  (forall x, affine (J x)) ->
  affine (heap_is_pack J).
Proof.
  Transparent heap_is_pack.
  intros. unfold affine, heap_is_pack in *.
  intros h [x HJx]. eauto.
Qed.
1102 1103 1104 1105 1106

End Affine.

Hint Resolve
     affine_empty affine_star affine_credits affine_empty_st
1107
     affine_gc affine_single affine_pack
1108 1109
: affine.

1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124
(* Split a [affine _] goal, following the base operators of the logic *)
Ltac affine_base :=
  repeat
    match goal with
    | |- affine (_ \* _) => apply affine_star
    | |- affine \[] => apply affine_empty
    | |- affine (\$ _) => apply affine_credits; auto with zarith
    | |- affine (\[_]) => apply affine_empty_st
    | |- affine \GC => apply affine_gc
    | |- affine (heap_is_pack _) => apply affine_pack
    end.

(* After using the rules for the standard operators of the logic with
[affine_base], try proving the remaining subgoals using the [affine] hint base.
*)
1125
Ltac affine :=
1126
  match goal with
Armaël Guéneau's avatar
Armaël Guéneau committed
1127
  | |- affine _ => affine_base; try (typeclasses eauto with affine)
1128
  end.
1129 1130


charguer's avatar
init  
charguer committed
1131
(********************************************************************)
charguer's avatar
charguer committed
1132 1133 1134
(* ** [xunfold] tactics *)

Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) :=
charguer's avatar
charguer committed
1135
  match number_to_nat K with
charguer's avatar
charguer committed
1136 1137 1138 1139 1140 1141 1142 1143 1144
  | 1%nat => set (X := E) at 1
  | 2%nat => set (X := E) at 2
  | 3%nat => set (X := E) at 3
  | 4%nat => set (X := E) at 4
  | 5%nat => set (X := E) at 5
  | 6%nat => set (X := E) at 6
  | 7%nat => set (X := E) at 7
  | 8%nat => set (X := E) at 8
  | 9%nat => set (X := E) at 9
1145
  | 10%nat => set (X := E) at 10
charguer's avatar
charguer committed
1146 1147 1148 1149
  | 11%nat => set (X := E) at 11
  | 12%nat => set (X := E) at 12
  | 13%nat => set (X := E) at 13
  | _ => fail "ltac_set: arity not supported"
charguer's avatar
init  
charguer committed
1150 1151
  end.

charguer's avatar
charguer committed
1152 1153 1154 1155 1156
(** [xunfold at n] unfold the definition of the arrow [~>]
    at the occurence [n] in the goal. *)

Definition hdata' (A:Type) (S:A->hprop) (x:A) : hprop := S x.

1157
Tactic Notation "xunfold" "at" constr(n) :=
charguer's avatar
charguer committed
1158
  let h := fresh "temp" in
1159
  ltac_set (h := hdata) at n;
charguer's avatar
charguer committed
1160 1161 1162 1163 1164 1165
  change h with hdata';
  unfold hdata';
  clear h.

(** [xunfold_clean] simplifies instances of
   [p ~> (fun _ => _)] by unfolding the arrow,
1166 1167
   but only when the body does not captures
   locally-bound variables.
charguer's avatar
charguer committed
1168 1169
   TODO: deprecated *)

1170
Tactic Notation "xunfold_clean" :=
charguer's avatar
charguer committed
1171
  try match goal with |- context C [?p ~> ?E] =>
1172
   match E with (fun _ => _) =>
charguer's avatar
charguer committed
1173
     let E' := eval cbv beta in (E p) in
1174
     let G' := context C [E'] in
charguer's avatar
charguer committed
1175
     let G := match goal with |- ?G => G end in
1176
     change G with G' end end.
charguer's avatar
charguer committed
1177 1178


1179
(** [xunfold E] unfolds all occurences of the representation
charguer's avatar
charguer committed
1180
    predicate [E].
charguer's avatar
charguer committed
1181
    Limitation: won't work if E has more than 12 arguments.
charguer's avatar
charguer committed
1182 1183 1184 1185 1186

    Implementation: converts all occurences of hdata to hdata',
    then unfolds these occurences one by one, and considers
    them for unfolding. *)

1187
Tactic Notation "xunfold" constr(E) :=
charguer's avatar
charguer committed
1188 1189 1190 1191 1192
  change hdata with hdata';
  let h := fresh "temp" in
  set (h := hdata');
  repeat (
    unfold h at 1;
1193
    let ok := match goal with
charguer's avatar
charguer committed
1194 1195 1196 1197 1198 1199 1200 1201
      | |- context [ hdata' (E) _ ] => constr:(true)
      | |- context [ hdata' (E _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _ _ _ _) _ ] => constr:(true)
charguer's avatar
charguer committed
1202 1203 1204