CFHeaps.v

Set Implicit Arguments.
Require Export LibCore Shared LibMonoid LibMap LibSet.


(********************************************************************)
(* ** States *)

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

(** Representation of heap items *)

Record dynamic := dyn {
  dyn_type : Type;
  dyn_value : dyn_type }.

Arguments dyn {dyn_type}.

Lemma dyn_inj : forall A (x y : A),
  dyn x = dyn y -> x = y.
Proof using. introv H. inverts~ H. Qed.

Lemma dyn_inj_type : forall A1 A2 (x1:A1) (x2:A2),
  dyn x1 = dyn x2 -> A1 = A2.
Proof using. introv H. inverts~ H. Qed.

Lemma dyn_eta : forall d,
  d = dyn (dyn_value d).
Proof using. intros. destruct~ d. Qed.


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

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

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

(** Finite domain of a partial function *)

Definition pfun_finite (A B : Type) (f : pfun A B) :=
  exists (L : list A), forall x, f x <> None -> mem x L.

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

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

(** Disjoint union of two partial functions *)

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

(** Finiteness of union *)

Lemma pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B),
  pfun_finite f1 -> pfun_finite f2 -> pfun_finite (pfun_union f1 f2).
Proof using.
  introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M.
  specializes F1 x. specializes F2 x. unfold pfun_union in M.
  rewrite mem_app_eq. destruct~ (f1 x).
Qed.

(** Symmetry of disjointness *)

Lemma pfun_disjoint_sym : forall (A B : Type),
  sym (@pfun_disjoint A B).
Proof using.
  introv H. unfolds pfun_disjoint. intros z. specializes H z. intuition.
Qed.

(** Commutativity of disjoint union *)

Tactic Notation "cases" constr(E) :=  (* TODO: move *)
  let H := fresh "Eq" in cases E as H.

Lemma pfun_union_comm : forall (A B : Type) (f1 f2 : pfun A B),
  pfun_disjoint f1 f2 ->
  pfun_union f1 f2 = pfun_union f2 f1.
Proof using.
  introv H. extens. intros x. unfolds pfun_disjoint, pfun_union.
  specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false.
Qed.

(*------------------------------------------------------------------*)
(* ** Representation of states *)

Section State.

(** Representation of locations *)

Definition loc : Type := nat.

Global Opaque loc.

(** The null location *)

Definition null : loc := 0%nat.

(** Representation of the field of an in-memory object;
    For a record, the field is the field index;
    For an array, the field is the cell index. *)

Definition field : Type := nat.

(** Representation of the address of a memory cell,
    as a pair of the location at which the object
    is allocated and the field within this object. *)

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

(** Representation of heaps *)

Inductive state : Type := state_of {
  state_data :> pfun address dynamic;
  state_finite : pfun_finite state_data }.

Arguments state_of : clear implicits.

(** Proving states equals *)

Lemma state_eq : forall f1 f2 F1 F2,
  (forall x, f1 x = f2 x) ->
  state_of f1 F1 = state_of f2 F2.
Proof using.
  introv H. asserts: (f1 = f2). extens~. subst.
  fequals. (* note: involves proof irrelevance *)
Qed.

(** Disjoint states *)

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

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

(** Union of states *)

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

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

(** Empty state *)

Program Definition state_empty : state :=
  state_of (fun a => None) _.
Next Obligation. exists (@nil address). auto_false. Qed.

(** Singleton state *)

Program Definition state_single (l:loc) (f:field) A (v:A) : state :=
  state_of (fun a' => If a' = (l,f) then Some (dyn v) else None) _.
Next Obligation.
  exists ((l,f)::nil). intros. case_if. subst~.
Qed.

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

(** Disjointness *)

Lemma state_disjoint_sym : forall h1 h2,
  state_disjoint h1 h2 -> state_disjoint h2 h1.
Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed.

Lemma state_disjoint_comm : forall h1 h2,
  \# h1 h2 = \# h2 h1.
Proof using. lets: state_disjoint_sym. extens*. Qed.

Lemma state_disjoint_empty_l : forall h,
  state_disjoint state_empty h.
Proof using. intros [f F] x. simple~. Qed.

Lemma state_disjoint_empty_r : forall h,
  state_disjoint h state_empty.
Proof using. intros [f F] x. simple~. Qed.

Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r.

Lemma state_disjoint_union_eq_r : forall h1 h2 h3,
  state_disjoint h1 (state_union h2 h3) =
  (state_disjoint h1 h2 /\ state_disjoint h1 h3).
Proof using.
  intros [f1 F1] [f2 F2] [f3 F3].
  unfolds state_disjoint, state_union. simpls.
  unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2].
  split; intros x; specializes M x;
   destruct (f2 x); destruct M; auto_false.
  intros x. specializes M1 x. specializes M2 x.
   destruct (f2 x); destruct M1; auto_false.
Qed.

Lemma state_disjoint_union_eq_l : forall h1 h2 h3,
  state_disjoint (state_union h2 h3) h1 =
  (state_disjoint h1 h2 /\ state_disjoint h1 h3).
Proof using.
  intros. rewrite state_disjoint_comm.
  apply state_disjoint_union_eq_r.
Qed.

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

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

Lemma state_disjoint_3_unfold : forall h1 h2 h3,
  \# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.

(** Union *)

Lemma state_union_neutral_l : forall h,
  state_union state_empty h = h.
Proof using.
  intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
  apply~ state_eq.
Qed.

Lemma state_union_neutral_r : forall h,
  state_union h state_empty = h.
Proof using.
  intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
  apply state_eq. intros x. destruct~ (f x).
Qed.

Lemma state_union_comm : forall h1 h2,
  state_disjoint h1 h2 ->
  state_union h1 h2 = state_union h2 h1.
Proof using.
  intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl.
  intros. rewrite~ pfun_union_comm.
Qed.

Lemma state_union_assoc :
  LibOperation.assoc state_union.
Proof using.
  intros [f1 F1] [f2 F2] [f3 F3]. unfolds state_union. simpls.
  apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x).
Qed.

End State.

(** Hints and tactics *)

Hint Resolve state_union_neutral_l state_union_neutral_r.

Hint Rewrite
  state_disjoint_union_eq_l
  state_disjoint_union_eq_r
  state_disjoint_3_unfold : rew_disjoint.

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



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

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

(** Representation of credits *)

Definition credits_type : Type := int.

(** Zero and one credits *)

Definition credits_zero : credits_type := 0.
Definition credits_one : credits_type := 1.

(** Representation of heaps *)

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

(** Projections *)

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

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

(** Predicate over pairs *)

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

Definition prod_st2 A B (P:binary A) (Q:binary B) (v1 v2:A*B) := (* todo move to TLC *)
  let (x1,y1) := v1 in
  let (x2,y2) := v2 in
  P x1 x2 /\ Q y1 y2.

Definition prod_func A B (F:A->A->A) (G:B->B->B) (v1 v2:A*B) := (* todo move to TLC *)
  let (x1,y1) := v1 in
  let (x2,y2) := v2 in
  (F x1 x2, G y1 y2).

(** Disjoint heaps *)

Definition heap_disjoint (h1 h2 : heap) : Prop :=
  prod_st2 state_disjoint (fun _ _ => True) h1 h2. (* todo: name (fun _ _ => True) *)

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

(** Union of heaps *)

Definition heap_union (h1 h2 : heap) : heap :=
  prod_func state_union (fun a b => (a + b)) h1 h2.

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

(** Empty heap *)

Definition heap_empty : heap :=
  (state_empty, 0).

(** Affine heaps *)

Definition heap_affine (h: heap) : Prop :=
  0 <= heap_credits h.

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

(** Disjointness *)

Lemma heap_disjoint_sym : forall h1 h2,
  heap_disjoint h1 h2 -> heap_disjoint h2 h1.
Proof using.
  intros [m1 n1] [m2 n2] H. simpls.
  hint state_disjoint_sym. autos*.
Qed.

Lemma heap_disjoint_comm : forall h1 h2,
  \# h1 h2 = \# h2 h1.
Proof using.
  intros [m1 n1] [m2 n2]. simpls.
  hint state_disjoint_sym. extens*.
Qed.

Lemma heap_disjoint_empty_l : forall h,
  heap_disjoint heap_empty h.
Proof using. intros [m n]. hint state_disjoint_empty_l. simple*. Qed.

Lemma heap_disjoint_empty_r : forall h,
  heap_disjoint h heap_empty.
Proof using. intros [m n]. hint state_disjoint_empty_r. simple*. Qed.

Hint Resolve heap_disjoint_sym heap_disjoint_empty_l heap_disjoint_empty_r.

Lemma heap_disjoint_union_eq_r : forall h1 h2 h3,
  heap_disjoint h1 (heap_union h2 h3) =
  (heap_disjoint h1 h2 /\ heap_disjoint h1 h3).
Proof using.
  intros [m1 n1] [m2 n2] [m3 n3].
  unfolds heap_disjoint, heap_union. simpls.
  rewrite state_disjoint_union_eq_r. extens*.
Qed.

Lemma heap_disjoint_union_eq_l : forall h1 h2 h3,
  heap_disjoint (heap_union h2 h3) h1 =
  (heap_disjoint h1 h2 /\ heap_disjoint h1 h3).
Proof using.
  intros. rewrite heap_disjoint_comm.
  apply heap_disjoint_union_eq_r.
Qed.

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

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

Lemma heap_disjoint_3_unfold : forall h1 h2 h3,
  \# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.

(** Union *)

Lemma heap_union_neutral_l : forall h,
  heap_union heap_empty h = h.
Proof using.
  intros [m n]. unfold heap_union, heap_empty. simpl.
  fequals. apply~ state_union_neutral_l.
Qed.

Lemma heap_union_neutral_r : forall h,
  heap_union h heap_empty = h.
Proof using.
  intros [m n]. unfold heap_union, heap_empty. simpl.
  fequals. apply~ state_union_neutral_r. math.
Qed.

Lemma heap_union_comm : forall h1 h2,
  heap_disjoint h1 h2 ->
  heap_union h1 h2 = heap_union h2 h1.
Proof using.
  intros [m1 n1] [m2 n2] H. simpls. fequals.
  applys* state_union_comm.
  math.
Qed.

Lemma heap_union_assoc :
  LibOperation.assoc heap_union.
Proof using.
  intros [m1 n1] [m2 n2] [m3 n3]. unfolds heap_union. simpls.
  fequals. applys state_union_assoc. math.
Qed.

(** Affine *)

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

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

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

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

(** Hints and tactics *)

Hint Resolve heap_union_neutral_l heap_union_neutral_r.

Hint Rewrite
  heap_disjoint_union_eq_l
  heap_disjoint_union_eq_r
  heap_disjoint_3_unfold : rew_disjoint.

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



(********************************************************************)
(* ** Predicate on Heaps *)

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

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

Definition hprop := heap -> Prop.

(** Empty heap *)

Definition heap_is_empty : hprop :=
  fun h => h = heap_empty.

(** Singleton heap *)

Definition heap_is_single (l:loc) (f:field) A (v:A) : hprop :=
  fun h => let (m,n) := h in m = state_single l f v /\ l <> null /\ n = 0%nat.

(** Heap union *)

Definition heap_is_star (H1 H2 : hprop) : hprop :=
  fun h => exists h1 h2, H1 h1
                      /\ H2 h2
                      /\ heap_disjoint h1 h2
                      /\ h = heap_union h1 h2.

(** Affine heap predicates *)

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

(** Lifting of existentials *)

Definition heap_is_pack A (Hof : A -> hprop) : hprop :=
  fun h => exists x, Hof x h.

(** Lifting of predicates *)

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

(** Garbage collection predicate: equivalent to [Hexists H, H \* \[affine H]]. *)

Definition heap_is_gc : hprop :=
  fun h => heap_affine h /\ exists H, H h.

(** Credits *)

Definition heap_is_credits (x:int) : hprop :=
  fun h => let (m,x') := h in m = state_empty /\ x' = x.

Opaque heap_union state_single heap_is_star heap_is_pack
  heap_is_gc heap_is_credits heap_affine affine.

(** Hprop is inhabited *)

Instance hprop_inhab : Inhab hprop.
Proof using. intros. apply (Inhab_of_val heap_is_empty). Qed.


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

Notation "\[]" := (heap_is_empty)
  (at level 0) : heap_scope.

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

Notation "\[ L ]" := (heap_is_empty_st L)
  (at level 0, L at level 99) : heap_scope.

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

Notation "\GC" := (heap_is_gc) : heap_scope.

Notation "'\$' x" := (heap_is_credits x)
  (at level 40, format "\$ x") : heap_scope.

Notation "'Hexists' x1 , H" := (heap_is_pack (fun x1 => H))
  (at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
  (at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 x4 , H" :=
  (Hexists x1, Hexists x2, Hexists x3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 x4 x5 , H" :=
  (Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.

Notation "'Hexists' x1 : T1 , H" := (heap_is_pack (fun x1:T1 => H))
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
  (at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) , H" :=
  (Hexists x1:T1, Hexists x2:T2, H)
  (at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) ( x5 : T5 ) , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, Hexists x5:T5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

Notation "'Hexists' ( x1 x2 : T ) , H" :=
  (Hexists x1:T, Hexists x2:T, H)
  (at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 x3 : T ) , H" :=
  (Hexists x1:T, Hexists x2:T, Hexists x3:T, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 x3 x4 : T ) , H" :=
  (Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 x3 x4 x5 : T ) , H" :=
  (Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, Hexists x5:T, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

Notation "'Hexists' ( x1 : T1 ) x2 , H" :=
  (Hexists x1:T1, Hexists x2, H)
  (at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 x3 , H" :=
  (Hexists x1:T1, Hexists x2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 x3 x4 , H" :=
  (Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 x3 x4 x5 , H" :=
  (Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 x5 , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.

Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 x5 , H" :=
  (Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, Hexists x5, H)
  (at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.


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

Notation "# H" := (fun (_:unit) => (H:hprop))
  (at level 39, H at level 99) : heap_scope.

Notation "\[= v ]" := (fun x => \[x = v])
  (at level 0) : heap_scope.

Notation "P ==+> Q" := (pred_incl P%h (heap_is_star P Q))
  (at level 55, only parsing) : heap_scope.
(* TODO: notation PRE P '/' ==> KEEP '/' POST Q *)

(* DEPRECATED
Notation "'hkeep' P '==>' Q" := (pred_le P%h (Q \* P))
  (at level 55, P at level 0, right associativity) : heap_scope.
*)


(*------------------------------------------------------------------*)
(* ** Properties of heap empty *)

Lemma heap_is_empty_prove :
  \[] heap_empty.
Proof using. hnfs~. Qed.

Lemma heap_is_empty_st_prove : forall (P:Prop),
  P -> \[P] heap_empty.
Proof using. intros. hnfs~. Qed.

Hint Resolve heap_is_empty_prove heap_is_empty_st_prove.


(*------------------------------------------------------------------*)
(* ** Properties of heap single *)

Lemma heap_is_single_null : forall (l:loc) (f:field) A (v:A) h,
  heap_is_single l f v h -> l <> null.
Proof using. intros. destruct h as [m n]. unfolds* heap_is_single. Qed.

Lemma heap_is_single_null_eq_false : forall A (v:A) (f:field),
  heap_is_single null f v = \[False].
Proof using.
  intros. unfold heap_is_single.
  unfold hprop. extens. intros [m n].
  unfold heap_is_empty_st. autos*.
Qed.

Lemma heap_is_single_null_to_false : forall A (v:A) (f:field),
  heap_is_single null f v ==> \[False].
Proof using. introv Hh. forwards*: heap_is_single_null. Qed.

Global Opaque heap_is_empty_st heap_is_single.


(*------------------------------------------------------------------*)
(* ** Properties of [star] and [pack] *)

Section Star.
Transparent heap_is_star heap_union.

Lemma star_comm : comm heap_is_star.
Proof using.
  intros H1 H2. unfold hprop, heap_is_star. extens. intros h.
  iff (h1&h2&M1&M2&D&U); rewrite~ heap_union_comm in U; exists* h2 h1.
Qed.

Lemma star_neutral_l : neutral_l heap_is_star \[].
Proof using.
  intros H. unfold hprop, heap_is_star. extens. intros h.
  iff (h1&h2&M1&M2&D&U) M.
  hnf in M1. subst h1 h. rewrite~ heap_union_neutral_l.
  exists heap_empty h. splits~.
Qed.

Lemma star_neutral_r : neutral_r heap_is_star \[].
Proof using.
  apply neutral_r_of_comm_neutral_l.
  apply star_comm. apply star_neutral_l.
Qed.

Lemma star_assoc : LibOperation.assoc heap_is_star.
Proof using.
  intros H1 H2 H3. unfold hprop, heap_is_star. extens. intros h. split.
  intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
   exists (heap_union h1 h2) h3. rewrite heap_disjoint_union_eq_r in D.
   splits.
    exists h1 h2. splits*.
    auto.
    rewrite* heap_disjoint_union_eq_l.
    rewrite~ <- heap_union_assoc.
  intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
   exists h1 (heap_union h2 h3). rewrite heap_disjoint_union_eq_l in D.
   splits.
    auto.
    exists h2 h3. splits*.
    rewrite* heap_disjoint_union_eq_r.
    rewrite~ heap_union_assoc.
Qed. (* later: exploit symmetry in the proof *)

Lemma star_comm_assoc : comm_assoc heap_is_star.
Proof using.
  apply comm_assoc_of_comm_and_assoc. apply star_comm. apply star_assoc.
Qed.

Lemma starpost_neutral : forall B (Q:B->hprop),
  Q \*+ \[] = Q.
Proof using. extens. intros. (* unfold starpost. *) rewrite* star_neutral_r. Qed.

Lemma star_cancel : forall H1 H2 H2',
  H2 ==> H2' -> H1 \* H2 ==> H1 \* H2'.
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.

Lemma star_is_single_same_loc : forall (l:loc) A (v1 v2:A) (f:field),
  (heap_is_single l f v1) \* (heap_is_single l f v2) ==> \[False].
Proof using.
  Transparent heap_is_single state_single.
  intros. intros h ((m1&n1)&(m2&n2)&(E1&?&?)&(E2&?&?)&(D&?)&E).
  unfolds heap_disjoint, state_disjoint, prod_st2, pfun_disjoint.
  specializes D (l,f). rewrite E1, E2 in D.
  unfold state_single in D. simpls. case_if. destruct D; tryfalse.
Qed.

Lemma heap_star_prop_elim : forall (P:Prop) H h,
  (\[P] \* H) h -> P /\ H h.
Proof using.
  introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_neutral_l.
Qed.

Lemma heap_extract_prop : forall (P:Prop) H H',
  (P -> H ==> H') -> (\[P] \* H) ==> H'.
Proof using. introv W Hh. applys_to Hh heap_star_prop_elim. autos*. Qed.

Lemma heap_weaken_pack : forall A (x:A) H J,
  H ==> J x -> H ==> (heap_is_pack J).
Proof using. introv W h. exists x. apply~ W. Qed.


End Star.


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

Definition sep_monoid := monoid_make heap_is_star heap_is_empty.

Global Instance Monoid_sep : Monoid sep_monoid.
Proof using.
  constructor; simpl.
  apply star_assoc.
  apply star_neutral_l.
  apply star_neutral_r.
Qed.

Global Instance Comm_monoid_sep : Comm_monoid sep_monoid.
Proof using.
  constructor; simpl.
  applys Monoid_sep.
  apply star_comm.
Qed.


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

Hint Rewrite
  star_neutral_l star_neutral_r starpost_neutral : rew_heap.
Hint Rewrite <- star_assoc : rew_heap.

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

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

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


(*------------------------------------------------------------------*)
(* ** Properties of heap credits *)

Section Credits.
Transparent heap_is_credits
  heap_is_empty heap_is_empty_st heap_is_star heap_union heap_disjoint.

Definition pay_one H H' :=
  H ==> \$ 1 \* H'.

Lemma credits_zero_eq : \$ 0 = \[].
Proof using.
  unfold heap_is_credits, heap_is_empty, heap_empty.
  applys pred_ext_1. intros [m n]. iff [M1 M2] M.  (* todo: extens should work *)
    subst*.
    inverts* M.
Qed.

Lemma credits_split_eq : forall (n m : int),
  \$ (n+m) = \$ n \* \$ m.
Proof using.
  intros c1 c2. unfold heap_is_credits, heap_is_star, heap_union, heap_disjoint.
  applys pred_ext_1. intros [m n]. (* todo: extens should work *)
  iff [M1 M2] ([m1 n1]&[m2 n2]&(M1&E1)&(M2&E2)&M3&M4).
    exists (state_empty,c1) (state_empty,c2). simpl. splits*.
      autos* state_disjoint_empty_l.
      subst. rewrite* state_union_neutral_l.
    inverts M4. subst*.
Qed.

(* Used by xgc_credit *)
Lemma credits_le_rest : forall (n m : int), (* todo: move later, inverse hyp *)
  n <= m -> exists H', affine H' /\ \$ m ==> \$ n \* H'.
Proof using.
  introv M. exists (\$ (m - n)). rewrite <- credits_split_eq.
  math_rewrite (n + (m-n) = m).
  splits~.
  Local Transparent affine. unfold affine, heap_is_credits.
  intros (? & ?) (? & ?); subst. apply heap_affine_credits.
  math.
Qed.

Lemma credits_join_eq : forall x y,
  \$ x \* \$ y = \$(x+y).
Proof using.
  introv. unfold heap_is_credits.
  applys pred_ext_1. intros h. splits.
  { intros ([m1 c1] & [m2 c2] & ([? ?] & [? ?] & [[? ?] ?])).
    subst. unfold heap_union. simpl.
    rewrite state_union_neutral_r. splits~. }
  { destruct h as [m c]. intros (? & ?). subst.
    unfold heap_is_star.
    exists (state_empty, x) (state_empty, y).
    splits~.
    { unfold heap_disjoint. simpl.
      splits~. apply state_disjoint_empty_l. }
    { unfold heap_union. simpl.
      rewrite~ state_union_neutral_r. } }
 Qed.

Lemma credits_join_eq_rest : forall x y (H:hprop),
  \$ x \* \$ y \* H = \$(x+y) \* H.
Proof using.
  introv. rewrite star_assoc. rewrite~ credits_join_eq.
Qed.

End Credits.


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

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

Hint Rewrite credits_split_eq : credits_split_rew.

Ltac credits_split :=
  autorewrite with credits_split_rew.

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

Lemma credits_swap : forall x (H:hprop),
  H \* (\$ x) = (\$ x) \* H.
Proof using. intros. rewrite~ star_comm. Qed.


Ltac credits_join_in H :=
  match H with
  | \$ ?x \* \$ ?y => rewrite (@credits_join_eq x y)
  | \$ ?x \* \$ ?y \* ?H' => rewrite (@credits_join_eq_rest x y H')
  | _ \* ?H' => credits_join_in H'
  end.

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

Ltac credits_join_left_repeat tt :=
  repeat (credits_join_left_step tt).

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

Ltac credits_join_pre_repeat tt :=
  repeat (credits_join_pre_step tt).

Ltac credits_join_core :=
  match goal with
  | |- ?HL ==> ?HR => credits_join_left_repeat tt
  | |- _ => credits_join_pre_repeat tt
  end.

Tactic Notation "credits_join" :=
  credits_join_core.

(** Tactic [skip_credits] eliminates credits.
    Use this tactic only for development purposes *)

Axiom skip_credits : forall x, \$ x = \[]. (* only used by "skip_credits" tactic *)

Hint Rewrite skip_credits : rew_skip_credits.

Ltac skip_credits_core :=
  autorewrite with rew_skip_credits.

Tactic Notation "skip_credits" :=
  skip_credits_core.



(********************************************************************)
  (* ** Specification predicates for values *)

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

Notation "'~~' B" := (hprop->(B->hprop)->Prop)
  (at level 8, only parsing) : type_scope.

(** Type for imperative data structures *)

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

(** Label for imperative data structures *)

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

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

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

Hint Transparent hdata : affine.

(** Specification of pure functions:
    [pure F P] is equivalent to [F [] (fun x => [P x])] *)

Definition pure B (R:~~B) :=
  fun P => R \[] (fun r => \[P r]).

(** Specification of functions that keep their input:
    [keep F H Q] is equivalent to [F H (Q \*+ H)] *)

Notation "'keep' R H Q" :=
  (R H%h (Q \*+ H)) (at level 25, R at level 0, H at level 0, Q at level 0).

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



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

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

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

Class Heapdata a A (G:htype A a) := {
  heapdata : forall x y X Y,
    x ~> G X \* y ~> G Y ==>
    x ~> G X \* y ~> G Y \* \[x <> y] }.


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

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

Definition Id {A:Type} (X:A) (x:A) :=
  \[ X = x ].

(*------------------------------------------------------------------*)
(* ** Any *)

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

Definition Any {A:Type} (X:unit) (x:A) :=
  \[True].


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

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


(*------------------------------------------------------------------*)
(* ** Properties of [affine] *)

Section Affine.
Transparent affine.

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

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

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

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

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

Lemma affine_single : forall l f A (v:A),
  affine (heap_is_single l f v).
Proof.
  Transparent heap_is_single.
  intros. unfold affine, heap_is_single.
  intros (m & c). intros (? & ? & ?). subst.
  apply heap_affine_single.
Qed.

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

End Affine.

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

(* Split a [affine _] goal, following the base operators of the logic *)
Ltac affine_base :=
  repeat
    match goal with
    | |- affine (_ \* _) => apply affine_star
    | |- affine \[] => apply affine_empty
    | |- affine (\$ _) => apply affine_credits; auto with zarith
    | |- affine (\[_]) => apply affine_empty_st
    | |- affine \GC => apply affine_gc
    | |- affine (heap_is_pack _) => apply affine_pack
    end.

(* After using the rules for the standard operators of the logic with
[affine_base], try proving the remaining subgoals using the [affine] hint base.
*)
Ltac affine :=
  match goal with
  | |- affine _ => affine_base; try (typeclasses eauto with affine)
  end.


(********************************************************************)
(* ** [xunfold] tactics *)

Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) :=
  match number_to_nat K with
  | 1%nat => set (X := E) at 1
  | 2%nat => set (X := E) at 2
  | 3%nat => set (X := E) at 3
  | 4%nat => set (X := E) at 4
  | 5%nat => set (X := E) at 5
  | 6%nat => set (X := E) at 6
  | 7%nat => set (X := E) at 7
  | 8%nat => set (X := E) at 8
  | 9%nat => set (X := E) at 9
  | 10%nat => set (X := E) at 10
  | 11%nat => set (X := E) at 11
  | 12%nat => set (X := E) at 12
  | 13%nat => set (X := E) at 13
  | _ => fail "ltac_set: arity not supported"
  end.

(** [xunfold at n] unfold the definition of the arrow [~>]
    at the occurence [n] in the goal. *)

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

Tactic Notation "xunfold" "at" constr(n) :=
  let h := fresh "temp" in
  ltac_set (h := hdata) at n;
  change h with hdata';
  unfold hdata';
  clear h.

(** [xunfold_clean] simplifies instances of
   [p ~> (fun _ => _)] by unfolding the arrow,
   but only when the body does not captures
   locally-bound variables.
   TODO: deprecated *)

Tactic Notation "xunfold_clean" :=
  try match goal with |- context C [?p ~> ?E] =>
   match E with (fun _ => _) =>
     let E' := eval cbv beta in (E p) in
     let G' := context C [E'] in
     let G := match goal with |- ?G => G end in
     change G with G' end end.


(** [xunfold E] unfolds all occurences of the representation
    predicate [E].
    Limitation: won't work if E has more than 12 arguments.

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

Tactic Notation "xunfold" constr(E) :=
  change hdata with hdata';
  let h := fresh "temp" in
  set (h := hdata');
  repeat (
    unfold h at 1;
    let ok := match goal with
      | |- context [ hdata' (E) _ ] => constr:(true)
      | |- context [ hdata' (E _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _ _ _) _ ] => constr:(true)
      | |- context [ hdata' (E _ _ _ _ _ _ _) _ ] => constr:(true)