(* * 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 *) Require Import List. Require Import ZArith. Require Import List. Require Import EqNat. Require Import Classical. Require Import util. Require Import heap. Require Import bipl. Require Import axiomatic. Import valandloc. Open Local Scope heap_scope. Open Local Scope sep_scope. Lemma update_heap2_sep_con: forall x v P Q , (update_heap2 x v P) ** Q ==> update_heap2 x v (P**Q). red; intros. inversion_clear H. inversion_clear H0. decompose [and] H; clear H. red in H1. inversion_clear H1. inversion_clear H. inversion_clear H3. inversion_clear H. red. exists x2; split; auto. exists x3; split. apply heap.lookup_equal with (heap.union x0 x1). apply heap.equal_sym; auto. apply heap.lookup_union; auto. exists (heap.update x2 (eval v s) x0). exists x1. split. apply heap.disjoint_update. auto. split. apply heap.equal_update_L. auto. auto. apply heap.lookup_In with x3; auto. auto. Qed. Lemma update_heap2_sep_con': forall P Q x1 x2 v1 v2, (update_heap2 x1 v1 P) ** (update_heap2 x2 v2 Q) ==> update_heap2 x1 v1 (update_heap2 x2 v2 (P**Q)). red; intros. generalize (update_heap2_sep_con x1 v1 P (update_heap2 x2 v2 Q)); intro. red in H0. generalize (H0 _ _ H); intro. red. red in H1. inversion_clear H1 as [p]. inversion_clear H2. inversion_clear H3 as [z]. exists p. split; auto. exists z. inversion_clear H2. split; auto. rewrite sep.con_com_equiv. apply (update_heap2_sep_con x2 v2 Q P). rewrite sep.con_com_equiv. auto. Qed. (* * slight variations of Reynolds' axioms *) Lemma semax_assign_var_e' :forall Q P x e, (P ==> update_store2 x e Q) -> {{ P }} x <- e {{ Q }}. intros. apply semax_strengthen_pre with (update_store2 x e Q) . auto. apply semax_assign_var_e. Qed. Lemma semax_assign_var_e'' : forall R P Q x e c, (P ==> update_store2 x e R) -> {{ R }} c {{ Q }} -> {{ P }} x <- e ; c {{ Q }}. intros. apply semax_seq with R. apply semax_assign_var_e'. auto. auto. Qed. Lemma semax_assign_var_lookup' : forall Q P x e, (P ==> lookup2 x e Q) -> {{ P }} x <-* e {{ Q }}. intros. apply semax_strengthen_pre with (lookup2 x e Q) . auto. apply semax_assign_var_lookup. Qed. Lemma semax_assign_var_lookup'' : forall R P Q x e c, (P ==> lookup2 x e R) -> {{ R }} c {{ Q }} -> {{ P }} x <-* e ; c {{ Q }}. intros. apply semax_seq with (Q:=R). apply semax_assign_var_lookup'. auto. auto. Qed. Lemma semax_assign_var_lookup_backwards' : forall P Q x e, (P ==> (fun s h => exists e0, ((e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 Q))) s h)) -> {{ P }} x <-* e {{ Q }}. intros. apply semax_strengthen_pre with (fun s => fun h => exists e0, ((e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 Q))) s h). auto. apply semax_assign_var_lookup_backwards. Qed. Lemma semax_assign_var_lookup_backwards'' : forall P Q R x e c, (P ==> (fun s h => exists e0, ((e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 R))) s h)) -> {{ R }} c {{ Q }} -> {{ P }} x <-* e; c {{ Q }}. intros. apply semax_seq with (Q:=R). apply semax_strengthen_pre with (fun s => fun h => exists e0, ((e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 R))) s h). auto. apply semax_assign_var_lookup_backwards. auto. Qed. Lemma semax_assign_lookup_expr' : forall Q P e1 e2, (P ==> update_heap2 e1 e2 Q) -> {{ P }} e1 *<- e2 {{ Q }}. intros. apply semax_strengthen_pre with (update_heap2 e1 e2 Q) . auto. apply semax_assign_lookup_expr. Qed. Lemma semax_assign_lookup_expr'' : forall R P Q c e1 e2, (P ==> update_heap2 e1 e2 R) -> {{ R }} c {{ Q }} -> {{ P }} e1 *<- e2 ; c {{ Q }}. intros. apply semax_seq with (Q:=R). apply semax_assign_lookup_expr'. auto. auto. Qed. Lemma semax_assign_lookup_expr_backwards' : forall Q P e1 e2, (P ==> (fun s h => exists e'', ((e1 |-> e'') ** ((e1 |-> e2) -* Q)) s h)) -> {{ P }} e1 *<- e2 {{ Q }}. intros. apply semax_strengthen_pre with (fun s => fun h => exists e'', ((e1 |-> e'') ** ((e1 |-> e2) -* Q)) s h). auto. apply semax_assign_lookup_expr_backwards. Qed. Lemma semax_assign_lookup_expr_backwards'' : forall Q P R e1 e2 c, (P ==> (fun s h => exists e'', ((e1 |-> e'') ** ((e1 |-> e2) -* R)) s h)) -> {{ R }} c {{ Q }} -> {{ P }} e1 *<- e2 ; c {{ Q }}. intros. apply semax_seq with (Q:=R). apply semax_assign_lookup_expr_backwards'. auto. auto. Qed. Lemma semax_while' : forall b c I P Q, (P ==> I) -> {{ fun s h => I s h /\ eval_b b s = true }} c {{ I }} -> ((fun s h => I s h /\ eval_b b s = false) ==> Q) -> {{ P }} while b c {{ Q }}. intros. apply semax_weaken_post with (fun s => fun h => I s h /\ eval_b b s = false). auto. apply semax_strengthen_pre with I. auto. apply semax_while. auto. Qed. Lemma semax_while'': forall b c I P Q c1, (P ==> I) -> {{ fun s h => I s h /\ eval_b b s = true }} c {{ I }} -> {{ fun s h => I s h /\ eval_b b s = false }} c1 {{ Q }} -> {{ P }} while b c; c1 {{ Q }}. intros. apply semax_seq with (fun s => fun h => I s h /\ eval_b b s = false). eapply semax_while'. red; intros. apply H. auto. auto. red; intros. auto. auto. Qed. Lemma semax_skip': forall P Q, (P ==> Q) -> {{ P }} skip {{ Q }}. intros. apply semax_strengthen_pre with Q. auto. apply semax_skip. Qed. Lemma mapsto_equiv' : forall s s' h e1 e2 e3 e4, (e1|->e2) s' h -> eval e1 s' = eval e3 s -> eval e2 s' = eval e4 s -> (e3|->e4) s h. intros. red in H. inversion_clear H. inversion_clear H2. red. exists x. rewrite <- H0. rewrite <- H1. auto. Qed. Lemma mapsto_equiv : forall s h e1 e2 e3 e4, (e1|->e2) s h -> eval e1 s = eval e3 s -> eval e2 s = eval e4 s -> (e3|->e4) s h. intros. eapply mapsto_equiv'. apply H; auto. auto. auto. Qed. Ltac Mapsto_equiv := match goal with | id: (?e1 |-> ?e2) ?s ?h |- (?e3 |-> ?e4) ?s ?h => apply (mapsto_equiv s h e1 e2 e3 e4); [apply id | simpl; (Resolve_presb || auto)| simpl; (Resolve_presb || auto)] end. Lemma singleton_equal: forall s h1 h2 e1 e2 e3 e4, (e1 |-> e2) s h1 -> (e3 |-> e4) s h2 -> eval e1 s = eval e3 s -> eval e2 s = eval e4 s -> heap.equal h1 h2. intros. red in H. red in H0. inversion_clear H. inversion_clear H0. inversion_clear H3. inversion_clear H. rewrite H1 in H0. rewrite H0 in H3. injection H3. intros. subst x0. rewrite H2 in H4. eapply heap.equal_trans with (heap.singleton x (eval e4 s)). Equal_heap. Equal_heap. Qed. Lemma forward_reasoning : forall x e P, inde (x::nil) P -> ~ In x (expr_var e) -> {{ P }} x <- e {{ fun s h => P s h /\ eval (var_e x) s = eval e s }}. intros. apply semax_strengthen_pre with ( fun s h => P s h /\ (exists v, eval (var_e x) s = v) ). intros. split. auto. exists (eval (var_e x) s). auto. apply semax_strengthen_pre with ( update_store2 x e (fun s=> fun h => (P s h) /\ (eval (var_e x) s = eval e s)) ). intros. red. split. red in H. assert (In x (x::nil)). simpl. left; auto. generalize (H s h x (eval e s) H2); intro X; inversion_clear X. inversion_clear H1. apply H3; auto. inversion_clear H1. inversion_clear H3. simpl. rewrite store.lookup_update'; auto. auto. apply inde_expr with (x::nil). red; simpl; split; intros. inversion_clear H3. inversion_clear H5. subst x1. auto. auto. contradiction. simpl; auto. apply semax_assign_var_e. Qed. Lemma frame_rule': forall P c Q, {{ P }} c {{ Q }} -> forall R1 R2, inde (modified_cmd_var c) R1 -> (R1 ==> R2) -> {{ P ** R1 }} c {{ Q ** R2 }}. intros. apply semax_weaken_post with (Q**R1). red; intros. inversion_clear H2. inversion_clear H3. inversion_clear H2. inversion_clear H4. inversion_clear H5. red. exists x; exists x0. auto. apply frame_rule. auto. auto. Qed. Lemma frame_rule'': forall c1 c2 P1 P2 Q1 Q2, {{ P1 }} c1 {{ Q1 }} -> {{ P2 }} c2 {{ Q2 }} -> inde (modified_cmd_var c1) P2 -> inde (modified_cmd_var c2) Q1 -> {{ P1 ** P2 }} c1 ; c2 {{ Q1 ** Q2 }}. intros. generalize (frame_rule P1 c1 Q1 H P2 H1); intro. generalize (frame_rule P2 c2 Q2 H0 Q1 H2); intro. assert ((Q1 ** P2) ==> (P2 ** Q1)). apply sep.con_com. assert ((Q2 ** Q1) ==> (Q1 ** Q2)). apply sep.con_com. apply semax_seq with (P2 ** Q1). apply semax_weaken_post with (Q1 ** P2). auto. auto. apply semax_weaken_post with (Q2 ** Q1). auto. auto. Qed. Lemma semax_assign_lookup_expr_frame_rule : forall x v c P Q v', {{ P }} c {{ Q }} -> inde (modified_cmd_var c) (x |-> v) -> {{ (x |-> v') ** P }} x *<- v ; c {{ (x |-> v) ** Q }}. intros. apply semax_seq with ((x |-> v) ** P). apply semax_assign_lookup_expr_global_alternative. apply semax_strengthen_pre with (P ** (x |-> v)). red; intros; rewrite sep.con_com_equiv; auto. apply semax_weaken_post with (Q ** (x |-> v)). red; intros; rewrite sep.con_com_equiv; auto. apply frame_rule. auto. auto. Qed. (* * definitions of arrays (contiguous areas of memory) and their properties *) Fixpoint Array (x:loc) (size:nat) {struct size} : assert := match size with O => sep.emp | S n => (fun s h => exists y, ((nat_e x) |-> (int_e y)) s h) ** (Array (x + 1) n) end. (* array are never rooted as the address 0 *) Lemma Array_zero : forall size s h, Array O size s h -> heap.equal h heap.emp. induction size. intros. simpl in H. red in H. auto. intros. simpl in H. inversion_clear H. inversion_clear H0. decompose [and] H; clear H. inversion_clear H1. inversion_clear H. inversion_clear H1. simpl in H. simpl in H3. unfold val2loc in H. generalize H ; clear H. destruct (Ztrichotomy_inf 0 0). dependent inversion s0. intros. discriminate H. intros. discriminate H. inversion_clear z. Qed. Lemma Array_inde_store : forall m n s h, Array n m s h -> forall s', Array n m s' h. induction m. simpl. auto. simpl. intros. inversion_clear H. inversion_clear H0. decompose [and] H; clear H. exists x. exists x0. split; auto. split; auto. split; auto. apply IHm with s; auto. Qed. Ltac Array_equiv := match goal with | id: Array ?adr1 ?size1 ?s1 ?h |- Array ?adr2 ?size2 ?s2 ?h => assert (Array_equivA1: adr2 = adr1); [omega | assert (Array_equivA2: size2 = size1); [omega | ((rewrite Array_equivA1) || idtac); ((rewrite Array_equivA2) || idtac); eapply (Array_inde_store); apply id ] ] end. Lemma Array_inde: forall l adr size, inde l (Array adr size). induction l. red. simpl. tauto. red. intros. simpl in H; inversion_clear H. subst a. red. split. intros. eapply Array_inde_store. apply H. intros. eapply Array_inde_store. apply H. red in IHl. apply IHl. auto. Qed. Lemma Array_heap_equal: forall size adr s h1 h2, heap.equal h1 h2 -> Array adr size s h1 -> Array adr size s h2. induction size. intros. simpl. simpl in H0. red in H0. red. rewrite <- (heap.equal_emp h1 H0). apply heap.equal_sym. auto. intros. simpl in H0. inversion_clear H0. inversion_clear H1. decompose [and] H0; clear H0. inversion_clear H2. simpl. exists x; exists x0. split. Disjoint_heap. split. apply heap.equal_trans with h1. apply heap.equal_sym. auto. auto. split. exists x1. auto. eapply IHsize. apply (heap.equal_refl x0). auto. Qed. Lemma Array_concat_split: forall size1 size2 adr, Array adr (size1+size2) <==> (Array adr size1 ** Array (adr+size1) size2). induction size1. split. intros. exists heap.emp; exists h. split. Disjoint_heap. split. Equal_heap. split. simpl. red. apply heap.equal_refl. assert (adr + 0 = adr). intuition. assert (0 +size2 = size2). intuition. rewrite H0; rewrite <- H1; auto. intro. inversion_clear H. inversion_clear H0. decompose [and] H; clear H. simpl in H1. red in H1. assert (adr + 0 = adr). intuition. assert (0 +size2 = size2). intuition. rewrite <- H; rewrite H3. eapply Array_heap_equal. assert (heap.equal x0 h). generalize (heap.equal_emp x H1); intro. subst x. apply (heap.equal_sym). apply heap.equal_trans with (heap.union heap.emp x0). auto. apply heap.equal_trans with (heap.union x0 heap.emp). apply heap.union_com. Disjoint_heap. apply heap.equal_union_emp. apply H5. auto. split. intros. simpl. simpl in H. inversion_clear H. inversion_clear H0. decompose [and] H; clear H. inversion_clear H1. generalize (IHsize1 size2 (adr + 1) s x0); intro X; inversion_clear X. generalize (H1 H4); clear H1 H3; intros. inversion_clear H1. inversion_clear H3. decompose [and] H1; clear H1. exists (heap.union x x2); exists x3. split. Disjoint_heap. split. Equal_heap. split. exists x; exists x2. split. Disjoint_heap. split. Equal_heap. split. exists x1. auto. auto. assert (adr + 1 + size1 = adr + S size1). intuition. rewrite <- H1. auto. intros. inversion_clear H. inversion_clear H0. decompose [and] H; clear H. simpl. simpl in H1. inversion_clear H1. inversion_clear H. decompose [and] H1; clear H1. inversion_clear H3. exists (x1); exists (heap.union x0 x2). split. Disjoint_heap. split. Equal_heap. split. exists x3. auto. generalize (IHsize1 size2 (adr + 1) s (heap.union x0 x2)); intro X; inversion_clear X. apply H6; clear H6 H3; intros. exists x2; exists x0. split. Disjoint_heap. split. Equal_heap. split. auto. assert (adr + 1 + size1 = adr + S size1). intuition. rewrite H3. auto. Qed. Ltac TArray_concat_split_r size1 size2:= match goal with | |- Array ?adr ?size ? s ?h => generalize (Array_concat_split size1 size2 adr s h); intro TArray_concat_split_rH1; inversion_clear TArray_concat_split_rH1 as [TArray_concat_split_rH11 TArray_concat_split_rH12]; assert (TArray_concat_split_rA1: size1 + size2 = size); [omega | (rewrite <- TArray_concat_split_rA1 || idtac); clear TArray_concat_split_rA1; apply TArray_concat_split_rH12; clear TArray_concat_split_rH11 TArray_concat_split_rH12] end. Ltac TArray_concat_split_l_l sz id:= match goal with | id: Array ?adr ?size ? s ?h |- _ => assert (TArray_concat_split_l_lA1: size = sz + (size - sz)); [omega | rewrite TArray_concat_split_l_lA1 in id; clear TArray_concat_split_l_lA1; generalize (Array_concat_split sz (size - sz) adr s h); intro TArray_concat_split_l_lH1; inversion_clear TArray_concat_split_l_lH1 as [TArray_concat_split_l_lH2 TArray_concat_split_l_lH3]; generalize (TArray_concat_split_l_lH2 id); clear TArray_concat_split_l_lH3; clear TArray_concat_split_l_lH2; intro ] end. Ltac TArray_concat_split_l_r sz id:= match goal with | id: Array ?adr ?size ? s ?h |- _ => assert (TArray_concat_split_l_lA1: size = (size - sz) + sz); [omega | rewrite TArray_concat_split_l_lA1 in id; clear TArray_concat_split_l_lA1; generalize (Array_concat_split (size - sz) sz adr s h); intro TArray_concat_split_l_lH1; inversion_clear TArray_concat_split_l_lH1 as [TArray_concat_split_l_lH2 TArray_concat_split_l_lH3]; generalize (TArray_concat_split_l_lH2 id); clear TArray_concat_split_l_lH3; clear TArray_concat_split_l_lH2; intro ] end. (* test *) Lemma Array_split : forall size' size, size' <= size -> forall adr s h, adr > 0 -> Array adr size s h -> (Array adr size' ** Array (adr+size') (size - size')) s h. intros. TArray_concat_split_l_l size' H1. auto. Qed. Lemma Array_disjoint : forall size adr s h, adr > 0 -> Array adr size s h -> forall adr', adr' >= adr+size -> forall z, heap.disjoint h (heap.singleton adr' z). induction size. simpl. intros. red in H0. generalize (heap.equal_emp _ H0); intros. subst h. apply heap.disjoint_com. apply heap.disjoint_emp. intros. simpl in H0. inversion_clear H0. inversion_clear H2. decompose [and] H0; clear H0. assert (adr + 1> 0). omega. assert (adr' >= (adr + 1) + size). omega. generalize (IHsize _ _ _ H0 H6 adr' H5); intros. apply heap.disjoint_com. apply heap.disjoint_equal with (heap.union x x0). apply heap.disjoint_union. split. inversion_clear H3. inversion_clear H8. simpl in H3. inversion_clear H3. rewrite Z_of_nat2loc in H8. injection H8; clear H8; intros; subst x2. eapply heap.disjoint_equal with (heap.singleton adr x1). apply heap.disjoint_singleton. omega. Equal_heap. omega. apply heap.disjoint_com. auto. apply heap.equal_sym; auto. Qed. Lemma Array_concat : forall size adr s h, adr > 0 -> Array adr size s h -> forall z, Array adr (size + 1) s (heap.union h (heap.singleton (adr+size) z)). induction size. intros. red in H0. red in H0. rewrite (heap.equal_emp _ H0). exists (heap.singleton (adr + 0) z). exists heap.emp. split. apply heap.disjoint_emp. split. apply heap.union_com. apply heap.disjoint_com; apply heap.disjoint_emp. simpl. split. exists z. red. exists adr. simpl. rewrite Z_of_nat2loc. split; auto. assert (adr + 0 = adr). omega. rewrite H1; auto. apply heap.equal_refl. auto. red. apply heap.equal_refl. intros. simpl in H0. inversion_clear H0. inversion_clear H1. decompose [and] H0; clear H0. assert ((adr + 1) > 0). omega. pattern (S size). rewrite plus_n_O. rewrite plus_Snm_nSm. TArray_concat_split_r 1 (size + 1). generalize (IHsize _ _ _ H0 H5 z); clear H0; intros. inversion_clear H2. exists x. exists (heap.union x0 (heap.singleton ((adr + 1) + size) z)). split. apply heap.disjoint_union. split; auto. inversion_clear H4. simpl in H2. inversion_clear H2. apply heap.disjoint_com. apply heap.disjoint_equal with (heap.singleton x2 x1). rewrite Z_of_nat2loc in H4. injection H4; clear H4; intros; subst x2. apply heap.disjoint_singleton. omega. auto. Equal_heap. split. assert (adr + (size + 1) = (adr + 1) + size). omega. rewrite H2; clear H2. apply heap.equal_trans with (heap.union (heap.union x x0) (heap.singleton (adr + 1 + size) z)). apply heap.equal_union. auto. apply heap.disjoint_equal with (heap.union x x0). apply heap.disjoint_union. split. inversion_clear H4. simpl in H2. inversion_clear H2. rewrite Z_of_nat2loc in H4. injection H4; clear H4; intros; subst x2. eapply heap.disjoint_equal with (heap.singleton adr x1). apply heap.disjoint_singleton. omega. Equal_heap. auto. apply heap.disjoint_com. eapply Array_disjoint with (size:=size) (adr:=adr + 1) (s:=s). omega. auto. auto. Equal_heap. apply heap.equal_sym. apply heap.union_assoc. split. red. Compose_sepcon x heap.emp. exists x1; auto. red; apply heap.equal_refl. auto. Qed. Lemma mapstos_to_array: forall l x x' sz s h, (x |--> l) s h -> eval x s = Z_of_nat x' -> sz = length l -> Array x' sz s h. induction l. simpl. intros. subst sz. simpl. trivial. simpl. intros. Decompose_sepcon H h1 h2. subst sz. Compose_sepcon h1 h2. exists (eval a s). eapply mapsto_equiv. apply H2. simpl. auto. simpl. auto. eapply IHl. apply H5. simpl. rewrite H0. rewrite inj_plus. trivial. auto. Qed. (* Definition of intialized arrays *) Fixpoint ArrayI (x:loc) (l:list Z) {struct l} : assert := match l with nil => sep.emp | hd::tl => (fun s h => ((nat_e x) |-> (int_e hd)) s h) ** (ArrayI (x + 1) tl) end. Lemma ArrayI_inde_store: forall l n s h, ArrayI n l s h -> forall s', ArrayI n l s' h. induction l. simpl. intros. red in H. red. auto. intros. simpl in H. Decompose_sepcon H h1 h2. simpl. Compose_sepcon h1 h2. eapply mapsto_equiv'. apply H0. auto. auto. eapply IHl. apply H3. Qed. Lemma ArrayI_heap_cong: forall lx s h h' x , heap.equal h h' -> ArrayI x lx s h -> ArrayI x lx s h'. induction lx. simpl. intros. red in H0; red. Equal_heap. intros. simpl in H0. simpl. Decompose_sepcon H0 h1 h2. exists h1; exists h2. split. Disjoint_heap. split. apply heap.equal_trans with h. Equal_heap. Equal_heap. auto. Qed. Lemma ArrayITT_heap_cong: forall s h h' x lx, heap.equal h h' -> (ArrayI x lx ** TT) s h -> (ArrayI x lx ** TT) s h'. intros. Decompose_sepcon H0 h1 h2. exists h1; exists h2. split. Disjoint_heap. split. apply heap.equal_trans with h. Equal_heap. Equal_heap. auto. Qed. Lemma ArrayI_disjoint_heap: forall lx x h' e1 x1 s h, x > 0 -> ArrayI x lx s h -> (e1 |-> x1) s h' -> ((eval e1 s < eval (nat_e x) s)%Z \/ (eval e1 s >= eval (nat_e (x + length lx)) s)%Z) -> h # h'. induction lx. do 6 intro. intro x_prop1. intros. simpl in H. red in H. rewrite (heap.equal_emp h H). eapply heap.disjoint_com. apply heap.disjoint_emp. simpl. do 6 intro. intro x_prop1. intros. Decompose_sepcon H h1 h2. eapply heap.disjoint_com. eapply heap.disjoint_equal with (h1 +++ h2). eapply heap.disjoint_union. split. red in H2. inversion_clear H2. simpl in H4. inversion_clear H4. eapply heap.disjoint_equal with (heap.singleton x0 a). red in H0. inversion_clear H0. inversion_clear H4. eapply heap.disjoint_com. eapply heap.disjoint_equal with (heap.singleton x2 (eval x1 s)). eapply heap.disjoint_singleton. inversion_clear H1. red; intros. subst x2. rewrite Z_of_nat2loc in H2. injection H2; intros; subst x. generalize (val2loc_eq_some _ _ H0); intros. rewrite H1 in H4. assert (forall x, ~(x < x)%Z). intuition. intuition. auto. red; intro. subst x2. rewrite Z_of_nat2loc in H2. injection H2; intros; subst x. clear H2. generalize (val2loc_eq_some _ _ H0); intros. rewrite H1 in H4. rewrite inj_plus in H4. intuition. assert (S (length lx) = length lx + 1). intuition. rewrite H2 in H4. assert (forall x y, y > 0 -> ~(Z_of_nat x >= (Z_of_nat x) + (Z_of_nat y))%Z). intuition. red in H8. eapply H8. assert (length lx + 1 > 0). omega. apply H9. apply H4. auto. Equal_heap. Equal_heap. apply heap.disjoint_com. assert (x_prop2: x + 1 > 0). intuition. apply (IHlx (x+1) h' e1 x1 s h2 x_prop2 H5 H0). inversion_clear H1. left. simpl. rewrite inj_plus. intuition. right. simpl. rewrite inj_plus. rewrite inj_plus. rewrite inj_plus in H4. assert (S (length lx) = length lx + 1). intuition. rewrite H1 in H4. clear H1. rewrite inj_plus in H4. intuition. Equal_heap. Qed. Lemma Data_destructive_update_inv2: forall lx x h1 h2 e1 x1 s h, x > 0 -> (ArrayI x lx ** TT) s h -> heap.disjoint h1 h2 -> heap.equal h (heap.union h1 h2) -> (e1 |-> x1) s h1 -> ((eval e1 s < eval (nat_e x) s)%Z \/ (eval e1 s >= eval (nat_e (x + length lx)) s)%Z) -> (ArrayI x lx ** TT) s h2. do 8 intro. intro x_prop. intros. Decompose_sepcon H h'1 h'2. generalize (ArrayI_disjoint_heap lx x h1 e1 x1 s h'1 x_prop H4 H2 H3); intros. assert (h'1 +++ h'2 === h1 +++ h2). apply heap.equal_trans with h. apply heap.equal_sym; auto. auto. generalize (heap.disjoint_comp h'1 h1 h2 h'2 (heap.disjoint_com _ _ H6) H0 H H8); intro H9. inversion_clear H9. inversion_clear H10. Compose_sepcon h'1 x0. auto. red; auto. Qed. Lemma Data_destructive_update_inv: forall lx x h1 h2 e1 x1 x2 h'1 h' s h, x > 0 -> (ArrayI x lx ** TT) s h -> heap.disjoint h1 h2 -> heap.equal h (heap.union h1 h2) -> (e1 |-> x1) s h1 -> (e1 |-> x2) s h'1 -> heap.disjoint h'1 h2 -> heap.equal h' (heap.union h'1 h2) -> ((eval e1 s < eval (nat_e x) s)%Z \/ (eval e1 s >= eval (nat_e (x + length lx)) s)%Z) -> (ArrayI x lx ** TT) s h'. do 11 intro. intro x_prop. intros. generalize (Data_destructive_update_inv2 lx x h1 h2 e1 x1 s h x_prop H H0 H1 H2 H6); intros. Decompose_sepcon H7 h21 h22. Compose_sepcon h21 (h22 +++ h'1). auto. red; auto. Qed. (* this tactics resolve some simple goals over store_update *) Ltac Resolve_simpl_store_update:= match goal with | |- TT ?s ?h => red; simpl; auto | id: (?P **? Q) ?s ?h |- (?P **? Q) ?s' ?h => apply (sep.con_inde_store P Q s s' h id); [(intros; Resolve_simpl_store_update || idtac)|(intros; Resolve_simpl_store_update || idtac)] | id: store.lookup ?v ?s = ?p |- store.lookup ?v (store.update ?v' ?p' ?s) = ?p => rewrite <- store.lookup_update; [auto | unfold v; unfold v'; Resolve_presb] | 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.