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)
      | |- 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)
      | _ => constr:(false)
      end in
    match ok with
    | true => unfold hdata'
    | false => change hdata' with hdata
    end);
  clear h;
  unfold E.


(** [xunfold E] unfolds a specific occurence of the representation
    predicate [E]. TODO: still needs to unfold [E] by hand. *)

Tactic Notation "xunfold" constr(E) "at" constr(n) :=
  let n := number_to_nat n in
  change hdata with hdata';
  let h := fresh "temp" in
  set (h := hdata');
  let E' := fresh "tempR" in
  set (E' := E);
  let rec aux n :=
    try (
      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)
        | |- 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)
        | _ => constr:(false)
        end in
      match ok with
      | true =>
         match n with
         | (S O)%nat =>
            unfold hdata'
         | (S ?n')%nat => change hdata' with hdata; aux n'
         end
      | false => change hdata' with hdata; aux n
      end)
     in
  aux n;
  unfold h;
  clear h;
  change hdata' with hdata;
  unfold E';
  clear E'.


(********************************************************************)
(* ** DEPRECATED  OLD XUNFOLD

  Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) :=
    match nat_from_number 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 7 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)
        | _ => constr:(false)
        end in
      match ok with
      | true => unfold hdata'
      | false => change hdata' with hdata
      end);
    clear h;
    unfold E.

  (** [xunfold E] unfolds a specific occurence of the representation
      predicate [E]. TODO: still needs to unfold [E] by hand. *)

  Tactic Notation "xunfold" constr(E) "at" constr(n) :=
    let n := nat_from_number n in
    change hdata with hdata';
    let h := fresh "temp" in
    set (h := hdata');
    let E' := fresh "tempR" in
    set (E' := E);
    let rec aux n :=
      try (
        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)
          | _ => constr:(false)
          end in
        match ok with
        | true =>
           match n with
           | (S O)%nat =>
              unfold hdata'
           | (S ?n')%nat => change hdata' with hdata; aux n'
           end
        | false => change hdata' with hdata; aux n
        end)
       in
    aux n;
    unfold h;
    clear h;
    change hdata' with hdata;
    unfold E';
    clear E'.
*)


(********************************************************************)
(* ** Other tactics *)

(********************************************************************)
(* ** Shared tactics *)

Ltac prepare_goal_hpull_himpl tt :=
  match goal with
  | |- @rel_incl' unit _ _ _ => let t := fresh "_tt" in intros t; destruct t
  | |- @rel_incl' _ _ _ _ => let r := fresh "r" in intros r
  | |- pred_incl _ _ => idtac
  end.

Ltac remove_empty_heaps_from H :=
  match H with context[ ?H1 \* \[] ] =>
    rewrite (@star_neutral_r H1) end.

Ltac remove_empty_heaps_left tt :=
  repeat match goal with |- ?H1 ==> _ => remove_empty_heaps_from H1 end.

Ltac remove_empty_heaps_right tt :=
  repeat match goal with |- _ ==> ?H2 => remove_empty_heaps_from H2 end.

Ltac on_formula_pre cont :=
  match goal with
  | |- _ ?H ?Q => cont H
  | |- _ _ ?H ?Q => cont H
  | |- _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ _ _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ _ _ _ _ _ ?H ?Q => cont H
  | |- _ _ _ _ _ _ _ _ _ _ ?H ?Q => cont H
  end.

Ltac on_formula_post cont :=
  match goal with
  | |- _ ?H ?Q => cont Q
  | |- _ _ ?H ?Q => cont Q
  | |- _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ _ _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ _ _ _ _ _ ?H ?Q => cont Q
  | |- _ _ _ _ _ _ _ _ _ _ ?H ?Q => cont Q
  end.

Ltac remove_empty_heaps_formula tt :=
  repeat (on_formula_pre ltac:(remove_empty_heaps_from)).


(********************************************************************)
(* ** Extraction from [H1] in [H1 ==> H2] *)

(** Lemmas *)

Lemma hpull_start : forall H H',
  \[] \* H ==> H' -> H ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hpull_stop : forall H H',
  H ==> H' -> H \* \[] ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hpull_keep : forall H1 H2 H3 H',
  (H2 \* H1) \* H3 ==> H' -> H1 \* (H2 \* H3) ==> H'.
Proof using. intros. rewrite (star_comm H2) in H. rew_heap in *. auto. Qed.

Lemma hpull_starify : forall H1 H2 H',
  H1 \* (H2 \* \[]) ==> H' -> H1 \* H2 ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hpull_assoc : forall H1 H2 H3 H4 H',
  H1 \* (H2 \* (H3 \* H4)) ==> H' -> H1 \* ((H2 \* H3) \* H4) ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hpull_prop : forall H1 H2 H' (P:Prop),
  (P -> H1 \* H2 ==> H') -> H1 \* (\[P] \* H2) ==> H'.
Proof using.
  introv W. intros h Hh.
  destruct Hh as (h1&h2'&?&(h2&h3&(?&?)&?&?&?)&?&?).
  apply~ W. exists h1 h3. subst h h2 h2'.
  rewrite heap_union_neutral_l in *. splits~.
Qed.

Lemma hpull_empty : forall H1 H2 H',
  (H1 \* H2 ==> H') -> H1 \* (\[] \* H2) ==> H'.
Proof using.
  introv W. intros h Hh. destruct Hh as (h1&h2'&?&(h2&h3&M&?&?&?)&?&?).
  apply~ W. inverts M. exists h1 h3. subst h h2'.
  rewrite heap_union_neutral_l in *. splits~.
Qed.

Lemma hpull_id : forall A (x X : A) H1 H2 H',
  (x = X -> H1 \* H2 ==> H') -> H1 \* (x ~> Id X \* H2) ==> H'.
Proof using. intros. unfold Id. apply~ hpull_prop. Qed.

Lemma hpull_exists : forall A H1 H2 H' (J:A->hprop),
  (forall x, H1 \* J x \* H2 ==> H') -> H1 \* (heap_is_pack J \* H2) ==> H'.
Proof using.
  introv W. intros h Hh.
  destruct Hh as (h1&h2'&?&(h2&h3&(?&?)&?&?&?)&?&?).
  applys~ W x. exists h1 (heap_union h2 h3). subst h h2'.
  splits~. exists h2 h3. splits~.
Qed.

(** Tactics *)

Ltac hpull_setup tt :=
  prepare_goal_hpull_himpl tt;
  lets: ltac_mark;
  apply hpull_start.

Ltac hpull_cleanup tt :=
  apply hpull_stop;
  remove_empty_heaps_left tt;
  tryfalse;
  gen_until_mark.

Ltac hpull_step tt :=
  match goal with |- _ \* ?HN ==> _ =>
  match HN with
  | ?H \* _ =>
     match H with
     | \[] => apply hpull_empty
     | \[_] => apply hpull_prop; intros
     | _ ~> Id _ => apply hpull_id; intros
     | heap_is_pack _ => apply hpull_exists; intros
     | _ \* _ => apply hpull_assoc
     | _ => apply hpull_keep
     end
  | \[] => fail 1
  | ?H => apply hpull_starify
  end end.

Ltac hpull_main tt :=
  hpull_setup tt;
  (repeat (hpull_step tt));
  hpull_cleanup tt.

Ltac hpull_post tt :=
  reflect_clean tt.

Ltac hpull_core :=
  hpull_main tt; hpull_post tt.

Ltac hpull_if_needed tt := (* deprecated  ==> see hpullable *)
  match goal with |- ?H ==> _ => match H with
  | context [ heap_is_pack _ ] => hpull_core
  | context [ _ ~> Id _ ] => hpull_core
  | context [ \[ _ ] ] => hpull_core
  end end.

Tactic Notation "hpull" :=
  hpull_core.
Tactic Notation "hpull" "as" simple_intropattern(I1) :=
  hpull; intros I1.
Tactic Notation "hpull" "as" simple_intropattern(I1) simple_intropattern(I2) :=
  hpull; intros I1 I2.
Tactic Notation "hpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) :=
  hpull; intros I1 I2 I3.
Tactic Notation "hpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) :=
  hpull; intros I1 I2 I3 I4.
Tactic Notation "hpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) :=
  hpull; intros I1 I2 I3 I4 I5.
Tactic Notation "hpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) :=
  hpull; intros I1 I2 I3 I4 I5 I6.
Tactic Notation "hpull" "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) :=
  hpull; intros I1 I2 I3 I4 I5 I6 I7.

Tactic Notation "hpulls" :=
  let E := fresh "TEMP" in hpull as E; subst_hyp E.


(********************************************************************)
(* ** Simplification in [H2] on [H1 ==> H2] *)

(** Hints *)

Inductive Hsimpl_hint : list Boxer -> Type :=
  | hsimpl_hint : forall (L:list Boxer), Hsimpl_hint L.

Ltac hsimpl_hint_put L :=
  let H := fresh "Hint" in
  generalize (hsimpl_hint L); intros H.

Ltac hsimpl_hint_next cont :=
  match goal with H: Hsimpl_hint ((boxer ?x)::?L) |- _ =>
    clear H; hsimpl_hint_put L; cont x end.

Ltac hsimpl_hint_remove tt :=
  match goal with H: Hsimpl_hint _ |- _ => clear H end.


(** Lemmas *)

Lemma hsimpl_start : forall H' H1,
  H' ==> \[] \* H1 -> H' ==> H1.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hsimpl_stop : forall H' H1,
  H' ==> H1 -> H' ==> H1 \* \[].
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hsimpl_keep : forall H' H1 H2 H3,
  H' ==> (H2 \* H1) \* H3 -> H' ==> H1 \* (H2 \* H3).
Proof using. intros. rewrite (star_comm H2) in H. rew_heap in *. auto. Qed.

Lemma hsimpl_assoc : forall H' H1 H2 H3 H4,
  H' ==> H1 \* (H2 \* (H3 \* H4)) -> H' ==> H1 \* ((H2 \* H3) \* H4).
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hsimpl_starify : forall H' H1 H2,
  H' ==> H1 \* (H2 \* \[]) -> H' ==> H1 \* H2.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hsimpl_empty : forall H' H1 H2,
  H' ==> H1 \* H2 -> H' ==> H1 \* (\[] \* H2).
Proof using.
  introv W PH1. destruct (W _ PH1) as (h1&h2&?&?&?&?).
  exists h1 h2. splits~. exists heap_empty h2. splits~.
Qed.

Lemma hsimpl_prop : forall H' H1 H2 (P:Prop),
  H' ==> H1 \* H2 -> P -> H' ==> H1 \* (\[P] \* H2).
Proof using.
  introv W HP PH1. destruct (W _ PH1) as (h1&h2&?&?&?&?).
  exists h1 h2. splits~. exists heap_empty h2. splits~.
Qed.

Lemma hsimpl_id : forall A (x X : A) H' H1 H2,
  H' ==> H1 \* H2 -> x = X -> H' ==> H1 \* (x ~> Id X \* H2).
Proof using. intros. unfold Id. apply~ hsimpl_prop. Qed.

Lemma hsimpl_id_unify : forall A (x : A) H' H1 H2,
  H' ==> H1 \* H2 -> H' ==> H1 \* (x ~> Id x \* H2).
Proof using. intros. apply~ hsimpl_id. Qed.

Lemma hsimpl_exists : forall A (x:A) H' H1 H2 (J:A->hprop),
  H' ==> H1 \* J x \* H2 -> H' ==> H1 \* (heap_is_pack J \* H2).
Proof using.
  introv W. intros h' PH'. destruct (W _ PH') as (h2&h4&?&(hx&h3&?&?&?&?)&?&?).
  exists h2 (heap_union hx h3). subst h' h4. splits~.
  exists hx h3. splits~. exists~ x.
Qed.

Lemma hsimpl_gc : forall H,
  affine H ->
  H ==> \GC.
Proof using.
  Local Transparent affine heap_is_gc.
  introv HA. unfold heap_is_gc, pred_incl.
  intros h Hh. unfold affine in HA.
  splits~. eauto.
Qed.

Lemma hsimpl_cancel_1 : forall H HA HR HT,
  HT ==> HA \* HR -> H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite star_comm_assoc. apply~ star_cancel. Qed.

Lemma hsimpl_cancel_2 : forall H HA HR H1 HT,
  H1 \* HT ==> HA \* HR ->
  H1 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_1. Qed.

Lemma hsimpl_cancel_3 : forall H HA HR H1 H2 HT,
  H1 \* H2 \* HT ==> HA \* HR -> H1 \* H2 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_2. Qed.

Lemma hsimpl_cancel_4 : forall H HA HR H1 H2 H3 HT,
  H1 \* H2 \* H3 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_3. Qed.

Lemma hsimpl_cancel_5 : forall H HA HR H1 H2 H3 H4 HT,
  H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_4. Qed.

Lemma hsimpl_cancel_6 : forall H HA HR H1 H2 H3 H4 H5 HT,
  H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_5. Qed.

Lemma hsimpl_cancel_7 : forall H HA HR H1 H2 H3 H4 H5 H6 HT,
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_6. Qed.

Lemma hsimpl_cancel_8 : forall H HA HR H1 H2 H3 H4 H5 H6 H7 HT,
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_7. Qed.

Lemma hsimpl_cancel_9 : forall H HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT,
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_8. Qed.

Lemma hsimpl_cancel_10 : forall H HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* H \* HT ==> HA \* (H \* HR).
Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_9. Qed.


Lemma hsimpl_cancel_credits_1 : forall (n m : int) HA HR HT,
  \$ (n - m) \* HT ==> HA \* HR ->
  \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using.
  introv E. math_rewrite (n = (n - m) + m).
  rewrite credits_split_eq. rewrite <- star_assoc.
  applys~ hsimpl_cancel_2.
Qed.

Lemma hsimpl_cancel_credits_2 : forall (n m : int) HA HR H1 HT,
  \$ (n - m) \* H1 \* HT ==> HA \* HR ->
  H1 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using.
  intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_1.
Qed.

Lemma hsimpl_cancel_credits_3 : forall (n m : int) HA HR H1 H2 HT,
  \$ (n - m) \* H1 \* H2 \* HT ==> HA \* HR ->
  H1 \* H2 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_2. Qed.

Lemma hsimpl_cancel_credits_4 : forall (n m : int) HA HR H1 H2 H3 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_3. Qed.

Lemma hsimpl_cancel_credits_5 : forall (n m : int) HA HR H1 H2 H3 H4 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_4. Qed.

Lemma hsimpl_cancel_credits_6 : forall (n m : int) HA HR H1 H2 H3 H4 H5 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_5. Qed.

Lemma hsimpl_cancel_credits_7 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_6. Qed.

Lemma hsimpl_cancel_credits_8 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_7. Qed.

Lemma hsimpl_cancel_credits_9 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_8. Qed.

Lemma hsimpl_cancel_credits_10 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
  \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \$ n \* HT ==> HA \* (\$ m \* HR).
Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_9. Qed.


Lemma hsimpl_cancel_eq_1 : forall H H' HA HR HT,
  H = H' -> HT ==> HA \* HR -> H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_1. Qed.

Lemma hsimpl_cancel_eq_2 : forall H H' HA HR H1 HT,
  H = H' -> H1 \* HT ==> HA \* HR ->
  H1 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_2. Qed.

Lemma hsimpl_cancel_eq_3 : forall H H' HA HR H1 H2 HT,
  H = H' -> H1 \* H2 \* HT ==> HA \* HR ->
  H1 \* H2 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_3. Qed.

Lemma hsimpl_cancel_eq_4 : forall H H' HA HR H1 H2 H3 HT,
  H = H' -> H1 \* H2 \* H3 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_4. Qed.

Lemma hsimpl_cancel_eq_5 : forall H H' HA HR H1 H2 H3 H4 HT,
  H = H' -> H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_5. Qed.

Lemma hsimpl_cancel_eq_6 : forall H H' HA HR H1 H2 H3 H4 H5 HT,
  H = H' -> H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_6. Qed.

Lemma hsimpl_cancel_eq_7 : forall H H' HA HR H1 H2 H3 H4 H5 H6 HT,
  H = H' -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_7. Qed.

Lemma hsimpl_cancel_eq_8 : forall H H' HA HR H1 H2 H3 H4 H5 H6 H7 HT,
  H = H' -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_8. Qed.

Lemma hsimpl_cancel_eq_9 : forall H H' HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT,
  H = H' -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_9. Qed.

Lemma hsimpl_cancel_eq_10 : forall H H' HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT,
  H = H' -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* H \* HT ==> HA \* (H' \* HR).
Proof using. intros. subst. apply~ hsimpl_cancel_10. Qed.

Lemma hsimpl_start_1 : forall H1 H',
  H1 \* \[] ==> H' -> H1 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed.

Lemma hsimpl_start_2 : forall H1 H2 H',
  H1 \* H2 \* \[] ==> H' ->
  H1 \* H2 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed.

Lemma hsimpl_start_3 : forall H1 H2 H3 H',
  H1 \* H2 \* H3 \* \[] ==> H' ->
  H1 \* H2 \* H3 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed.

Lemma hsimpl_start_4 : forall H1 H2 H3 H4 H',
  H1 \* H2 \* H3 \* H4 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)

Lemma hsimpl_start_5 : forall H1 H2 H3 H4 H5 H',
  H1 \* H2 \* H3 \* H4 \* H5 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 \* H5 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)

Lemma hsimpl_start_6 : forall H1 H2 H3 H4 H5 H6 H',
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)

Lemma hsimpl_start_7 : forall H1 H2 H3 H4 H5 H6 H7 H',
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)

Lemma hsimpl_start_8 : forall H1 H2 H3 H4 H5 H6 H7 H8 H',
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)

Lemma hsimpl_start_9 : forall H1 H2 H3 H4 H5 H6 H7 H8 H9 H',
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)

Lemma hsimpl_start_10 : forall H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H',
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* H10 \* \[] ==> H' ->
  H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* H10 ==> H'.
Proof using. intros. rew_heap in H. auto. Qed. (* slow *)


(** Tactics *)

Ltac hsimpl_left_empty tt :=
  match goal with |- ?HL ==> _ =>
  match HL with
  | \[] => idtac
  | _ \* \[] => idtac
  | _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \[] => idtac
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H => apply hsimpl_start_10
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H => apply hsimpl_start_9
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H => apply hsimpl_start_8
  | _ \* _ \* _ \* _ \* _ \* _ \* ?H => apply hsimpl_start_7
  | _ \* _ \* _ \* _ \* _ \* ?H => apply hsimpl_start_6
  | _ \* _ \* _ \* _ \* ?H => apply hsimpl_start_5
  | _ \* _ \* _ \* ?H => apply hsimpl_start_4
  | _ \* _ \* ?H => apply hsimpl_start_3
  | _ \* ?H => apply hsimpl_start_2
  | ?H => apply hsimpl_start_1
  end end.


Ltac check_arg_true v :=
  match v with
  | true => idtac
  | false => fail 1
  end.

Ltac hsimpl_setup process_credits :=
  prepare_goal_hpull_himpl tt;
  try (check_arg_true process_credits; credits_join_left_repeat tt);
  hsimpl_left_empty tt;
  apply hsimpl_start.

Ltac hsimpl_cleanup tt :=
  try apply hsimpl_stop;
  try apply hsimpl_stop;
  try apply pred_incl_refl;
  try hsimpl_hint_remove tt;
  try remove_empty_heaps_right tt;
  try remove_empty_heaps_left tt;
  try apply hsimpl_gc;
  try affine.

Ltac hsimpl_try_same tt :=
  first
  [ apply hsimpl_cancel_1
  | apply hsimpl_cancel_2
  | apply hsimpl_cancel_3
  | apply hsimpl_cancel_4
  | apply hsimpl_cancel_5
  | apply hsimpl_cancel_6
  | apply hsimpl_cancel_7
  | apply hsimpl_cancel_8
  | apply hsimpl_cancel_9
  | apply hsimpl_cancel_10
  ].

Ltac hsimpl_find_same H HL :=
  match HL with
  | ?H' \* _ => unify H H'; apply hsimpl_cancel_1
  | _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_2
  | _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_3
  | _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_4
  | _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_5
  | _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_6
  | _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_7
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_8
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_9
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* ?H' \* _ => unify H H'; apply hsimpl_cancel_10
  end.

Ltac hsimpl_find_data l HL cont :=
  match HL with
  | hdata _ l \* _ => apply hsimpl_cancel_eq_1
  | _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_2
  | _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_3
  | _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_4
  | _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_5
  | _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_6
  | _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_7
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_8
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_9
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_10
  end; [ cont tt | ].

Ltac hsimpl_find_credits HL :=
  match HL with
  | \$ _ \* _ => apply hsimpl_cancel_credits_1
  | _ \* \$ _ \* _ => apply hsimpl_cancel_credits_2
  | _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_3
  | _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_4
  | _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_5
  | _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_6
  | _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_7
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_8
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_9
  | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_10
  end.

Ltac hsimpl_extract_exists tt :=
  first [
    hsimpl_hint_next ltac:(fun x =>
      match x with
      | __ => eapply hsimpl_exists
      | _ => apply (@hsimpl_exists _ x)
      end)
  | eapply hsimpl_exists ].

Ltac hsimpl_find_data_post tt :=
  try solve
   [ reflexivity
   | fequal; fequal; first [ eassumption | symmetry; eassumption ] ];
  try match goal with |- hdata ?X ?l = hdata ?Y ?l => match constr:((X,Y)) with
  | (?F1 _, ?F1 _) => fequal; fequal
  | (?F1 ?F2 _, ?F1 ?F2 _) => fequal; fequal
  | (?F1 ?F2 ?F3 _, ?F1 ?F2 ?F3 _) => fequal; fequal
  | (?F1 ?F2 ?F3 ?F4 _, ?F1 ?F2 ?F3 ?F4 _) => fequal; fequal
  | (?F1 ?F2 ?F3 ?F4 ?F5 _, ?F1 ?F2 ?F3 ?F4 ?F5 _) => fequal; fequal
  | (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 _) => fequal; fequal
  | (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 _) => fequal; fequal
  | (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 _) => fequal; fequal
  | (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 ?F9 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 ?F9 _) => fequal; fequal
  end end.

(* todo: better implemented in cps style ? *)


(** Maintain the goal in the form
     H1 \* ... \* HN \* [] ==> HA \* HR
   where HA is initially empty and accumulates elements not simplifiable
   and HR contains the values that are to be cancelled out;
   the last item of HR is always a [].
   As long as HR is of the form H \* H', we try to match H with one of the Hi.
  *)

Ltac check_noevar2 M := (* todo: merge *)
  first [ has_evar M; fail 1 | idtac ].

(* deprecated
  match goal with |- ?HL ==> ?HA \* ?HN =>
  match HN with
  | ?H \* _ =>
    match H with
    | \[] => apply hsimpl_empty
    | \[_] => apply hsimpl_prop
    | heap_is_pack _ => hsimpl_extract_exists tt
    | _ \* _ => apply hsimpl_assoc
    | heap_is_single _ _ _ => hsimpl_try_same tt
    | Group _ _ => hsimpl_try_same tt
    | ?H => check_noevar2 H; hsimpl_find_same H HL
    | hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post)
    | ?x ~> Id _ => check_noevar2 x; apply hsimpl_id
    | ?x ~> ?T _ => check_noevar2 x;
                    let M := fresh in assert (M: T = Id); [ reflexivity | clear M ];
                    apply hsimpl_id; [ | reflexivity ]
    | ?x ~> ?T ?X => check_noevar2 x; is_evar T; is_evar X; apply hsimpl_id_unify
    | _ => apply hsimpl_keep
    end
  | \[] => fail 1
  | _ => apply hsimpl_starify
  end end.
*)

Ltac check_noevar3 M := (* todo: rename *)
  first [ is_evar M; fail 1 | idtac ].

Ltac hsimpl_hook H := fail.


Ltac hsimpl_step process_credits :=
  match goal with |- ?HL ==> ?HA \* ?HN =>
  match HN with
  | ?H \* _ =>
    match H with
    | ?H => hsimpl_hook H
    | \[] => apply hsimpl_empty
    | \[_] => apply hsimpl_prop
    | heap_is_pack _ => hsimpl_extract_exists tt
    | _ \* _ => apply hsimpl_assoc
    | heap_is_single _ _ _ => hsimpl_try_same tt
    | Group _ _ => hsimpl_try_same tt  (* may fail *)
    | ?H => (* should be check_noevar3 on the next line TODO *)
       first [ is_evar H; fail 1 | idtac ];
       hsimpl_find_same H HL (* may fail *)
    | \$ _ => check_arg_true process_credits; hsimpl_find_credits HL
    | hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *)
    | ?x ~> Id _ => check_noevar2 x; apply hsimpl_id (* may fail *)
    | ?x ~> ?T _ => check_noevar2 x;
                    let M := fresh in assert (M: T = Id); [ reflexivity | clear M ];
                    apply hsimpl_id; [ | reflexivity ]
                    (* may fail *)
    | ?x ~> ?T ?X => check_noevar2 x; is_evar T; is_evar X; apply hsimpl_id_unify
    | _ => apply hsimpl_keep
    end
  | \[] => fail 1
  | _ => apply hsimpl_starify
  end end.

(* TODO: factorize the logging version of the code with the normal code *)
Ltac hsimpl_step_debug process_credits :=
  match goal with |- ?HL ==> ?HA \* ?HN =>
idtac HN;
  match HN with
  | ?H \* _ =>
    match H with
    | \[] => apply hsimpl_empty
    | \[_] => apply hsimpl_prop
    | heap_is_pack _ => hsimpl_extract_exists tt
    | _ \* _ => idtac "sep"; apply hsimpl_assoc
    | heap_is_single _ _ _ => hsimpl_try_same tt
    | Group _ _ => hsimpl_try_same tt  (* may fail *)
    | ?H => idtac "find";
        first [ has_evar H; idtac "has evar"; fail 1 | idtac "has no evar" ];
         hsimpl_find_same H HL (* may fail *)
    | \$ _ => check_arg_true process_credits; idtac "credits"; hsimpl_find_credits HL
    | hdata _ ?l => idtac "hdata"; hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *)
    | ?x ~> Id _ => idtac "id";  check_noevar x; apply hsimpl_id (* todo: why is this requiring a fail 2 ? *)
    | ?x ~> _ _ => idtac "some";  check_noevar2 x; apply hsimpl_id_unify
    | ?X => idtac "keep"; apply hsimpl_keep
    end
  | \[] => fail 1
  | _ => idtac "starify"; apply hsimpl_starify
  end end.

Ltac hsimpl_main process_credits :=
  hsimpl_setup process_credits;
  (repeat (hsimpl_step process_credits));
  hsimpl_cleanup tt.

(* todo: rename hsimpl into hcancel above *)

Tactic Notation "hcancel" :=
  hsimpl_main false.
Tactic Notation "hcancel" constr(L) :=
  match type of L with
  | list Boxer => hsimpl_hint_put L
  | _ => hsimpl_hint_put (boxer L :: nil)
  end; hcancel.

Ltac hpull_and_hcancel tt :=
  hpull; intros; hcancel.

Tactic Notation "hsimpl" := hpull_and_hcancel tt.
Tactic Notation "hsimpl" "~" := hsimpl; auto_tilde.
Tactic Notation "hsimpl" "*" := hsimpl; auto_star.
Tactic Notation "hsimpl" constr(L) :=
  match type of L with
  | list Boxer => hsimpl_hint_put L
  | _ => hsimpl_hint_put (boxer L :: nil)
  end; hsimpl.
Tactic Notation "hsimpl" constr(X1) constr(X2) :=
  hsimpl (>> X1 X2).
Tactic Notation "hsimpl" constr(X1) constr(X2) constr(X3) :=
  hsimpl (>> X1 X2 X3).

Tactic Notation "hsimpl" "~" constr(L) :=
  hsimpl L; auto_tilde.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) :=
  hsimpl X1 X2; auto_tilde.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) :=
  hsimpl X1 X2 X3; auto_tilde.

Tactic Notation "hsimpl" "*" constr(L) :=
  hsimpl L; auto_star.
Tactic Notation "hsimpl" "*" constr(X1) constr(X2) :=
  hsimpl X1 X2; auto_star.
Tactic Notation "hsimpl" "*" constr(X1) constr(X2) constr(X3) :=
  hsimpl X1 X2 X3; auto_star.

(** [hsimpls] is the same as [hsimpl; subst] *)

Tactic Notation "hsimpls" :=
  hsimpl; subst.
Tactic Notation "hsimpls" "~" :=
  hsimpls; auto_tilde.
Tactic Notation "hsimpls" "*" :=
  hsimpls; auto_star.

Tactic Notation "hsimpls" constr(L) :=
  hsimpl L; subst.
Tactic Notation "hsimpls" "~" constr(L) :=
  hsimpls L; auto_tilde.
Tactic Notation "hsimpls" "*" constr(L) :=
  hsimpls L; auto_star.

(** [hsimpl_credits] is the same as [hsimpl] excepts that it tries
    to perform arithmetic to simplify credits. Note: to execute
    [hsimpl_credits L], run [hsimpl L] first, then [hsimpl_credits]. *)

Ltac hsimpl_credits_core :=
  hpull; intros; hsimpl_main true.

Tactic Notation "hsimpl_credits" :=
  hsimpl_credits_core.
Tactic Notation "hsimpl_credits" "~" :=
  hsimpl_credits_core; auto_tilde.
Tactic Notation "hsimpl_credits" "*" :=
  hsimpl_credits_core; auto_star.




(********************************************************************)
(* ** xunfold+hsimpl *)

Tactic Notation "xunfolds" constr(E) :=
  xunfold E; hsimpl.
Tactic Notation "xunfolds" "~" constr(E) :=
  xunfolds E; auto_tilde.
Tactic Notation "xunfolds" "*" constr(E) :=
  xunfolds E; auto_star.



(********************************************************************)
(* ** credits_split + hsimpl *)

(* DEPRECATED *)

Tactic Notation "chsimpl" := credits_split; hsimpl.
Tactic Notation "chsimpl" "~" := chsimpl; auto_tilde.
Tactic Notation "chsimpl" "*" := chsimpl; auto_star.


(********************************************************************)
(* ** Other stuff *)

Lemma heap_weaken_star : forall H1' H1 H2 H3,
  (H1 ==> H1') -> (H1' \* H2 ==> H3) -> (H1 \* H2 ==> H3).
Proof using.
  introv W M (h1&h2&N). unpack N. apply M. exists~ h1 h2.
Qed. (* todo: move *)

Lemma hsimpl_to_qunit : forall (H:hprop) (Q:unit->hprop),
  Q = (fun _ => H) ->
  H ==> Q tt.
Proof using. intros. subst. auto. Qed. (* todo: needed? *)
Hint Resolve hsimpl_to_qunit.


(*------------------------------------------------------------------*)
(* ** Tactic [hpullable] *)

(** Include one of the following definitions to activate/deactivate
    the checking of extractible existentials and facts from
    pre-conditions:
      Ltac hpullable_activate tt ::= constr:(true).
      Ltac hpullable_activate tt ::= constr:(true).
    *)

Ltac hpullable_activate tt :=
  constr:(true).

(** Raises an error indicating the need to extract information *)

Ltac hpullable_error tt :=
  fail 100 "need to first call xpull.".

(** [hpullable_rec H] raises an error if the heap predicate [H]
    contains existentials or non-empty pure facts. *)

Ltac hpullable_rec H :=
  let rec_after_simpl tt :=
    let H' := eval simpl in H in
     match H' with
     | H => hpullable_error tt
     | _ => hpullable_rec H'
     end
  in
  match H with
  | \[] => idtac
  | \[_ = _ :> unit] => idtac
  | \[_] => hpullable_error tt
  | Hexists _,_ => hpullable_error tt
  | ?H1 \* ?H2 =>
     hpullable_rec H1;
     hpullable_rec H2
  | (fun _ => _) _ => rec_after_simpl tt
  | (let _ := _ in _) => rec_after_simpl tt
  | (let '(_,_) := _ in _) => rec_after_simpl tt
  | _ => idtac
  end.

(** [hpullable tt] applies to a goal of the form (H ==> H')
    and raises an error if [H] contains extractible quantifiers
    or facts *)

Ltac hpullable tt :=
  match goal with |- ?H ==> ?H' => hpullable_rec H end.


(*------------------------------------------------------------------*)
(* ** Tactic [hchange] *)

Lemma hchange_lemma : forall H1 H1' H H' H2,
  (H1 ==> H1') -> (H ==> H1 \* H2) -> (H1' \* H2 ==> H') -> (H ==> H').
Proof using.
  intros. applys* (@pred_incl_trans heap) (H1 \* H2).
  applys* (@pred_incl_trans heap) (H1' \* H2). hsimpl~.
Qed.

Ltac hchange_apply L cont1 cont2 :=
  eapply hchange_lemma;
    [ applys L | cont1 tt | cont2 tt ].

Ltac hchange_forwards L modif cont1 cont2 :=
  forwards_nounfold_then L ltac:(fun K =>
  match modif with
  | __ =>
     match type of K with
     | _ = _ => hchange_apply (@pred_incl_proj1 _ _ _ K) cont1 cont2
     | _ => hchange_apply K cont1 cont2
     end
  | _ => hchange_apply (@modif _ _ _ K) cont1 cont2
  end).

Ltac hcancel_cont tt :=
  instantiate; hcancel.
Ltac hsimpl_cont tt :=
  instantiate; hsimpl.

Ltac hchange_core E modif cont1 cont2 :=
  hpull; intros;
  match E with
  (*  | ?H ==> ?H' => hchange_with_core H H' --todo*)
  | _ => hchange_forwards E modif ltac:(cont1) ltac:(cont2)
  end.

Ltac hchange_debug_base E modif :=
  hchange_forwards E modif ltac:(idcont) ltac:(idcont).

Tactic Notation "hchange_debug" constr(E) :=
  hchange_debug_base E __.
Tactic Notation "hchange_debug" "->" constr(E) :=
  hchange_debug_base E pred_incl_proj1.
Tactic Notation "hchange_debug" "<-" constr(E) :=
  hchange_debug_base pred_incl_proj2.

Ltac hchange_base E modif :=
  hchange_core E modif ltac:(hcancel_cont) ltac:(idcont).

Tactic Notation "hchange" constr(E) :=
  hchange_base E __.
Tactic Notation "hchange" "->" constr(E) :=
  hchange_base E pred_incl_proj1.
Tactic Notation "hchange" "<-" constr(E) :=
  hchange_base E pred_incl_proj2.

Tactic Notation "hchange" "~" constr(E) :=
  hchange E; auto_tilde.
Tactic Notation "hchange" "*" constr(E) :=
  hchange E; auto_star.

Ltac hchanges_base E modif :=
  hchange_core E modif ltac:(hcancel_cont) ltac:(hsimpl_cont).

Tactic Notation "hchanges" constr(E) :=
  hchanges_base E __.
Tactic Notation "hchanges" "->" constr(E) :=
  hchanges_base E pred_incl_proj1.
Tactic Notation "hchange" "<-" constr(E) :=
  hchanges_base E pred_incl_proj2.

Tactic Notation "hchanges" "~" constr(E) :=
  hchanges E; auto_tilde.
Tactic Notation "hchanges" "*" constr(E) :=
  hchanges E; auto_star.

Tactic Notation "hchange" constr(E1) constr(E2) :=
  hchange E1; hchange E2.
Tactic Notation "hchange" constr(E1) constr(E2) constr(E3) :=
  hchange E1; hchange E2 E3.


(********************************************************************)
(* ** Additional lemmas about heap entailment *)

Lemma hsimpl_absurd : forall H (P:Prop),
  (~ P -> H ==> \[False]) ->
  H ==+> \[P].
Proof using. introv M. tests: P. { hsimpl~. } { hchange~ M. hpull. } Qed.


(********************************************************************)
(* ** Properties of Heap_data *)

Lemma Heapdata_prove : forall a A (G:htype A a),
  (forall x X1 X2, x ~> G X1 \* x ~> G X2 ==> \[False]) ->
  Heapdata G.
Proof using.
  introv H. constructors. intros x y X Y. tests: (x = y).
    hchanges (>> H y X Y).
    hsimpl~.
Qed.

Lemma Heapdata_false : forall a A (G:htype A a) x X1 X2,
  Heapdata G ->
  x ~> G X1 \* x ~> G X2 ==> \[False].
Proof using. introv H. hchanges (>> heapdata x x X1 X2). Qed.


(********************************************************************)
(* ** Properties of groups *)

(* LATER: attach the finiteness property to the Group predicate *)


Lemma Group_create:
  forall a A (G : htype A a),
  \[] ==> Group G \{}.
Proof using.
  intros. unfold Group. hsimpl.
  rewrite LibMap.fold_empty. simple*.
  unfolds. rewrite dom_empty. applys finite_empty.
Qed. (* todo: cleanup set proofs *)

(* LATER: could do without `{Inhab A} *)
Lemma Group_add_fresh : forall a (x:a) A `{Inhab A} (M:map a A) (G:htype A a) X,
  Heapdata G ->
  Group G M \* (x ~> G X) ==> Group G (M[x:=X]) \* \[x \notindom M].
Proof using.
  intros. tests: (x \indom M).
  (* case in *)
  match goal with |- _ ==> ?X => generalize X as R; intros end.
  unfold Group. hpull as F.
  rewrite (eq_union_restrict_remove_one C).
  rewrite~ LibMap.fold_union.
    simpl. rewrite LibMap.fold_single.
      hchange~ (>> Heapdata_false x). hsimpl.
      typeclass.
    typeclass.
    unfolds. rewrite dom_remove. applys~ finite_remove.
    unfolds. rewrite dom_single. applys finite_single.
    rewrite LibMap.disjoint_eq_disjoint_dom. rewrite dom_single.
     rewrite dom_remove. rewrite disjoint_single_r_eq.
     unfold notin. rewrite in_remove_eq.
     rewrite notin_single_eq. rew_logic*.
  (* case notin *)
  intros. unfold Group. hpull as F.
  rewrite LibMap.update_eq_union_single.
  rewrite~ LibMap.fold_union.
    simpl. rewrite~ LibMap.fold_single.
      hsimpl. applys C.
      unfolds. rewrite dom_union. applys~ finite_union.
       rewrite dom_single. applys finite_single.
      typeclass.
      typeclass.
    unfolds. rewrite dom_single. applys finite_single.
    rewrite LibMap.disjoint_eq_disjoint_dom. rewrite dom_single.
     rewrite disjoint_single_r_eq. auto.
Qed. (* todo: factorize proof better, improve set manipulations *)

(* LATER: could do without `{Inhab A} *)
Lemma Group_add : forall a (x:a) A `{Inhab A} (M:map a A) (G:htype A a) X,
  Heapdata G ->
  Group G M \* (x ~> G X) ==> Group G (M[x:=X]).
Proof using.
  intros. hchange~ Group_add_fresh. hsimpl.
Qed.

(* LATER: prove reciprocal to Group_add
   when x notin M, using Group rem lemma*)

Arguments Group_add [a] x [A].

Lemma Group_rem : forall a (x:a) A (IA:Inhab A) (M:map a A) (G:htype A a),
  x \indom M ->
  Group G M = Group G (M \- \{x}) \* (x ~> G (M[x])).
Proof using.
  intros. unfold Group.
  forwards~ E: LibMap.eq_union_restrict_remove_one x M.
  asserts: (LibMap.finite (x \:= M[x])).
    unfolds. rewrite dom_single. applys finite_single.
  asserts: (M \-- x \# x \:= M[x]).
    rewrite LibMap.disjoint_eq_disjoint_dom. rewrite dom_single.
     rewrite dom_remove. rewrite disjoint_single_r_eq.
     unfold notin. rewrite in_remove_eq.
     rewrite notin_single_eq. rew_logic*.
  applys pred_incl_antisym.
  (* left to right *)
  hpull as F.
  asserts: (LibMap.finite (M \-- x)).
    unfolds. rewrite dom_remove. applys~ finite_remove.
  rewrite E at 1.
  rewrite~ LibMap.fold_union.
    rewrite~ LibMap.fold_single.
      simpl. hsimpl. auto.
      typeclass.
    typeclass.
  (* right to left *)
  hpull as F.
  asserts: (LibMap.finite M).
    lets R: F. unfolds in R. rewrite dom_remove in R.
    lets: finite_remove_one_inv R. auto.
  rewrite E at 3.
  rewrite~ LibMap.fold_union.
    rewrite~ LibMap.fold_single.
      simpl. hsimpl. auto.
      typeclass.
    typeclass.
Qed. (* todo: cleanup and factorize with earlier proofs *)

Arguments Group_rem [a] x [A] {IA}.

Lemma Group_add' : forall a (x:a) A {IA:Inhab A} (M:map a A) (G:htype A a) X,
  x \indom M ->
  Group G (M \- \{x}) \* (x ~> G X) = Group G (M[x:=X]).
Proof using.
  intros. rewrite~ (Group_rem x (M[x:=X])).
  rewrite LibMap.read_update_same. rewrite~ LibMap.remove_one_update.
  rewrite dom_update. set_prove.
Qed.

Arguments Group_add' [a] x [A] {IA}.

Lemma Group_star_disjoint : forall a A `{Inhab A} (G : htype A a) (M1 M2 : map a A),
  Heapdata G ->
  (Group G M1 \* Group G M2) ==+> \[ M1 \# M2 ].
Proof.
  introv IA HG. applys hsimpl_absurd ;=> D.
  rewrite~ LibMap.disjoint_eq_disjoint_dom in D.
  rewrite disjoint_not_eq in D.
  destruct D as (x&D1&D2).
  hchange* (>> Group_rem x M1).
  hchange* (>> Group_rem x M2).
  hchange (heapdata x x). hpull.
Qed.
(* LATER: above, add instance of disjoint_eq on MAP, to avoid
   the rewrite disjoint_def step. *)

(* LATER: hypothesis [Inhab A] should not be needed; see LibMap.fold_union. *)
Lemma Group_join : forall a A `{Inhab A} (G : htype A a) (M1 M2 : map a A),
  Heapdata G ->
  Group G M1 \* Group G M2 ==>
  Group G (M1 \u M2) \* \[ M1 \# M2 ].
Proof.
  introv IA HG. hchange~ (>> Group_star_disjoint M1 M2). hpull ;=> D.
  unfold Group. hpull ;=> F1 F2.
  hint Comm_monoid_sep.
  rewrite~ LibMap.fold_union. simpl. hsimpl.
  { auto. }
  { (* LATER: LibMap.finite_union lemma (or typeclass) *)
    unfold LibMap.finite. rewrite dom_union. apply~ finite_union. }
Qed.

(* LATER
Lemma Group_split : forall a A (R : htype A a) (M1 M2 : map a A),
  dom M1 \# dom M2 ->
  Group R (M1 \u M2) ==> Group R M1 \* Group R M2.
*)


(********************************************************************)
(* ** Locality *)

(*------------------------------------------------------------------*)
(* ** Definition of [local] *)

(** "Local" = Frame rule + consequence rule + garbage collection *)

Definition local B (F:~~B) : ~~B :=
  fun (H:hprop) (Q:B->hprop) =>
    forall h, H h -> exists H1 H2 Q1,
       (H1 \* H2) h
    /\ F H1 Q1
    /\ Q1 \*+ H2 ===> Q \*+ \GC.

(** Characterization of "local" judgments *)

Definition is_local B (F:~~B) :=
  F = local F.

(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x].
    It is useful for describing loop invariants. *)

Definition is_local_pred A B (S:A->~~B) :=
  forall x, is_local (S x).

(** The weakening property is implied by locality *)

Definition weakenable B (F:~~B) :=
  forall H Q , F H Q ->
  forall H' Q', H' ==> H -> Q ===> Q' -> F H' Q'.


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

(** The [local] operator can be freely erased from a conclusion *)

Lemma local_erase : forall B (F:~~B),
  forall H Q, F H Q -> local F H Q.
Proof using.
  intros. exists H \[] Q. splits.
  rew_heap~. auto. hsimpl.
Qed.

(** Nested applications [local] are redundant *)

Lemma local_local : forall B (F:~~B),
  local (local F) = local F.
Proof using.
  extens. intros H Q. iff M.
  introv PH.
  destruct (M _ PH) as (H1&H2&Q1&PH12&N&Qle).
  destruct PH12 as (h1&h2&PH1&PH2&Ph12&Fh12).
  destruct (N _ PH1) as (H1'&H2'&Q1'&PH12'&N'&Qle').
  exists H1' (H2' \* H2) Q1'. splits.
   rewrite star_assoc. exists~ h1 h2.
   auto.
   intros x. hchange (Qle' x). hchange~ (Qle x).
    hchange (@hsimpl_gc (\GC \* \GC)). affine. hsimpl.
  apply~ local_erase.
Qed.

(** A definition whose head is [local] satisfies [is_local] *)

Lemma local_is_local : forall B (F:~~B),
  is_local (local F).
Proof using. intros. unfolds. rewrite~ local_local. Qed.

Hint Resolve local_is_local.

(** A introduction rule to establish [is_local] *)

Lemma is_local_prove : forall B (F:~~B),
  (forall H Q, F H Q <-> local F H Q) -> is_local F.
Proof using.
  intros. unfold is_local. apply fun_ext_2.
  intros. applys prop_ext. applys H.
Qed.

(** Weaken and frame and gc property [local] *)

Lemma local_frame_gc : forall B (F:~~B) H H1 H2 Q1 Q,
  is_local F ->
  F H1 Q1 ->
  H ==> H1 \* H2 ->
  Q1 \*+ H2 ===> Q \*+ \GC ->
  F H Q.
Proof using.
  introv L M WH WQ. rewrite L. introv Ph.
  exists H1 H2 Q1. splits; rew_heap~.
Qed.

(** Weaken and frame properties from [local] *)

Lemma local_frame : forall B H1 H2 Q1 (F:~~B) H Q,
  is_local F ->
  F H1 Q1 ->
  H ==> H1 \* H2 ->
  Q1 \*+ H2 ===> Q ->
  F H Q.
Proof using.
  introv L M WH WQ. rewrite L. introv Ph.
  exists H1 H2 Q1. splits; rew_heap~.
  hchange WQ. hsimpl.
Qed.

(** Frame property from [local] *)

Lemma local_frame_direct : forall H' B H Q (F:~~B),
  is_local F ->
  F H Q ->
  F (H \* H') (Q \*+ H').
Proof using. intros. apply* local_frame. Qed.

(** Weakening on pre and post from [local] *)

Lemma local_weaken : forall B H' Q' (F:~~B) H Q,
  is_local F ->
  F H' Q' ->
  H ==> H' ->
  Q' ===> Q ->
  F H Q.
Proof using.
  intros. eapply local_frame with (H2 := \[]); eauto; rew_heap~.
Qed.

(* DEPRECATED
Lemma local_weaken' : forall B (F:~~B),
  is_local F -> weakenable F.
Proof using. intros_all. apply* local_weaken. Qed.
*)

(** Garbage collection on precondition from [local] *)


Lemma local_gc_pre : forall H' B (F:~~B) H Q,
  is_local F ->
  H ==> H' \* \GC ->
  F H' Q ->
  F H Q.
Proof using.
  introv LF H1 H2. applys~ local_frame_gc H2.
Qed.

(** Variant of the above, useful for tactics to specify
    the garbage collected part *)

Lemma local_gc_pre_on : forall HG H' B (F:~~B) H Q,
  is_local F ->
  affine HG ->
  H ==> HG \* H' ->
  F H' Q ->
  F H Q.
Proof using.
  introv L HA M W. rewrite L. introv Ph.
  exists H' HG Q. splits.
  rewrite star_comm. apply~ M.
  auto.
  hsimpl.
Qed.

(** Weakening on pre and post with gc from [local] *)

Lemma local_weaken_gc : forall B H' Q' (F:~~B) H Q,
  is_local F ->
  F H' Q' ->
  H ==> H' ->
  Q' ===> Q \*+ \GC ->
  F H Q.
Proof using.
  intros. eapply local_frame_gc with (H2 := \[]); eauto; rew_heap~.
Qed.

Lemma local_weaken_gc_pre : forall B H' Q' (F:~~B) (H:hprop) Q,
  is_local F ->
  F H' Q' ->
  H ==> H' \* \GC ->
  Q' ===> Q ->
  F H Q.
Proof using.
  intros. apply* (@local_gc_pre_on (\GC) H'). affine. hchange H2. hsimpl.
  applys* local_weaken.
Qed.

(** Weakening on pre from [local] *)

Lemma local_weaken_pre : forall H' B (F:~~B) H Q,
  is_local F ->
  F H' Q ->
  H ==> H' ->
  F H Q.
Proof using. intros. apply* local_weaken. Qed.

(** Weakening on post from [local] *)

Lemma local_weaken_post : forall B Q' (F:~~B) H Q,
  is_local F ->
  F H Q' ->
  Q' ===> Q ->
  F H Q.
Proof using. intros. apply* local_weaken. Qed.

(** Garbage collection on post-condition from [local] *)

Lemma local_gc_post : forall B Q' (F:~~B) H Q,
  is_local F ->
  F H Q' ->
  Q' ===> Q \*+ \GC ->
  F H Q.
Proof using.
  introv L M W. rewrite L. introv Ph.
  exists H \[] Q'. splits; rew_heap~.
Qed.

(* DEPRECATED
Lemma local_gc_post' : forall H' B Q' (F:~~B) H Q,
  is_local F ->
  F H Q' ->
  Q' ===> Q \*+ H' ->
  F H Q.
Proof using.
  introv L M W. rewrite L. introv Ph.
  exists H \[] Q'. splits; rew_heap~. hchange W. hsimpl.
Qed.
*)

(** Extraction of premisses from [local] *)

Lemma local_intro_prop : forall B (F:~~B) H (P:Prop) Q,
  is_local F -> (P -> F H Q) -> F (\[P] \* H) Q.
Proof using.
  introv L M. rewrite L. introv (h1&h2&(PH1&HP)&PH2&?&?).
  subst h1. rewrite heap_union_neutral_l in H1. subst h2.
  exists H \[] Q. splits; rew_heap~. hsimpl.
Qed.

Lemma local_intro_prop_heap : forall B (F:~~B) (H:hprop) (P:Prop) Q,
  is_local F -> (forall h, H h -> P) -> (P -> F H Q) -> F H Q.
Proof using.
  introv L W M. rewrite L. introv Hh. forwards~: (W h).
  exists H \[] Q. splits; rew_heap~. hsimpl.
Qed.


(** Extraction of existentials from [local] *)

Lemma local_extract_exists : forall B (F:~~B) A (J:A->hprop) Q,
  is_local F ->
  (forall x, F (J x) Q) ->
  F (heap_is_pack J) Q.
Proof using.
  introv L M. rewrite L. introv (x&Hx).
  exists (J x) \[] Q. splits~. rew_heap~. hsimpl.
Qed.

(** Extraction of existentials below a star from [local] *)

Lemma local_intro_exists : forall B (F:~~B) H A (J:A->hprop) Q,
  is_local F ->
  (forall x, F ((J x) \* H) Q) ->
   F (heap_is_pack J \* H) Q.
Proof using.
  introv L M. rewrite L. introv (h1&h2&(X&HX)&PH2&?&?).
  exists (J X \* H) \[] Q. splits.
  rew_heap~. exists~ h1 h2.
  auto.
  hsimpl.
Qed.

(** Extraction of heap representation from [local] *)

Lemma local_name_heap : forall B (F:~~B) (H:hprop) Q,
  is_local F ->
  (forall h, H h -> F (= h) Q) ->
  F H Q.
Proof using.
  introv L M. rewrite L. introv Hh. exists (= h) \[] Q. splits~.
  exists h heap_empty. splits~. hsimpl.
Qed.

(** Weakening under a [local] modifier *)

Lemma local_weaken_body : forall (B:Type) (F F':~~B),
  (forall H Q, F H Q -> F' H Q) ->
  local F ===> local F'.
Proof using.
  introv M. intros H Q N. introv Hh.
  destruct (N _ Hh) as (H1&H2&Q1&P1&P2&P3). exists___*.
Qed.




(********************************************************************)
(* ** Tactic [xlocal] for proving [is_local] goals *)

(** Tactic [xlocal] ---later extended in CFTactics *)

Ltac xlocal_core tt :=
  first [ assumption | apply local_is_local ].
  (* match goal with |- is_local _ =>  end. *)

Tactic Notation "xlocal" :=
  xlocal_core tt.


(********************************************************************)
(* ** Extraction tactic for local goals *)

(** Lemmas *)

Lemma hclean_start : forall B (F:~~B) H Q,
  is_local F -> F (\[] \* H) Q -> F H Q.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hclean_keep : forall B (F:~~B) H1 H2 H3 Q,
  F ((H2 \* H1) \* H3) Q -> F (H1 \* (H2 \* H3)) Q.
Proof using. intros. rewrite (star_comm H2) in H. rew_heap in *. auto. Qed.

Lemma hclean_assoc : forall B (F:~~B) H1 H2 H3 H4 Q,
  F (H1 \* (H2 \* (H3 \* H4))) Q -> F (H1 \* ((H2 \* H3) \* H4)) Q.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hclean_starify : forall B (F:~~B) H1 H2 Q,
  F (H1 \* (H2 \* \[])) Q -> F (H1 \* H2) Q.
Proof using. intros. rew_heap in *. auto. Qed.

Lemma hclean_empty : forall B (F:~~B) H1 H2 Q,
  is_local F -> (F (H1 \* H2) Q) -> F (H1 \* (\[] \* H2)) Q.
Proof using. intros. rew_heap. auto. Qed.

Lemma hclean_prop : forall B (F:~~B) H1 H2 (P:Prop) Q,
  is_local F -> (P -> F (H1 \* H2) Q) -> F (H1 \* (\[P] \* H2)) Q.
Proof using.
  intros. rewrite star_comm_assoc. apply~ local_intro_prop.
Qed.

Lemma hclean_id : forall A (x X : A) B (F:~~B) H1 H2 Q,
  is_local F -> (x = X -> F (H1 \* H2) Q) -> F (H1 \* (x ~> Id X \* H2)) Q.
Proof using. intros. unfold Id. apply~ hclean_prop. Qed.

Lemma hclean_exists : forall B (F:~~B) H1 H2 A (J:A->hprop) Q,
  is_local F ->
  (forall x, F (H1 \* ((J x) \* H2)) Q) ->
   F (H1 \* (heap_is_pack J \* H2)) Q.
Proof using.
  intros. rewrite star_comm_assoc. apply~ local_intro_exists.
  intros. rewrite~ star_comm_assoc.
Qed.

Ltac hclean_setup tt :=
  pose ltac_mark;
  apply hclean_start; [ try xlocal | ].

Ltac hclean_cleanup tt :=
  remove_empty_heaps_formula tt;
  gen_until_mark.

Ltac hclean_step tt :=
  let go HP :=
    match HP with _ \* ?HN =>
    match HN with
    | ?H \* _ =>
      match H with
      | \[] => apply hclean_empty; try xlocal
      | \[_] => apply hclean_prop; [ try xlocal | intro ]
      | heap_is_pack _ => apply hclean_exists; [ try xlocal | intro ]
      | _ ~> Id _ => apply hclean_id; [ try xlocal | intro ]
      | _ \* _ => apply hclean_assoc
      | _ => apply hclean_keep
      end
    | \[] => fail 1
    | _ => apply hclean_starify
    end end in
  on_formula_pre ltac:(go).


Ltac hclean_main tt :=
  hclean_setup tt;
  (repeat (hclean_step tt));
  hclean_cleanup tt.

Tactic Notation "hclean" := hclean_main tt.
Tactic Notation "hclean" "~" := hclean; auto_tilde.
Tactic Notation "hclean" "*" := hclean; auto_star.