LambdaSepRO.v 61.7 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8
(**

This file formalizes "Separation Logic with Temporary
Read-Only Permissions", as described in the ESOP'17
paper by Arthur Charguéraud and François Pottier.

This file contains:
- a definition of heaps as pairs of states,
charguer's avatar
charguer committed
9
- an instantiation of the functor from the file SepFunctor.v,
charguer's avatar
charguer committed
10 11 12 13 14 15 16 17 18
- a definition of triples,
- statement and proofs of SL reasoning rules.

Author: Arthur Charguéraud.
License: MIT.

*)

Set Implicit Arguments.
charguer's avatar
charguer committed
19
From Sep Require Export LambdaSemantics SepTactics.
charguer's avatar
charguer committed
20
Open Scope fmap_scope.
charguer's avatar
charguer committed
21
Arguments exist [A] [P].
charguer's avatar
charguer committed
22 23


charguer's avatar
charguer committed
24
(* -- TODO: move to TLC LibTactics *)
charguer's avatar
charguer committed
25 26 27
Ltac fequal_base ::=
  let go := f_equal_fixed; [ fequal_base | ] in
  match goal with
charguer's avatar
charguer committed
28
  | |- exist _ _ = exist _ _ => apply exist_eq_exist
charguer's avatar
charguer committed
29 30 31 32 33 34 35 36
  | |- (_,_,_) = (_,_,_) => go
  | |- (_,_,_,_) = (_,_,_,_) => go
  | |- (_,_,_,_,_) = (_,_,_,_,_) => go
  | |- (_,_,_,_,_,_) = (_,_,_,_,_,_) => go
  | |- _ => f_equal_fixed
  end.


charguer's avatar
charguer committed
37 38


charguer's avatar
charguer committed
39
(* ********************************************************************** *)
charguer's avatar
charguer committed
40 41 42 43 44
(* * Construction of core of the logic *)

Module SepROCore.


charguer's avatar
charguer committed
45
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
46 47
(* ** Types *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
48 49
Definition heap : Type :=
  { h : (state*state)%type | let '(f,r) := h in fmap_disjoint f r }.
charguer's avatar
charguer committed
50 51 52 53

Definition hprop := heap -> Prop.


charguer's avatar
charguer committed
54
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
55 56 57 58 59
(* ** Operations on heaps *)

(** Empty heap *)

Program Definition heap_empty : heap :=
charguer's avatar
charguer committed
60
  (fmap_empty, fmap_empty).
charguer's avatar
charguer committed
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80

(** Projections *)

Definition heap_f (h:heap) : state :=
  match h with exist (f,r) _ => f end.

Definition heap_r (h:heap) : state :=
  match h with exist (f,r) _ => r end.

Notation "h '^f'" := (heap_f h)
   (at level 9, format "h '^f'") : heap_scope.

Notation "h '^r'" := (heap_r h)
   (at level 9, format "h '^r'") : heap_scope.

Open Scope heap_scope.

(** Starable heaps: disjoint owned heaps, agreeible read-only heaps *)

Definition heap_compat (h1 h2 : heap) : Prop :=
charguer's avatar
charguer committed
81
    fmap_agree h1^r h2^r
charguer's avatar
charguer committed
82 83 84
 /\ (\# (h1^f) (h2^f) (h1^r \+ h2^r)).

(** Union of heaps.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
85
    The operation [h1 \u h2] is partial. When the arguments are
charguer's avatar
charguer committed
86 87 88 89 90
    not compatible, it returns an unspecified result.
    We implement it using a classical logic test, so as to avoid
    dependently-typed programming. *)

Global Instance heap_inhab : Inhab heap.
charguer's avatar
charguer committed
91
Proof using. applys Inhab_of_val heap_empty. Qed.
charguer's avatar
charguer committed
92 93 94 95

Program Definition heap_union (h1 h2 : heap) : heap :=
  If (heap_compat h1 h2) then (h1^f \+ h2^f, h1^r \+ h2^r) else arbitrary.
Next Obligation.
charguer's avatar
charguer committed
96
  destruct H. fmap_disjoint.
charguer's avatar
charguer committed
97 98 99
Qed.

Notation "h1 \u h2" := (heap_union h1 h2)
charguer's avatar
charguer committed
100
   (at level 37, right associativity) : heap_scope.
charguer's avatar
charguer committed
101 102 103 104 105 106 107

(** State of heap *)

Coercion heap_state (h : heap) : state :=
  (h^f \+ h^r).


charguer's avatar
charguer committed
108
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
109 110
(* ** Operators *)

charguer's avatar
charguer committed
111
Definition hempty : hprop :=
112
  fun h => h = heap_empty.
charguer's avatar
charguer committed
113

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114 115
Program Definition hstar (H1 H2 : hprop) : hprop :=
  fun h => exists h1 h2,
charguer's avatar
charguer committed
116
               H1 h1
charguer's avatar
charguer committed
117
            /\ H2 h2
charguer's avatar
charguer committed
118
            /\ heap_compat h1 h2
charguer's avatar
charguer committed
119 120
            /\ h = h1 \u h2.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
121
Definition hexists A (J : A -> hprop) : hprop :=
charguer's avatar
charguer committed
122 123
  fun h => exists x, J x h.

charguer's avatar
charguer committed
124 125 126
Definition hforall A (J : A -> hprop) : hprop :=
  fun h => forall x, J x h.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
127
Definition htop :=
charguer's avatar
charguer committed
128
  hexists (fun (H:hprop) => H).
charguer's avatar
charguer committed
129 130


charguer's avatar
charguer committed
131
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
132 133
(* ** Notation *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
134
Notation "\[]" := (hempty)
charguer's avatar
charguer committed
135
  (at level 0) : heap_scope.
charguer's avatar
charguer committed
136
Notation "H1 '\*' H2" := (hstar H1 H2)
charguer's avatar
charguer committed
137
  (at level 41, right associativity) : heap_scope.
charguer's avatar
charguer committed
138 139
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
  (at level 40) : heap_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
140
Notation "\Top" := (htop) : heap_scope.
charguer's avatar
charguer committed
141 142 143
Open Scope heap_scope.


charguer's avatar
charguer committed
144
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
145 146
(* ** Tactic for automation *)

charguer's avatar
charguer committed
147
(* Hint Extern 1 (_ = _ :> heap) => fmap_eq. LATER *)
charguer's avatar
charguer committed
148

charguer's avatar
charguer committed
149
Tactic Notation "fmap_disjoint_pre" :=
charguer's avatar
charguer committed
150 151
  subst; rew_disjoint; jauto_set.

charguer's avatar
charguer committed
152 153
Hint Extern 1 (\# _ _) => fmap_disjoint_pre.
Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre.
charguer's avatar
charguer committed
154

charguer's avatar
charguer committed
155
Hint Resolve fmap_agree_sym.
charguer's avatar
charguer committed
156 157


charguer's avatar
charguer committed
158
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
159 160
(* ** Equalities on [heap] *)

charguer's avatar
charguer committed
161
Lemma heap_fmap_def : forall h,
charguer's avatar
charguer committed
162 163 164
  heap_state h = (h^f \+ h^r).
Proof using. auto. Qed.

charguer's avatar
charguer committed
165
Hint Rewrite heap_fmap_def : rew_disjoint.
charguer's avatar
charguer committed
166 167 168 169 170 171

Lemma heap_disjoint_components : forall h,
  \# (h^f) (h^r).
Proof using. intros ((f,r)&D). simple~. Qed.

Lemma heap_make : forall f r,
charguer's avatar
charguer committed
172
  fmap_disjoint f r -> exists (h:heap), h^f = f /\ h^r = r.
charguer's avatar
charguer committed
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
Proof using. introv M. exists~ ((exist (f,r) M : heap)). Qed.

Lemma heap_eq : forall h1 h2,
  (h1^f = h2^f /\ h1^r = h2^r) -> h1 = h2.
Proof using.
  intros ((f1,r1)&D1) ((f2,r2)&D2) (M1&M2). simpls. subst. fequals.
Qed.

Lemma heap_eq_forward : forall h1 h2,
  h1 = h2 ->
  h1^f = h2^f /\ h1^r = h2^r.
Proof using. intros ((f1&r1)&D1) ((f2&r2)&D2) M. inverts~ M. Qed.

Ltac unstate := unfold heap_state; simpl.


charguer's avatar
charguer committed
189
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
190 191 192
(* ** Auxiliary function [heap_ro] *)

(** [heap_ro h] defines the read-only heap associated with [h],
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
193
    i.e. covering the same memory cells, but with all tagged
charguer's avatar
charguer committed
194 195 196
    as read-only. *)

Program Definition heap_ro h : heap :=
charguer's avatar
charguer committed
197
  (fmap_empty, h^f \+ h^r).
charguer's avatar
charguer committed
198 199

Lemma heap_ro_f : forall h,
charguer's avatar
charguer committed
200
  (heap_ro h)^f = fmap_empty.
charguer's avatar
charguer committed
201 202 203 204 205 206
Proof using. auto. Qed.

Lemma heap_ro_r : forall h,
  (heap_ro h)^r = h^f \+ h^r.
Proof using. auto. Qed.

charguer's avatar
charguer committed
207 208 209
Lemma heap_ro_state : forall h,
  heap_state (heap_ro h) = heap_state h.
Proof using.
charguer's avatar
charguer committed
210 211
  intros h. do 2 rewrite heap_fmap_def. rewrite heap_ro_f, heap_ro_r.
  fmap_eq.
charguer's avatar
charguer committed
212 213
Qed.

charguer's avatar
charguer committed
214

charguer's avatar
charguer committed
215
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
216 217 218 219 220 221 222
(* ** Properties of [heap_union] *)

Lemma heap_union_def : forall h1 h2,
  heap_compat h1 h2 -> exists D,
  h1 \u h2 = exist (h1^f \+ h2^f, h1^r \+ h2^r) D.
Proof using.
  introv M. unfold heap_union.
charguer's avatar
charguer committed
223
  rewrite (classicT_l M). esplit. destruct~ M.
charguer's avatar
charguer committed
224 225 226
Qed.

Lemma heap_union_spec : forall h1 h2,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
227 228
  heap_compat h1 h2 ->
     (h1 \u h2)^f = h1^f \+ h2^f
charguer's avatar
charguer committed
229 230 231 232 233 234 235 236 237
  /\ (h1 \u h2)^r = h1^r \+ h2^r.
Proof using.
  introv M. lets (D&E): heap_union_def M. rewrite~ E.
Qed.

Lemma heap_union_f : forall h1 h2,
  heap_compat h1 h2 ->
  (h1 \u h2)^f = h1^f \+ h2^f.
Proof using.
charguer's avatar
charguer committed
238
  introv D. unfold heap_union. rewrite (classicT_l D).
charguer's avatar
charguer committed
239
  destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2).
charguer's avatar
charguer committed
240
  unstate. fmap_eq.
charguer's avatar
charguer committed
241 242 243 244 245 246
Qed.

Lemma heap_union_r : forall h1 h2,
  heap_compat h1 h2 ->
  (h1 \u h2)^r = h1^r \+ h2^r.
Proof using.
charguer's avatar
charguer committed
247
  introv D. unfold heap_union. rewrite (classicT_l D).
charguer's avatar
charguer committed
248
  destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2).
charguer's avatar
charguer committed
249
  unstate. fmap_eq.
charguer's avatar
charguer committed
250 251 252
Qed.


charguer's avatar
charguer committed
253
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
254 255 256
(* ** Properties of [heap_compat] *)

Lemma heap_compat_def : forall h1 h2,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
257
    heap_compat h1 h2
charguer's avatar
charguer committed
258
  =   ( (fmap_agree h1^r h2^r)
charguer's avatar
charguer committed
259 260 261 262 263 264
    /\ (\# (h1^f) (h2^f) (h1^r \+ h2^r))).
Proof using. auto. Qed.

Hint Rewrite heap_compat_def : rew_disjoint.

Lemma heap_compat_sym : forall h1 h2,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
265
  heap_compat h1 h2 ->
charguer's avatar
charguer committed
266 267 268 269 270 271 272 273 274
  heap_compat h2 h1.
Proof using. introv (M1&M2). split~. Qed.

Hint Resolve heap_compat_sym.

Lemma heap_compat_empty_l : forall h,
  heap_compat heap_empty h.
Proof using.
  intros. lets: heap_disjoint_components h.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
275
  unfold heap_empty. split; simpl.
charguer's avatar
charguer committed
276
  { apply fmap_agree_empty_l. }
charguer's avatar
charguer committed
277
  { fmap_disjoint. }
charguer's avatar
charguer committed
278 279 280 281 282 283 284 285 286 287 288
Qed.

Lemma heap_compat_empty_r : forall h,
  heap_compat h heap_empty.
Proof using.
  hint heap_compat_sym, heap_compat_empty_l. auto.
Qed.

Lemma heap_compat_union_l : forall h1 h2 h3,
  heap_compat h1 h2 ->
  heap_compat h1 h3 ->
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
289
  heap_compat h2 h3 ->
charguer's avatar
charguer committed
290 291 292 293 294
  heap_compat (h1 \u h2) h3.
Proof using.
  Hint Unfold heap_compat.
  intros ((f1&r1)&S1) ((f2&r2)&S2) ((f3&r3)&S3).
  intros (C1&D1) (C2&D2) (C3&D3). split; simpls.
charguer's avatar
charguer committed
295
  { rewrite heap_union_r; [|auto]. simpl. applys~ fmap_agree_union_l. }
charguer's avatar
charguer committed
296
  { rewrite heap_union_r; [|auto]. rewrite heap_union_f; [|auto].
charguer's avatar
charguer committed
297
    simpl. fmap_disjoint. }
charguer's avatar
charguer committed
298 299 300 301 302
Qed.

Lemma heap_compat_union_r : forall h1 h2 h3,
  heap_compat h1 h2 ->
  heap_compat h1 h3 ->
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
303
  heap_compat h2 h3 ->
charguer's avatar
charguer committed
304 305 306 307
  heap_compat h1 (h2 \u h3).
Proof using. hint heap_compat_sym, heap_compat_union_l. autos*. Qed.

Lemma heap_compat_refl_if_ro : forall h,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
308
  h^f = fmap_empty ->
charguer's avatar
charguer committed
309 310
  heap_compat h h.
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
311
  introv M. split.
charguer's avatar
charguer committed
312 313
  { apply fmap_agree_refl. }
  { rewrite M. fmap_disjoint. }
charguer's avatar
charguer committed
314 315 316 317 318 319 320
Qed.

Lemma heap_compat_ro_l : forall h1 h2,
  heap_compat h1 h2 ->
  heap_compat (heap_ro h1) h2.
Proof using.
  introv (N1&N2). split; simpl.
charguer's avatar
charguer committed
321
  { applys~ fmap_agree_union_l. applys~ fmap_agree_of_disjoint. }
charguer's avatar
charguer committed
322
  { fmap_disjoint. }
charguer's avatar
charguer committed
323 324 325 326 327 328 329 330 331 332 333 334
Qed.

Lemma heap_compat_ro_r : forall h1 h2,
  heap_compat h1 h2 ->
  heap_compat h1 (heap_ro h2).
Proof using.
  hint heap_compat_ro_l, heap_compat_sym. autos*.
Qed.

Lemma heap_compat_ro : forall h1 h2,
  heap_compat h1 h2 ->
  heap_compat (heap_ro h1) (heap_ro h2).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
335 336
Proof using.
  introv (M1&M2). split.
charguer's avatar
charguer committed
337
  { do 2 rewrite heap_ro_r.
charguer's avatar
charguer committed
338 339
    applys~ fmap_agree_union_lr. }
  { do 2 rewrite heap_ro_f. fmap_disjoint. }
charguer's avatar
charguer committed
340 341 342
Qed.


charguer's avatar
charguer committed
343
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
344 345
(* ** Properties of [heap_empty] *)

charguer's avatar
charguer committed
346 347
Lemma heap_empty_state : heap_state heap_empty = fmap_empty.
Proof. unfold heap_empty. unstate. fmap_eq. Qed.
charguer's avatar
charguer committed
348 349 350 351

Hint Rewrite heap_empty_state : rew_heap.


charguer's avatar
charguer committed
352
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
353 354 355 356 357 358
(* ** More properties of [heap_union] *)

Program Lemma heap_union_comm : forall h1 h2,
  (* heap_compat h1 h2 ->   Hypothesis not needed! *)
  h1 \u h2 = h2 \u h1.
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
359
  intros. hint heap_compat_sym. unfold heap_union.
charguer's avatar
charguer committed
360 361 362
  tests E: (heap_compat h1 h2); tests E': (heap_compat h2 h1);
   try auto_false.
  fequals. fequals.
charguer's avatar
charguer committed
363 364
  { applys fmap_union_comm_of_disjoint. { destruct E. fmap_disjoint. } }
  { applys fmap_union_comm_of_agree. { destruct~ E. } }
charguer's avatar
charguer committed
365 366 367
Qed.

Lemma heap_union_assoc : forall h1 h2 h3,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
368
  heap_compat h1 h2 ->
charguer's avatar
charguer committed
369 370 371
  heap_compat h2 h3 ->
  heap_compat h1 h3 ->
  (h1 \u h2) \u h3 = h1 \u (h2 \u h3).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
372 373
Proof using.
  introv M1 M2 M3. applys heap_eq.
charguer's avatar
charguer committed
374 375 376 377 378 379 380 381 382
  forwards~ (E1&E2): heap_union_spec (h1 \u h2) h3.
  { applys~ heap_compat_union_l. }
  rewrites (rm E1). rewrites (rm E2).
  forwards~ (E1&E2): heap_union_spec h1 h2.
  rewrites (rm E1). rewrites (rm E2).
  forwards~ (E1&E2): heap_union_spec h1 (h2 \u h3).
  { applys~ heap_compat_union_r. }
  rewrites (rm E1). rewrites (rm E2).
  rewrite~ heap_union_f. rewrite~ heap_union_r.
charguer's avatar
charguer committed
383
  split; fmap_eq.
charguer's avatar
charguer committed
384 385 386 387 388 389 390 391
Qed.

Hint Resolve heap_union_comm.

Lemma heap_union_empty_l : forall h,
  heap_empty \u h = h.
Proof using.
  intros h. unfold heap_union.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
392 393
  rewrite (classicT_l (heap_compat_empty_l h)).
  destruct h as ((f,r)&D). simpl.
charguer's avatar
charguer committed
394
  fequals_rec; fmap_eq.
charguer's avatar
charguer committed
395 396 397 398
Qed.

Lemma heap_union_empty_r : forall h,
  h \u heap_empty = h.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
399
Proof using.
charguer's avatar
charguer committed
400 401 402 403 404 405 406
  intros. rewrite heap_union_comm. apply heap_union_empty_l.
Qed.

Lemma heap_union_state : forall h1 h2,
  heap_compat h1 h2 ->
  heap_state (h1 \u h2) = heap_state h1 \+ heap_state h2.
Proof using.
charguer's avatar
charguer committed
407
  introv D. unfold heap_union. rewrite (classicT_l D).
charguer's avatar
charguer committed
408
  destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2).
charguer's avatar
charguer committed
409
  unstate. fmap_eq.
charguer's avatar
charguer committed
410 411
Qed.

charguer's avatar
charguer committed
412
Hint Rewrite heap_union_state : rew_fmap.
charguer's avatar
charguer committed
413

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
414
Hint Rewrite heap_union_empty_l heap_union_empty_r
charguer's avatar
charguer committed
415
  heap_ro_f heap_ro_r heap_union_f heap_union_r : rew_heap.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
416
  (* add heap_union_assoc? *)
charguer's avatar
charguer committed
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434

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

Ltac heap_eq :=
  solve [ rew_heap; subst; auto ].


charguer's avatar
charguer committed
435
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
436 437 438 439 440 441 442 443 444 445
(* ** More properties of [heap_compat] *)

Lemma heap_compat_union_l_inv_l : forall h1 h2 h3,
  heap_compat (h1 \u h2) h3 ->
  heap_compat h1 h2 ->
  heap_compat h2 h3.
Proof using.
  introv M2 M1. lets (C1&D1): M1. lets (C2&D2): M2.
  rew_heap~ in C2.
  rew_heap~ in D2.
charguer's avatar
charguer committed
446
  forwards~ (N1&N2): fmap_agree_union_l_inv C2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
447
Qed.
charguer's avatar
charguer committed
448 449 450 451 452 453 454 455

Lemma heap_compat_union_l_inv_r : forall h1 h2 h3,
  heap_compat (h1 \u h2) h3 ->
  heap_compat h1 h2 ->
  heap_compat h1 h3.
Proof using.
  introv M1 M2. rewrite heap_union_comm in M1.
  applys* heap_compat_union_l_inv_l.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
456
Qed.
charguer's avatar
charguer committed
457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476

Lemma heap_compat_union_l_inv : forall h1 h2 h3,
  heap_compat (h1 \u h2) h3 ->
  heap_compat h1 h2 ->
  heap_compat h1 h3 /\ heap_compat h2 h3.
Proof using.
  hint heap_compat_union_l_inv_l, heap_compat_union_l_inv_r. autos*.
Qed.

Lemma heap_compat_union_r_inv : forall h1 h2 h3,
  heap_compat h1 (h2 \u h3) ->
  heap_compat h2 h3 ->
  heap_compat h1 h2 /\ heap_compat h1 h3.
Proof using.
  introv M1 M2. rewrite heap_union_comm in M1.
  lets M1': heap_compat_sym M1.
  forwards~ (N1&N2): heap_compat_union_l_inv M1'.
Qed.


charguer's avatar
charguer committed
477
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
478
(* ** Properties of empty *)
charguer's avatar
charguer committed
479

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
480
Lemma hempty_intro :
charguer's avatar
charguer committed
481 482 483
  \[] heap_empty.
Proof using. hnfs~. Qed.

charguer's avatar
charguer committed
484
Lemma hempty_inv : forall h,
charguer's avatar
charguer committed
485 486
  \[] h ->
  h = heap_empty.
487
Proof using. introv M. auto. Qed.
charguer's avatar
charguer committed
488 489


charguer's avatar
charguer committed
490
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
491 492 493 494
(* ** Properties of star *)

Section Properties.

charguer's avatar
charguer committed
495
Hint Resolve hempty_intro
charguer's avatar
charguer committed
496 497 498
  heap_compat_empty_l heap_compat_empty_r
  heap_union_empty_l heap_union_empty_r.

charguer's avatar
charguer committed
499
Lemma hstar_hempty_l : forall H,
charguer's avatar
charguer committed
500
  hempty \* H = H.
charguer's avatar
charguer committed
501
Proof using.
charguer's avatar
charguer committed
502
  intros. applys hprop_extens. intros h.
charguer's avatar
charguer committed
503
  iff (h1&h2&M1&M2&D&U) M.
charguer's avatar
charguer committed
504
  { forwards E: hempty_inv M1. subst.
charguer's avatar
charguer committed
505
    rewrite~ heap_union_empty_l. }
charguer's avatar
charguer committed
506 507 508
  { exists~ heap_empty h. }
Qed.

charguer's avatar
charguer committed
509
Lemma hstar_comm : forall H1 H2,
charguer's avatar
charguer committed
510
   H1 \* H2 = H2 \* H1.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
511
Proof using.
charguer's avatar
charguer committed
512
  intros. unfold hprop, hstar. extens. intros h.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
513
  hint fmap_agree_sym.
charguer's avatar
charguer committed
514
  iff (h1&h2&M1&M2&D&U).
charguer's avatar
charguer committed
515 516
  { exists h2 h1. subst. splits~. }
  { exists h2 h1. subst. splits~. }
charguer's avatar
charguer committed
517
Qed.
charguer's avatar
charguer committed
518

charguer's avatar
charguer committed
519
Lemma hstar_assoc : forall H1 H2 H3,
charguer's avatar
charguer committed
520
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
521
Proof using.
charguer's avatar
charguer committed
522
  intros. unfold hprop, hstar. extens. intros h. split.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
523
  { intros (h'&h3&(h1&h2&M2&P1&P2&E1)&M3&M1&E2). subst h'.
charguer's avatar
charguer committed
524 525 526 527
    lets~ (M1a&M1b): heap_compat_union_l_inv M1.
    exists h1 (h2 \u h3). splits.
    { auto. }
    { exists h2 h3. splits*. }
charguer's avatar
charguer committed
528
    { applys* heap_compat_union_r. }
charguer's avatar
charguer committed
529
    { subst. applys~ heap_union_assoc. } }
charguer's avatar
charguer committed
530
  { intros (h1&h'&P1&(h2&h3&M2&P2&P3&E1)&M1&E2). subst h'.
charguer's avatar
charguer committed
531 532 533 534
    lets~ (M1a&M1b): heap_compat_union_r_inv M1.
    exists (h1 \u h2) h3. splits.
    { exists h1 h2. splits*. }
    { auto. }
charguer's avatar
charguer committed
535
    { applys* heap_compat_union_l. }
charguer's avatar
charguer committed
536
    { subst. symmetry. applys~ heap_union_assoc. } }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
537
Qed.
charguer's avatar
charguer committed
538 539


charguer's avatar
charguer committed
540
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
541 542
(* ** Interaction of star with other operators *)

charguer's avatar
charguer committed
543 544
Lemma hstar_hexists : forall A (J:A->hprop) H,
  (hexists J) \* H = hexists (fun x => (J x) \* H).
charguer's avatar
charguer committed
545 546
Proof using.
  intros. applys hprop_extens. intros h. iff M.
charguer's avatar
charguer committed
547 548
  { destruct M as (h1&h2&(x&M1)&M2&D&U). exists~ x h1 h2. }
  { destruct M as (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. exists~ x. }
charguer's avatar
charguer committed
549 550
Qed.

551
Lemma hstar_hforall : forall H A (J:A->hprop),
charguer's avatar
charguer committed
552 553 554 555 556
  (hforall J) \* H ==> hforall (J \*+ H).
Proof using.
  intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
Qed.

charguer's avatar
charguer committed
557
Lemma himpl_frame_l : forall H2 H1 H1',
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
558
  H1 ==> H1' ->
charguer's avatar
charguer committed
559 560 561
  (H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

charguer's avatar
charguer committed
562 563
Lemma local_local_aux : forall (B:Type),
  let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
charguer's avatar
charguer committed
564 565 566 567 568
    ( forall h, H h -> exists H1 H2 Q1,
       (H1 \* H2) h
    /\ F H1 Q1
    /\ Q1 \*+ H2 ===> Q \*+ \Top) in
  (\Top \* \Top = \Top) ->
charguer's avatar
charguer committed
569
  forall F (H:hprop) (Q:B->hprop),
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
570
  local (local F) H Q ->
charguer's avatar
charguer committed
571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586
  local F H Q.
Proof using.
  intros B local R F H Q M. introv PH.
  lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
  lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
  lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
  exists H1' (H2' \* H2) Q1'. splits.
  { rewrite <- hstar_assoc. exists~ h1 h2. }
  { auto. }
  { intros x. lets R1: himpl_frame_l \Top ((rm Qle) x).
    lets R2: himpl_frame_l H2 ((rm Qle') x).
    rewrite <- R. repeat rewrite hstar_assoc in *.
    applys himpl_trans R1. applys himpl_trans R2.
    rewrite~ (@hstar_comm H2). }
Qed.

charguer's avatar
charguer committed
587 588 589 590 591
End Properties.

End SepROCore.


charguer's avatar
charguer committed
592
(* ********************************************************************** *)
charguer's avatar
charguer committed
593 594
(* * Properties of the logic *)

charguer's avatar
charguer committed
595
Module Export SepROTactics := SepLogicTactics SepROCore.
charguer's avatar
charguer committed
596 597


charguer's avatar
charguer committed
598
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
599 600
(* ** Singleton heap *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
601 602
Definition hsingle (l:loc) (v:val) : hprop :=
  fun h =>    h^f = fmap_single l v
charguer's avatar
charguer committed
603
           /\ h^r = fmap_empty
charguer's avatar
charguer committed
604
           /\ l <> null.
charguer's avatar
charguer committed
605

charguer's avatar
charguer committed
606
Notation "l '~~~>' v" := (hsingle l v)
charguer's avatar
charguer committed
607 608
  (at level 32, no associativity) : heap_scope.

charguer's avatar
charguer committed
609
Lemma hstar_hsingle_same_loc_disjoint : forall (l:loc) (v1 v2:val),
charguer's avatar
charguer committed
610
  (l ~~~> v1) \* (l ~~~> v2) ==> \[False].
charguer's avatar
charguer committed
611
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
612
  intros. unfold hsingle.
charguer's avatar
charguer committed
613
  intros h (((m1&n1)&D1)&((m2&n2)&D2)&(E1&X1)&(E2&X2)&D&E). false.
charguer's avatar
alloc  
charguer committed
614
  subst. simpls. subst. applys* fmap_disjoint_single_single_same_inv l v1 v2.
charguer's avatar
charguer committed
615 616
Qed.

charguer's avatar
charguer committed
617
Global Opaque hsingle.
charguer's avatar
charguer committed
618

charguer's avatar
charguer committed
619
(* ** Configure [hcancel] to make it aware of [hsingle] *)
charguer's avatar
charguer committed
620

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
621
Ltac hcancel_hook H :=
charguer's avatar
charguer committed
622
  match H with
charguer's avatar
charguer committed
623
  | hsingle _ _ => hcancel_try_same tt
charguer's avatar
charguer committed
624 625
  end.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
626
Global Opaque hsingle.
charguer's avatar
charguer committed
627 628 629



charguer's avatar
charguer committed
630
(* ********************************************************************** *)
charguer's avatar
charguer committed
631 632 633 634 635 636 637
(* * Auxiliary Definitions *)

Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.


charguer's avatar
charguer committed
638
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
639 640 641 642 643
(* ** Definitions of [duplicatable] *)

Definition duplicatable (H:hprop) : Prop :=
  H ==> H \* H.

charguer's avatar
charguer committed
644
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
645 646
(* ** Definitions and properties of [normal] *)

647 648
Class Normal (H:hprop) : Prop :=
  normal_emp h : H h -> h^r = fmap_empty.
649
Hint Mode Normal ! : typeclass_instances.
charguer's avatar
charguer committed
650

651
Notation Normal_post Q := (forall x, Normal (Q x)).
charguer's avatar
charguer committed
652

653 654
Instance Normal_hempty :
  Normal \[].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
655
Proof using.
charguer's avatar
charguer committed
656
  Transparent hempty hpure.
657
  introv M. unfolds hempty, hpure. subst. autos*.
charguer's avatar
charguer committed
658 659
Qed.

660 661
Instance Normal_hpure : forall P,
  Normal \[P].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
662
Proof using.
charguer's avatar
charguer committed
663
  Transparent hpure.
664
  introv (p&M). unfolds hempty. subst. auto.
charguer's avatar
charguer committed
665 666
Qed.

667 668
Lemma Normal_hempty' : (* simpler proof *)
  Normal \[].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
669
Proof using.
670
  intros. rewrite hempty_eq_hpure_true. applys~ Normal_hpure.
charguer's avatar
charguer committed
671 672
Qed.

673 674
Instance Normal_hsingle : forall l v,
  Normal (hsingle l v).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
675
Proof using.
charguer's avatar
charguer committed
676 677
  Transparent hsingle.
  introv M. unfolds hsingle. autos*.
charguer's avatar
charguer committed
678 679
Qed.

680 681 682 683
Instance Normal_hstar : forall H1 H2,
  Normal H1 ->
  Normal H2 ->
  Normal (H1 \* H2).
charguer's avatar
charguer committed
684
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
685
  introv N1 N2 (h1&h2&P1&P2&M1&EQ).
charguer's avatar
charguer committed
686 687 688
  lets (_&E): heap_eq_forward EQ. simpls. rewrite E.
  rewrite~ heap_union_r.
  rewrites (>> N1 P1). rewrites (>> N2 P2).
charguer's avatar
charguer committed
689
  rewrite~ fmap_union_empty_r.
charguer's avatar
charguer committed
690 691
Qed.

692 693 694
Instance Normal_hexists : forall A (J:A->hprop),
  Normal_post J ->
  Normal (hexists J).
charguer's avatar
charguer committed
695 696
Proof using. introv M (x&N). rewrites~ (>> M N). Qed.

697 698 699 700
Instance Normal_hor : forall H1 H2,
  Normal H1 ->
  Normal H2 ->
  Normal (hor H1 H2).
charguer's avatar
charguer committed
701 702 703 704 705 706
Proof using.
  introv M1 M2 [N|N].
  { rewrites~ (>> M1 N). }
  { rewrites~ (>> M2 N). }
Qed.

707 708 709
Instance Normal_hand_l : forall H1 H2,
  Normal H1 ->
  Normal (hand H1 H2).
charguer's avatar
charguer committed
710 711
Proof using. introv M (N1&N2). forwards*: M N1. Qed.

712 713 714
Instance Normal_hand_r : forall H1 H2,
  Normal H2 ->
  Normal (hand H1 H2).
charguer's avatar
charguer committed
715 716
Proof using. introv M (N1&N2). forwards*: M N2. Qed.

717 718
Lemma Normal_himpl : forall H1 H2,
  Normal H2 ->
charguer's avatar
charguer committed
719
  (H1 ==> H2) ->
720
  Normal H1.
charguer's avatar
charguer committed
721 722
Proof using. introv HS HI M. lets: HI M. applys* HS. Qed.

723
(* Note: Normal_hwand is not true *)
charguer's avatar
charguer committed
724

725 726 727
Lemma Normal_hpure_star_hprop : forall (P:Prop) H,
  (P -> Normal H) ->
  Normal (\[P] \* H).
charguer's avatar
charguer committed
728
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
729
  introv N (h1&h2&P1&P2&M1&EQ).
charguer's avatar
charguer committed
730 731 732 733 734 735
  lets (_&E): heap_eq_forward EQ. simpls. rewrite E.
  rewrite~ heap_union_r.
  lets (MP&ME): hpure_inv P1. rewrites (>> hempty_inv (rm ME)).
  rewrites~ (>> N P2). rew_fmap~.
Qed.

charguer's avatar
charguer committed
736
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
737 738 739
(* ** Definitions and properties of [ROl] *)

Definition RO (H:hprop) : hprop :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
740
  fun h => exists h', H h'
charguer's avatar
charguer committed
741
                   /\ h^f = fmap_empty
charguer's avatar
charguer committed
742 743 744
                   /\ h^r = h'^f \+ h'^r.

Lemma RO_duplicatable : forall H,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
745
  duplicatable (RO H).
charguer's avatar
charguer committed
746 747 748 749 750 751
Proof using.
  intros H h M. lets (h'&M1&M2&M3): M. subst.
  lets D: heap_compat_refl_if_ro M2.
  exists h h. splits~.
  { applys heap_eq. rewrite~ heap_union_f.
    rewrite~ heap_union_r. rewrite M2.
charguer's avatar
charguer committed
752
    split. fmap_eq. rewrite~ fmap_union_self. }
charguer's avatar
charguer committed
753 754 755 756 757 758 759 760 761 762
Qed.

Lemma RO_covariant : forall H1 H2,
  H1 ==> H2 ->
  (RO H1) ==> (RO H2).
Proof using.
  introv M. intros h (h'&M1&M2&M3). exists~ h'.
Qed.

Lemma RO_RO : forall H,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
763
  RO (RO H) = RO H.
charguer's avatar
charguer committed
764
Proof using.
charguer's avatar
charguer committed
765
  intros. apply pred_ext_1. intros h.
charguer's avatar
charguer committed
766 767
  iff (h'&(h''&M1'&M2'&M3')&M2&M3) (h'&M1&M2&M3).
  { exists h''. splits~.
charguer's avatar
charguer committed
768
    rewrite M3. rewrite M3'. rewrite M2'. fmap_eq. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
769 770
  { exists h. splits~.
    { exists h'. split~. }
charguer's avatar
charguer committed
771
    { rewrite M2. fmap_eq. } }
charguer's avatar
charguer committed
772 773
Qed.

charguer's avatar
charguer committed
774 775 776 777
Lemma RO_empty :
  RO \[] = \[].
Proof using.
  intros. apply pred_ext_1. intros h.
778 779 780
  unfold hempty. iff (h'&M1&M2&M3) M1.
  { rewrite M1 in M3. rew_fmap. apply heap_eq. auto. }
  { exists h. rewrite M1. splits~. rew_fmap~. }
charguer's avatar
charguer committed
781 782 783 784 785 786
Qed.

Lemma RO_pure : forall P,
  RO \[P] = \[P].
Proof using.
  intros. apply pred_ext_1. intros h.
787 788 789
  iff (h'&(M1p&M2)&M3&M4) (MP&M1); unfolds hempty.
  { rewrite M2 in M4. rew_fmap. split~. apply heap_eq. auto. }
  { exists h. rewrite M1. splits~. { split~. split~. } { rew_fmap~. } }
charguer's avatar
charguer committed
790 791 792 793 794 795 796 797
Qed.

Lemma RO_empty' : (* simpler proof *)
  RO \[] = \[].
Proof using.
  intros. rewrite hempty_eq_hpure_true. rewrite~ RO_pure.
Qed.

charguer's avatar
charguer committed
798
Lemma RO_hexists : forall A (J:A->hprop),
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
799
    RO (hexists J)
charguer's avatar
charguer committed
800 801
  = Hexists x, RO (J x).
Proof using.
charguer's avatar
charguer committed
802
  intros. apply pred_ext_1. intros h.
charguer's avatar
charguer committed
803 804 805 806 807 808
  iff (h'&(x&M1)&M2&M3) (x&(h'&M1&M2&M3)).
  { exists x. exists* h'. }
  { exists h'. splits~. { exists~ x. } }
Qed.

Lemma RO_or : forall H1 H2,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
809
     RO (hor H1 H2)
charguer's avatar
charguer committed
810
  ==> hor (RO H1) (RO H2).
charguer's avatar
charguer committed
811 812 813 814 815 816 817 818 819 820 821 822 823 824
Proof using.
  intros. intros h (h'&[M1|M1]&M2&M3).
  { left. exists h'. split~. }
  { right. exists h'. split~. }
Qed.

Lemma RO_star : forall H1 H2,
  RO (H1 \* H2) ==> (RO H1 \* RO H2).
Proof using.
  intros. intros h (h'&(h1&h2&N1&P1&P2&N2)&M2&M3).
  lets C: (@heap_compat_ro h1 h2).
  exists (heap_ro h1) (heap_ro h2). splits.
  { exists~ h1. }
  { exists~ h2. }
charguer's avatar
charguer committed
825
  { auto. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
826
  { applys heap_eq. rew_heap~. split.
charguer's avatar
charguer committed
827 828
    { rewrite M2. fmap_eq. }
    { rewrite M3,N2. rew_heap~. fmap_eq. } }
charguer's avatar
charguer committed
829 830 831
Qed.

Lemma heap_ro_pred : forall (H:hprop) h,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
832
  H h ->
charguer's avatar
charguer committed
833 834 835
  RO H (heap_ro h).
Proof using. introv N. exists h. split~. Qed.

charguer's avatar
charguer committed
836
Arguments RO_star : clear implicits.
charguer's avatar
charguer committed
837 838


charguer's avatar
charguer committed
839
(* ********************************************************************** *)
charguer's avatar
charguer committed
840 841
(* * Reasoning rules, low-level proofs *)

charguer's avatar
charguer committed
842

charguer's avatar
charguer committed
843
Hint Resolve heap_compat_union_l heap_compat_union_r.
charguer's avatar
charguer committed
844
Hint Resolve fmap_agree_empty_l fmap_agree_empty_r.
charguer's avatar
charguer committed
845 846


charguer's avatar
charguer committed
847
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
848 849 850
(* ** Definition and properties of [on_rw_sub] *)

Program Definition on_rw_sub H h :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
851 852
  exists h1 h2, heap_compat h1 h2
             /\ h = h1 \u h2
charguer's avatar
charguer committed
853
             /\ h1^r = fmap_empty
charguer's avatar
charguer committed
854 855 856
             /\ H h1.

Lemma on_rw_sub_base : forall H h,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
857
  H h ->
charguer's avatar
charguer committed
858
  h^r = fmap_empty ->
charguer's avatar
charguer committed
859 860 861 862 863 864 865
  on_rw_sub H h.
Proof using.
  intros H h M N. exists h heap_empty. splits~.
  { applys heap_compat_empty_r. }
  { heap_eq. }
Qed.

charguer's avatar
charguer committed
866 867
Lemma on_rw_sub_htop : forall H h,
  on_rw_sub (H \* \Top) h ->
charguer's avatar
charguer committed
868 869
  on_rw_sub H h.
Proof using.
charguer's avatar
charguer committed
870
  introv (h1&h2&N1&N2&N3&(h3&h4&M2&(H'&M3)&D&U)).
charguer's avatar
charguer committed
871
  subst h h1. rew_heap~ in N3.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
872
  lets~ (N1a&N1b): heap_compat_union_l_inv N1.
charguer's avatar
charguer committed
873 874
  exists h3 (h4 \u h2). splits~.
  { applys~ heap_union_assoc. }
charguer's avatar
charguer committed
875
  { forwards~: fmap_union_eq_empty_inv_l N3. }
charguer's avatar
charguer committed
876 877
Qed.

charguer's avatar
charguer committed
878 879
Lemma on_rw_sub_htop' : forall H h,
  (H \* \Top) h ->
880
  Normal H ->
charguer's avatar
charguer committed
881 882 883 884 885
  on_rw_sub H h.
Proof using.
  introv (h1&h2&N1&N2&N3&N4) N. exists h1 h2. splits~.
Qed.

charguer's avatar
charguer committed
886
Lemma on_rw_sub_htop_inv : forall H h,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
887
  on_rw_sub H h ->
charguer's avatar
charguer committed
888
  (H \* \Top) h.
charguer's avatar
charguer committed
889 890
Proof using.
  introv M. destruct M as (h1&h2&M1&M2&M3&M4). subst.
charguer's avatar
charguer committed
891
  exists h1 h2. splits~. exists~ (= h2).
charguer's avatar
charguer committed
892 893 894 895 896 897 898
Qed.

Lemma on_rw_sub_union_r : forall H h1 h2,
  on_rw_sub H h1 ->
  heap_compat h1 h2 ->
  on_rw_sub H (h1 \u h2).
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
899 900
  introv (h11&h12&N1&N2&N3&N4) C.
  subst h1. lets~ (N1a&N1b): heap_compat_union_l_inv C.
charguer's avatar
charguer committed
901 902 903 904 905 906 907 908 909 910 911 912 913
  exists h11 (h12 \u h2). splits~.
  { applys~ heap_union_assoc. }
Qed.

Lemma on_rw_sub_weaken : forall Q Q' v h,
  on_rw_sub (Q v) h ->
  Q ===> Q' ->
  on_rw_sub (Q' v) h.
Proof using.
  introv (h1&h2&N1&N2&N3&N4) HQ. lets N4': HQ N4. exists~ h1 h2.
Qed.


charguer's avatar
charguer committed
914
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
915 916
(* ** Definition of triples *)

charguer's avatar
charguer committed
917 918 919
Implicit Types v w : val.
Implicit Types t : trm.

charguer's avatar
charguer committed
920 921 922 923
(** Recall that the projection [heap_state : heap >-> state]
   is used as a Coercion, so that we can write [h] where the
   union of the underlying states is expected. *)

charguer's avatar
charguer committed
924
Definition triple (t:trm) (H:hprop) (Q:val->hprop) :=
charguer's avatar
charguer committed
925 926
  forall h1 h2, heap_compat h1 h2 -> H h1 ->
  exists h1' v,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
927
       heap_compat h1' h2
charguer's avatar
charguer committed
928
    /\ red (h1 \u h2) t (h1' \u h2) v
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
929
    /\ h1'^r = h1^r
charguer's avatar
charguer committed
930 931 932
    /\ on_rw_sub (Q v) h1'.


charguer's avatar
charguer committed
933
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
934 935
(* ** Structural rules *)

charguer's avatar
charguer committed
936
Lemma rule_extract_hexists : forall t A (J:A->hprop) Q,
charguer's avatar
charguer committed
937
  (forall x, triple t (J x) Q) ->
charguer's avatar
charguer committed
938
  triple t (hexists J) Q.
charguer's avatar
charguer committed
939 940
Proof using. introv M D (x&Jx). applys* M. Qed.

charguer's avatar
charguer committed
941
Lemma rule_extract_hprop : forall t (P:Prop) H Q,
charguer's avatar
charguer committed
942 943 944
  (P -> triple t H Q) ->
  triple t (\[P] \* H) Q.
Proof using.
charguer's avatar
charguer committed
945 946
  intros t. applys (rule_extract_hprop_from_extract_hexists (triple t)).
  applys rule_extract_hexists.
charguer's avatar
charguer committed
947 948 949 950 951
Qed.

Lemma rule_extract_or : forall t H1 H2 Q,
  triple t H1 Q ->
  triple t H2 Q ->
charguer's avatar
charguer committed
952
  triple t (hor H1 H2) Q.
charguer's avatar
charguer committed
953 954 955 956
Proof using.
  introv M1 M2 D [M|M]. applys* M1. applys* M2.
Qed.

charguer's avatar
charguer committed
957 958
Lemma rule_htop_post : forall t H Q,
  triple t H (Q \*+ \Top) ->
charguer's avatar
charguer committed
959 960
  triple t H Q.
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
961
  introv M D P1.
charguer's avatar
charguer committed
962
  forwards* (h1'&v&(N1&N2&N3&N4)): (rm M) h1.
charguer's avatar
charguer committed
963
  exists h1' v. splits~. applys~ on_rw_sub_htop.
charguer's avatar
charguer committed
964 965
Qed.

charguer's avatar
charguer committed
966
Lemma rule_htop_pre : forall t H Q,
charguer's avatar
charguer committed
967
  triple t H Q ->
charguer's avatar
charguer committed
968
  triple t (H \* \Top) Q.
charguer's avatar
charguer committed
969
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
970
  introv M. intros h1 h2 D (h11&h12&P11&P12&R1&R2). subst h1.
charguer's avatar
charguer committed
971 972 973 974
  lets~ (D1&D2): heap_compat_union_l_inv (rm D).
  forwards* (h1'&v&(N1&N2&N3&N4)): (rm M) (h12 \u h2) (rm P11).
  lets~ (D3&D4): heap_compat_union_r_inv (rm N1).
  exists (h1' \u h12) v. splits~.
charguer's avatar
charguer committed
975
  { fmap_red~. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
976
  { rew_heap~. rewrite N3. fmap_eq~. }
charguer's avatar
charguer committed
977 978 979 980 981 982 983 984
  { applys~ on_rw_sub_union_r. }
Qed.

Lemma rule_consequence : forall t H' Q' H Q,
  H ==> H' ->
  triple t H' Q' ->
  Q' ===> Q ->
  triple t H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
985 986 987
Proof using.
  introv MH M MQ. intros h1 h2 D P1.
  lets P1': (rm MH) (rm P1).
charguer's avatar
charguer committed
988 989 990 991 992 993 994 995
  forwards~ (h1'&v&(N1&N2&N3&N4)): (rm M) h2 (rm P1').
  exists h1' v. splits~.
  { applys~ on_rw_sub_weaken Q'. }
Qed.

Lemma rule_or_symmetric : forall t H1 H2 Q1 Q2,
  triple t H1 Q1 ->
  triple t H2 Q2 ->
charguer's avatar
charguer committed
996
  triple t (hor H1 H2) (fun x => hor (Q1 x) (Q2 x)).
charguer's avatar
charguer committed
997 998 999 1000 1001 1002 1003 1004
Proof using.
  introv M1 M2. apply~ rule_extract_or.
  applys~ rule_consequence. applys M1. { intros_all. hnfs*. }
  applys~ rule_consequence. applys M2. { intros_all. hnfs*. }
Qed.

Lemma rule_frame_read_only : forall t H1 Q1 H2,
  triple t (H1 \* RO H2) Q1 ->
1005
  Normal H2 ->
charguer's avatar
charguer committed
1006
  triple t (H1 \* H2) (Q1 \*+ H2).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1007 1008
Proof using.
  introv M N. intros h1 h2 D (h11&h12&P11&P12&R1&R2).
charguer's avatar
charguer committed
1009 1010 1011
  lets R1': heap_compat_ro_r R1.
  lets E12: (rm N) P12.
  subst h1. lets~ (D1&D2): heap_compat_union_l_inv (rm D).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1012
  asserts R12: (heap_state (heap_ro h12) = heap_state h12).
charguer's avatar
charguer committed
1013
  { unstate. rewrite E12. fmap_eq. }
charguer's avatar
charguer committed
1014
  asserts C: (heap_compat (h11 \u heap_ro h12) h2).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1015
  { apply~ heap_compat_union_l. applys~ heap_compat_ro_l. }
charguer's avatar
charguer committed
1016 1017 1018 1019
  forwards~ (h1'&v&(N1&N2&N3&N4)): (rm M) (h11 \u (heap_ro h12)) h2.
  { exists h11 (heap_ro h12). splits~.
    { applys~ heap_ro_pred. } }
  rew_heap~ in N3. rewrite E12 in N3.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1020
  lets G: heap_disjoint_components h1'.
charguer's avatar
charguer committed
1021
  forwards (h1''&F1&F2): heap_make (h1'^f \+ h12^f) (h11^r).
charguer's avatar
charguer committed
1022
  { rewrite N3 in G. fmap_disjoint. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1023 1024 1025
  asserts C': (heap_compat h1'' h2).
  { unfolds. rewrite F1,F2. split.
    { destruct~ D1. }
charguer's avatar
charguer committed
1026
    { lets G2: heap_disjoint_components h2. rewrite N3 in G.
charguer's avatar
charguer committed
1027
      fmap_disjoint. } }
charguer's avatar
charguer committed
1028 1029
  exists h1'' v. splits.
  { auto. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1030 1031
  { fmap_red~.
    { rewrite~ R12. }
charguer's avatar
charguer committed
1032 1033
    { fequals. unstate. rewrite F1,F2,N3. fmap_eq. } }
  { rew_heap~. rewrite F2,E12. fmap_eq~. }
charguer's avatar
charguer committed
1034 1035
  {  clears h2.
     rename h1'' into hd. rename H2 into Hb. sets Ha: (Q1 v).
charguer's avatar
charguer committed
1036
     rename h1' into ha.  rewrite~ fmap_union_empty_r in N3.