(*
 *  Seplog is an implementation of separation logic (an extension of Hoare
 *  logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the
 *  Coq proof assistant (version 8, http://coq.inria.fr) together with a
 *  sample verification of the heap manager of the Topsy operating system
 *  (version 2, http://www.topsy.net). More information is available at
 *  http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog.
 *
 *  Copyright (c) 2005 Reynald Affeldt and Nicolas Marti
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
 *)

Load seplog_header.

Definition HM_FREEFAILED := (int_e 0%Z).
Definition HM_FREEOK := (int_e 1%Z).

Import valandloc.

Open Local Scope Z_scope.

Definition Allocated := (int_e 0).
Definition Free := (int_e 1).

Definition status := 0.
Definition next := 1.

Definition hmStart : var.v := 0%nat.
Definition hmEnd : var.v := 1%nat.

Open Local Scope vc_scope.

Definition ENTRYSIZE (x:var.v) (tmp:var.v) := 
    (tmp <-* (x -.> next));
    (tmp <- ((var_e tmp) -e (var_e x) -e (int_e 2%Z)));
    (ifte ((nat_e 0) >> (var_e tmp)) thendo (tmp <- (nat_e 0)) elsedo (skip')).

Close Local Scope vc_scope.
Close Local Scope Z_scope.

(* A desciption of the heap list and useful lemmas *)

Inductive Heap_List : list (loc * nat * expr) -> loc -> loc -> store.s -> heap.h -> Prop :=

  Heap_List_last: forall s next startl endl h, endl = 0 -> next = 0 ->  startl > 0 ->
    ((nat_e startl) |--> (Allocated::(nat_e next)::nil)) s h ->
    Heap_List nil startl endl s h

  |   Heap_List_trans: forall s startl endl h , endl > 0 -> startl = endl ->  
    sep.emp s h ->
    Heap_List nil startl endl s h

  | Heap_List_suiv: forall s h next startl endl h1 h2 hd_adr hd_size hd_expr tl ,
    heap.disjoint h1 h2 -> heap.equal h (heap.union h1 h2) ->
    hd_expr = Allocated \/ hd_expr = Free ->
    next = (startl + 2 + hd_size) ->
    startl = hd_adr ->
    startl > 0 ->
    (((nat_e startl) |--> (hd_expr::(nat_e next)::nil)) ** (Array (startl+2) (hd_size))) s h1 ->
    Heap_List tl next endl s h2 ->
    Heap_List ((hd_adr, hd_size,hd_expr)::tl) startl endl s h.

Lemma Heap_List_heap_equal : forall l adr1 adr2 s h x1,
  heap.equal h x1 ->
  Heap_List l adr1 adr2 s x1 ->
  Heap_List l adr1 adr2 s h. 
intros.
inversion_clear H0.
subst adr2 next0.
simpl in H4.
inversion_clear H4.
inversion_clear H0.
decompose [and] H1; clear H1.
inversion_clear H6.
inversion_clear H1.
decompose [and] H5; clear H5.
eapply Heap_List_last.
auto.
intuition.
auto.
simpl.
exists x; exists (heap.union x2 x3).
split.
Disjoint_heap.
split.
assert (heap.equal h (heap.union x x0)).
apply (heap.equal_trans h x1 (heap.union x x0)).
auto.
auto.
Equal_heap.
split.
auto.
exists x2; exists x3.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
auto.
apply Heap_List_trans.
auto.
auto.
red in H3.
rewrite (heap.equal_emp x1 H3) in H.
rewrite (heap.equal_emp h H).
red.
apply heap.equal_refl.
subst adr1.
assert (heap.equal h (heap.union h1 h2)).
apply (heap.equal_trans h x1 (heap.union h1 h2)).
auto.
auto.
eapply Heap_List_suiv with (h1 := h1) (h2 := h2).
Disjoint_heap.
Equal_heap.
auto.
apply H4.
auto.
auto.
auto.
auto.
Qed.

Lemma Heap_List_one_cell : forall a_adr a_size a_type s h,
  a_adr > 0 ->
  a_type = Allocated \/ a_type = Free ->
  (
    Heap_List ((a_adr,a_size,a_type)::nil) a_adr 0 s h 
    <-> 
    (((nat_e a_adr) |--> (a_type::(nat_e (a_adr + 2 + a_size))::nil)) ** 
      (Array (a_adr+2) (a_size)) ** 
      ((nat_e (a_adr + 2 + a_size)) |--> (Allocated::(nat_e 0)::nil))) s h
  ).
split.
intros.
inversion_clear H1.
inversion_clear H9.
subst next0 next1.
clear H1 H6.
exists h1; exists h2.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
auto.
inversion H1.
intros.
inversion_clear H1.
inversion_clear H2.
decompose [and] H1; clear H1.
simpl.
eapply Heap_List_suiv with (h1 := x) (h2 := x0).
Disjoint_heap.
Equal_heap.
auto.
intuition.
auto.
auto.
auto.
eapply Heap_List_last.
auto.
intuition.
intuition.
auto.
Qed.

Lemma Heap_List_split' : forall a b startl s h,
  startl > 0 ->
  (Heap_List (a ++ b) startl 0 s h 
    <-> 
    (exists j, ((Heap_List a startl j) ** (Heap_List b j 0)) s h)).
induction a.
split.
intros.
simpl in H0.
exists startl.
exists (heap.emp); exists h.
split.
Disjoint_heap.
split.
Equal_heap.
split.
apply Heap_List_trans.
auto.
auto.
red.
apply heap.equal_refl.
auto.
intros.
simpl.
inversion_clear H0.
inversion_clear H1.
inversion_clear H0.
decompose [and] H1; clear H1.
inversion_clear H2.
subst x.
inversion_clear H5.
inversion H8.
inversion H1.
inversion H11.
subst x.
red in H6.
generalize (heap.equal_emp x0 H6); intro.
subst x0.
assert (heap.equal h x1).
apply (heap.equal_trans h (heap.union heap.emp x1) x1).
auto.
apply (heap.equal_trans (heap.union heap.emp x1) (heap.union x1 heap.emp) x1).
apply heap.union_com.
auto.
apply (heap.equal_union_emp).
auto.
eapply Heap_List_heap_equal.
apply H2.
auto.
split.
intros.
simpl in H0.
inversion_clear H0.
subst startl.
assert (next0 > 0).
omega.
generalize (IHa b next0 s h2 H0); intro X; inversion_clear X.
generalize (H5 H8); intro; clear H0 H9 H5.
inversion_clear H10.
inversion_clear H0.
inversion_clear H5.
decompose [and] H0; clear H0.
exists x.
exists (heap.union h1 x0); exists x1.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply Heap_List_suiv with (h1 := h1) (h2:= x0).
Disjoint_heap.
Equal_heap.
auto.
apply H4.
auto.
auto.
auto.
auto.
auto.
intros.
inversion_clear H0.
inversion_clear H1.
inversion_clear H0.
decompose [and] H1; clear H1.
simpl.
inversion_clear H2.
subst startl.
eapply Heap_List_suiv with (h1 := h1) (h2 := (heap.union h2 x1)).
Disjoint_heap.
Equal_heap.
auto.
apply H7.
auto.
auto.
auto.
assert (next0 > 0).
omega.
generalize (IHa b next0 s (heap.union h2 x1) H2); intro X; inversion_clear X.
apply H12; clear H8 H12.
exists x.
exists h2; exists x1.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
auto.
Qed.

Lemma Heap_List_split : forall a b startl endl s h,
     startl > 0 ->
     endl > 0 ->
     (Heap_List (a ++ b) startl endl s h 
     <-> 
     (exists j, ((Heap_List a startl j) ** (Heap_List b j endl)) s h)).
induction a.
simpl.
intros.
split.
intros.
exists startl.
Compose_sepcon heap.emp h.
eapply Heap_List_trans.
auto.
auto.
red; apply heap.equal_refl.
auto.
intros.
inversion_clear H1.
Decompose_sepcon H2 h1 h2.
inversion H2.
subst x startl0 endl0 s0 h0.
inversion_clear H5.
inversion H10.
subst endl; inversion H0.
subst hd_adr.
inversion H13.
subst startl startl0 endl0 s0 h0.
red in H7.
assert (heap.equal h h2).
Equal_heap.
eapply Heap_List_heap_equal.
apply H6.
auto.
simpl.
intros.
split.
intros.
inversion_clear H1.
subst hd_adr.
assert (next0 > 0).
subst next0; omega.
generalize (IHa b next0 endl s h2 H1 H0); intro X; inversion_clear X.
generalize (H6 H9); clear H6 H10.
intros.
inversion_clear H6.
Decompose_sepcon H10 h21 h22.
exists x.
Compose_sepcon (heap.union h21 h1) h22.
eapply Heap_List_suiv with (h1 := h1) (h2 := h21).
Disjoint_heap.
Equal_heap.
auto.
apply H5.
auto.
auto.
auto.
auto.
auto.
intros.
inversion_clear H1.
Decompose_sepcon H2 h1 h2.
inversion_clear H2.
eapply Heap_List_suiv with (h1 := h3) (h2 := (heap.union h4 h2)).
Disjoint_heap.
Equal_heap.
auto.
apply H8.
auto.
auto.
auto.
assert (next0 > 0).
subst next0; omega.
generalize (IHa b next0 endl s (heap.union h4 h2) H2 H0); intro X; inversion_clear X.
apply H14; clear H14 H13.
exists x.
Compose_sepcon h4 h2.
auto.
auto.
Qed.

Lemma Heap_List_last_cell : forall a b_adr b_size b_type startl s h,     
  b_adr > 0 ->
  startl > 0 ->
  b_type = Allocated \/ b_type = Free ->
  (
    Heap_List (a ++ ((b_adr,b_size,b_type)::nil)) startl 0 s h 
    <-> 
    (((Heap_List a startl b_adr) ** 
      ((((nat_e b_adr) |--> (b_type::(nat_e (b_adr + 2 + b_size))::nil)) ** 
	(Array (b_adr+2) (b_size))) ** 
      (((nat_e (b_adr + 2 + b_size)) |--> (Allocated::(nat_e 0)::nil))))) s h)
  ).
split.
intros.
generalize (Heap_List_split' a ((b_adr,b_size,b_type)::nil) startl s h H0); intro X; inversion_clear X.
generalize (H3 H2); clear H3 H4.
intros.
inversion_clear H3.
inversion_clear H4.
inversion_clear H3.
decompose [and] H4; clear H4.
inversion_clear H8.
subst x.
inversion_clear H14.
subst next1; clear H8.
exists x0; exists (heap.union h1 h2).
split.
Disjoint_heap.
split.
Equal_heap.
split; auto.
exists h1; exists h2.
split.
Disjoint_heap.
split.
Equal_heap.
split; auto.
subst next0.
auto.
subst next0.
auto.
inversion H8.
intros.
inversion_clear H2.
inversion_clear H3.
decompose [and] H2; clear H2.
inversion_clear H7.
inversion_clear H2.
decompose [and] H6; clear H6.
generalize (Heap_List_split' a ((b_adr,b_size,b_type)::nil) startl s h H0); intro X; inversion_clear X.
apply H9; clear H6 H9.
exists b_adr.
exists x; exists x0.
split.
Disjoint_heap.
split.
Equal_heap.
split; auto.
eapply Heap_List_suiv with (h1 := x1) (h2 := x2).
Disjoint_heap.
Equal_heap.
auto.
intuition.
auto.
auto.
auto.
eapply Heap_List_last.
auto.
intuition.
omega.
auto.
Qed.

Lemma Heap_List_start_pos: forall l startl s h,
   (Heap_List l startl 0) s h ->
        startl > 0.
intros.
inversion_clear H.
auto.
inversion H0.
auto.
Qed.

Lemma Heap_List_block_pos: forall l startl adr size status s h,
  Heap_List l startl 0 s h ->
  In (adr, size, status) l ->
  adr >= startl.
induction l.
simpl.
tauto.
simpl.
intros.
induction a; induction a.
inversion_clear H.
subst next0.
inversion_clear H0.
subst startl.
injection H.
omega.
generalize (IHl (startl + 2 + b0) adr size status0 s h2 H8 H).
omega.
Qed.

Lemma Heap_List_block_pos' : forall l adr size type startl endl s h,
  Heap_List l startl endl s h ->
  In (adr,size,type) l ->
  adr > 0.
induction l.
simpl.
tauto.
intros.
simpl in H0.
inversion_clear H0.
subst a.
inversion_clear H.
subst adr; auto.
inversion_clear H.
eapply IHl.
apply H8.
apply H1.
Qed.

Lemma Heap_List_start_end_pos : forall l startl endl s h,
  startl > 0 -> 
  endl > 0 ->
  Heap_List l startl endl s h ->
  startl <= endl.
induction l.
intros.
inversion_clear H1.
subst endl; inversion H0.
omega.
simpl.
intros.
induction a.
induction a.
inversion_clear H1.
subst a next0.
assert (startl + 2 + b0 > 0).
omega.
generalize (IHl (startl + 2 + b0) endl s h2 H1 H0 H9); intros.
omega.
Qed.

Lemma Heap_List_block_end_pos : forall l startl endl x size status s h,
  startl > 0 -> 
  endl > 0 ->
  Heap_List l startl endl s h ->
  In (x, size, status) l ->
  ((x + size + 2) <= endl).
induction l.
simpl.
tauto.
simpl.
intros.
induction a; induction a.
inversion_clear H1.
subst next0 startl.
inversion_clear H2.
injection H1.
intros.
subst b b0 a.
assert (x + 2 + size > 0).
omega.
generalize (Heap_List_start_end_pos l (x + 2 + size) endl s h2 H2 H0 H10); intros.
omega.
eapply IHl with (startl := (a + 2 + b0)).
omega.
auto.
apply H10.
apply H1.
Qed.

Lemma Heap_List_block_block_pos : forall l1 l2 adr s h x size status x' size' status',
  adr > 0 ->
  Heap_List (l1 ++ l2) adr 0 s h ->
  In (x, size, status) l1 ->
  In (x', size', status') l2 ->
  x + 2 + size <= x'.
intros.
generalize (Heap_List_split' l1 l2 adr s h H); intro X; inversion_clear X.
generalize (H3 H0); clear H3 H4.
intro X; inversion_clear X.
Decompose_sepcon H3 h1 h2.
generalize (Heap_List_block_pos l2 x0 x' size' status' s h2 H7 H2); intros.
generalize (Heap_List_start_pos l2 x0 s h2 H7); intros.
generalize (Heap_List_block_end_pos l1 adr x0 x size status0 s h1 H H8 H4 H1); intros.
omega.
Qed.

Lemma Heap_List_block_size : forall l badr bsize bstatus bsize' bstatus' adr s h,
  Heap_List l adr 0 s h ->
  In (badr, bsize, bstatus) l ->
  In (badr, bsize', bstatus') l ->
  bsize = bsize'.
induction l.
simpl.
tauto.
simpl; intros.
inversion_clear H0.
inversion_clear H1.
rewrite H2 in H0.
injection H0 ;auto.
subst a.
inversion_clear H.
subst badr next0.
generalize (Heap_List_block_pos l (adr + 2 + bsize) adr bsize' bstatus' s h2 H8 H0); intro.
omega.
inversion_clear H1.
subst a.
inversion_clear H.
subst badr next0.
generalize (Heap_List_block_pos l (adr + 2 + bsize') adr bsize bstatus s h2 H8 H2); intro.
omega.
inversion_clear H.
eapply IHl.
apply H9.
apply H2.
apply H0.
Qed.

Lemma Compaction : forall l1 l2 x1 sizex1 sizex2 startl s h,
   startl > 0 ->
   (Heap_List (l1 ++ ((x1,sizex1,Free)::(x1 + 2 + sizex1,sizex2,Free)::nil) ++ l2) startl 0) s h ->
   (((nat_e x1 +e (int_e 1%Z))|->(nat_e (x1 + 2 + sizex1))) ** 
	 (((nat_e x1 +e (int_e 1%Z))|-> nat_e (x1 + sizex1 + 4 + sizex2)) -*
	        (Heap_List (l1 ++ ((x1, sizex1 + 2 + sizex2, Free)::nil) ++ l2 ) startl 0))) s h.

intros.
generalize (Heap_List_split' l1 (((x1,sizex1,Free)::(x1 + 2 + sizex1,sizex2,Free)::nil) ++ l2) startl s h H); intro X; inversion_clear X.
generalize (H1 H0); clear H1 H2; intro.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
decompose [and] H2; clear H2.
assert (x > 0).
eapply Heap_List_start_pos.
apply H6.
generalize (Heap_List_split' ((x1,sizex1,Free)::(x1 + 2 + sizex1,sizex2,Free)::nil) l2 x s x2 H2); intro X; inversion_clear X.
generalize (H5 H6); clear H5 H7; intro.
inversion_clear H5.
inversion_clear H7.
inversion_clear H5.
decompose [and] H7; clear H7.
clear H0 H6.
inversion_clear H8.
subst x.
clear H2.
inversion_clear H14.
inversion_clear H2.
decompose [and] H8; clear H8.
simpl in H12.
inversion_clear H12.
inversion_clear H8.
decompose [and] H12; clear H12.
inversion_clear H20.
inversion_clear H12.
decompose [and] H19; clear H19.
red in H23.
generalize (heap.equal_emp _ H23); intro; subst x10.
clear H23.
exists x9; exists (heap.union x7 (heap.union x6 (heap.union h2 (heap.union x5 x0)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
red in H20.
red.
inversion_clear H20.
inversion_clear H19.
exists x10.
split.
rewrite <- H20.
simpl.
intuition.
simpl.
subst next0.
intuition.
red.
intros.
inversion_clear H19.
generalize (Heap_List_split' l1 (((x1,sizex1 + 2 + sizex2,Free)::nil) ++ l2) startl s h'' H); intro X; inversion_clear X.
apply H25; clear H25 H19.
exists x1.
exists x0; exists (heap.union x7 (heap.union x6 (heap.union h2 (heap.union h' x5)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
generalize (Heap_List_split' ((x1,sizex1 + 2 + sizex2,Free)::nil) l2 x1 s (heap.union x7 (heap.union x6 (heap.union h2 (heap.union h' x5)))) H13); intro X; inversion_clear X.
apply H25; clear H25 H19.
exists x3.
exists (heap.union h' (heap.union x7 (heap.union x6 h2))); exists x5.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply Heap_List_suiv with (h1 := (heap.union h' (heap.union x7 (heap.union x6 h2)))) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
auto.
intuition.
auto.
auto.
exists (heap.union x7 h'); exists (heap.union x6 h2).
split.
Disjoint_heap.
split.
Equal_heap.
split.
simpl.
exists x7; exists h'.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
exists h'; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
inversion_clear H24.
inversion_clear H19.
exists x10.
split.
rewrite <- H24.
simpl.
intuition.
simpl.
assert (x1 + sizex1 + 4 + sizex2 = x1 + 2 + (sizex1 + 2 + sizex2)).
omega.
rewrite <- H19; auto.
red.
apply (heap.equal_refl).
generalize (Array_concat_split sizex1 (2 + sizex2) (x1+2) s (heap.union x6 h2)); intro X; inversion_clear X.
assert (sizex1 + (2 + sizex2) = sizex1 + 2 + sizex2).
intuition.
rewrite <- H26.
apply H25.
clear H26 H25 H19.
exists x6; exists h2.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
inversion_clear H15.
inversion_clear H31.
subst x3.
inversion_clear H11.
inversion H35.
inversion H15.
inversion H38.
red in H33.
generalize (Array_concat_split 2 (sizex2) (x1 + 2 + sizex1) s h2); intro X; inversion_clear X.
apply H34.
clear H31 H34.
inversion_clear H30.
inversion_clear H31.
decompose [and] H30; clear H30.
exists x10; exists x11.
split.
Disjoint_heap.
split.
Equal_heap.
split.
generalize (Array_concat_split 1 1 (x1 + 2 + sizex1) s x10); intro X; inversion_clear X.
assert (1+1 = 2).
intuition.
rewrite H38 in H36; clear H38.
apply H36.
clear H30 H36.
simpl in H34.
inversion_clear H34.
inversion_clear H30.
decompose [and] H34; clear H34.
exists x12; exists x13.
split.
Disjoint_heap.
split.
Equal_heap.
split.
subst next0.
simpl.
exists x12; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
exists 1%Z.
red.
red in H36.
inversion_clear H36.
inversion_clear H10.
exists x14.
split.
rewrite <- H34.
simpl.
intuition.
unfold Free in H36.
intuition.
red.
apply heap.equal_refl.
simpl.
inversion_clear H40.
inversion_clear H34.
decompose [and] H39; clear H39.
red in H43.
exists x14; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
exists (Z_of_nat next1).
red.
red in H40.
inversion_clear H40.
inversion_clear H39.
exists x16.
rewrite <- H40.
simpl.
subst next0.
simpl in H42.
split.
rewrite inj_plus.
assert (1%Z = Z_of_nat 1)%Z.
intuition.
rewrite H10.
clear H10.
intuition.
auto.
red.
apply heap.equal_refl.
subst next0.
auto.
eapply Heap_List_trans.
eapply Heap_List_start_pos.
apply H11.
inversion_clear H15.
inversion_clear H31.
assert (x3 > 0).
eapply Heap_List_start_pos.
apply H11.
subst x3; inversion H31.
subst next0 next1 x3.
intuition.
red.
apply heap.equal_refl.
auto.
Qed.

Lemma Splitting : forall l1 l2 x size1 size2 s h startl,
   startl > 0 ->
   Heap_List (l1 ++ ((x, size1 + 2 + size2, Free)::nil) ++ l2) startl 0 s h ->
   exists e'' : expr,
     (((nat_e (x + 3 + size1)) |-> e'') **
      (((nat_e (x + 3 + size1)) |-> (nat_e (x + 4 + size1 + size2))) -*
       (fun (s1 : store.s) (h1 : heap.h) =>
        exists e''0 : expr,
          (((nat_e (x + 2 + size1)) |-> e''0) **
           (((nat_e (x + 2 + size1)) |-> Free) -*
            (fun (s2 : store.s) (h2 : heap.h) =>
             exists e''1 : expr,
               (((nat_e (x + 1)) |-> e''1) **
                (((nat_e (x + 1)) |-> (nat_e (x + 2 + size1))) -*
                 (fun (s : store.s) (h : heap.h) =>
                  Heap_List (l1 ++ ((x, size1,Free)::(x + 2 + size1, size2,Free)::nil) ++ l2) startl 0 s h))) s2 h2))) s1 h1))) s h.
intros.
generalize (Heap_List_split' l1 (((x, size1 + 2 + size2, Free) :: nil) ++ l2) startl s h H); intro X; inversion_clear X.
generalize (H1 H0); clear H0 H1 H2; intros.
inversion_clear H0.
Decompose_sepcon H1 h1 h2.
inversion_clear H4.
subst x0.
Decompose_sepcon H10 h31 h32.
generalize (Array_concat_split size1 (2 + size2) (x + 2) s h32); intro X; inversion_clear X.
assert (size1 + 2 + size2 = size1 + (2 + size2)).
omega.
rewrite H15 in H13; clear H15.
generalize (H12 H13); clear H12 H13 H14; intros.
Decompose_sepcon H12 h321 h322.
generalize (Array_concat_split 2 (size2) (x + 2 + size1) s h322); intro X; inversion_clear X.
generalize (H15 H16); clear H15 H16 H17; intros.
Decompose_sepcon H15 h3221 h3222.
generalize (Array_concat_split 1 1 (x + 2 + size1) s h3221); intro X; inversion_clear X.
assert (1 + 1 = 2).
omega.
rewrite H21 in H18; clear H21.
generalize (H18 H16); clear H16 H18 H20; intros.
Decompose_sepcon H16 h32211 h32212.
simpl in H18.
Decompose_sepcon H18 h322111 h322112.
red in H25.
inversion_clear H21.
simpl in H22.
Decompose_sepcon H22 h322121 h322122.
red in H28.
inversion_clear H22.
subst next0.
simpl in H8.
Decompose_sepcon H8 h311 h312.
Decompose_sepcon H30 h3121 h3122.
red in H33.
exists (int_e x1).
Compose_sepcon h322121 (heap.union h32211 (heap.union h3222 (heap.union h321 (heap.union h31 (heap.union h4 h1))))).
eapply mapsto_equiv.
apply H27.
simpl.
auto with *.
trivial.
Intro_sepimp h'322121 h'.
exists (int_e x0).
Compose_sepcon h322111 (heap.union h'322121 (heap.union h3222 (heap.union h321 (heap.union h31 (heap.union h4 h1))))).
eapply mapsto_equiv.
apply H24.
simpl.
trivial.
trivial.
Intro_sepimp h'322111 h''.
exists (nat_e (x + 2 + (size1 + 2 + size2))).
Compose_sepcon h3121 (heap.union h311 (heap.union h321 (heap.union h3222 (heap.union h'322121 (heap.union h'322111 (heap.union h4 h1)))))).
eapply mapsto_equiv.
apply H30.
simpl.
Presb_Z.
simpl.
Presb_Z.
Intro_sepimp h'3121 h'''.
generalize (Heap_List_split' l1 (((x, size1, Free) :: (x + 2 + size1, size2, Free) :: nil) ++ l2) startl s h''' H); intro X; inversion_clear X.
apply H43; clear H42 H43.
exists x.
Compose_sepcon h1 (heap.union h4 (heap.union h311 (heap.union h'3121 (heap.union h321 (heap.union h3222 (heap.union h'322111 h'322121)))))).
auto.
generalize (Heap_List_split' ((x, size1, Free) :: (x + 2 + size1, size2, Free) :: nil) l2 x s (heap.union h4 (heap.union h311 (heap.union h'3121 (heap.union h321 (heap.union h3222 (heap.union h'322111 h'322121)))))) H9); intro X; inversion_clear X.
apply H43; clear H42 H43.
exists (x + 2 + (size1 + 2 + size2)).
Compose_sepcon (heap.union h311 (heap.union h'3121 (heap.union h321 (heap.union h3222 (heap.union h'322111 h'322121))))) h4.
eapply Heap_List_suiv with (h1 := (heap.union h311 (heap.union h'3121 h321))) (h2 := (heap.union h'322111 (heap.union h'322121 h3222))).

Open Local Scope heap_scope.

Disjoint_heap.
Equal_heap.
right; auto.
intuition.
auto.
auto.
Compose_sepcon (heap.union h'3121 h311) h321.
simpl.
Compose_sepcon h311 h'3121.
auto.
Compose_sepcon h'3121 heap.emp.
eapply mapsto_equiv.
apply H40.
simpl.
Presb_Z.
simpl.
Presb_Z.
red; apply heap.equal_refl.
auto.
eapply Heap_List_suiv with (h1 := (heap.union h'322111 (heap.union h'322121 h3222))) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
right; auto.
intuition.
auto.
omega.
Compose_sepcon (heap.union h'322111 h'322121) h3222.
simpl.
Compose_sepcon h'322111 h'322121.
auto.
Compose_sepcon h'322121 heap.emp.
eapply mapsto_equiv.
apply H34.
simpl.
Presb_Z.
simpl.
Presb_Z.
red; apply heap.equal_refl.
auto.
eapply Heap_List_trans.
omega.
omega.
red; apply heap.equal_refl.
auto.
Qed.

Lemma Heap_List_compact : forall l startl last s h,
   (Heap_List l startl last ** Heap_List nil last 0) s h -> Heap_List l startl 0 s h.
induction l.
intros.
inversion_clear H.
inversion_clear H0.
decompose [and] H; clear H.
assert (last > 0).
eapply Heap_List_start_pos.
apply H4.
inversion_clear H1.
subst last; inversion H.
red in H6.
clear H3.
subst last.
assert (heap.equal h x0).
generalize (heap.equal_emp _ H6); intro; subst x.
apply heap.equal_trans with (heap.union heap.emp x0).
auto.
apply heap.equal_trans with ( heap.union x0  heap.emp).
eapply heap.union_com.
auto.
eapply heap.equal_union_emp.
eapply Heap_List_heap_equal.
apply H1.
auto.
intros.
inversion_clear H.
inversion_clear H0.
decompose [and] H; clear H.
inversion_clear H1.
eapply Heap_List_suiv with (h1 := h1) (h2 := (heap.union h2 x0)).
Disjoint_heap.
Equal_heap.
auto.
apply H6.
auto.
auto.
auto.
eapply IHl.
exists h2; exists x0.
split.
Disjoint_heap.
split.
Equal_heap.
split.
apply H10.
auto.
Qed.

Lemma Change_Status_Allocated : forall l1 l2 x1 sizex1 startl s h,
  startl > 0 ->
  (Heap_List (l1 ++ ((x1, sizex1, Free)::nil) ++ l2) startl 0) s h ->
  (((nat_e x1) |-> Free) ** 
    (((nat_e x1) |-> Allocated) -* (Heap_List (l1++((x1,sizex1,Allocated)::nil)++l2) startl 0))) s h.
intros.
generalize (Heap_List_split' l1 (((x1, sizex1, Free)::nil) ++ l2) startl s h H); intro X; inversion_clear X.
generalize (H1 H0); clear H1 H2; intro.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
decompose [and] H2; clear H2.
assert (x > 0).
eapply Heap_List_start_pos.
apply H6.
generalize (Heap_List_split' ((x1, sizex1, Free)::nil) l2 x s x2 H2); intro X; inversion_clear X.
generalize (H5 H6); clear H5 H7; intro.
inversion_clear H5.
inversion_clear H7.
inversion_clear H5.
decompose [and] H7; clear H7.
clear H0 H6.
inversion_clear H8.
subst x.
clear H2.
inversion_clear H14.
inversion_clear H2.
decompose [and] H8; clear H8.
simpl in H12.
inversion_clear H12.
inversion_clear H8.
decompose [and] H12; clear H12.
inversion_clear H20.
inversion_clear H12.
decompose [and] H19; clear H19.
red in H23.
generalize (heap.equal_emp _ H23); intro; subst x10.
clear H23.
exists x7; exists (heap.union x9 (heap.union x6 (heap.union h2 (heap.union x5 x0)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
intros.
inversion_clear H19.
generalize (Heap_List_split' l1 (((x1, sizex1, Allocated)::nil) ++ l2) startl s h'' H); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x1.
exists x0; exists (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
generalize (Heap_List_split' ((x1, sizex1, Allocated)::nil) l2 x1 s (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))) H13); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x3.
inversion_clear H15.
assert (x3 > 0).
eapply Heap_List_start_pos.
apply H11.
subst x3; inversion H15.
red in H26.
exists (heap.union h' (heap.union x9 x6)); exists x5.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply Heap_List_suiv with (h1 := heap.union h' (heap.union x6 x9)) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
left; auto.
apply H10.
auto.
auto.
exists (heap.union h' x9); exists x6.
split.
Disjoint_heap.
split.
Equal_heap.
split.
simpl.
exists h'; exists x9.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
exists x9; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
apply heap.equal_refl.
auto.
eapply Heap_List_trans.
auto.
auto.
red.
apply heap.equal_refl.
auto.
Qed.

Lemma Change_Status_Allocated' : forall l1 l2 x1 sizex1 startl status s h,
   startl > 0 ->
   (Heap_List (l1 ++ ((x1, sizex1, status)::nil) ++ l2) startl 0) s h ->
   ((((nat_e x1))|-> status) ** 
     ((((nat_e x1) |-> Allocated)) -* (Heap_List (l1 ++ ((x1,sizex1,Allocated)::nil) ++ l2) startl 0))) s h.
intros.
generalize (Heap_List_split' l1 (((x1, sizex1, status0)::nil) ++ l2) startl s h H); intro X; inversion_clear X.
generalize (H1 H0); clear H1 H2; intro.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
decompose [and] H2; clear H2.
assert (x > 0).
eapply Heap_List_start_pos.
apply H6.
generalize (Heap_List_split' ((x1, sizex1, status0)::nil) l2 x s x2 H2); intro X; inversion_clear X.
generalize (H5 H6); clear H5 H7; intro.
inversion_clear H5.
inversion_clear H7.
inversion_clear H5.
decompose [and] H7; clear H7.
clear H0 H6.
inversion_clear H8.
subst x.
clear H2.
inversion_clear H14.
inversion_clear H2.
decompose [and] H8; clear H8.
simpl in H12.
inversion_clear H12.
inversion_clear H8.
decompose [and] H12; clear H12.
inversion_clear H20.
inversion_clear H12.
decompose [and] H19; clear H19.
red in H23.
generalize (heap.equal_emp _ H23); intro; subst x10.
clear H23.
exists x7; exists (heap.union x9 (heap.union x6 (heap.union h2 (heap.union x5 x0)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
intros.
inversion_clear H19.
generalize (Heap_List_split' l1 (((x1, sizex1, Allocated)::nil) ++ l2) startl s h'' H); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x1.
exists x0; exists (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
generalize (Heap_List_split' ((x1, sizex1, Allocated)::nil) l2 x1 s (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))) H13); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x3.
inversion_clear H15.
assert (x3 > 0).
eapply Heap_List_start_pos.
apply H11.
subst x3; inversion H15.
red in H26.
exists (heap.union h' (heap.union x9 x6)); exists x5.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply Heap_List_suiv with (h1 := heap.union h' (heap.union x6 x9)) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
left; auto.
apply H10.
auto.
auto.
exists (heap.union h' x9); exists x6.
split.
Disjoint_heap.
split.
Equal_heap.
split.
simpl.
exists h'; exists x9.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
exists x9; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
apply heap.equal_refl.
auto.
eapply Heap_List_trans.
auto.
auto.
red.
apply heap.equal_refl.
auto.
Qed.

Lemma Change_Status_Free : forall l1 l2 x1 sizex1 startl s h,
   startl > 0 ->
   (Heap_List (l1 ++ ((x1, sizex1, Allocated)::nil) ++ l2) startl 0) s h ->
   (((nat_e x1)|-> Allocated) ** 
     ((((nat_e x1) |-> Free)) -* (Heap_List (l1 ++ ((x1, sizex1, Free)::nil) ++ l2) startl 0))) s h.
intros.
generalize (Heap_List_split' l1 (((x1, sizex1, Allocated)::nil) ++ l2) startl s h H); intro X; inversion_clear X.
generalize (H1 H0); clear H1 H2; intro.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
decompose [and] H2; clear H2.
assert (x > 0).
eapply Heap_List_start_pos.
apply H6.
generalize (Heap_List_split' ((x1, sizex1,Allocated)::nil) l2 x s x2 H2); intro X; inversion_clear X.
generalize (H5 H6); clear H5 H7; intro.
inversion_clear H5.
inversion_clear H7.
inversion_clear H5.
decompose [and] H7; clear H7.
clear H0 H6.
inversion_clear H8.
subst x.
clear H2.
inversion_clear H14.
inversion_clear H2.
decompose [and] H8; clear H8.
simpl in H12.
inversion_clear H12.
inversion_clear H8.
decompose [and] H12; clear H12.
inversion_clear H20.
inversion_clear H12.
decompose [and] H19; clear H19.
red in H23.
generalize (heap.equal_emp _ H23); intro; subst x10.
clear H23.
exists x7; exists (heap.union x9 (heap.union x6 (heap.union h2 (heap.union x5 x0)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
intros.
inversion_clear H19.
generalize (Heap_List_split' l1 (((x1, sizex1, Free)::nil) ++ l2) startl s h'' H); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x1.
exists x0; exists (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
generalize (Heap_List_split' ((x1, sizex1, Free)::nil) l2 x1 s (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))) H13); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x3.
inversion_clear H15.
assert (x3 > 0).
eapply Heap_List_start_pos.
apply H11.
subst x3; inversion H15.
red in H26.
exists (heap.union h' (heap.union x9 x6)); exists x5.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply Heap_List_suiv with (h1 := heap.union h' (heap.union x6 x9)) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
right; auto.
apply H10.
auto.
auto.
exists (heap.union h' x9); exists x6.
split.
Disjoint_heap.
split.
Equal_heap.
split.
simpl.
exists h'; exists x9.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
exists x9; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
apply heap.equal_refl.
auto.
eapply Heap_List_trans.
auto.
auto.
red.
apply heap.equal_refl.
auto.
Qed.

Lemma Change_Status_Free' : forall l1 l2 x1 sizex1 startl s h x status0,
   startl > 0 ->
   (Heap_List (l1 ++ ((x1, sizex1, status0)::nil) ++ l2) startl 0) s h ->
   eval (var_e x) s = eval (nat_e x1) s ->   
   ((((x -.> status))|-> status0) ** 
   ((((x -.> status) |-> Free)) -* (Heap_List (l1 ++ ((x1, sizex1, Free)::nil) ++ l2) startl 0))) s h.
do 7 intro.
intro V.
intro ST.
do 2 intro.
intro W.
generalize (Heap_List_split' l1 (((x1, sizex1, ST)::nil) ++ l2) startl s h H); intro X; inversion_clear X.
generalize (H1 H0); clear H1 H2; intro.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
decompose [and] H2; clear H2.
assert (x > 0).
eapply Heap_List_start_pos.
apply H6.
generalize (Heap_List_split' ((x1, sizex1,ST)::nil) l2 x s x2 H2); intro X; inversion_clear X.
generalize (H5 H6); clear H5 H7; intro.
inversion_clear H5.
inversion_clear H7.
inversion_clear H5.
decompose [and] H7; clear H7.
clear H0 H6.
inversion_clear H8.
subst x.
clear H2.
inversion_clear H14.
inversion_clear H2.
decompose [and] H8; clear H8.
simpl in H12.
inversion_clear H12.
inversion_clear H8.
decompose [and] H12; clear H12.
inversion_clear H20.
inversion_clear H12.
decompose [and] H19; clear H19.
red in H23.
generalize (heap.equal_emp _ H23); intro; subst x10.
clear H23.
exists x7; exists (heap.union x9 (heap.union x6 (heap.union h2 (heap.union x5 x0)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply mapsto_equiv.
apply H16.
simpl.
simpl in W.
rewrite W.
auto with *.
auto.
red.
intros.
inversion_clear H19.
generalize (Heap_List_split' l1 (((x1, sizex1, Free)::nil) ++ l2) startl s h'' H); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x1.
exists x0; exists (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
generalize (Heap_List_split' ((x1, sizex1, Free)::nil) l2 x1 s (heap.union h' (heap.union x9 (heap.union x6 (heap.union h2 x5)))) H13); intro X; inversion_clear X.
apply H25; clear H19 H25.
exists x3.
inversion_clear H15.
assert (x3 > 0).
eapply Heap_List_start_pos.
apply H11.
subst x3; inversion H15.
red in H26.
exists (heap.union h' (heap.union x9 x6)); exists x5.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply Heap_List_suiv with (h1 := heap.union h' (heap.union x6 x9)) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
right; auto.
apply H10.
auto.
auto.
exists (heap.union h' x9); exists x6.
split.
Disjoint_heap.
split.
Equal_heap.
split.
simpl.
exists h'; exists x9.
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply mapsto_equiv.
apply H24.
simpl.
simpl in W; rewrite W.
auto with *.
auto.
exists x9; exists heap.emp.
split.
Disjoint_heap.
split.
Equal_heap.
split.
auto.
red.
apply heap.equal_refl.
auto.
eapply Heap_List_trans.
auto.
auto.
red.
apply heap.equal_refl.
auto.
Qed.

Lemma Heap_List_inde_store: forall l startl endl s h,
  Heap_List l startl endl s h -> forall s', 
    Heap_List l startl endl s' h.
intros.
induction H.
eapply Heap_List_last.
auto.
apply H0.
auto.
trivial.
subst endl.
eapply Heap_List_trans.
trivial.
trivial.
trivial.
eapply Heap_List_suiv.
apply H.
trivial.
trivial.
apply H2.
trivial.
trivial.
Decompose_sepcon H5 h11 h12.
Compose_sepcon h11 h12.
intuition.
subst hd_expr.
trivial.
subst hd_expr.
trivial.
eapply Array_inde_store; apply H10.
trivial.
Qed.

Lemma list_split' : forall (l: list (loc * loc * expr)) adr size type,
  In (adr, size, type) l ->
  exists l1, exists l2, l = l1 ++ ((adr,size,type)::nil) ++ l2.
intros.
apply (list_split _ _ _ H); intro.
Qed.

Lemma Heap_List_var_lookup_next : forall l startl s h adr size type x y (P:assert) ,
  Heap_List l startl 0 s h ->
  In (adr, size, type) l ->
  eval (var_e x) s = Z_of_nat adr -> 
  update_store2 y (nat_e (adr + 2 + size)) P s h ->
  (forall s h h', heap.equal h h' -> P s h -> P s h') ->
  (((x -.> next)|->(nat_e (adr + 2 + size))) ** 
  (((x -.> next)|->(nat_e (adr + 2 + size))) -* (update_store2 y (nat_e (adr + 2 + size)) P ))) s h.
do 14 intro.
intro P_cong.
simpl in H1.
generalize (list_split' l adr size type H0); intro.
inversion_clear H3.
inversion_clear H4.
assert (startl > 0).
eapply Heap_List_start_pos.
apply H.
subst l.
generalize (Heap_List_split' x0 (((adr,size,type)::nil) ++ x1) startl s h H4); intro X; inversion_clear X.
generalize (H3 H); intros; clear H3 H5; intros.
inversion_clear H6.
inversion_clear H3.
inversion_clear H5.
decompose [and] H3; clear H3.
assert (x2 > 0).
eapply Heap_List_start_pos.
apply H9.
generalize (Heap_List_split' ((adr,size,type)::nil) x1 x2 s x4 H3); intro X; inversion_clear X.
generalize (H8 H9); clear H8 H10; intros.
inversion_clear H8.
inversion_clear H10.
inversion_clear H8.
decompose [and] H10; clear H10.
clear H9.
inversion_clear H11.
subst x2.
clear H3.
inversion_clear H18.
inversion_clear H3.
decompose [and] H11; clear H11.
simpl in H16.
inversion_clear H16.
inversion_clear H11.
decompose [and] H16; clear H16.
inversion_clear H24.
inversion_clear H16.
decompose [and] H23; clear H23.
red in H27.
inversion_clear H19.
assert (x5 > 0).
eapply Heap_List_start_pos.
apply H14.
subst x5; inversion H19.
subst x5.
red in H28.
exists x11; exists (heap.union x9 (heap.union x8 (heap.union x7 x3))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply mapsto_equiv.
apply H24.
simpl.
unfold next; rewrite H1; intuition.
subst next0.
intuition.
red; intros.
inversion_clear H19.
assert (heap.equal h' x11).
eapply singleton_equal.
apply H30.
apply H24.
simpl.
unfold next; rewrite H1; intuition.
subst next0.
intuition.
red.
red in H2.
assert (heap.equal h'' h).
eapply heap.equal_trans.
apply H26.
Equal_heap.
eapply P_cong.
apply heap.equal_sym.
apply H31.
apply H2.
Qed.

Lemma Heap_List_var_lookup_status: forall l startl s h adr size type x y (P:assert),
  Heap_List l startl 0 s h ->
  In (adr, size, type) l ->
  eval (var_e x) s = Z_of_nat adr -> 
  update_store2 y type P s h ->
  (forall s h h', heap.equal h h' -> P s h -> P s h') ->
  (((x -.> status)|-> type) ** (((x -.> status)|-> type) -* (update_store2 y type P ))) s h.
do 14 intro.
intro P_cong.
simpl in H1.
generalize (list_split' l adr size type H0); intro.
inversion_clear H3.
inversion_clear H4.
assert (startl > 0).
eapply Heap_List_start_pos.
apply H.
subst l.
generalize (Heap_List_split' x0 (((adr,size,type)::nil) ++ x1) startl s h H4); intro X; inversion_clear X.
generalize (H3 H); intros; clear H3 H5; intros.
inversion_clear H6.
inversion_clear H3.
inversion_clear H5.
decompose [and] H3; clear H3.
assert (x2 > 0).
eapply Heap_List_start_pos.
apply H9.
generalize (Heap_List_split' ((adr,size,type)::nil) x1 x2 s x4 H3); intro X; inversion_clear X.
generalize (H8 H9); clear H8 H10; intros.
inversion_clear H8.
inversion_clear H10.
inversion_clear H8.
decompose [and] H10; clear H10.
clear H9.
inversion_clear H11.
subst x2.
clear H3.
inversion_clear H18.
inversion_clear H3.
decompose [and] H11; clear H11.
simpl in H16.
inversion_clear H16.
inversion_clear H11.
decompose [and] H16; clear H16.
inversion_clear H24.
inversion_clear H16.
decompose [and] H23; clear H23.
red in H27.
inversion_clear H19.
assert (x5 > 0).
eapply Heap_List_start_pos.
apply H14.
subst x5; inversion H19.
subst x5.
red in H28.
exists x9; exists (heap.union x11 (heap.union x8 (heap.union x7 x3))).
split.
Disjoint_heap.
split.
Equal_heap.
split.
eapply mapsto_equiv.
apply H20.
simpl.
unfold status; rewrite H1; intuition.
intuition.
red; intros.
inversion_clear H19.
assert (heap.equal h' x9).
eapply singleton_equal.
apply H30.
apply H20.
simpl.
unfold next; rewrite H1; intuition.
intuition.
red.
red in H2.
assert (heap.equal h'' h).
eapply heap.equal_trans.
apply H26.
Equal_heap.
eapply P_cong.
apply heap.equal_sym.
apply H31.
apply H2.
Qed.

(* Some simple tactic used to make clear proof *)

Ltac Resolve_simpl1:=
   match goal with

      | |- TT ?s ?h => red; simpl; auto

      | id: Array ?adr ?size ?s ?h |- Array ?adr ?size ?s2 ?h =>
                 eapply Array_inde_store; apply id

      | id: ArrayI ?adr ?size ?s ?h |- ArrayI ?adr ?size ?s2 ?h =>
                 eapply ArrayI_inde_store; apply id

      | id: Heap_List ?l ?l' ?n ?s ?h |- Heap_List ?l ?l' ?n ?s' ?h =>
		 eapply Heap_List_inde_store; apply id

      | id: (?P **? Q) ?s ?h |- (?P **? Q) ?s' ?h => 
            apply (sep.con_inde_store P Q s s' h id); [(intros; Resolve_simpl1)|(intros; Resolve_simpl1)]

      | id: store.lookup ?v ?s = ?p |- store.lookup ?v (store.update ?v' ?p' ?s) = ?p =>
                 rewrite <- store.lookup_update; [auto | unfold v; unfold v'; omega]
                 
      | id: Array ?adr ?size ?s ?h |- Array ?adr ?size ?s' ?h =>
                 apply (Array_inde_store size adr s h  id s')

      | id: store.lookup ?v ?s = ?p |- store.lookup ?v (store.update ?v' ?p' ?s) = ?p =>
                 rewrite <- store.lookup_update; auto; Resolve_var_neq

      | |- store.lookup ?v (store.update ?v ?p ?s) = ?p1 => 
             rewrite store.lookup_update'; auto
      
   end.

Ltac Resolve_assign_var:=
      simpl; red; intuition; repeat (Resolve_simpl1).