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.