(* * 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 ZArith. Require Import EqNat. Require Import Bool. Require Import ZArith. Require Import List. Require Import Classical. Load util. (* local requirement *) Require Import Relations. (* definition of values, locations, and heaps *) Module valandloc. (* Definition val := Z.*) Definition val2nat : Z -> option nat. intro w. generalize (Ztrichotomy_inf w Z0); intro X; inversion_clear X. inversion_clear H. exact None. exact (Some O). induction w. inversion H. exact (Some (nat_of_P p)). inversion H. Defined. Definition veqdec := Z_eq_dec. Lemma eqb_val0 : forall v1, (Zeq_bool v1 Z0) = true -> v1=Z0. intros. unfold eqb in H. apply (Zeq_bool_true _ _ H). Qed. Lemma eqb_v0' : forall v1 v1', (Zeq_bool v1 v1') = false -> v1 <> v1'. intros. unfold Zeq_bool in H. generalize (Zeq_bool_false v1 v1'); intros. tauto. Qed. Definition loc := nat. Definition eqdec := eq_nat_dec. Definition lle := Peano.le. Lemma order : (order _ lle). apply Build_order. exact le_n. exact le_trans. exact le_antisym. Qed. (*Definition loc2val := Z_of_nat.*) Definition val2loc : Z -> option loc. intro w. generalize (Ztrichotomy_inf w Z0); intro X; inversion_clear X. inversion_clear H. exact None. exact None. induction w. inversion H. exact (Some (nat_of_P p)). inversion H. Defined. Definition val2loc' : forall (w:Z), (Zgt w Z0) -> forall ll, (val2loc w)=(Some ll) -> w=(Z_of_nat ll). intros. inversion H. generalize (Zcompare_Gt_spec _ _ H2); intro. inversion_clear H1. simpl in H3. rewrite Zplus_0_r in H3. subst w. rewrite (Zpos_eq_Z_of_nat_o_nat_of_P x). unfold Z_of_nat. unfold val2loc in H0. generalize H0; clear H0. case (Ztrichotomy_inf (Zpos x) Z0). intro. inversion_clear s. inversion H0. discriminate H0. simpl. intros. injection H0; intro; subst ll; auto. Qed. Lemma Z_of_nat2loc : forall n, n > 0 -> val2loc (Z_of_nat n) = Some n. intros. unfold val2loc. destruct (Ztrichotomy_inf (Z_of_nat n) 0). inversion s. destruct n. inversion_clear H0. inversion_clear H0. destruct n. inversion_clear H. discriminate H0. destruct n. inversion_clear H. simpl. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto. Qed. Lemma val2loc_eq_some: forall x v, val2loc x = Some v -> x = Z_of_nat v. unfold val2loc. intro. destruct (Ztrichotomy_inf x 0). dependent inversion s. intros. inversion_clear H. intros. inversion_clear H. simpl. induction x. inversion z. simpl. intros. injection H. intuition. subst v. clear H. apply Zpos_eq_Z_of_nat_o_nat_of_P. inversion z. Qed. Lemma val2loc_neg : forall z, (Zle z Z0) -> val2loc z = None. unfold val2loc. intros. destruct (Ztrichotomy_inf z 0). dependent inversion s. auto. auto. simpl. generalize (Zgt_not_le _ _ z0); intro. tauto. Qed. End valandloc. Import valandloc. Module Type HEAP. Parameter l : Set. Parameter v : Set. Parameter h : Set. Parameter emp : h. Parameter singleton : l -> v -> h. Parameter Inh : l -> h -> Prop. Parameter lookup : l -> h -> option v. Parameter lookup_singleton : forall n w, lookup n (singleton n w) = Some w. Parameter lookup_In : forall h n z, lookup n h = Some z -> Inh n h. Parameter heap_is_function : forall h x z, lookup x h = Some z -> forall z', lookup x h = Some z' -> z = z'. Parameter equal : h -> h -> Prop. Notation "k '===' m" := (equal k m) (at level 79) : heap_scope. Open Local Scope heap_scope. Parameter equal_ext: forall h1 h2, (h1 === h2) -> h1 = h2. Parameter equal_emp : forall h, h === emp -> h = emp. Parameter equal_refl : forall h, h === h. Parameter equal_sym : forall h1 h2, h1 === h2 -> h2 === h1. Parameter equal_trans : forall h1 h2 h3, h1 === h2 -> h2 === h3 -> h1 === h3. Parameter lookup_equal : forall h1 h2, h1 === h2 -> forall n z, lookup n h1 = Some z -> lookup n h2 = Some z. Parameter update : l -> v -> h -> h. Parameter update_singleton : forall n w w', update n w' (singleton n w) === singleton n w'. Parameter equal_update : forall h1 h2, h1 === h2 -> forall n z, update n z h1 === update n z h2. Parameter union : h -> h -> h. Notation "k '+++' m" := (union k m) (at level 78) : heap_scope. Parameter equal_union_emp : forall h1, h1 +++ emp === h1. Parameter union_assoc : forall h1 h2 h3, h1 +++ (h2 +++ h3) === (h1 +++ h2) +++ h3. Parameter lookup_union_or: forall h1 h2 n z, lookup n (h1 +++ h2) = Some z -> lookup n h1 = Some z \/ lookup n h2 = Some z. Parameter disjoint : h -> h -> Prop. Notation "k '#' m" := (disjoint k m) (at level 79) : heap_scope. Parameter disjoint_emp : forall h, h # emp. Parameter disjoint_singleton : forall x y z z', x <> y -> (singleton x z) # (singleton y z'). Parameter disjoint_singleton' : forall x y z z', (singleton x z) # (singleton y z') -> x <> y. Parameter disjoint_com : forall h0 h1, h0 # h1 -> h1 # h0. Parameter disjoint_update : forall n z h1 h2, h1 # h2 -> (update n z h1) # h2. Parameter disjoint_union : forall h1 h2 h0, h0 # h1 /\ h0 # h2 -> h0 # (h1 +++ h2). Parameter disjoint_union' : forall h1 h2 h0, h0 # (h1 +++ h2) -> h0 # h1 /\ h0 # h2. Parameter equal_union_disjoint : forall x1 x2 x x0, x === (x1 +++ x2) /\ x # x0 -> x1 # x0. Parameter equal_union : forall h1 h2, h1 === h2 -> forall h0, h0 # h1 -> h1 +++ h0 === h2 +++ h0. (* union is not commutative in general! *) Parameter union_com : forall h1 h2, h1 # h2 -> h1 +++ h2 === h2 +++ h1. Parameter lookup_union : forall h1 h2, h1 # h2 -> forall n z, lookup n h1 = Some z -> lookup n (h1 +++ h2) = Some z. Parameter equal_update_L : forall h1 h2, h1 # h2 -> forall h, h === h1 +++ h2 -> forall n z, Inh n h1 -> update n z h === (update n z h1) +++ h2. Parameter lookup_exists_partition: forall h a b, lookup a h = Some b -> exists h'' , h === (singleton a b) +++ h'' /\ (singleton a b) # h''. Parameter disjoint_equal : forall h1 h2, h1 # h2 -> forall h3, h2 === h3 -> h1 # h3. Parameter disjoint_comp : forall h'1 h1 h2 h'2, h1 # h'1 -> h1 # h2 -> h'1 # h'2 -> h'1 +++ h'2 === h1 +++ h2 -> exists h', h'1 # h' /\ h2 === (h' +++ h'1). Parameter dif : h -> l -> h. Notation "k '---' l" := (dif k l) (at level 78) : heap_scope. Parameter dif_singleton_emp: forall a b, (singleton a b) --- a === emp. Parameter dif_union: forall h1 h2 a, (h1 +++ h2) --- a === (h1 --- a) +++ (h2 --- a). Parameter dif_equal: forall h1 h2 l, h1 === h2 -> (h1 --- l) === (h2 --- l). Parameter dif_disjoint: forall h a b, h # (singleton a b) -> (h --- a) === h. Parameter dif_disjoint': forall h1 h2 l, h1 # h2 -> (h1 --- l) # (h2 --- l). End HEAP. Module heap : HEAP with Definition l := loc with Definition v := Z. Definition l := loc. Definition v := Z. Fixpoint lb (loc:l) (he:list (l*v)) {struct he} : Prop := match he with | nil => True | hd::tl => (loc < (fst hd)) /\ (lb loc tl) end. Fixpoint set (he:(list (l*v))) : Prop := match he with nil => True | hd::tl => (lb (fst hd) tl) /\ (set tl) end. Inductive h' : Set := mk_h : forall lst, set lst -> h'. Definition h := h'. Definition lst := fun k : h => let (lst, _) := k in lst. Definition prf := fun k : h => let (lst, val) as h return (set (lst h)) := k in val. Definition set_nil : set nil. red; auto. Defined. Definition emp := mk_h nil set_nil. Definition dom' (k:list (l*v)) := map (fun x => fst x) k. Lemma In_dom: forall (a:l) (b:v) h, In (a,b) h -> In a (dom' h). induction h0. simpl; contradiction. simpl; intro. inversion_clear H. subst a0. auto. auto. Qed. Lemma loc_non_empty: forall p (h:list (l*v)), In p (dom' h) -> exists v, In (p,v) h. induction h0. simpl. tauto. intros. simpl in H. inversion_clear H. subst p. exists (snd a). simpl. induction a; auto. generalize (IHh0 H0); intro. inversion_clear H. exists x. simpl; auto. Qed. Lemma map_app : forall (A B:Set) (l1 l2:(list A)) (f:A->B), map f (l1++l2) = (map f l1)++(map f l2). induction l1. simpl. auto. simpl. intros. rewrite IHl1. auto. Qed. Definition dom k := dom' (lst k). Definition set_singleton : forall n v, set ((n,v)::nil). red; simpl; auto. Defined. Definition singleton := fun n:l => fun w:v => mk_h ((n, w)::nil) (set_singleton n w). Definition Inh := fun n k => In n (dom k). (*****) Fixpoint nat_lt (n m:nat) {struct n}: bool := match n with 0 => match m with 0 => false | S m' => true end | S n' => match m with 0 => false | S m' => nat_lt n' m' end end. Definition nat_le (n m:nat) : bool := orb (beq_nat n m) (nat_lt n m). Fixpoint nat_gt (n m:nat) {struct n}: bool := match n with 0 => false | S n' => match m with 0 => true | S m' => nat_gt n' m' end end. Definition nat_ge (n m:nat) : bool := orb (beq_nat n m) (nat_gt n m). Lemma nat_lt_true: forall n m, nat_lt n m = true -> n < m. double induction n m. simpl; intro X; inversion X. intros. omega. simpl. intros. inversion H0. simpl; intros. cut (n1 < n0). omega. apply (H0 n0 H1). Qed. Lemma nat_lt_true': forall n m, n < m -> nat_lt n m = true. double induction n m. intro X; inversion X. intros. simpl. auto. simpl. intros. inversion H0. simpl; intros. assert (n1 < n0). omega. eapply H0; auto. Qed. Lemma nat_lt_false: forall n m, nat_lt n m = false -> n >= m. double induction n m. intuition. simpl; intros. inversion H0. simpl; intros. intuition. simpl; intros. cut (n1 >= n0). omega. apply H0; auto. Qed. Lemma nat_lt_false': forall n m, n >= m -> nat_lt n m = false. double induction n m. simpl; auto. simpl; intros. inversion H0. simpl; auto. simpl; intros. apply H0; omega. Qed. Lemma nat_lt_assym: forall n m, nat_lt n m = true -> nat_lt m n= false. intros. generalize (nat_lt_true _ _ H); intro. apply nat_lt_false'. intuition. Qed. Lemma nat_lt_irrefl: forall n , nat_lt n n = false. induction n. simpl; auto. simpl. auto. Qed. Lemma nat_lt_trans: forall n m p, nat_lt n m = true -> nat_lt m p = true -> nat_lt n p = true. intros. eapply nat_lt_true'. generalize (nat_lt_true _ _ H); intro. generalize (nat_lt_true _ _ H0); intro. intuition. Qed. Lemma nat_lt_classic: forall n m, nat_lt n m = true \/ nat_lt n m = false. intros. elim nat_lt; [left; auto | right; auto]. Qed. Lemma beq_nat_com: forall n m, beq_nat n m = beq_nat m n. double induction n m. intuition. intuition. intuition. simpl. intuition. Qed. Ltac Contrad_lt := intros; Hyp_lt_clean; match goal with | id: ?a = ?b |- _ => subst a; Contrad_lt | id: ?a < ?a |- _ => generalize (lt_irrefl a); tauto | id1: ?b < ?a, id': ?a < ?b |- _ => generalize (lt_asym a b); tauto | id1: ?b < ?a, id': ?a < ?b' |- _ => generalize (lt_trans b a b' id1 id'); clear id'; intros; Contrad_lt | |- _ => tauto end with Hyp_lt_clean := match goal with | id: ?a = ?a |- _ => clear id; Hyp_lt_clean | id: ?a < ?b, id': ?a < ?b |- _ => clear id; Hyp_lt_clean | |- _ => idtac end. (*****) (*********** lookup ***********) (* TODO: optimiser la fonction (heap ordonnees) *) Fixpoint lookup' (n:l) (k:(list (l*v))) {struct k} : option v := match k with nil => None | hd::tl => match (beq_nat n (fst hd)) with true => Some (snd hd) | false => lookup' n tl end end. Lemma lb_notin : forall k a, lb (fst a) k -> ~(In a k). induction k. auto. intros. simpl in H. intro. simpl in H0. inversion_clear H0. subst a0. inversion_clear H. generalize (lt_irrefl (fst a)); tauto. inversion_clear H. generalize (IHk _ H2); intro. auto. Qed. Lemma lb_notin' : forall k a, (In a k) -> ~ (lb (fst a) k). induction k; auto. intros. simpl in H; inversion_clear H. subst a0. simpl. intro. inversion_clear H. generalize (lt_irrefl (fst a)); tauto. intro. simpl in H. inversion_clear H. generalize (IHk _ H0); auto. Qed. Lemma lb_In_uneq: forall k a b c, (In (a,b) k) -> lb c k -> beq_nat a c = false. induction k. simpl; contradiction. induction a; simpl. intros. inversion_clear H0. inversion_clear H. injection H0. intros; subst a0 b0. cut (a <> c); [idtac | omega]. apply beq_dif_false. eapply IHk. apply H0. auto. Qed. Lemma lb_In_nat_lt: forall k a b c, (In (a,b) k) -> lb c k -> nat_lt a c = false. induction k. simpl; contradiction. induction a; simpl. intros. inversion_clear H0; inversion_clear H. injection H0; intros; subst a0 b0. apply nat_lt_false'. omega. eapply IHk. apply H0. auto. Qed. Lemma lookup'_set : forall k, set k -> forall a, In a k -> lookup' (fst a) k = Some (snd a). induction k. contradiction. induction a0; induction a; simpl ;intros. inversion_clear H0. injection H1; intros. subst a0 b0. rewrite <- beq_nat_refl. auto. simpl in H. inversion_clear H. rewrite (lb_In_uneq k a0 b a). generalize (IHk H2 (a0,b)). simpl; auto. auto. auto. Qed. Lemma lookup'_set' : forall l1, set l1 -> forall n z, lookup' n l1 = Some z -> In (n,z) l1. induction l1. simpl. intros. inversion H0. induction a. simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H1 in H0. injection H0. rewrite (beq_nat_true n a H1); intro; subst z; left; auto. rewrite H1 in H0. inversion_clear H. right; apply (IHl1 H3 n z H0). Qed. Definition lookup n k := lookup' n (lst k). Lemma lookup_singleton : forall n w, lookup n (singleton n w) = Some w. unfold singleton. unfold lookup. simpl. intro. rewrite <- beq_nat_refl. tauto. Qed. Lemma lookup_In : forall h n z, lookup n h = Some z -> Inh n h. intros. unfold lookup in H. induction h0. simpl in H. generalize (lookup'_set' _ s n z H); intro. red. simpl. unfold dom. simpl. apply In_dom with z. auto. Qed. Lemma heap_is_function : forall k n z, lookup n k = Some z -> forall z', lookup n k = Some z' -> z = z'. induction k. induction lst0. unfold lookup. simpl. intros. discriminate H. unfold lookup. induction a. simpl. intro. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H. intros. rewrite H0 in H1; injection H1; auto. rewrite H. intros. unfold lookup in IHlst0. simpl in IHlst0. eapply IHlst0; [apply (proj2 s) | apply H0 | apply H1]. Qed. (* update *) (* TODO: optimiser la fonction (heap ordonnees) *) Fixpoint update' (n:l) (w:v) (k:(list (l*v))) {struct k} : list (l*v) := match k with nil => k | hd::tl => match (beq_nat n (fst hd)) with true => ((fst hd), w)::tl | false => hd::(update' n w tl) end end. Lemma update'_lb : forall k n z, lb n k -> update' n z k = k. induction k. simpl; auto. simpl. induction a. simpl; intros. inversion_clear H. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. Contrad_lt. rewrite H. rewrite IHk. auto. auto. Qed. Lemma lb_update : forall n k, lb n k -> forall m w, lb n (update' m w k). induction k; auto. induction a; simpl; intros. inversion_clear H. generalize (beq_nat_classic m a); intro X; inversion_clear X. generalize (beq_nat_true m a H); intros. subst a. rewrite <- beq_nat_refl. simpl. intuition. rewrite H. simpl. intuition. Qed. Lemma set_update: forall k, set k -> forall n w, set (update' n w k). induction k; auto. induction a. simpl. intros. inversion_clear H. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. subst a. rewrite <- beq_nat_refl. simpl. intuition. rewrite H. simpl. split. apply lb_update. auto. intuition. Qed. Definition update n w k := mk_h (update' n w (lst k)) (set_update (lst k) (prf k) n w). Lemma update_dom' : forall k n z, dom' (update' n z k) = dom' k. induction k. simpl; auto. induction a. simpl. intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. subst a. rewrite <- beq_nat_refl. simpl. intuition. rewrite H. simpl. rewrite IHk. auto. Qed. Lemma update_dom : forall k n z, dom (update n z k) = dom k. induction k. induction lst0. unfold dom; simpl. auto. induction a. unfold dom; simpl. intro. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. subst a. rewrite <- beq_nat_refl. simpl. intuition. rewrite H. simpl. unfold dom in IHlst0; simpl in IHlst0. intros. rewrite IHlst0. auto. apply (proj2 s). Qed. (*********** element removal ***********) Fixpoint del' (n:l) (k:(list (l*v))) {struct k} : list (l*v) := match k with nil => nil | hd::tl => match (beq_nat n (fst hd)) with true => (del' n tl) | false => hd::(del' n tl) end end. Lemma lb_del' : forall k n, lb n k -> forall m, lb n (del' m k). induction k; simpl; auto. induction a; simpl; intros. inversion_clear H. generalize (beq_nat_classic m a); intro X; inversion_clear X. generalize (beq_nat_true m a H); intros. subst a. rewrite <- beq_nat_refl. intuition. rewrite H. simpl. intuition. Qed. Lemma set_del' : forall k, set k -> forall n, set (del' n k). induction k. simpl. auto. induction a; simpl; intros. inversion_clear H. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. subst a. rewrite <- beq_nat_refl. intuition. rewrite H. simpl. split; [apply lb_del'; auto | intuition]. Qed. Lemma lb_del'' : forall k n, lb n k -> del' n k = k. induction k; auto. induction a; simpl; intros. inversion_clear H. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. Contrad_lt. rewrite H. rewrite IHk; [auto | auto]. Qed. Lemma del'_del' : forall k n m, del' n (del' m k) = del' m (del' n k). induction k. simpl; auto. induction a; simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_classic m a); intro X; inversion_clear X. generalize (beq_nat_true n a H); intros. generalize (beq_nat_true m a H0); intros. subst n m. rewrite <- beq_nat_refl; auto. rewrite H; rewrite H0. generalize (beq_nat_true n a H); intros; subst a. simpl. rewrite <- beq_nat_refl; auto. generalize (beq_nat_classic m a); intro X; inversion_clear X. rewrite H; rewrite H0. generalize (beq_nat_true m a H0); intros; subst a. simpl; rewrite <- beq_nat_refl; auto. rewrite H; rewrite H0. simpl. rewrite H; rewrite H0. rewrite IHk. auto. Qed. (* Lemma del'_del' : forall k n m, del' n (del' m k) = del' m (del' n k). induction k. simpl. auto. simpl. intros. case (lt_eq_lt_dec m (fst a)). intro. dependent inversion s. simpl. case (lt_eq_lt_dec n (fst a)). intro. dependent inversion s0. simpl. case (lt_eq_lt_dec m (fst a)). intro. dependent inversion s1. rewrite IHk; auto. subst m. generalize (lt_irrefl (fst a)); tauto. intro. generalize (lt_asym _ _ l2); tauto. subst n. rewrite IHk; auto. intro. simpl. case (lt_eq_lt_dec m (fst a)). intro. dependent inversion s0. rewrite IHk; auto. subst m. generalize (lt_irrefl (fst a)); tauto. intro. rewrite IHk; auto. subst m. case (lt_eq_lt_dec n (fst a)). intro. dependent inversion s0. simpl. case (lt_eq_lt_dec (fst a) (fst a)). intro. dependent inversion s1. generalize (lt_irrefl (fst a)); tauto. rewrite IHk; auto. intro. generalize (lt_irrefl (fst a)); tauto. subst n. auto. intros. simpl. case (lt_eq_lt_dec (fst a) (fst a)). intro. dependent inversion s0. generalize (lt_irrefl (fst a)); tauto. rewrite IHk; auto. generalize (lt_irrefl (fst a)); tauto. intros. case (lt_eq_lt_dec n (fst a)). intro. dependent inversion s. simpl. case (lt_eq_lt_dec n (fst a)). intro. dependent inversion s0. case (lt_eq_lt_dec m (fst a)). intro. dependent inversion s1. rewrite IHk; auto. subst m. generalize (lt_irrefl (fst a)); tauto. intros. rewrite IHk; auto. subst n. generalize (lt_irrefl (fst a)); tauto. intro. case (lt_eq_lt_dec m (fst a)). intro. dependent inversion s0. generalize (lt_asym _ _ l3); tauto. subst m. generalize (lt_irrefl (fst a)); tauto. intro. rewrite IHk; auto. subst n. simpl. case (lt_eq_lt_dec (fst a) (fst a)). intro. dependent inversion s0. generalize (lt_irrefl (fst a)); tauto. rewrite IHk; auto. generalize (lt_irrefl (fst a)); tauto. intros. simpl. case (lt_eq_lt_dec n (fst a)). intro. dependent inversion s. generalize (lt_asym _ _ l2); tauto. subst n. generalize (lt_irrefl (fst a)); tauto. intros. case (lt_eq_lt_dec m (fst a)). intro. dependent inversion s. rewrite IHk; auto. subst m. generalize (lt_irrefl (fst a)); tauto. intro. rewrite IHk; auto. Qed. *) Lemma del'_del'' : forall k n, del' n (del' n k) = del' n k. induction k. simpl; auto. induction a; simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H. apply IHk. rewrite H. simpl. rewrite H. rewrite IHk; auto. Qed. Lemma pp : forall k x, (In x (dom k)) -> forall y, y <> x -> (In x (dom' (del' y (lst k)))). induction k. induction lst0. simpl. tauto. unfold dom in IHlst0. simpl in IHlst0. induction a; simpl in s; simpl; intros. inversion_clear H. subst a. rewrite (beq_dif_false y x); [idtac | auto]. simpl. left; auto. generalize (beq_nat_classic y a); intro X; inversion_clear X. rewrite H. eapply IHlst0. apply (proj2 s). auto. auto. rewrite H. simpl. right. eapply IHlst0. apply (proj2 s). auto. auto. Qed. Lemma pp' : forall k x y, x <> y -> In x (map (fun x => fst x) (del' y (lst k))) -> In x (dom k). induction k. induction lst0. auto. unfold dom in IHlst0. simpl in IHlst0. induction a; simpl in s; simpl; intros. generalize (beq_nat_classic y a); intro X; inversion_clear X. rewrite H1 in H0. right; eapply IHlst0. apply (proj2 s). apply H. auto. rewrite H1 in H0. simpl in H0. inversion_clear H0. left; auto. right; eapply IHlst0. apply (proj2 s). apply H. auto. Qed. Lemma pp'' : forall k x y, x <> y -> In x (dom' (del' y k)) -> In x (dom' k). induction k. simpl. auto. induction a; simpl; intros. generalize (beq_nat_classic y a); intro X; inversion_clear X. generalize (beq_nat_true _ _ H1); intro; subst y. rewrite <- beq_nat_refl in H0. right; eapply IHk. apply H. auto. rewrite H1 in H0. simpl in H0. inversion_clear H0. intuition. right; eapply IHk. apply H. auto. Qed. Lemma In_del' : forall k c n, In c (del' n k) -> (fst c) <> n -> In c k. induction k. simpl; tauto. induction c; induction a. simpl. intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H1 in H. right. eapply IHk. apply H. simpl; auto. rewrite H1 in H. inversion_clear H. left; auto. right. eapply IHk. apply H2. simpl; auto. Qed. (*********** element addition ***********) Fixpoint add_lst (n: l) (w: v) (lst: list (l * v)) {struct lst}: list (l * v) := match lst with nil => (n,w)::nil | (n',w')::tl => match (nat_lt n' n) with true => (n',w')::(add_lst n w tl) | false => match (beq_nat n' n) with true => (n',w)::tl | false => (n,w)::(n',w')::tl end end end. Lemma lb_trans: forall k n m , lb m k -> n < m -> lb n k. induction k. simpl. intros; apply I. intros. simpl in H; simpl. split; [omega | idtac]. apply (IHk n m (proj2 H) H0). Qed. Lemma lb_add_lst : forall k n, lb n k -> forall m, n < m -> forall w, lb n (add_lst m w k). induction k. simpl; auto. induction a. simpl; intros. inversion_clear H. generalize (beq_nat_classic a m); intro X; inversion_clear X. rewrite H. assert (nat_lt a m = false). generalize (nat_lt_classic a m); intro X; inversion_clear X. generalize (beq_nat_true a m H); intros. generalize (nat_lt_true a m H3); intros. Contrad_lt. auto. rewrite H3. simpl. intuition. rewrite H. generalize (nat_lt_classic a m); intro X; inversion_clear X. rewrite H3. simpl. auto. rewrite H3. simpl. auto. Qed. Lemma add_lst_lb: forall k a b, lb a k -> add_lst a b k = (a, b)::k. induction k. simpl ;auto. induction a. simpl. intros. inversion_clear H. generalize (beq_nat_classic a a0); intro X; inversion_clear X. generalize (beq_nat_true a a0 H); Contrad_lt. rewrite H. generalize (nat_lt_classic a a0); intro X; inversion_clear X. generalize (nat_lt_true a a0 H2); intros. Contrad_lt. rewrite H2. auto. Qed. Lemma set_add : forall lst, set lst -> forall n w, set (add_lst n w lst). induction lst0. simpl; auto. induction a; simpl; intros. inversion_clear H. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H. generalize (nat_lt_classic a n); intro X; inversion_clear X. generalize (nat_lt_true a n H2); intros. generalize (beq_nat_true a n H); Contrad_lt. rewrite H2. simpl. intuition. rewrite H. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H2. simpl. split. apply lb_add_lst. auto. generalize (nat_lt_true a n H2); auto. auto. rewrite H2. assert (n < a). generalize (nat_lt_false a n H2); auto. intros. inversion H3. subst a. rewrite <- beq_nat_refl in H; inversion H. omega. simpl. intuition. eapply lb_trans. apply H0. auto. Qed. (*********** heap equivalence ***********) Definition equal (h1: h) (h2: h) := (lst h1) = (lst h2). Notation "k '===' m" := (equal k m) (at level 79) : heap_scope. Open Local Scope heap_scope. Lemma equal_ext: forall h1 h2, (h1 === h2) -> h1 = h2. destruct h1 as [lst1 prf1]. destruct h2 as [lst2 prf2]. unfold equal. simpl. intros. subst lst1. rewrite (proof_irrelevance _ prf1 prf2). auto. Qed. Lemma equal_refl : forall h, h === h. intros. destruct h0 as [lst0 prf0]. unfold equal. simpl. auto. Qed. Lemma equal_sym : forall h1 h2, h1 === h2 -> h2 === h1. destruct h1 as [lst1 prf1]. destruct h2 as [lst2 prf2]. unfold equal. auto. Qed. Lemma equal_trans : forall h1 h2 h3, h1 === h2 -> h2 === h3 -> h1 === h3. destruct h1 as [lst1 prf1]. destruct h2 as [lst2 prf2]. destruct h3 as [lst3 prf3]. unfold equal. simpl. intros. subst lst1; subst lst2; auto. Qed. Lemma equal_emp : forall h, h === emp -> h = emp. destruct h0 as [lst0 prf0]. unfold equal. simpl. intros. subst lst0. unfold emp. rewrite (proof_irrelevance _ prf0 set_nil). auto. Qed. Lemma update_singleton : forall n w w', update n w' (singleton n w) === singleton n w'. unfold equal. simpl. intros. rewrite <- beq_nat_refl. auto. Qed. Lemma lookup_equal : forall h1 h2, h1 === h2 -> forall n z, lookup n h1 = Some z -> lookup n h2 = Some z. destruct h1 as [lst1 prf1]. destruct h2 as [lst2 prf2]. unfold equal. simpl. intro. subst lst1. rewrite (proof_irrelevance _ prf1 prf2). auto. Qed. (*********** heap union ***********) Fixpoint app' (h1 h2 : (list (l*v))) {struct h1} : list (l*v) := match h1 with nil => h2 | hd::tl => (add_lst (fst hd) (snd hd) (app' tl h2)) end. Lemma set_app' : forall h1 h2, (set h1) -> (set h2) -> set (app' h1 h2). induction h1. simpl. auto. simpl. intros. apply set_add. apply IHh1. apply (proj2 H). auto. Qed. Lemma add_lst_del': forall lst n w n', set lst -> n' <> n -> add_lst n w (del' n' lst) = del' n' (add_lst n w lst). induction lst0. simpl; intros. rewrite (beq_dif_false n' n H0); simpl. auto. induction a; simpl; intros. inversion_clear H. generalize (beq_dif_false n' n H0); intros. generalize (beq_nat_classic n' a); intro X; inversion_clear X. rewrite H3. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H4. generalize (beq_nat_true n' a H3); intro; subst n'; simpl; rewrite <- beq_nat_refl; intuition. rewrite H4. generalize (beq_nat_classic a n); intro X; inversion_clear X. generalize (beq_nat_true n' a H3); intros. generalize (beq_nat_true a n H5); intros. Contrad_lt. rewrite H5. simpl. rewrite H. rewrite H3. rewrite IHlst0. generalize (beq_nat_true n' a H3); intros. subst a. clear H H5 H3. rewrite add_lst_lb. simpl. rewrite (beq_dif_false n' n H0). auto. eapply lb_trans. apply H1. generalize (nat_lt_classic n n'); intro X; inversion_clear X. apply nat_lt_true. auto. generalize (nat_lt_false n' n H4); intros. generalize (nat_lt_false n n' H); intros. assert (n = n'). intuition. assert False. apply H0. auto. contradiction. auto. auto. rewrite H3. simpl. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H4. simpl. rewrite H3. rewrite IHlst0. auto. auto. auto. rewrite H4. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H5. simpl. rewrite H3. auto. rewrite H5. simpl. rewrite H. rewrite H3. auto. Qed. Lemma add_lst_del'': forall lst n w, del' n (add_lst n w lst) = del' n lst. induction lst0. simpl. intros. rewrite <- beq_nat_refl. auto. induction a; simpl; auto. intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H0); intros. generalize (nat_lt_true a n H); intros. Contrad_lt. rewrite H0. simpl. rewrite H0. rewrite IHlst0. auto. rewrite H. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H0. rewrite beq_nat_com. rewrite H0. simpl. rewrite beq_nat_com. rewrite H0. auto. rewrite H0. rewrite beq_nat_com. rewrite H0. simpl. rewrite <- beq_nat_refl. rewrite beq_nat_com. rewrite H0. auto. Qed. Lemma del'_app' : forall k m n, set m -> set k -> (del' n (app' k m))=(app' (del' n k) (del' n m)). induction k; simpl; auto. induction a. simpl. intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H1. rewrite (beq_nat_true n a H1). rewrite add_lst_del''. intuition. rewrite H1. simpl. rewrite <- add_lst_del'. rewrite IHk. auto. intuition. intuition. apply set_app'. intuition. intuition. apply (beq_nat_false). auto. Qed. Lemma app'_nil : forall k, (set k) -> (app' k nil) = k. induction k; auto. induction a. simpl. intros. rewrite IHk;[ apply add_lst_lb; apply (proj1 H) | apply (proj2 H)]. Qed. Lemma add_lst_add_lst: forall lst n' w' n w, set lst -> n' <> n -> add_lst n w (add_lst n' w' lst) = add_lst n' w' (add_lst n w lst). induction lst0. simpl. intros. generalize (beq_nat_classic n' n); intro X; inversion_clear X. generalize (beq_nat_true n' n H1); intro. Contrad_lt. rewrite H1. generalize (nat_lt_classic n' n); intro X; inversion_clear X. rewrite H2. generalize (nat_lt_classic n n'); intro X; inversion_clear X. rewrite (nat_lt_assym _ _ H2) in H3; inversion H3. rewrite H3. rewrite beq_nat_com. rewrite H1. auto. rewrite H2. rewrite beq_nat_com. rewrite H1. generalize (nat_lt_classic n n'); intro X; inversion_clear X. rewrite H3. auto. generalize (nat_lt_false n' n H2); intros. generalize (nat_lt_false n n' H3); intros. intuition. assert (n' = n). intuition. generalize (H0 H6); contradiction. induction a; simpl; intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H1. generalize (nat_lt_classic a n'); intro X; inversion_clear X. rewrite H2. simpl. rewrite H1. rewrite H2. rewrite IHlst0. auto. intuition. auto. rewrite H2. generalize (beq_nat_classic a n'); intro X; inversion_clear X. rewrite H3. simpl. rewrite H1. rewrite H2. rewrite H3. auto. rewrite H3. simpl. generalize (nat_lt_false _ _ H2); intros. generalize (nat_lt_true _ _ H1); intros. assert (n' < n). intuition. rewrite (nat_lt_true' _ _ H6). rewrite H1. rewrite H2. rewrite H3. auto. generalize (nat_lt_classic a n'); intro X; inversion_clear X. rewrite H2. rewrite H1. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H3. simpl. rewrite H1. rewrite H3. rewrite H2. auto. simpl. rewrite H1. rewrite H3. simpl. generalize (nat_lt_false _ _ H1); intros. generalize (nat_lt_true _ _ H2); intros. assert (n < n'). intuition. rewrite (nat_lt_true' _ _ H6). generalize (beq_nat_classic a n'); intro X; inversion_clear X. rewrite H7. rewrite H2. auto. rewrite H2. auto. rewrite H1; rewrite H2. generalize (beq_nat_classic a n'); intro X; inversion_clear X. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite <- (beq_nat_true _ _ H3) in H0. rewrite <- (beq_nat_true _ _ H4) in H0. tauto. rewrite H3; rewrite H4. simpl. rewrite H1; rewrite H2. rewrite H3; rewrite H4. generalize (nat_lt_classic n n'); intro X; inversion_clear X. rewrite H5. auto. generalize (beq_nat_true _ _ H3); intro; subst a. clear H3. generalize (nat_lt_false _ _ H5); intros. generalize (nat_lt_false _ _ H1); intros. assert (n' = n). intuition. generalize (H0 H7); contradiction. rewrite H3. generalize (beq_nat_classic a n); intro X; inversion_clear X. generalize (beq_nat_true _ _ H4); intro; subst a. rewrite H4. simpl. generalize (nat_lt_false _ _ H2); intros. assert (n' = n \/ n' < n). inversion_clear H5. left; auto. right. intuition. inversion_clear H6. contradiction. rewrite (nat_lt_true' _ _ H7). rewrite nat_lt_irrefl. rewrite <- beq_nat_refl. rewrite H3. rewrite H2. auto. rewrite H4. simpl. generalize (nat_lt_classic n' n); intro X; inversion_clear X. rewrite H5. rewrite H1. rewrite H4. rewrite (nat_lt_assym _ _ H5). rewrite beq_dif_false; [auto | auto]. rewrite H5. rewrite beq_dif_false; [idtac | auto]. generalize (nat_lt_classic n n'); intro X; inversion_clear X. rewrite H6. rewrite H3. rewrite H2. auto. generalize (nat_lt_false _ _ H5); intros. generalize (nat_lt_false _ _ H6); intros. assert (n' = n). intuition. contradiction. Qed. Lemma add_lst_add_lst': forall lst n w' w, add_lst n w (add_lst n w' lst) = add_lst n w lst. induction lst0. simpl. intros. rewrite nat_lt_irrefl. rewrite <- beq_nat_refl. auto. induction a. simpl; intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H. simpl. rewrite H. rewrite IHlst0. auto. rewrite H. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H0. simpl. rewrite H. rewrite H0. auto. rewrite H0. simpl. rewrite nat_lt_irrefl. rewrite <- beq_nat_refl. auto. Qed. Lemma add_lst_app': forall lst1 lst2 n w, set lst1 -> set lst2 -> add_lst n w (app' lst1 lst2) = app' (add_lst n w lst1) lst2. induction lst1. simpl. auto. induction a; simpl. intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H1. simpl. rewrite <- IHlst1. eapply add_lst_add_lst. apply set_app'. intuition. auto. generalize (nat_lt_true _ _ H1); intro; intuition. intuition. auto. rewrite H1. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H2. simpl. generalize (beq_nat_true _ _ H2); intro; subst a. rewrite add_lst_add_lst'. auto. rewrite H2. simpl. auto. Qed. Definition union h1 h2 := mk_h (app' (lst h1) (lst h2)) (set_app' _ _ (prf h1) (prf h2)). Notation "k '+++' m" := (union k m) (at level 78) : heap_scope. Definition dif h l := mk_h (del' l (lst h) ) (set_del' (lst h) (prf h) l). Notation "k '---' m" := (dif k m) (at level 78) : heap_scope. Lemma dif_singleton_emp: forall a b, (singleton a b) --- a === emp. intros. unfold singleton. unfold dif. simpl. unfold equal. simpl. rewrite <- beq_nat_refl. auto. Qed. Lemma dif_union: forall h1 h2 a, (h1 +++ h2) --- a === (h1 --- a) +++ (h2 --- a). intros. destruct h1 as [h1 s1]. destruct h2 as [h2 s2]. unfold dif. simpl. unfold union. simpl. unfold equal. simpl. apply (del'_app' h1 h2 a s2 s1). Qed. Lemma dif_not_in_dom: forall h l, ~(In l (dom h)) -> (h --- l) === h. destruct h0 as [h0 s0]. induction h0. intros. unfold dif; unfold equal. simpl. auto. intros. unfold dif; unfold equal. induction a. simpl. generalize (beq_nat_classic l0 a); intro X; inversion_clear X. rewrite (beq_nat_true _ _ H0) in H. unfold dom in H. simpl in H. intuition. rewrite H0; simpl. unfold dif in IHh0; unfold equal in IHh0; simpl in IHh0. assert (~(In l0 (dom (mk_h h0 (proj2 s0))))). simpl in H. unfold dom; simpl; red; intros. intuition. rewrite (IHh0 (proj2 s0) l0 H1). auto. Qed. Lemma dif_equal: forall h1 h2 l, h1 === h2 -> ((dif h1 l) === (dif h2 l)). destruct h1 as [h1 s1]. destruct h2 as [h2 s2]. unfold dif; unfold equal; unfold dom. simpl. intros. subst h1. auto. Qed. Lemma equal_union_emp : forall h1, h1 +++ emp === h1. destruct h1 as [h1 s1]. induction h1. red; simpl. auto. induction a. red; simpl. rewrite app'_nil. simpl in s1. apply add_lst_lb. apply (proj1 s1). apply (proj2 s1). Qed. Lemma union_emp'' : forall h1, h1 +++ emp === emp -> h1 === emp. induction h1 as [h1 s1]. unfold union; unfold equal; simpl; auto. induction h1. auto. induction a. simpl. intros. rewrite app'_nil in H. rewrite add_lst_lb in H. auto. simpl in s1. apply (proj1 s1). apply (proj2 s1). Qed. Lemma union_assoc : forall h1 h2 h3, h1 +++ (h2 +++ h3) === (h1 +++ h2) +++ h3. destruct h1. destruct h2. destruct h3. unfold equal; unfold union; simpl. induction lst0. simpl. auto. induction a. simpl. intros. simpl in s. simpl in IHlst0. rewrite IHlst0; [idtac | exact (proj2 s)]. rewrite add_lst_app'; [auto | idtac | auto]. apply set_app'; [apply (proj2 s) | auto]. Qed. (*********** disjoint ***********) Definition disjoint h1 h2 := inter (dom h1) (dom h2) nil. Notation "k '#' m" := (disjoint k m) (at level 79) : heap_scope. Lemma disjoint_com: forall h1 h2, h1 # h2 -> h2 # h1. intros. unfold disjoint. red; split; intros. unfold disjoint in H. red in H. generalize (H x); intro X; inversion_clear X; tauto. red in H0; tauto. Qed. Lemma equal_union : forall h1 h2, h1 === h2 -> forall h0, h0 # h1 -> h1 +++ h0 === h2 +++ h0. unfold union; unfold equal; simpl. intros. rewrite H. auto. Qed. (* union is commutative only when sets are disjoint *) Lemma union_com : forall h1 h2, h1 # h2 -> h1 +++ h2 === h2 +++ h1. unfold union; unfold equal; simpl. intros. induction h1. induction h2. simpl. unfold disjoint in H; unfold inter in H; unfold dom in H; simpl in H. generalize lst0 s lst1 s0 H. clear lst0 s lst1 s0 H. induction lst0. simpl. intros. rewrite app'_nil. auto. intuition. induction a. simpl; intros. rewrite IHlst0. generalize lst1 a b IHlst0 s s0 H. clear lst1 a b IHlst0 s s0 H. induction lst1. simpl; intros. rewrite add_lst_lb. auto. intuition. simpl. induction a. simpl. intros. rewrite <- IHlst1. rewrite add_lst_add_lst. auto. apply set_app'. intuition. intuition. red; intros. subst a0. generalize (H a). intuition. apply IHlst0. intuition. intuition. intros. generalize (H x); intro; intuition. intuition. intuition. intros. split. intros. generalize (H x); intro X; inversion_clear X. apply H1. intuition. intros; contradiction. Qed. Lemma In_dom'_add_lst: forall k a b, In a (dom' (add_lst a b k)). induction k. simpl. intuition. induction a; simpl. intros. generalize (nat_lt_classic a a0); intro X; inversion_clear X. rewrite H. simpl. right. apply IHk. rewrite H. generalize (beq_nat_classic a a0); intro X; inversion_clear X. rewrite (beq_nat_true _ _ H0). rewrite <- beq_nat_refl. simpl; left; auto. rewrite H0. simpl. auto. Qed. Lemma In_dom'_add_lst': forall k x a b, In x (dom' k) -> In x (dom' (add_lst a b k)). induction k. simpl; contradiction. induction a; simpl; intros. inversion_clear H. subst a. generalize (nat_lt_classic x a0); intro X; inversion_clear X. rewrite H. simpl. intuition. rewrite H. generalize (beq_nat_classic x a0); intro X; inversion_clear X. rewrite (beq_nat_true _ _ H0). rewrite <- beq_nat_refl. simpl; intuition. rewrite H0. simpl; intuition. generalize (nat_lt_classic a a0); intro X; inversion_clear X. rewrite H. simpl. right. apply IHk. auto. rewrite H. generalize (beq_nat_classic a a0); intro X; inversion_clear X. rewrite (beq_nat_true _ _ H1). rewrite <- beq_nat_refl. simpl; intuition. rewrite H1. simpl; intuition. Qed. Lemma In_dom_union : forall k x, In x (dom k) -> forall m, In x (dom (k +++ m)). unfold dom; unfold union; simpl. destruct k. destruct m. induction lst0. simpl in H. contradiction. induction a; simpl. simpl in s. simpl in H. inversion_clear H. subst a. apply In_dom'_add_lst. simpl in IHlst0. apply In_dom'_add_lst'. apply IHlst0. intuition. intuition. Qed. Lemma In_dom_union' : forall m k x, In x (dom k) -> In x (dom (m +++ k)). destruct m. destruct k. generalize lst0 s lst1 s0. clear lst0 s lst1 s0. unfold dom; unfold union; simpl. induction lst0. simpl. intros. auto. induction a; simpl; intros. apply In_dom'_add_lst'. apply IHlst0. intuition. intuition. intuition. Qed. Lemma add_lst'_In_dom': forall k x a b, In x (dom' (add_lst a b k)) -> x = a \/ In x (dom' k). induction k. simpl. intuition. induction a; simpl; intros. generalize (nat_lt_classic a a0); intro X; inversion_clear X. rewrite H0 in H. simpl in H. inversion_clear H. intuition. generalize (IHk _ _ _ H1); intro X; inversion_clear X. intuition. intuition. rewrite H0 in H. generalize (beq_nat_classic a a0); intro X; inversion_clear X. rewrite H1 in H. simpl in H. inversion_clear H. intuition. intuition. rewrite H1 in H. simpl in H. inversion_clear H. intuition. inversion_clear H2. intuition. intuition. Qed. Lemma In_union_dom : forall k m x, In x (dom (k +++ m)) -> (In x (dom k)) \/ (In x (dom m)). destruct m. destruct k. generalize lst0 s lst1 s0. clear lst0 s lst1 s0. unfold dom; unfold union; simpl. induction lst1. simpl. intuition. induction a; simpl; intros. simpl in H. generalize (add_lst'_In_dom' _ _ _ _ H); intro X; inversion_clear X. intuition. generalize (IHlst1 (proj2 s0) x H0); intro X; inversion_clear X. intuition. intuition. Qed. Lemma distributivity : forall h1 h2, forall h0, h0 # (union h1 h2) <-> (h0 # h1) /\ (h0 # h2). split; intros. split. red; red; split; intros. red in H; red in H. generalize (H x); intro X; inversion_clear X. apply H1. split. intuition. apply In_dom_union. intuition. simpl in H0; contradiction. red; red; split; intros. red in H; red in H. generalize (H x); intro X; inversion_clear X. apply H1. split. intuition. apply In_dom_union'. intuition. simpl in H0. contradiction. inversion_clear H. red; red; split; intros. inversion_clear H. generalize (In_union_dom _ _ _ H3); intro. inversion_clear H. red in H0. red in H0. generalize (H0 x); tauto. red in H1; red in H1. generalize (H1 x); tauto. simpl in H; contradiction. Qed. Lemma disjoint_union' : forall h1 h2 h0, h0 # (h1 +++ h2) -> h0 # h1 /\ h0 # h2. intros. generalize (distributivity h1 h2 h0); intro. intuition. Qed. Lemma equal_disjoint : forall h1 h2, h1 === h2 -> forall h3, h1 # h3 -> h2 # h3. do 3 intro. red in H. induction h1. induction h2. simpl in H. induction H. intros. auto. Qed. Lemma equal_union_disjoint : forall x1 x2, forall x x0, x === (x1 +++ x2) /\ (x # x0) -> x1 # x0. intros. generalize (distributivity x1 x2 x0); intro. inversion_clear H0. assert (disjoint x0 (union x1 x2)). apply disjoint_com. apply equal_disjoint with x. intuition. intuition. generalize (H1 H0); intro. inversion_clear H3. apply disjoint_com. auto. Qed. Lemma disjoint_union : forall h1 h2, forall h0, (h0 # h1) /\ (h0 # h2) -> (h0 # (h1 +++ h2)). intros. generalize (distributivity h1 h2 h0); intro. tauto. Qed. Lemma lookup'_add_lst : forall k n w, lookup' n (add_lst n w k) = Some w. induction k. simpl. intros. rewrite <- beq_nat_refl; auto. induction a. simpl. intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H. simpl. generalize (nat_lt_true a n H); intros. assert (n <> a). intuition. rewrite (beq_dif_false n a H1). apply IHk. rewrite H. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H0. simpl. rewrite beq_nat_com; rewrite H0; auto. rewrite H0. simpl. rewrite <- beq_nat_refl; auto. Qed. Lemma lookup'_add_lst' : forall k n w n' , n <> n' -> lookup' n' (add_lst n w k) = lookup' n' k. induction k. simpl. intros. rewrite beq_nat_com. rewrite (beq_dif_false n n' H); auto. induction a; simpl; intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H0. simpl. generalize (beq_nat_classic n' a); intro X; inversion_clear X. rewrite H1. auto. rewrite H1. apply IHk. auto. rewrite H0. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H1. generalize (beq_nat_classic n' a); intro X; inversion_clear X. rewrite <- (beq_nat_true _ _ H1) in H; rewrite <- (beq_nat_true _ _ H2) in H. tauto. rewrite H2. simpl. rewrite H2. auto. rewrite H1. generalize (beq_nat_classic n' a); intro X; inversion_clear X. rewrite H2. simpl. rewrite beq_nat_com. rewrite (beq_dif_false n n' H). rewrite H2. auto. simpl. rewrite beq_nat_com. rewrite (beq_dif_false n n' H). rewrite H2. auto. Qed. Lemma lookup_union : forall h1 h2, h1 # h2 -> forall n z, lookup n h1 = Some z -> lookup n (h1 +++ h2) = Some z. destruct h1. destruct h2. unfold disjoint; unfold inter; unfold union; unfold lookup; simpl. generalize lst0 s lst1 s0. clear lst0 s lst1 s0. induction lst0. simpl; intros. inversion H0. induction a; simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (beq_nat_true n a H1); intro; subst a; rewrite <- beq_nat_refl in H0. injection H0; intro; subst b. apply lookup'_add_lst. rewrite lookup'_add_lst'. rewrite H1 in H0. eapply IHlst0 with (s := (proj2 s)) (s0 := s0). unfold dom. simpl. intros. generalize (H x); intros. unfold dom in H2. simpl in H2. intuition. auto. generalize (beq_nat_false _ _ H1). intuition. Qed. Lemma disjoint_update : forall n z h1 h2, h1 # h2 -> (update n z h1) # h2. unfold disjoint. intros. rewrite (update_dom h1 n z). auto. Qed. Lemma update'_del' : forall k n z m, n <> m -> (update' n z (del' m k)) = (del' m (update' n z k)). induction k. simpl. auto. induction a; simpl; intros. generalize (beq_nat_classic m a); intro X; inversion_clear X. rewrite H0. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite (beq_nat_true _ _ H1) in H; rewrite <- (beq_nat_true _ _ H0) in H. tauto. rewrite H1. simpl. rewrite H0. apply IHk. auto. rewrite H0. generalize (beq_nat_classic n a); intro X; inversion_clear X. simpl. rewrite H1. simpl. rewrite H0. auto. simpl. rewrite H1. simpl. rewrite H0. rewrite IHk. auto. auto. Qed. Lemma update'_not_In_dom: forall k n w, ~ In n (dom' k) -> update' n w k = k. induction k. simpl; auto. induction a; simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite (beq_nat_true n a H0) in H. intuition. rewrite H0. rewrite IHk. auto. intuition. Qed. Lemma update'_app : forall l1 l2 n z, set l1 -> set l2 -> (inter (dom' l1) (dom' l2) nil) -> update' n z (app l1 l2) = app (update' n z l1) (update' n z l2). unfold inter; simpl. induction l1. simpl. auto. induction a; simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H2. simpl. assert (~ In a (dom' l2)). generalize (H1 a); intros. intuition. rewrite update'_not_In_dom. auto. rewrite (beq_nat_true _ _ H2). auto. rewrite H2. simpl. rewrite IHl1. auto. intuition. intuition. intros. generalize (H1 x); intro; intuition. Qed. Lemma equal_update : forall h1 h2, h1 === h2 -> forall n z, update n z h1 === update n z h2. intros. rewrite (equal_ext h1 h2 H). unfold equal. auto. Qed. Lemma update_add_lst: forall k n w w', update' n w (add_lst n w' k) = (add_lst n w k). induction k. simpl; intros. rewrite <- beq_nat_refl. auto. induction a; simpl. intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H. simpl. generalize (beq_nat_classic n a); intro X; inversion_clear X. generalize (nat_lt_true a n H); intro. generalize (beq_nat_true n a H0); intro; Contrad_lt. rewrite H0. rewrite IHk. auto. rewrite H. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H0. simpl. rewrite beq_nat_com. rewrite H0. auto. rewrite H0. simpl. rewrite <- beq_nat_refl. auto. Qed. Lemma update_add_lst': forall k n n' w w', n' <> n -> update' n w (add_lst n' w' k) = (add_lst n' w' (update' n w k)). induction k. simpl. intros. rewrite beq_nat_com. rewrite (beq_dif_false _ _ H). auto. induction a; simpl; intros. generalize (nat_lt_classic a n'); intro X; inversion_clear X. rewrite H0. simpl. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H1. simpl. rewrite H0. auto. rewrite H1. simpl. rewrite H0. rewrite IHk. auto. auto. rewrite H0. generalize (beq_nat_classic a n'); intro X; inversion_clear X. rewrite H1. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite (beq_nat_true n a H2) in H; rewrite (beq_nat_true _ _ H1) in H; tauto. rewrite H2. simpl. rewrite H2. rewrite H0. rewrite H1. auto. rewrite H1. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H2. simpl. rewrite beq_nat_com. rewrite (beq_dif_false _ _ H). rewrite H2. rewrite H0. rewrite H1. auto. rewrite H2. simpl. rewrite beq_nat_com. rewrite (beq_dif_false _ _ H). rewrite H2. rewrite H0. rewrite H1. auto. Qed. Lemma equal_update_L : forall h1 h2, h1 # h2 -> forall h, h === (h1 +++ h2) -> forall n z, Inh n h1 -> (update n z h) === (update n z h1) +++ h2. destruct h1. destruct h2. unfold disjoint; unfold inter. destruct h0. unfold equal; unfold union; unfold Inh. simpl. generalize lst0 s lst1 s0 H lst2 s1. clear lst0 s lst1 s0 H lst2 s1. induction lst0. simpl. contradiction. induction a; simpl; intros. inversion_clear H1. subst n. rewrite <- beq_nat_refl. subst lst2. simpl. rewrite update_add_lst. auto. subst lst2. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H0. simpl. rewrite (beq_nat_true n a H0). rewrite update_add_lst. auto. rewrite H0. simpl. rewrite update_add_lst'. assert (forall x : l, In x (dom (mk_h lst0 (proj2 s))) /\ In x (dom (mk_h lst1 s0)) <-> In x nil) . unfold dom; simpl. intros. generalize (H x); intros; intuition. rewrite (IHlst0 (proj2 s) lst1 s0 H1 (app' lst0 lst1) ). auto. apply set_app'. apply (proj2 s). auto. auto. intuition. generalize (beq_nat_false _ _ H0); intro; auto. Qed. Lemma disjoint_equal : forall h1 h2, h1 # h2 -> forall h3, h2 === h3 -> h1 # h3. intros. rewrite (equal_ext _ _ H0) in H. auto. Qed. Lemma disjoint_emp : forall h, h # emp. unfold disjoint. unfold inter. unfold dom. destruct h0. simpl. intuition. Qed. Lemma disjoint_singleton : forall x y z z', x <> y -> heap.disjoint (heap.singleton x z) (heap.singleton y z'). red. red. firstorder. simpl in H1. simpl in H0. subst x. subst y. simpl. auto. Qed. Lemma disjoint_singleton' : forall x y z z', heap.disjoint (heap.singleton x z) (heap.singleton y z') -> x <> y. red. intros. unfold disjoint in H. unfold inter in H. subst x. unfold singleton in H. simpl in H. generalize (H y); intro X; inversion_clear X. intuition. Qed. Lemma compose_union_equiv: forall h a b (s: set ((a,b)::h)) (s': set h) , mk_h ((a,b) :: h) s === (singleton a b) +++ (mk_h h s'). unfold union. unfold equal. simpl. induction h0. simpl; auto. induction a; simpl; intros. generalize (nat_lt_classic a a0); intro X; inversion_clear X. decompose [and] s. generalize (nat_lt_true _ _ H); Contrad_lt. rewrite H. generalize (beq_nat_classic a a0); intro X; inversion_clear X. decompose [and] s. generalize (beq_nat_true _ _ H0); Contrad_lt. rewrite H0. auto. Qed. Lemma lookup'_del_neq: forall h x y v, x <> y -> lookup' x (del' y h) = Some v -> lookup' x h = Some v. induction h0. simpl. auto. induction a; simpl; intros. generalize (beq_nat_classic y a); intro X; inversion_clear X. generalize (beq_nat_classic x a); intro X; inversion_clear X. rewrite (beq_nat_true _ _ H1) in H; rewrite (beq_nat_true _ _ H2) in H; tauto. rewrite H2. eapply IHh0. apply H. rewrite H1 in H0. auto. rewrite H1 in H0. simpl in H0. generalize (beq_nat_classic x a); intro X; inversion_clear X. rewrite H2. rewrite H2 in H0. auto. rewrite H2. rewrite H2 in H0. eapply IHh0. apply H. auto. Qed. Lemma lookup_union_or: forall h1 h2 n z, lookup n (h1 +++ h2) = Some z -> lookup n h1 = Some z \/ lookup n h2 = Some z. destruct h1. destruct h2. unfold union; unfold lookup. simpl. generalize lst0 s lst1 s0. clear lst0 s lst1 s0. induction lst0. simpl. auto. induction a; simpl; intros. generalize (beq_nat_classic n a); intro X; inversion_clear X. rewrite H0. rewrite (beq_nat_true _ _ H0) in H. rewrite lookup'_add_lst in H. left; auto. rewrite H0. rewrite lookup'_add_lst' in H. eapply IHlst0. intuition. intuition. auto. generalize (beq_nat_false _ _ H0); auto. Qed. Lemma dif_disjoint: forall h a b, h # (singleton a b) -> ((dif h a) === h). destruct h0 as [h0 s0]. intros. apply dif_not_in_dom. red; intros. unfold dom in H0. simpl in H0. unfold disjoint in H. unfold inter in H. unfold singleton in H. unfold dom in H. simpl in H. generalize (H a); intros. tauto. Qed. Lemma dif_disjoint': forall h1 h2 l, h1 # h2 -> ((dif h1 l) # (dif h2 l)). destruct h1 as [h1 s1]. destruct h2 as [h2 s2]. unfold disjoint; unfold dom; unfold inter; unfold dif. simpl. generalize h1 s1 h2 s2. clear h1 s1 h2 s2. induction h1. simpl. intuition. induction a; simpl. intros. generalize (beq_nat_classic l0 a); intro X; inversion_clear X. generalize (beq_nat_true _ _ H0); intro; subst l0. rewrite <- beq_nat_refl. apply IHh1. intuition. intuition. intros. generalize (H x0); intros. intuition. rewrite H0. simpl. generalize (beq_nat_false _ _ H0); intros. assert (forall x : l, In x (dom' h1) /\ In x (dom' h2) <-> False) . intros. generalize (H x0); intro. intuition. generalize (IHh1 (proj2 s1) _ s2 l0 H2); intro. generalize (H3 x). generalize (H x). intros; intuition. subst a. apply H13. eapply (pp''). assert (x <> l0). auto. apply H4. auto. Qed. Lemma In_dom_add_lst: forall k n w n', n <> n' -> In n' (dom' (add_lst n w k)) -> In n' (dom' k). induction k. simpl. intros. intuition. induction a; simpl; intros. generalize (nat_lt_classic a n); intro X; inversion_clear X. rewrite H1 in H0. simpl in H0. inversion_clear H0. left; auto. right. eapply IHk. apply H. apply H2. rewrite H1 in H0. generalize (beq_nat_classic a n); intro X; inversion_clear X. rewrite H2 in H0. simpl in H0. auto. rewrite H2 in H0. simpl in H0. inversion_clear H0. tauto. inversion_clear H3. auto. auto. Qed. Lemma lookup_exists_partition: forall h a b, lookup a h = Some b -> exists h'' , h === (singleton a b) +++ h'' /\ (singleton a b) # h''. destruct h0. unfold union. unfold lookup. unfold equal. unfold disjoint; unfold dom; unfold inter. simpl. generalize lst0 s. clear lst0 s. induction lst0. simpl. intros. inversion H. induction a; simpl; intros. generalize (beq_nat_classic a0 a); intro X; inversion_clear X. generalize (beq_nat_true _ _ H0); intro; subst a0. clear H0. rewrite <- beq_nat_refl in H. injection H; intro; subst b0. exists (mk_h lst0 (proj2 s)). simpl. split. rewrite add_lst_lb. auto. intuition. intros. intuition. subst a. generalize (loc_non_empty _ _ H5); intro X; inversion_clear X. generalize (lb_notin' _ _ H3); intro X; simpl X; tauto. rewrite H0 in H. generalize (IHlst0 (proj2 s) a0 b0 H); intros. inversion_clear H1. destruct x. simpl in H2. inversion_clear H2. exists (singleton a b +++ (mk_h lst1 s0)). simpl. subst lst0. split. inversion_clear s. rewrite add_lst_add_lst. rewrite <- add_lst_lb. auto. auto. auto. generalize (beq_nat_false _ _ H0); auto. intros. generalize (H3 x). intros. intuition. subst a0. apply H9. eapply In_dom_add_lst with (n := a). generalize (beq_nat_false _ _ H0); intro; auto. apply H10. Qed. Lemma lookup_disjoint_None: forall h a b, h # singleton a b -> lookup a h = None. destruct h0. induction lst0. simpl; auto. unfold lookup; unfold disjoint; unfold inter; unfold dom. induction a; simpl; intros. simpl in s. generalize (beq_nat_classic a0 a); intro X; inversion_clear X. generalize (beq_nat_true a0 a H0); intro; subst a0. generalize (H a); intro; intuition. rewrite H0. unfold lookup in IHlst0. simpl in IHlst0. apply (IHlst0 (proj2 s) a0 b). unfold disjoint; unfold inter; unfold dom. simpl. intros. generalize (H x); intros. tauto. Qed. Lemma disjoint_comp : forall h'1 h1 h2 h'2, h1 # h'1 -> h1 # h2 -> h'1 # h'2 -> (h'1 +++ h'2) === (h1 +++ h2) -> (exists h', h'1 # h' /\ h2 === (h' +++ h'1)). destruct h'1. generalize lst0 s. clear lst0 s. induction lst0. simpl; intros. exists h2. assert (mk_h nil s = emp). unfold emp. rewrite (proof_irrelevance _ s set_nil). auto. rewrite H3. clear H3. split. apply disjoint_com. apply disjoint_emp. apply equal_sym. apply equal_union_emp. induction a; simpl; intros. assert (a_set: set ((a,b)::nil)). red. simpl. tauto. assert (lookup a (mk_h ((a, b) :: lst0) s +++ h'2) = Some b). unfold lookup. simpl. rewrite lookup'_add_lst. auto. assert (lookup a (h1 +++ h2) = Some b). eapply lookup_equal. apply H2. auto. assert (lst0_set: set lst0). simpl in s. inversion_clear s; auto. assert (lookup a h2 = Some b). generalize (lookup_union_or h1 h2 a b H4); intro X; inversion_clear X. assert (h1 # (singleton a b) +++ mk_h lst0 lst0_set). eapply disjoint_equal with (mk_h ((a,b)::lst0) s). auto. unfold union; unfold equal. simpl. rewrite add_lst_lb. auto. apply (proj1 s). generalize (disjoint_union' _ _ _ H6); intro X; inversion_clear X. generalize (lookup_disjoint_None h1 a b H7); intro. rewrite H5 in H9; inversion H9. auto. generalize (lookup_exists_partition _ _ _ H5); intro. inversion_clear H6. decompose [and] H7; clear H7. assert (L1: h1 # mk_h lst0 lst0_set). unfold disjoint; unfold inter. intros. unfold disjoint in H; unfold inter in H. generalize (H x0); intro. simpl in H7. simpl. unfold dom. simpl. intuition. assert (L2: h1 # x). apply disjoint_com. eapply equal_union_disjoint with (x := h2) (x2 := singleton a b). split. apply equal_trans with (singleton a b +++ x). auto. apply union_com. auto. apply disjoint_com; auto. assert (L3: mk_h lst0 lst0_set # h'2). unfold disjoint; unfold inter; unfold dom; simpl. intros. generalize (H1 x0). intros. unfold disjoint in H7; unfold inter in H7; unfold dom in H7; simpl in H7. intuition. assert (L4: mk_h lst0 lst0_set +++ h'2 === h1 +++ x). assert (mk_h ((a, b) :: lst0) s +++ h'2 === h1 +++ singleton a b +++ x). apply equal_trans with (h1 +++ h2). auto. apply equal_trans with (h1 +++ (singleton a b +++ x)). apply equal_trans with (h2 +++ h1). apply union_com. auto. apply equal_trans with ((singleton a b +++ x) +++ h1). apply equal_union. auto. auto. apply union_com. apply disjoint_com. eapply disjoint_equal. apply H0. auto. apply union_assoc. assert (mk_h ((a, b) :: lst0) s +++ h'2 === singleton a b +++ h1 +++ x). apply equal_trans with (h1 +++ singleton a b +++ x). auto. apply equal_union. apply union_com. unfold disjoint; unfold inter; simpl. intros. unfold disjoint in H; unfold inter in H; simpl in H. generalize (H x0); intro; intuition. apply disjoint_union. split. eapply equal_union_disjoint with (x2 := singleton a b) (x := h2). split. apply equal_trans with (singleton a b +++ x). auto. apply union_com. auto. apply disjoint_com; auto. apply disjoint_com; auto. destruct x; destruct h1; destruct h'2. unfold union in H9; unfold equal in H9. simpl in H9. generalize (dif_equal _ _ a H7); intros. generalize (dif_union (mk_h ((a, b) :: lst0) s) (mk_h lst3 s2) a); intros. generalize (dif_union (mk_h lst2 s1 +++ singleton a b) (mk_h lst1 s0) a); intros. generalize (dif_union (mk_h lst2 s1) (singleton a b) a); intros. assert (A1: mk_h lst2 s1 --- a === mk_h lst2 s1). apply dif_disjoint with b. unfold disjoint in H. unfold inter in H. unfold dom in H. unfold disjoint. unfold inter. unfold dom. intros. generalize (H x); intros. simpl; simpl in H14. tauto. rewrite (equal_ext _ _ (dif_singleton_emp a b)) in H13. rewrite (equal_ext _ _ A1) in H13. clear A1. rewrite (equal_ext _ _ (equal_union_emp (mk_h lst2 s1))) in H13. rewrite (equal_ext _ _ H13) in H12. clear H13. assert (A1: mk_h lst1 s0 --- a === mk_h lst1 s0). apply dif_disjoint with b. apply disjoint_com; auto. rewrite (equal_ext _ _ A1) in H12. clear A1. rewrite (equal_ext _ _ H12) in H10. clear H12. assert (A1: mk_h lst3 s2 --- a === mk_h lst3 s2). apply dif_disjoint with b. unfold disjoint in H1. unfold inter in H1. unfold dom in H1. unfold disjoint. unfold inter. unfold dom. intros. generalize (H1 x); intros. simpl; simpl in H12. tauto. rewrite (equal_ext _ _ A1) in H11. clear A1. assert (A1: (mk_h ((a, b) :: lst0) s --- a) === mk_h lst0 lst0_set). unfold equal; unfold dif; simpl. rewrite <- beq_nat_refl. apply lb_del''. apply (proj1 s). rewrite (equal_ext _ _ A1) in H11. clear A1. rewrite (equal_ext _ _ H11) in H10. clear H11. auto. generalize (IHlst0 lst0_set h1 x h'2 L1 L2 L3 L4). intros. inversion_clear H7. inversion_clear H9. exists (x0). split. apply disjoint_com. eapply disjoint_equal with (singleton a b +++ mk_h lst0 lst0_set). apply disjoint_union. split. eapply equal_union_disjoint. split. apply H10. apply disjoint_com; auto. apply disjoint_com; auto. apply equal_sym. apply compose_union_equiv. apply equal_trans with (singleton a b +++ x). auto. apply equal_trans with (singleton a b +++ (x0 +++ mk_h lst0 lst0_set)). apply equal_trans with (x +++ singleton a b). apply union_com. auto. apply equal_trans with ((x0 +++ mk_h lst0 lst0_set) +++ singleton a b). apply equal_union. auto. auto. apply union_com. apply disjoint_com. eapply disjoint_equal. apply H8. auto. apply equal_sym. apply equal_trans with (x0 +++ (singleton a b +++ mk_h lst0 lst0_set)). apply equal_trans with (mk_h ((a,b)::lst0) s +++ x0). apply union_com. eapply disjoint_equal with ((singleton a b) +++ (mk_h lst0 lst0_set)). apply disjoint_union. split. eapply equal_union_disjoint. split. apply H10. apply disjoint_com; auto. apply disjoint_com; auto. apply equal_sym. apply compose_union_equiv. apply equal_trans with (((singleton a b) +++ (mk_h lst0 lst0_set)) +++ x0). apply equal_union. apply compose_union_equiv. apply disjoint_equal with ((singleton a b) +++ (mk_h lst0 lst0_set)). apply disjoint_union. split. eapply equal_union_disjoint. split. apply H10. apply disjoint_com; auto. apply disjoint_com; auto. apply equal_sym. apply compose_union_equiv. apply union_com. apply disjoint_com. apply disjoint_union. split. eapply equal_union_disjoint. split. apply H10. apply disjoint_com; auto. apply disjoint_com; auto. apply equal_trans with ((x0 +++ singleton a b) +++ mk_h lst0 lst0_set). apply union_assoc. apply equal_sym. apply equal_trans with (( singleton a b +++ x0 ) +++ mk_h lst0 lst0_set). apply union_assoc. apply equal_union. apply union_com. apply disjoint_com. eapply equal_union_disjoint with (x:= x). split. apply H10. apply disjoint_com. auto. apply disjoint_union. split. eapply equal_union_disjoint with (x:= x) (x2 := x0). split. apply equal_trans with ( x0 +++ mk_h lst0 lst0_set). auto. apply union_com. apply disjoint_com. auto. apply disjoint_com. auto. auto. Qed. End heap. Notation "k '===' m" := (heap.equal k m) (at level 79) : heap_scope. Notation "k '---' l" := (heap.dif k l) (at level 78) : heap_scope. Notation "k '+++' m" := (heap.union k m) (at level 78) : heap_scope. Notation "k '#' m" := (heap.disjoint k m) (at level 79) : heap_scope.