LambdaSep.v 35.8 KB
Newer Older
charguer's avatar
charguer committed
1
(**
charguer's avatar
charguer committed
2

charguer's avatar
charguer committed
3
This file formalizes standard Separation Logic. It contains:
charguer's avatar
charguer committed
4
- a definition of heaps as finite maps from location to values,
charguer's avatar
charguer committed
5 6
- an instantiation of the functor from the file [SepFunctor.v],
- an instantiation of the functor from the file [SepTactics.v],
charguer's avatar
charguer committed
7
- a definition of triples,
charguer's avatar
charguer committed
8 9 10 11
- statement and proofs of structural rules,
- statement and proofs of rules for terms,
- statement and proofs of rules for primitive operations,
- bonuses: an alternative definition of triples, and derived rules.
charguer's avatar
charguer committed
12 13 14 15 16 17 18

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 22 23

Ltac auto_star ::= jauto.

charguer's avatar
charguer committed
24
Implicit Types f : var.
charguer's avatar
charguer committed
25 26 27 28
Implicit Types v w : val.
Implicit Types t : trm.
Implicit Types n : int.
Implicit Types l : loc.
charguer's avatar
charguer committed
29
Implicit Types k : field.
charguer's avatar
charguer committed
30

charguer's avatar
charguer committed
31

charguer's avatar
charguer committed
32
(* ********************************************************************** *)
charguer's avatar
charguer committed
33
(* * Construction of the logic *)
charguer's avatar
charguer committed
34 35

Module SepBasicCore.
charguer's avatar
charguer committed
36

charguer's avatar
charguer committed
37 38 39
(** All the definitions from this section are explained in the
  [Module Type SepLogicCore], from file [SepFunctor.v]. *)

charguer's avatar
charguer committed
40

charguer's avatar
charguer committed
41
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
42
(* ** Types *)
charguer's avatar
charguer committed
43

charguer's avatar
charguer committed
44 45 46
(** A heap is a state (a finite map from location to values)
   as defined in [LambdaSemantics.v]. *)

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

charguer's avatar
charguer committed
49 50
(** A heap predicate, type [hprop] is a predicate over such heaps. *)

charguer's avatar
charguer committed
51 52
Definition hprop := heap -> Prop.

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

charguer's avatar
charguer committed
56

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

charguer's avatar
charguer committed
60 61
(** For uniformity with other instantiations of the Separation Logic
  functor, we introduce local names for operations and lemmas on heaps. *)
charguer's avatar
charguer committed
62

63
Definition heap_empty : heap := fmap_empty.
charguer's avatar
charguer committed
64

charguer's avatar
charguer committed
65
Notation "h1 \u h2" := (fmap_union h1 h2)
charguer's avatar
charguer committed
66
   (at level 37, right associativity) : heap_scope.
charguer's avatar
charguer committed
67

charguer's avatar
charguer committed
68
Definition heap_union_empty_l := fmap_union_empty_l.
charguer's avatar
charguer committed
69

charguer's avatar
charguer committed
70
Definition heap_union_empty_r := fmap_union_empty_r.
charguer's avatar
charguer committed
71

charguer's avatar
charguer committed
72
Definition heap_union_comm := fmap_union_comm_of_disjoint.
charguer's avatar
charguer committed
73

charguer's avatar
charguer committed
74 75
Open Scope heap_scope.

charguer's avatar
charguer committed
76

charguer's avatar
charguer committed
77
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
78
(* ** Operators *)
charguer's avatar
charguer committed
79

charguer's avatar
charguer committed
80
(** Empty heap predicate: [ \[] ] *)
charguer's avatar
charguer committed
81

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
82
Definition hempty : hprop :=
charguer's avatar
charguer committed
83
  fun h => h = heap_empty.
charguer's avatar
charguer committed
84

charguer's avatar
charguer committed
85
(** Separating conjunction: [H1 \* H2] *)
charguer's avatar
charguer committed
86

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
87 88 89
Definition hstar (H1 H2 : hprop) : hprop :=
  fun h => exists h1 h2, H1 h1
                      /\ H2 h2
charguer's avatar
charguer committed
90 91 92
                      /\ (\# h1 h2)
                      /\ h = h1 \+ h2.

charguer's avatar
charguer committed
93
(** Lifting of existentials: [Hexists x, H] *)
charguer's avatar
charguer committed
94

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

charguer's avatar
charguer committed
98 99 100 101 102
(** Lifting of univerals *)

Definition hforall A (J : A -> hprop) : hprop :=
  fun h => forall x, J x h.

charguer's avatar
charguer committed
103
(** The top heap predicate: [ \Top ], same as [Hexists H, H] *)
charguer's avatar
charguer committed
104

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
105
Definition htop :=
charguer's avatar
charguer committed
106
  hexists (fun (H:hprop) => H).
charguer's avatar
charguer committed
107 108


charguer's avatar
charguer committed
109
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
110
(* ** Notation *)
charguer's avatar
charguer committed
111

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
112
Notation "\[]" := (hempty)
charguer's avatar
charguer committed
113
  (at level 0) : heap_scope.
charguer's avatar
charguer committed
114

charguer's avatar
charguer committed
115
Notation "H1 '\*' H2" := (hstar H1 H2)
charguer's avatar
charguer committed
116
  (at level 41, right associativity) : heap_scope.
charguer's avatar
charguer committed
117

charguer's avatar
charguer committed
118 119
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
  (at level 40) : heap_scope.
charguer's avatar
charguer committed
120

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
121
Notation "\Top" := (htop) : heap_scope.
charguer's avatar
charguer committed
122

charguer's avatar
charguer committed
123 124 125
Open Scope heap_scope.


charguer's avatar
charguer committed
126
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
127
(* ** Tactic for automation *)
charguer's avatar
charguer committed
128 129 130

(* TODO: check how much is really useful *)

charguer's avatar
charguer committed
131
Hint Extern 1 (_ = _ :> heap) => fmap_eq.
charguer's avatar
charguer committed
132

charguer's avatar
charguer committed
133
Tactic Notation "fmap_disjoint_pre" :=
charguer's avatar
charguer committed
134 135
  subst; rew_disjoint; jauto_set.

charguer's avatar
charguer committed
136 137
Hint Extern 1 (\# _ _) => fmap_disjoint_pre.
Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre.
charguer's avatar
charguer committed
138

charguer's avatar
charguer committed
139

charguer's avatar
charguer committed
140
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
141
(* ** Properties of empty *)
charguer's avatar
charguer committed
142

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
143
Lemma hempty_intro :
charguer's avatar
charguer committed
144
  \[] heap_empty.
charguer's avatar
charguer committed
145 146
Proof using. hnfs~. Qed.

charguer's avatar
charguer committed
147
Lemma hempty_inv : forall h,
charguer's avatar
charguer committed
148 149 150
  \[] h ->
  h = heap_empty.
Proof using. auto. Qed.
charguer's avatar
charguer committed
151 152


charguer's avatar
charguer committed
153
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
154
(* ** Properties of star *)
charguer's avatar
charguer committed
155 156 157

Section Properties.

charguer's avatar
charguer committed
158
Hint Resolve hempty_intro.
charguer's avatar
charguer committed
159

charguer's avatar
array  
charguer committed
160 161 162 163 164 165 166
Lemma hstar_intro : forall H1 H2 h1 h2,
  H1 h1 ->
  H2 h2 ->
  \# h1 h2 ->
  (H1 \* H2) (h1 \+ h2).
Proof using. intros. exists~ h1 h2. Qed.

charguer's avatar
charguer committed
167
Lemma hstar_hempty_l : forall H,
charguer's avatar
charguer committed
168
  hempty \* H = H.
charguer's avatar
charguer committed
169 170
Proof using.
  intros. applys hprop_extens. intros h.
charguer's avatar
charguer committed
171
  iff (h1&h2&M1&M2&D&U) M.
charguer's avatar
charguer committed
172
  { forwards E: hempty_inv M1. subst.
charguer's avatar
charguer committed
173
    rewrite~ heap_union_empty_l. }
174
  { exists heap_empty h. unfold heap_empty. auto. }
charguer's avatar
charguer committed
175 176
Qed.

charguer's avatar
charguer committed
177
Lemma hstar_comm : forall H1 H2,
charguer's avatar
charguer committed
178
   H1 \* H2 = H2 \* H1.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
179
Proof using.
charguer's avatar
charguer committed
180
  intros H1 H2. unfold hprop, hstar. extens. intros h.
charguer's avatar
charguer committed
181
  iff (h1&h2&M1&M2&D&U); rewrite~ heap_union_comm in U; exists* h2 h1.
charguer's avatar
charguer committed
182 183
Qed.

charguer's avatar
charguer committed
184
Lemma hstar_assoc : forall H1 H2 H3,
charguer's avatar
charguer committed
185
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
186
Proof using.
charguer's avatar
charguer committed
187 188 189 190 191
  intros H1 H2 H3. applys hprop_extens. intros h. split.
  { intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
    exists h1 (h2 \+ h3). splits~. { exists* h2 h3. } }
  { intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
    exists (h1 \+ h2) h3. splits~. { exists* h1 h2. } }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
192
Qed.
charguer's avatar
charguer committed
193 194


charguer's avatar
charguer committed
195
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
196
(* ** Interaction of star with other operators *)
charguer's avatar
charguer committed
197

charguer's avatar
charguer committed
198 199
Lemma hstar_hexists : forall A (J:A->hprop) H,
  (hexists J) \* H = hexists (fun x => (J x) \* H).
charguer's avatar
charguer committed
200 201 202 203 204 205
Proof using.
  intros. applys hprop_extens. intros h. iff M.
  { 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. }
Qed.

charguer's avatar
charguer committed
206 207 208 209 210 211
Lemma hstar_hforall : forall H A (J:A->hprop), 
  (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
212
Lemma himpl_frame_l : forall H2 H1 H1',
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
213
  H1 ==> H1' ->
charguer's avatar
charguer committed
214 215 216
  (H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

charguer's avatar
charguer committed
217 218
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
219 220 221 222 223
    ( 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
224
  forall F (H:hprop) (Q:B->hprop),
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
225
  local (local F) H Q ->
charguer's avatar
charguer committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
  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
241 242 243

End Properties.

charguer's avatar
charguer committed
244
End SepBasicCore.
charguer's avatar
charguer committed
245 246


charguer's avatar
charguer committed
247
(* ********************************************************************** *)
charguer's avatar
charguer committed
248
(* * Properties of the logic *)
charguer's avatar
charguer committed
249

charguer's avatar
charguer committed
250 251 252 253 254 255
(* ---------------------------------------------------------------------- *)
(* ** Functor instantiations *)

(** Here, we instantiate the functors to obtained derived definitions,
  lemmas, notation, and tactics. *)

charguer's avatar
charguer committed
256
Module Export SepBasicTactics := SepLogicTactics SepBasicCore.
charguer's avatar
charguer committed
257

charguer's avatar
charguer committed
258
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
259
(* ** Singleton heap *)
charguer's avatar
charguer committed
260

charguer's avatar
charguer committed
261
(** Definition of the singleton heap predicate, written [r ~~~> v] *)
charguer's avatar
charguer committed
262

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
263
Definition hsingle (l:loc) (v:val) : hprop :=
charguer's avatar
charguer committed
264
  fun h => h = fmap_single l v /\ l <> null.
charguer's avatar
charguer committed
265

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

charguer's avatar
charguer committed
269
Lemma hstar_hsingle_same_loc_disjoint : forall l v1 v2,
charguer's avatar
charguer committed
270
  (l ~~~> v1) \* (l ~~~> v2) ==> \[False].
charguer's avatar
charguer committed
271
Proof using.
charguer's avatar
charguer committed
272
  intros. unfold hsingle. intros h (h1&h2&E1&E2&D&E). false.
charguer's avatar
alloc  
charguer committed
273
  subst. applys* fmap_disjoint_single_single_same_inv.
charguer's avatar
charguer committed
274 275
Qed.

charguer's avatar
charguer committed
276
Lemma hsingle_not_null : forall l v,
charguer's avatar
charguer committed
277
  (l ~~~> v) ==> (l ~~~> v) \* \[l <> null].
charguer's avatar
charguer committed
278 279
Proof using.
  introv. intros h (Hh&Nl).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
280
  exists h heap_empty. splits~.
charguer's avatar
charguer committed
281
  { unfold hsingle. splits~. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
282
  { applys~ hpure_intro. applys~ hempty_intro. }
283
  { unfold heap_empty. auto. }
charguer's avatar
charguer committed
284 285
Qed.

charguer's avatar
charguer committed
286

charguer's avatar
charguer committed
287 288 289
(* ---------------------------------------------------------------------- *)
(* ** Singleton field heap *)

charguer's avatar
charguer committed
290 291
(** Definition of the heap predicate describing a single record field,
  written [l `.` f ~> v]. *)
charguer's avatar
alloc  
charguer committed
292

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
293 294
Definition hfield (l:loc) (k:field) (v:val) : hprop :=
  (l+k)%nat ~~~> v \* \[ l <> null ].
charguer's avatar
charguer committed
295

charguer's avatar
charguer committed
296 297 298
Notation "l `.` k '~~~>' v" := (hfield l k v)
  (at level 32, k at level 0, no associativity,
   format "l `.` k  '~~~>'  v") : heap_scope.
charguer's avatar
alloc  
charguer committed
299

charguer's avatar
charguer committed
300 301
Lemma hstar_hfield_same_loc_disjoint : forall l k v1 v2,
  (l`.`k ~~~> v1) \* (l`.`k ~~~> v2) ==> \[False].
charguer's avatar
charguer committed
302 303 304 305
Proof using.
  intros. unfold hfield. hpull ;=> N1 N2.
  applys hstar_hsingle_same_loc_disjoint.
Qed.
charguer's avatar
charguer committed
306

charguer's avatar
charguer committed
307 308
Lemma hfield_not_null : forall l k v,
  (l`.`k ~~~> v) ==> (l`.`k ~~~> v) \* \[l <> null].
charguer's avatar
charguer committed
309
Proof using.
charguer's avatar
charguer committed
310
  intros. subst. unfold hfield. hchanges~ hsingle_not_null.
charguer's avatar
charguer committed
311 312
Qed.

charguer's avatar
charguer committed
313
Arguments hfield_not_null : clear implicits.
charguer's avatar
charguer committed
314

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
315
Lemma hfield_eq_fun_hsingle :
charguer's avatar
charguer committed
316
  hfield = (fun l k v => ((l+k)%nat ~~~> v) \* \[l <> null]).
charguer's avatar
array  
charguer committed
317 318
Proof using. intros. auto. Qed.

charguer's avatar
charguer committed
319 320
Lemma hfield_to_hsingle : forall l k v,
  (l`.`k ~~~> v) ==> ((l+k)%nat ~~~> v) \* \[l <> null].
charguer's avatar
array  
charguer committed
321 322
Proof using. intros. auto. Qed.

charguer's avatar
charguer committed
323
Lemma hsingle_to_hfield : forall l k v,
charguer's avatar
charguer committed
324
  l <> null ->
charguer's avatar
charguer committed
325
  ((l+k)%nat ~~~> v) ==> l`.`k ~~~> v.
charguer's avatar
charguer committed
326 327
Proof using. intros. unfold hfield. hsimpl~. Qed.

charguer's avatar
charguer committed
328
Arguments hsingle_to_hfield : clear implicits.
charguer's avatar
array  
charguer committed
329

charguer's avatar
charguer committed
330 331
Global Opaque hsingle hfield.

charguer's avatar
charguer committed
332 333 334

(* ---------------------------------------------------------------------- *)
(* ** Configuration of [hsimpl] *)
charguer's avatar
alloc  
charguer committed
335

charguer's avatar
charguer committed
336
(* ** Configure [hsimpl] to make it aware of [hsingle] *)
charguer's avatar
charguer committed
337

charguer's avatar
charguer committed
338
Ltac hcancel_hook H ::=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
339 340 341
  match H with
  | hsingle _ _ => hcancel_try_same tt
  | hfield _ _ _ => hcancel_try_same tt
charguer's avatar
charguer committed
342 343 344
  end.


charguer's avatar
charguer committed
345 346 347 348 349 350 351 352 353
(* ---------------------------------------------------------------------- *)
(* ** Auxiliary definitions for [rule_if] and [rule_seq] *)

Definition is_val_bool (v:val) : Prop :=
  exists b, v = val_bool b.

Definition is_val_unit (v:val) : Prop :=
  v = val_unit.

charguer's avatar
charguer committed
354 355 356 357 358 359 360 361
  (* LATER: introduce definitions

    is_post_unit Q :=
      (forall (v:val), v <> val_unit -> (Q1 v) ==> \[False]) ->

    is_post_bool Q :=
      (forall (v:val), v <> true -> v <> false -> (Q1 v) ==> \[False]) ->
  *)
charguer's avatar
charguer committed
362 363 364 365

(* ---------------------------------------------------------------------- *)
(* ** Auxiliary definitions for [rule_alloc] *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
366
Fixpoint Alloc (k:nat) (l:loc) :=
charguer's avatar
array  
charguer committed
367 368
  match k with
  | O => \[]
charguer's avatar
charguer committed
369
  | S k' => (Hexists v, l ~~~> v) \* (Alloc k' (S l)%nat)
charguer's avatar
array  
charguer committed
370
  end.
charguer's avatar
charguer committed
371

charguer's avatar
array  
charguer committed
372 373
Lemma Alloc_zero_eq : forall l,
  Alloc O l = \[].
charguer's avatar
charguer committed
374 375
Proof using. auto. Qed.

charguer's avatar
array  
charguer committed
376
Lemma Alloc_succ_eq : forall l k,
charguer's avatar
charguer committed
377
  Alloc (S k) l = (Hexists v, l ~~~> v) \* Alloc k (S l)%nat.
charguer's avatar
charguer committed
378 379
Proof using. auto. Qed.

charguer's avatar
array  
charguer committed
380
Global Opaque Alloc.
charguer's avatar
charguer committed
381

charguer's avatar
array  
charguer committed
382
Hint Rewrite Alloc_zero_eq Alloc_succ_eq : rew_Alloc.
charguer's avatar
charguer committed
383

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
384
Tactic Notation "rew_Alloc" :=
charguer's avatar
array  
charguer committed
385 386
  autorewrite with rew_Alloc.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
387
Lemma Alloc_fmap_conseq : forall l k v,
charguer's avatar
charguer committed
388
  l <> null ->
charguer's avatar
array  
charguer committed
389
  (Alloc k l) (fmap_conseq l k v).
charguer's avatar
charguer committed
390 391
Proof using.
  Transparent loc null.
charguer's avatar
array  
charguer committed
392 393 394 395 396
  introv N. gen l. induction k; intros; rew_Alloc.
  { rewrite fmap_conseq_zero. applys~ hempty_intro. }
  { rewrite fmap_conseq_succ. applys hstar_intro.
    { applys hexists_intro. split~. }
    { applys IHk. unfolds loc, null. math. }
charguer's avatar
charguer committed
397 398 399
    { applys~ fmap_disjoint_single_conseq. } }
Qed.

charguer's avatar
charguer committed
400 401 402 403
Lemma Alloc_split_eq : forall k1 (k:nat) p,
  (k1 <= k)%nat ->
  Alloc k p = Alloc k1 p \* Alloc (k-k1)%nat (p + k1)%nat.
Proof using.
charguer's avatar
charguer committed
404
  Transparent loc field. unfold field.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
405
  intros k1 k. gen k1. induction k; introv N.
charguer's avatar
charguer committed
406
  {math_rewrite (k1 = 0%nat). rew_Alloc. rew_heap~. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
407
  { destruct k1 as [|k1']; rew_nat.
charguer's avatar
charguer committed
408 409 410 411
    { rew_Alloc. rew_heap~. }
    { rew_Alloc. rewrite (IHk k1'); [|math]. rew_heap~. } }
Qed.

charguer's avatar
charguer committed
412
Arguments Alloc_split_eq : clear implicits.
charguer's avatar
charguer committed
413 414 415 416 417 418 419

Lemma Alloc_split_inv : forall k1 k2 p,
  Alloc k1 p \* Alloc k2 (p + k1)%nat ==> Alloc (k1+k2)%nat p.
Proof using.
  intros. rewrites (Alloc_split_eq k1 (k1+k2)%nat p); [|math]. rew_nat~.
Qed.

charguer's avatar
charguer committed
420 421 422
(** Tactic for helping reasoning about concrete calls to [alloc] *)

Ltac simpl_abs := (* TODO: will be removed once [abs] computes *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
423
  match goal with
charguer's avatar
charguer committed
424 425 426 427
  | |- context [ abs 0 ] => change (abs 0) with 0%nat
  | |- context [ abs 1 ] => change (abs 1) with 1%nat
  | |- context [ abs 2 ] => change (abs 2) with 2%nat
  | |- context [ abs 3 ] => change (abs 3) with 3%nat
charguer's avatar
charguer committed
428 429 430
  end.


charguer's avatar
charguer committed
431
(* ********************************************************************** *)
charguer's avatar
charguer committed
432
(* * Reasoning Rules *)
charguer's avatar
charguer committed
433 434


charguer's avatar
charguer committed
435
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
436
(* ** Definition of triples *)
charguer's avatar
charguer committed
437

charguer's avatar
charguer committed
438 439 440
(** This is a total-correctness definition of a triple, for a
  deterministic language. (Remark: our definition makes sense even though
  technically allocation picks fresh locations in a non-deterministic
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
441 442 443
  manner, because identity of locations do not influence program
  behaviors.)

charguer's avatar
charguer committed
444
  Below, the evaluation of [t] in state [h] terminates on value [v]
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
445
  in state [h'], when [h] satisfies the pre-condition [H] starred
charguer's avatar
charguer committed
446
  with a heap predicate [H'] describing the framed part, and where
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
447
  the final state [h'] satisfies the post-condition [Q] applied to the
charguer's avatar
charguer committed
448 449
  result value [v], starred with the framed part [H'], and starred
  with [\Top] to account for garbage collection.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
450

charguer's avatar
charguer committed
451 452 453
  Remark: in a C-style language, [\Top] needs to be defined in a
  more restrictive way to enforce deallocation of malloc-ed blocks. *)

charguer's avatar
charguer committed
454
Definition triple (t:trm) (H:hprop) (Q:val->hprop) :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
455 456 457
  forall H' h,
  (H \* H') h ->
  exists h' v,
charguer's avatar
charguer committed
458
       red h t h' v
charguer's avatar
charguer committed
459
    /\ (Q v \* \Top \* H') h'.
charguer's avatar
charguer committed
460 461


charguer's avatar
charguer committed
462 463 464
(* ---------------------------------------------------------------------- *)
(* ** Triples satisfy the [local] predicate *)

charguer's avatar
charguer committed
465 466 467
(** This lemma is exploited indirectly by tactics such as [xapply],
  which perform application of lemmas modulo framing. *)

charguer's avatar
charguer committed
468 469
Lemma is_local_triple : forall t,
  is_local (triple t).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
470
Proof using.
charguer's avatar
charguer committed
471
  intros. applys pred_ext_2. intros H Q. iff M.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
472
  { intros h Hh. forwards (h'&v&N1&N2): M \[] h. { hhsimpl. }
charguer's avatar
charguer committed
473 474 475 476 477 478 479 480
    exists H \[] Q. splits~. { hhsimpl. } { hsimpl. } }
  { intros H' h Hh. lets (h1&h2&N1&N2&N3&N4): Hh. hnf in M.
    lets (H1&H2&Q1&R1&R2&R3): M N1.
    forwards (h'&v&S1&S2): R2 (H2\*H') h.
    { subst h. rewrite <- hstar_assoc. exists~ h1 h2. }
    exists h' v. splits~. rewrite <- htop_hstar_htop.
    applys himpl_inv S2.
    hchange (R3 v). rew_heap.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
481
    rewrite (hstar_comm_assoc \Top H'). hsimpl. }
charguer's avatar
charguer committed
482 483 484 485
Qed.

(** Make tactic [xlocal] aware that triples are local *)

charguer's avatar
charguer committed
486
Ltac xlocal_base tt ::=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
487
  try first [ applys is_local_local
charguer's avatar
charguer committed
488
            | applys is_local_triple ].
charguer's avatar
charguer committed
489 490


charguer's avatar
charguer committed
491
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
492
(* ** Structural rules *)
charguer's avatar
charguer committed
493

charguer's avatar
charguer committed
494
Lemma rule_extract_hexists : forall t (A:Type) (J:A->hprop) Q,
charguer's avatar
charguer committed
495
  (forall x, triple t (J x) Q) ->
charguer's avatar
charguer committed
496
  triple t (hexists J) Q.
charguer's avatar
charguer committed
497
Proof using.
charguer's avatar
charguer committed
498
  introv M. intros HF h N. rewrite hstar_hexists in N.
charguer's avatar
charguer committed
499 500 501
  destruct N as (x&N). applys* M.
Qed.

charguer's avatar
charguer committed
502
Lemma rule_extract_hprop : forall t (P:Prop) H Q,
charguer's avatar
charguer committed
503 504 505
  (P -> triple t H Q) ->
  triple t (\[P] \* H) Q.
Proof using.
charguer's avatar
charguer committed
506 507
  intros t. applys (rule_extract_hprop_from_extract_hexists (triple t)).
  applys rule_extract_hexists.
charguer's avatar
charguer committed
508 509
Qed.

charguer's avatar
charguer committed
510 511 512 513 514
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
515
Proof using.
charguer's avatar
charguer committed
516 517
  introv MH M MQ. intros HF h N.
  forwards (h'&v&R&K): (rm M) HF h. { hhsimpl~. }
charguer's avatar
charguer committed
518
  exists h' v. splits~. { hhsimpl. hchanges (MQ v). }
charguer's avatar
charguer committed
519 520 521 522 523
Qed.

Lemma rule_frame : forall t H Q H',
  triple t H Q ->
  triple t (H \* H') (Q \*+ H').
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
524
Proof using.
charguer's avatar
charguer committed
525
  introv M. intros HF h N. rewrite hstar_assoc in N.
charguer's avatar
charguer committed
526
  forwards (h'&v&R&K): (rm M) (H' \* HF) h. { hhsimpl~. }
charguer's avatar
charguer committed
527
  exists h' v. splits~. { hhsimpl~. }
charguer's avatar
charguer committed
528 529
Qed.

charguer's avatar
charguer committed
530 531
Lemma rule_htop_post : forall t H Q,
  triple t H (Q \*+ \Top) ->
charguer's avatar
charguer committed
532 533
  triple t H Q.
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
534 535
  introv M. intros HF h N. forwards* (h'&v&R&K): (rm M) HF h.
  exists h' v. splits~. { rewrite <- htop_hstar_htop. hhsimpl. }
charguer's avatar
charguer committed
536 537
Qed.

charguer's avatar
charguer committed
538
Lemma rule_htop_pre : forall t H Q,
charguer's avatar
charguer committed
539
  triple t H Q ->
charguer's avatar
charguer committed
540
  triple t (H \* \Top) Q.
charguer's avatar
charguer committed
541
Proof using.
charguer's avatar
charguer committed
542
  introv M. applys rule_htop_post. applys~ rule_frame.
charguer's avatar
charguer committed
543 544
Qed.

charguer's avatar
rules  
charguer committed
545 546
(* ---------------------------------------------------------------------- *)
(* ** Term rules *)
charguer's avatar
charguer committed
547

charguer's avatar
charguer committed
548 549 550 551
Lemma rule_val : forall v H Q,
  H ==> Q v ->
  triple (trm_val v) H Q.
Proof using.
charguer's avatar
charguer committed
552
  introv M. intros HF h N. exists h v. splits.
charguer's avatar
charguer committed
553 554 555 556
  { applys red_val. }
  { hhsimpl. hchanges M. }
Qed.

charguer's avatar
charguer committed
557 558 559
Lemma rule_fun : forall x t1 H Q,
  H ==> Q (val_fun x t1) ->
  triple (trm_fun x t1) H Q.
charguer's avatar
charguer committed
560 561
Proof using.
  introv M. intros HF h N. exists___. splits.
charguer's avatar
charguer committed
562 563 564 565 566 567 568 569 570 571
  { applys red_fun. }
  { hhsimpl. hchanges M. }
Qed.

Lemma rule_fix : forall f x t1 H Q,
  H ==> Q (val_fix f x t1) ->
  triple (trm_fix f x t1) H Q.
Proof using.
  introv M. intros HF h N. exists___. splits.
  { applys red_fix. }
charguer's avatar
charguer committed
572 573 574
  { hhsimpl. hchanges M. }
Qed.

charguer's avatar
charguer committed
575 576
Lemma rule_if : forall Q1 t0 t1 t2 H Q,
  triple t0 H Q1 ->
charguer's avatar
charguer committed
577
  (forall (b:bool), triple (if b then t1 else t2) (Q1 b) Q) ->
charguer's avatar
charguer committed
578
  (forall v, ~ is_val_bool v -> (Q1 v) ==> \[False]) ->
charguer's avatar
charguer committed
579 580
  triple (trm_if t0 t1 t2) H Q.
Proof using.
charguer's avatar
charguer committed
581
  introv M1 M2 M3. intros HF h N.
charguer's avatar
charguer committed
582
  forwards* (h1'&v&R1&K1): (rm M1) HF h.
charguer's avatar
charguer committed
583
  tests C: (is_val_bool v).
charguer's avatar
charguer committed
584
  { destruct C as (b&E). subst. forwards* (h'&v'&R&K): (rm M2) h1'.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
585
    exists h' v'. splits~.
charguer's avatar
charguer committed
586 587 588
    { applys* red_if. }
    { rewrite <- htop_hstar_htop. rew_heap~. } }
  { specializes M3 C.
charguer's avatar
charguer committed
589
    asserts Z: ((\[False] \* \Top \* HF) h1').
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
590
    { applys himpl_trans K1. hchange M3. hsimpl. hsimpl. }
charguer's avatar
charguer committed
591
    repeat rewrite hfalse_hstar_any in Z.
charguer's avatar
charguer committed
592
    lets: hpure_inv Z. false*. } (* TODO: shorten this *)
charguer's avatar
charguer committed
593 594
Qed.

charguer's avatar
charguer committed
595 596 597 598
Lemma rule_if_bool : forall (b:bool) t1 t2 H Q,
  (b = true -> triple t1 H Q) ->
  (b = false -> triple t2 H Q) ->
  triple (trm_if b t1 t2) H Q.
charguer's avatar
charguer committed
599
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
600
  introv M1 M2. applys rule_if (fun r => \[r = val_bool b] \* H).
charguer's avatar
charguer committed
601
  { applys rule_val. hsimpl~. }
charguer's avatar
charguer committed
602
  { intros b'. applys~ rule_extract_hprop. intros E. inverts E. case_if*. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
603
  { intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. }
charguer's avatar
charguer committed
604 605
Qed.

charguer's avatar
charguer committed
606 607 608
Lemma rule_seq : forall t1 t2 H Q Q1,
  triple t1 H Q1 ->
  (forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
609
  triple t2 (Q1 val_unit) Q ->
charguer's avatar
charguer committed
610 611
  triple (trm_seq t1 t2) H Q.
Proof using.
charguer's avatar
charguer committed
612
  introv M1 M2 M3. intros HF h N.
charguer's avatar
charguer committed
613
  lets~ (h1'&v1&R1&K1): (rm M1) HF h.
charguer's avatar
charguer committed
614
  asserts E: (v1 = val_unit).
615
  { specializes M2 v1. applys not_not_inv. intros E.
charguer's avatar
charguer committed
616
    asserts Z: ((\[False] \* \Top \* HF) h1').
617
    { applys himpl_trans K1. hchange~ M2. hsimpl. }
charguer's avatar
charguer committed
618 619
    repeat rewrite hfalse_hstar_any in Z.
    lets: hpure_inv Z. false*. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
620
    (* TODO: shorten this, and factorize with rule_if *)
621
  subst. forwards* (h2'&v2&R2&K2): (rm M3) (\Top \* HF) h1'.
charguer's avatar
charguer committed
622 623
  exists h2' v2. splits~.
  { applys~ red_seq R2. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
624
  { rewrite <- htop_hstar_htop. hhsimpl. }
charguer's avatar
charguer committed
625 626
Qed.

charguer's avatar
charguer committed
627 628
Lemma rule_let : forall x t1 t2 H Q Q1,
  triple t1 H Q1 ->
charguer's avatar
charguer committed
629
  (forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
charguer's avatar
charguer committed
630 631 632 633
  triple (trm_let x t1 t2) H Q.
Proof using.
  introv M1 M2. intros HF h N.
  lets~ (h1'&v1&R1&K1): (rm M1) HF h.
charguer's avatar
charguer committed
634
  forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
charguer's avatar
charguer committed
635 636
  exists h2' v2. splits~.
  { applys~ red_let R2. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
637
  { rewrite <- htop_hstar_htop. hhsimpl. }
charguer's avatar
charguer committed
638 639
Qed.

charguer's avatar
charguer committed
640 641 642 643 644
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
  F = (val_funs xs t1) ->
  var_funs (length Vs) xs ->
  triple (substs xs Vs t1) H Q ->
  triple (trm_apps F Vs) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
645
Proof using.
charguer's avatar
charguer committed
646 647 648 649 650 651 652 653 654
  introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
  exists h' v. splits~. { subst. applys* red_app_funs_val. }
Qed.

Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q,
  F = (val_fixs f xs t1) ->
  var_fixs f (length Vs) xs ->
  triple (subst f F (substs xs Vs t1)) H Q ->
  triple (trm_apps F Vs) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
655
Proof using.
charguer's avatar
charguer committed
656 657 658 659
  introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
  exists h' v. splits~. { subst. applys* red_app_fixs_val. }
Qed.

charguer's avatar
charguer committed
660 661 662 663 664 665 666

(* ---------------------------------------------------------------------- *)
(* ** Rules for loops *)

Lemma rule_while_raw : forall t1 t2 H Q,
  triple (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) H Q ->
  triple (trm_while t1 t2) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
667
Proof using.
charguer's avatar
charguer committed
668 669 670 671 672 673 674 675 676 677
  introv M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
  exists h' v. splits~. { applys* red_while. }
Qed.

Lemma rule_while : forall t1 t2 H Q,
  (forall t,
     (forall H' Q', triple (trm_if t1 (trm_seq t2 t) val_unit) H' Q' ->
                    triple t H' Q') ->
    triple t H Q) ->
  triple (trm_while t1 t2) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
678
Proof using.
charguer's avatar
charguer committed
679 680 681 682 683 684
  introv M. applys M. introv K. applys rule_while_raw. applys K.
Qed.

Lemma rule_while_inv : forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop) t1 t2 H,
  let Q := (fun r => \[r = val_unit] \* Hexists Y, I false Y) in
  wf R ->
charguer's avatar
charguer committed
685
  (H ==> (Hexists b X, I b X) \* \Top) -> (* TODO: replace \top with H' *)
charguer's avatar
charguer committed
686 687 688
  (forall t b X,
      (forall b' X', R X' X -> triple t (I b' X') Q) ->
      triple (trm_if t1 (trm_seq t2 t) val_unit) (I b X) Q) ->
charguer's avatar
charguer committed
689
  triple (trm_while t1 t2) H Q. (* TODO: allow for weakening on Q *)
charguer's avatar
charguer committed
690 691 692
Proof using.
  introv WR H0 HX. xchange (rm H0). xpull ;=> b0 X0.
  rewrite hstar_comm. applys rule_htop_pre. gen b0.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
693
  induction_wf IH: WR X0. intros. applys rule_while_raw.
charguer's avatar
charguer committed
694 695 696
  applys HX. intros b' X' HR'. applys~ IH.
Qed.

charguer's avatar
charguer committed
697 698
Lemma rule_for_raw : forall (x:var) (n1 n2:int) t3 H (Q:val->hprop),
  triple (
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
699
    If (n1 <= n2)
charguer's avatar
charguer committed
700 701 702
      then (trm_seq (subst x n1 t3) (trm_for x (n1+1) n2 t3))
      else val_unit) H Q ->
  triple (trm_for x n1 n2 t3) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
703
Proof using.
charguer's avatar
charguer committed
704 705 706 707 708
  introv M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
  exists h' v. splits~. { applys~ red_for. }
Qed.

(* TODO: simplify proof using rule_for_raw *)
charguer's avatar
charguer committed
709
Lemma rule_for_gt : forall x n1 n2 t3 H Q,
charguer's avatar
charguer committed
710
  n1 > n2 ->
charguer's avatar
charguer committed
711 712
  (fun r => \[r = val_unit] \* H) ===> (Q \*+ \Top) ->
  triple (trm_for x n1 n2 t3) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
713
Proof using.
charguer's avatar
charguer committed
714
  introv N M. intros H' h Hf. exists h val_unit. splits~.
charguer's avatar
charguer committed
715
  { applys* red_for_gt. }
charguer's avatar
charguer committed
716
  { hhsimpl. hchange~ M. hsimpl. }
charguer's avatar
charguer committed
717 718
Qed.

charguer's avatar
charguer committed
719
(* TODO: simplify proof using rule_for_raw *)
charguer's avatar
charguer committed
720
Lemma rule_for_le : forall Q1 x n1 n2 t3 H Q,
charguer's avatar
charguer committed
721 722 723 724 725
  n1 <= n2 ->
  triple (subst x n1 t3) H Q1 ->
  triple (trm_for x (n1+1) n2 t3) (Q1 val_unit) Q ->
  (forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
  triple (trm_for x n1 n2 t3) H Q.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
726
Proof using.
charguer's avatar
charguer committed
727 728
  introv N M1 M2 M3. intros HF h Hf. forwards (h1'&v1&R1&K1): (rm M1) Hf.
  asserts E: (v1 = val_unit).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
729
  { specializes M3 v1. applys not_not_inv. intros E.
charguer's avatar
charguer committed
730
    asserts Z: ((\[False] \* \Top \* HF) h1').
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
731
    { applys himpl_trans K1. hchange~ M3. hsimpl. }
charguer's avatar
charguer committed
732 733
    repeat rewrite hfalse_hstar_any in Z.
    lets: hpure_inv Z. false*. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
734
    (* TODO: shorten this, and factorize with rule_if *)
charguer's avatar
charguer committed
735 736 737 738 739 740
  subst. forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
  exists h2' v2. splits~.
  { applys* red_for_le. }
  { rewrite <- htop_hstar_htop. hhsimpl. }
Qed.

charguer's avatar
charguer committed
741
(* TODO: simplify proof using rule_for_raw *)
charguer's avatar
charguer committed
742 743 744 745 746
Lemma rule_for : forall x (n1 n2:int) t3 H Q,
  (If (n1 <= n2) then
    (exists Q1,
      triple (subst x n1 t3) H Q1 /\
      triple (trm_for x (n1+1) n2 t3) (Q1 val_unit) Q /\
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
747 748
      (forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]))
  else
charguer's avatar
charguer committed
749 750 751 752 753 754 755 756
    ((fun r => \[r = val_unit] \* H) ===> Q)) ->
  triple (trm_for x n1 n2 t3) H Q.
Proof using.
  introv M. case_if.
  { destruct M. applys* rule_for_le. }
  { xapplys* rule_for_gt. { math. } intros r. hchanges* M. }
Qed.

charguer's avatar
charguer committed
757
(* TODO: simplify proof using rule_for_raw *)
charguer's avatar
charguer committed
758
Lemma rule_for_inv : forall (I:int->hprop) H' x n1 n2 t3 H Q,
charguer's avatar
charguer committed
759
  (n1 <= n2+1) ->
charguer's avatar
charguer committed
760
  (H ==> I n1 \* H') ->
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
761
  (forall i, n1 <= i <= n2 ->
charguer's avatar
charguer committed
762 763 764 765 766
     triple (subst x i t3) (I i) (fun r => \[r = val_unit] \* I (i+1))) ->
  (I (n2+1) \* H' ==> Q val_unit \* \Top) ->
  triple (trm_for x n1 n2 t3) H Q.
Proof using.
  introv N M1 M2 M3. xchange (rm M1). gen N M2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
767
  induction_wf IH: (wf_upto (n2+1)) n1; intros.
charguer's avatar
charguer committed
768
  asserts M4: (triple (trm_for x (n2 + 1)%I n2 t3) (I (n2+1) \* H') Q).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
769 770
  { applys rule_for_gt. { math. }
    { intros r. hpull ;=> E. subst. hchanges M3. } }
charguer's avatar
charguer committed
771
  tests C: (n1 = n2+1).
charguer's avatar
charguer committed
772
  { xapplys M4. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
773
  { applys rule_for_le.
charguer's avatar
charguer committed
774
    { math. }
charguer's avatar
charguer committed
775
    { xapplys M2. { math. } }
charguer's avatar
charguer committed
776 777 778
    { simpl. xpull ;=> _. tests C': (n1 = n2).
      { xapplys M4. }
      { xapplys IH. { hnf; math. } { math. } { intros. applys M2. math. } } }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
779
    { intros v Nv. hpull. } }
charguer's avatar
charguer committed
780
Qed.
charguer's avatar
charguer committed
781 782


charguer's avatar
charguer committed
783 784 785
(* ---------------------------------------------------------------------- *)
(** Primitive functions over the state *)

charguer's avatar
alloc  
charguer committed
786
Section RulesStateOps.
charguer's avatar
charguer committed
787
Transparent hstar hsingle hfield hexists loc null.
charguer's avatar
charguer committed
788

charguer's avatar
charguer committed
789
Lemma rule_ref : forall v,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
790 791
  triple (val_ref v)
    \[]
charguer's avatar
charguer committed
792
    (fun r => Hexists l, \[r = val_loc l] \* l ~~~> v).
charguer's avatar
charguer committed
793 794
Proof using.
  intros. intros HF h N.
charguer's avatar
alloc  
charguer committed
795
  forwards~ (l&Dl&Nl): (fmap_single_fresh null h v).
charguer's avatar
charguer committed
796
  sets h1': (fmap_single l v).
charguer's avatar
charguer committed
797
  exists (h1' \u h) (val_loc l). splits~.
charguer's avatar
charguer committed
798
  { applys~ red_ref. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
799
  { exists h1' h. split.
charguer's avatar
alloc  
charguer committed
800
    { exists l. applys~ himpl_hprop_r. unfold h1'. hnfs~. }
charguer's avatar
charguer committed
801
    { splits~. hhsimpl~. } }
charguer's avatar
charguer committed
802 803 804
Qed.

Lemma rule_get : forall v l,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
805 806
  triple (val_get (val_loc l))
    (l ~~~> v)
charguer's avatar
charguer committed
807
    (fun x => \[x = v] \* (l ~~~> v)).
charguer's avatar
charguer committed
808 809
Proof using.
  intros. intros HF h N. exists h v. splits~.
charguer's avatar
charguer committed
810
  { applys red_get. destruct N as (?&?&(?&?)&?&?&?).
charguer's avatar
charguer committed
811
    subst h. applys~ fmap_union_single_l_read. }
charguer's avatar
charguer committed
812
  { rew_heap. rewrite hstar_pure. split~. hhsimpl~. }
charguer's avatar
charguer committed
813 814
Qed.

charguer's avatar
charguer committed
815
Lemma rule_set : forall w l v,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
816 817
  triple (val_set (val_loc l) w)
    (l ~~~> v)
charguer's avatar
charguer committed
818
    (fun r => \[r = val_unit] \* l ~~~> w).
charguer's avatar
charguer committed
819
Proof using.
charguer's avatar
charguer committed
820
  intros. intros HF h N. destruct N as (h1&h2&(N0&N1)&N2&N3&N4).
charguer's avatar
charguer committed
821
  hnf in N1. sets h1': (fmap_single l w).
charguer's avatar
charguer committed
822
  exists (h1' \u h2) val_unit. splits~.
charguer's avatar
charguer committed
823
  { applys red_set. subst h h1. applys~ fmap_union_single_to_update. }
charguer's avatar
charguer committed
824
  { rew_heap. rewrite hstar_pure. split~.
charguer's avatar
charguer committed
825 826
    { exists h1' h2. splits~.
      { hnfs~. }
charguer's avatar
charguer committed
827
      { hhsimpl~. }
charguer's avatar
charguer committed
828
      { subst h1. applys~ fmap_disjoint_single_set v. } } }
charguer's avatar
charguer committed
829 830
Qed.

charguer's avatar
charguer committed
831 832 833 834

(* ---------------------------------------------------------------------- *)
(** Alloc function *)

charguer's avatar
alloc  
charguer committed
835
Lemma rule_alloc : forall n,
charguer's avatar
charguer committed
836
  n >= 0 ->
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
837 838
  triple (val_alloc n)
    \[]
charguer's avatar
charguer committed
839
    (fun r => Hexists l, \[r = val_loc l /\ l <> null] \* Alloc (abs n) l).
charguer's avatar
alloc  
charguer committed
840 841 842 843 844 845
Proof using. (* Note: [abs n] currently does not compute in Coq. *)
  introv N Hh.
  forwards~ (l&Dl&Nl): (fmap_conseq_fresh null h (abs n) val_unit).
  sets h1': (fmap_conseq l (abs n) val_unit).
  exists (h1' \u h) (val_loc l). splits~.
  { applys (red_alloc (abs n)); eauto.
charguer's avatar
charguer committed
846
    rewrite~ abs_nonneg. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
847
  { exists h1' h. split.
charguer's avatar
array  
charguer committed
848
    { exists l. applys~ himpl_hprop_r. applys~ Alloc_fmap_conseq. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
849
    { splits~. hhsimpl~. } }
charguer's avatar
alloc  
charguer committed
850 851 852 853
Qed.

End RulesStateOps.

charguer's avatar
array  
charguer committed
854

charguer's avatar
charguer committed
855 856 857
(* ---------------------------------------------------------------------- *)
(** Other primitive functions *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
858
Lemma rule_eq : forall v1