Commit 67969a5b by charguer

renaming

parent 3d310509
 ... @@ -232,7 +232,7 @@ Implicit Types f g h : fmap A B. ... @@ -232,7 +232,7 @@ Implicit Types f g h : fmap A B. (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Equality *) (* ** Equality *) Lemma fmap_eq : forall (f1 f2:map A B) F1 F2, Lemma fmap_make_eq : forall (f1 f2:map A B) F1 F2, (forall x, f1 x = f2 x) -> (forall x, f1 x = f2 x) -> fmap_make f1 F1 = fmap_make f2 F2. fmap_make f1 F1 = fmap_make f2 F2. Proof using. Proof using. ... @@ -240,6 +240,11 @@ Proof using. ... @@ -240,6 +240,11 @@ Proof using. subst. fequals. (* note: involves proof irrelevance *) subst. fequals. (* note: involves proof irrelevance *) Qed. Qed. Lemma fmap_eq_inv_fmap_data_eq : forall h1 h2, h1 = h2 -> forall x, fmap_data h1 x = fmap_data h2 x. Proof using. intros. fequals. Qed. (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Disjointness *) (* ** Disjointness *) ... @@ -284,7 +289,8 @@ Proof using. ... @@ -284,7 +289,8 @@ Proof using. Qed. Qed. Lemma fmap_single_same_loc_disjoint : forall (x:A) (v1 v2:B), Lemma fmap_single_same_loc_disjoint : forall (x:A) (v1 v2:B), \# (fmap_single x v1) (fmap_single x v2) -> False. \# (fmap_single x v1) (fmap_single x v2) -> False. Proof using. Proof using. introv D. specializes D x. simpls. case_if. destruct D; tryfalse. introv D. specializes D x. simpls. case_if. destruct D; tryfalse. Qed. Qed. ... @@ -319,10 +325,10 @@ Qed. ... @@ -319,10 +325,10 @@ Qed. (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Union *) (* ** Union *) Lemma fmap_union_idempotent : forall h, Lemma fmap_union_self : forall h, h \+ h = h. h \+ h = h. Proof using. Proof using. intros [f F]. apply~ fmap_eq. simpl. intros x. intros [f F]. apply~ fmap_make_eq. simpl. intros x. unfold map_union. cases~ (f x). unfold map_union. cases~ (f x). Qed. Qed. ... @@ -330,14 +336,14 @@ Lemma fmap_union_empty_l : forall h, ... @@ -330,14 +336,14 @@ Lemma fmap_union_empty_l : forall h, fmap_empty \+ h = h. fmap_empty \+ h = h. Proof using. Proof using. intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. apply~ fmap_eq. apply~ fmap_make_eq. Qed. Qed. Lemma fmap_union_empty_r : forall h, Lemma fmap_union_empty_r : forall h, h \+ fmap_empty = h. h \+ fmap_empty = h. Proof using. Proof using. intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. apply fmap_eq. intros x. destruct~ (f x). apply fmap_make_eq. intros x. destruct~ (f x). Qed. Qed. Lemma fmap_union_eq_empty_inv_l : forall h1 h2, Lemma fmap_union_eq_empty_inv_l : forall h1 h2, ... @@ -345,7 +351,7 @@ Lemma fmap_union_eq_empty_inv_l : forall h1 h2, ... @@ -345,7 +351,7 @@ Lemma fmap_union_eq_empty_inv_l : forall h1 h2, h1 = fmap_empty. h1 = fmap_empty. Proof using. Proof using. intros (f1&F1) (f2&F2) M. inverts M as M. intros (f1&F1) (f2&F2) M. inverts M as M. applys fmap_eq. intros l. applys fmap_make_eq. intros l. unfolds map_union. unfolds map_union. lets: func_same_1 l M. lets: func_same_1 l M. cases (f1 l); auto_false. cases (f1 l); auto_false. ... @@ -356,25 +362,25 @@ Lemma fmap_union_eq_empty_inv_r : forall h1 h2, ... @@ -356,25 +362,25 @@ Lemma fmap_union_eq_empty_inv_r : forall h1 h2, h2 = fmap_empty. h2 = fmap_empty. Proof using. Proof using. intros (f1&F1) (f2&F2) M. inverts M as M. intros (f1&F1) (f2&F2) M. inverts M as M. applys fmap_eq. intros l. applys fmap_make_eq. intros l. unfolds map_union. unfolds map_union. lets: func_same_1 l M. lets: func_same_1 l M. cases (f1 l); auto_false. cases (f1 l); auto_false. Qed. Qed. Lemma fmap_union_comm_disjoint : forall h1 h2, Lemma fmap_union_comm_of_disjoint : forall h1 h2, \# h1 h2 -> \# h1 h2 -> h1 \+ h2 = h2 \+ h1. h1 \+ h2 = h2 \+ h1. Proof using. Proof using. intros [f1 F1] [f2 F2] H. simpls. apply fmap_eq. simpl. intros [f1 F1] [f2 F2] H. simpls. apply fmap_make_eq. simpl. intros. rewrite~ map_union_comm. intros. rewrite~ map_union_comm. Qed. Qed. Lemma fmap_union_comm_agree : forall h1 h2, Lemma fmap_union_comm_of_agree : forall h1 h2, fmap_agree h1 h2 -> fmap_agree h1 h2 -> h1 \+ h2 = h2 \+ h1. h1 \+ h2 = h2 \+ h1. Proof using. Proof using. intros [f1 F1] [f2 F2] H. simpls. apply fmap_eq. simpl. intros [f1 F1] [f2 F2] H. simpls. apply fmap_make_eq. simpl. intros l. specializes H l. unfolds map_union. simpls. intros l. specializes H l. unfolds map_union. simpls. cases (f1 l); cases (f2 l); auto. fequals. applys* H. cases (f1 l); cases (f2 l); auto. fequals. applys* H. Qed. Qed. ... @@ -383,24 +389,19 @@ Lemma fmap_union_assoc : forall h1 h2 h3, ... @@ -383,24 +389,19 @@ Lemma fmap_union_assoc : forall h1 h2 h3, (h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3). (h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3). Proof using. Proof using. intros [f1 F1] [f2 F2] [f3 F3]. unfolds fmap_union. simpls. intros [f1 F1] [f2 F2] [f3 F3]. unfolds fmap_union. simpls. apply fmap_eq. intros x. unfold map_union. destruct~ (f1 x). apply fmap_make_eq. intros x. unfold map_union. destruct~ (f1 x). Qed. Qed. Lemma map_eq_forward : forall h1 h2, h1 = h2 -> forall x, fmap_data h1 x = fmap_data h2 x. Proof using. intros. fequals. Qed. (* (* Lemma fmap_union_eq_inv : forall h2 h1 h1' : fmap, Lemma fmap_union_eq_inv_of_disjoint : forall h2 h1 h1' : fmap, \# h1 h2 -> \# h1 h2 -> fmap_agree h1' h2 -> fmap_agree h1' h2 -> h1 \+ h2 = h1' \+ h2 -> h1 \+ h2 = h1' \+ h2 -> h1 = h1'. h1 = h1'. Proof using. Proof using. intros [f2 F2] [f1 F1] [f1' F1'] D D' E. intros [f2 F2] [f1 F1] [f1' F1'] D D' E. applys fmap_eq. intros x. specializes D x. specializes D' x. applys fmap_make_eq. intros x. specializes D x. specializes D' x. lets E': map_eq_forward (rm E) x. simpls. lets E': fmap_eq_inv_fmap_data_eq (rm E) x. simpls. unfolds map_union. unfolds map_union. cases (f1 x); cases (f2 x); try solve [cases (f1' x); destruct D; congruence ]. cases (f1 x); cases (f2 x); try solve [cases (f1' x); destruct D; congruence ]. destruct D; try false. destruct D; try false. ... @@ -412,15 +413,15 @@ Proof using. ... @@ -412,15 +413,15 @@ Proof using. Qed. Qed. *) *) Lemma fmap_union_eq_inv : forall h2 h1 h1', Lemma fmap_union_eq_inv_of_disjoint : forall h2 h1 h1', \# h1 h2 -> \# h1 h2 -> \# h1' h2 -> \# h1' h2 -> h1 \+ h2 = h1' \+ h2 -> h1 \+ h2 = h1' \+ h2 -> h1 = h1'. h1 = h1'. Proof using. Proof using. intros [f2 F2] [f1' F1'] [f1 F1] D D' E. intros [f2 F2] [f1' F1'] [f1 F1] D D' E. applys fmap_eq. intros x. specializes D x. specializes D' x. applys fmap_make_eq. intros x. specializes D x. specializes D' x. lets E': map_eq_forward (rm E) x. simpls. lets E': fmap_eq_inv_fmap_data_eq (rm E) x. simpls. unfolds map_union. unfolds map_union. cases (f1' x); cases (f1 x); cases (f1' x); cases (f1 x); destruct D; try congruence; destruct D; try congruence; ... @@ -445,7 +446,7 @@ Proof using. ... @@ -445,7 +446,7 @@ Proof using. specializes M l E1. specializes M l E1. Qed. Qed. Lemma fmap_agree_disjoint : forall h1 h2, Lemma fmap_agree_of_disjoint : forall h1 h2, fmap_disjoint h1 h2 -> fmap_disjoint h1 h2 -> fmap_agree h1 h2. fmap_agree h1 h2. Proof using. Proof using. ... @@ -490,7 +491,7 @@ Proof using. ... @@ -490,7 +491,7 @@ Proof using. introv M1 (M2a&M2b&M2c). introv M1 (M2a&M2b&M2c). rewrite fmap_disjoint_union_eq_r in *. rewrite fmap_disjoint_union_eq_r in *. applys fmap_agree_union_l; applys fmap_agree_union_r; applys fmap_agree_union_l; applys fmap_agree_union_r; try solve [ applys* fmap_agree_disjoint ]. try solve [ applys* fmap_agree_of_disjoint ]. auto. auto. Qed. Qed. ... @@ -515,7 +516,7 @@ Lemma fmap_agree_union_lr_inv_agree_agree : forall f1 f2 f3, ... @@ -515,7 +516,7 @@ Lemma fmap_agree_union_lr_inv_agree_agree : forall f1 f2 f3, fmap_agree f1 f2 -> fmap_agree f1 f2 -> fmap_agree f2 f3. fmap_agree f2 f3. Proof using. Proof using. introv M D. rewrite~ (@fmap_union_comm_agree f1 f2) in M. introv M D. rewrite~ (@fmap_union_comm_of_agree f1 f2) in M. applys* fmap_agree_union_ll_inv. applys* fmap_agree_union_ll_inv. Qed. Qed. ... @@ -560,29 +561,29 @@ Qed. ... @@ -560,29 +561,29 @@ Qed. (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Read and write *) (* ** Read and write *) Lemma fmap_union_single_read : forall f1 f2 l v, Lemma fmap_union_single_l_read : forall f1 f2 l v, f1 = fmap_single l v -> f1 = fmap_single l v -> fmap_data (f1 \+ f2) l = Some v. fmap_data (f1 \+ f2) l = Some v. Proof using. Proof using. intros. subst. simpl. unfold map_union. case_if~. intros. subst. simpl. unfold map_union. case_if~. Qed. Qed. Lemma fmap_union_single_write : forall f1 f1' f2 l v v', Lemma fmap_union_single_to_update : forall f1 f1' f2 l v v', f1 = fmap_single l v -> f1 = fmap_single l v -> f1' = fmap_single l v' -> f1' = fmap_single l v' -> (f1' \+ f2) = fmap_update (f1 \+ f2) l v'. (f1' \+ f2) = fmap_update (f1 \+ f2) l v'. Proof using. Proof using. intros. subst. unfold fmap_update. intros. subst. unfold fmap_update. rewrite <- fmap_union_assoc. fequals. rewrite <- fmap_union_assoc. fequals. applys fmap_eq. intros l'. applys fmap_make_eq. intros l'. unfolds map_union, fmap_single; simpl. case_if~. unfolds map_union, fmap_single; simpl. case_if~. Qed. Qed. End FmapProp. End FmapProp. Implicit Arguments fmap_union_assoc [A B]. Implicit Arguments fmap_union_assoc [A B]. Implicit Arguments fmap_union_comm_disjoint [A B]. Implicit Arguments fmap_union_comm_of_disjoint [A B]. Implicit Arguments fmap_union_comm_agree [A B]. Implicit Arguments fmap_union_comm_of_agree [A B]. (* ********************************************************************** *) (* ********************************************************************** *) ... @@ -656,7 +657,7 @@ Lemma fmap_union_eq_cancel_2 : forall h1 h1' h2 h2', ... @@ -656,7 +657,7 @@ Lemma fmap_union_eq_cancel_2 : forall h1 h1' h2 h2', h1 \+ h2 = h1' \+ h1 \+ h2'. h1 \+ h2 = h1' \+ h1 \+ h2'. Proof using. Proof using. intros. subst. rewrite <- fmap_union_assoc. intros. subst. rewrite <- fmap_union_assoc. rewrite (fmap_union_comm_disjoint h1 h1'). rewrite (fmap_union_comm_of_disjoint h1 h1'). rewrite~ fmap_union_assoc. auto. rewrite~ fmap_union_assoc. auto. Qed. Qed. ... @@ -665,7 +666,7 @@ Lemma fmap_union_eq_cancel_2' : forall h1 h1' h2, ... @@ -665,7 +666,7 @@ Lemma fmap_union_eq_cancel_2' : forall h1 h1' h2, h2 = h1' -> h2 = h1' -> h1 \+ h2 = h1' \+ h1. h1 \+ h2 = h1' \+ h1. Proof using. Proof using. intros. subst. apply~ fmap_union_comm_disjoint. intros. subst. apply~ fmap_union_comm_of_disjoint. Qed. Qed. Lemma fmap_union_eq_cancel_3 : forall h1 h1' h2 h2' h3', Lemma fmap_union_eq_cancel_3 : forall h1 h1' h2 h2' h3', ... @@ -773,15 +774,19 @@ Qed. ... @@ -773,15 +774,19 @@ Qed. (** [fmap_red] proves a goal of the form [red h1 t h2 v] (** [fmap_red] proves a goal of the form [red h1 t h2 v] using an hypothesis of the shape [red h1' t h2' v], using an hypothesis of the shape [red h1' t h2' v], generating [h1 = h1'] and [h2 = h2'] as subgoals, and generating [h1 = h1'] and [h2 = h2'] as subgoals, and attempting to solve them using the tactic [fmap_red]. *) attempting to solve them using the tactic [fmap_eq]. The tactic should be configured depending on [red]. For example: Ltac fmap_red_base tt := fail. Ltac fmap_red_base tt := (* Example: Ltac fmap_red_base tt := match goal with H: red _ ?t _ _ |- red _ ?t _ _ => match goal with H: red _ ?t _ _ |- red _ ?t _ _ => applys_eq H 2 4; try fmap_eq end. applys_eq H 2 4; try fmap_eq end. The default implementation is a dummy one. *) *) Ltac fmap_red_base tt := fail. Tactic Notation "fmap_red" := Tactic Notation "fmap_red" := fmap_red_base tt. fmap_red_base tt. ... ...
 ... @@ -15,7 +15,7 @@ Open Scope heap_scope. ... @@ -15,7 +15,7 @@ Open Scope heap_scope. (* ********************************************************************** *) (* ********************************************************************** *) (* ** Type of a formula *) (* * Type of a formula *) (** A formula is a binary relation relating a pre-condition (** A formula is a binary relation relating a pre-condition and a post-condition. *) and a post-condition. *) ... @@ -27,7 +27,7 @@ Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. ... @@ -27,7 +27,7 @@ Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. (* ********************************************************************** *) (* ********************************************************************** *) (* ** The [local] predicate *) (* * The [local] predicate *) (** Nested applications [local] are redundant *) (** Nested applications [local] are redundant *) ... @@ -219,7 +219,7 @@ Ltac simpl_cf := ... @@ -219,7 +219,7 @@ Ltac simpl_cf := (* ********************************************************************** *) (* ********************************************************************** *) (* ** Soundness proof *) (* * Soundness proof *) (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Two substitution lemmas for the soundness proof *) (* ** Two substitution lemmas for the soundness proof *) ... ...
 ... @@ -16,7 +16,7 @@ Open Scope heap_scope. ... @@ -16,7 +16,7 @@ Open Scope heap_scope. (* ********************************************************************** *) (* ********************************************************************** *) (* ** Type of a formula *) (* * Type of a formula *) (** A formula is a binary relation relating a pre-condition (** A formula is a binary relation relating a pre-condition and a post-condition. *) and a post-condition. *) ... @@ -28,7 +28,7 @@ Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. ... @@ -28,7 +28,7 @@ Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. (* ********************************************************************** *) (* ********************************************************************** *) (* ** The [local] predicate *) (* * The [local] predicate *) (** Nested applications [local] are redundant *) (** Nested applications [local] are redundant *) ... @@ -59,7 +59,7 @@ Hint Resolve local_is_local. ... @@ -59,7 +59,7 @@ Hint Resolve local_is_local. (* ********************************************************************** *) (* ********************************************************************** *) (* ** Characteristic formula generator *) (* * Characteristic formula generator *) (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Input language for the characteristic formula generator, (* ** Input language for the characteristic formula generator, ... @@ -226,7 +226,7 @@ Ltac simpl_cf := ... @@ -226,7 +226,7 @@ Ltac simpl_cf := (* ********************************************************************** *) (* ********************************************************************** *) (* ** Soundness proof *) (* * Soundness proof *) (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) (* ** Two substitution lemmas for the soundness proof *) (* ** Two substitution lemmas for the soundness proof *) ... ...
 ... @@ -49,7 +49,7 @@ Notation "h1 \u h2" := (fmap_union h1 h2) ... @@ -49,7 +49,7 @@ Notation "h1 \u h2" := (fmap_union h1 h2) Definition heap_union_empty_l := fmap_union_empty_l. Definition heap_union_empty_l := fmap_union_empty_l. Definition heap_union_empty_r := fmap_union_empty_r. Definition heap_union_empty_r := fmap_union_empty_r. Definition heap_union_comm := fmap_union_comm_disjoint. Definition heap_union_comm := fmap_union_comm_of_disjoint. (* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *) ... @@ -371,7 +371,7 @@ Lemma rule_get : forall v l, ... @@ -371,7 +371,7 @@ Lemma rule_get : forall v l, Proof using. Proof using. intros. intros HF h N. exists h v. splits~. intros. intros HF h N. exists h v. splits~. { applys red_get. destruct N as (?&?&(?&?)&?&?&?). { applys red_get. destruct N as (?&?&(?&?)&?&?&?). subst h. applys~ fmap_union_single_read. } subst h. applys~ fmap_union_single_l_read. } { rew_heap. rewrite hprop_star_pure. split~. hhsimpl~. } { rew_heap. rewrite hprop_star_pure. split~. hhsimpl~. } Qed. Qed. ... @@ -381,7 +381,7 @@ Proof using. ... @@ -381,7 +381,7 @@ Proof using. intros. intros HF h N. destruct N as (h1&h2&(N0&N1)&N2&N3&N4). intros. intros HF h N. destruct N as (h1&h2&(N0&N1)&N2&N3&N4). hnf in N1. sets h1': (fmap_single l w). hnf in N1. sets h1': (fmap_single l w). exists (h1' \u h2) val_unit. splits~. exists (h1' \u h2) val_unit. splits~. { applys red_set. subst h h1. applys~ fmap_union_single_write. } { applys red_set. subst h h1. applys~ fmap_union_single_to_update. } { rew_heap. rewrite hprop_star_pure. split~. { rew_heap. rewrite hprop_star_pure. split~. { exists h1' h2. splits~. { exists h1' h2. splits~. { hnfs~. } { hnfs~. } ... ...
 ... @@ -676,7 +676,7 @@ Proof using. ... @@ -676,7 +676,7 @@ Proof using. destruct N as (h1&h2&(N1a&N1b)&N2&N3&N4). destruct N as (h1&h2&(N1a&N1b)&N2&N3&N4). forwards (E1&E2): heap_eq_forward (rm N4). simpls. forwards (E1&E2): heap_eq_forward (rm N4). simpls. exists 0%nat h v. splits~. exists 0%nat h v. splits~. { applys red_get. rewrite E1. applys~ fmap_union_single_read. } { applys red_get. rewrite E1. applys~ fmap_union_single_l_read. } { rew_heap. rewrite hprop_star_pure. split~. hhsimpl~. } { rew_heap. rewrite hprop_star_pure. split~. hhsimpl~. } Qed. Qed. ... @@ -688,7 +688,7 @@ Proof using. ... @@ -688,7 +688,7 @@ Proof using. sets m1': (fmap_single l w). sets m1': (fmap_single l w). exists 0%nat ((m1' \+ h2^s), h2^c) val_unit. splits~. exists 0%nat ((m1' \+ h2^s), h2^c) val_unit. splits~. { applys red_set. rewrite E1. unfold m1'. rewrite N1a. { applys red_set. rewrite E1. unfold m1'. rewrite N1a. applys~ fmap_union_single_write. } applys~ fmap_union_single_to_update. } { rew_heap. rewrite hprop_star_pure. split~. { rew_heap. rewrite hprop_star_pure. split~. { exists (m1',0%nat) h2. splits~. { exists (m1',0%nat) h2. splits~. { hnfs~. } { hnfs~. } ... ...
 ... @@ -319,7 +319,7 @@ Lemma heap_compat_ro_l : forall h1 h2, ... @@ -319,7 +319,7 @@ Lemma heap_compat_ro_l : forall h1 h2, heap_compat (heap_ro h1) h2. heap_compat (heap_ro h1) h2. Proof using. Proof using. introv (N1&N2). split; simpl. introv (N1&N2). split; simpl. { applys~ fmap_agree_union_l. applys~ fmap_agree_disjoint. } { applys~ fmap_agree_union_l. applys~ fmap_agree_of_disjoint. } { fmap_disjoint. } { fmap_disjoint. } Qed. Qed. ... @@ -361,8 +361,8 @@ Proof using. ... @@ -361,8 +361,8 @@ Proof using. tests E: (heap_compat h1 h2); tests E': (heap_compat h2 h1); tests E: (heap_compat h1 h2); tests E': (heap_compat h2 h1); try auto_false. try auto_false. fequals. fequals. fequals. fequals. { applys fmap_union_comm_disjoint. { destruct E. fmap_disjoint. } } { applys fmap_union_comm_of_disjoint. { destruct E. fmap_disjoint. } } { applys fmap_union_comm_agree. { destruct~ E. } } { applys fmap_union_comm_of_agree. { destruct~ E. } } Qed. Qed. Lemma heap_union_assoc : forall h1 h2 h3, Lemma heap_union_assoc : forall h1 h2 h3, ... @@ -694,7 +694,7 @@ Proof using. ... @@ -694,7 +694,7 @@ Proof using. exists h h. splits~. exists h h. splits~. { applys heap_eq. rewrite~ heap_union_f. { applys heap_eq. rewrite~ heap_union_f. rewrite~ heap_union_r. rewrite M2. rewrite~ heap_union_r. rewrite M2. split. fmap_eq. rewrite~ fmap_union_idempotent. } split. fmap_eq. rewrite~ fmap_union_self. } Qed. Qed. Lemma RO_covariant : forall H1 H2, Lemma RO_covariant : forall H1 H2, ... @@ -990,7 +990,7 @@ Proof using. ... @@ -990,7 +990,7 @@ Proof using. { rewrite F1,V2. rew_heap~. rewrite Y1,W1. { rewrite F1,V2. rew_heap~. rewrite Y1,W1. rewrite fmap_union_empty_l. rewrite fmap_union_empty_l. do 2 rewrite fmap_union_assoc. fequals. do 2 rewrite fmap_union_assoc. fequals. applys fmap_union_comm_disjoint. auto. } applys fmap_union_comm_of_disjoint. auto. } { rew_heap~. rewrite V3,E12,W2,Y2,F2. fmap_eq. } } { rew_heap~. rewrite V3,E12,W2,Y2,F2. fmap_eq. } } { rew_heap~. rewrite V3,E12. fmap_eq. } { rew_heap~. rewrite V3,E12. fmap_eq. } { exists~ hx hb. } } { exists~ hx hb. } } ... @@ -1048,7 +1048,7 @@ Proof using. ... @@ -1048,7 +1048,7 @@ Proof using. rewrite~ heap_union_assoc. } rewrite~ heap_union_assoc. } { rewrite~ heap_union_assoc. } } } { rewrite~ heap_union_assoc. } } } { rew_heap~. rewrite T3. rew_heap~. rewrite <- N3. rew_heap~. { rew_heap~. rewrite T3. rew_heap~. rewrite <- N3. rew_heap~. rewrite (fmap_union_comm_agree (hx^r \+ hy^r) h12^r). rewrite (fmap_union_comm_of_agree (hx^r \+ hy^r) h12^r). rewrite~ fmap_union_assoc. applys fmap_agree_union_l. rewrite~ fmap_union_assoc. applys fmap_agree_union_l. destruct~ N1aa. destruct~ N1ba. } destruct~ N1aa. destruct~ N1ba. } { applys~ on_rw_sub_union_r. } { applys~ on_rw_sub_union_r. } ... @@ -1132,7 +1132,7 @@ Proof using. ... @@ -1132,7 +1132,7 @@ Proof using. rewrites E2' in E2. rewrite fmap_union_empty_r in E2. rewrites E2' in E2. rewrite fmap_union_empty_r in E2. exists h1 v. splits~. exists h1 v. splits~. { rew_fmap~. applys red_get. rewrite heap_fmap_def. { rew_fmap~. applys red_get. rewrite heap_fmap_def. rewrite E1,E2,E1'. rew_fmap. applys~ fmap_union_single_read. } rewrite E1,E2,E1'. rew_fmap. applys~ fmap_union_single_l_read. } { exists heap_empty h1. splits~. { exists heap_empty h1. splits~. { applys~ heap_compat_empty_l. } { applys~ heap_compat_empty_l. } { heap_eq. } { heap_eq. } ... @@ -1154,7 +1154,7 @@ Proof using. ... @@ -1154,7 +1154,7 @@ Proof using. splits~. splits~. { rew_fmap~. applys red_set. { rew_fmap~. applys red_set. rewrite (@heap_fmap_def h1'). rewrite (@heap_fmap_def h1). rewrite (@heap_fmap_def h1'). rewrite (@heap_fmap_def h1). rewrite E1,E2,E1',E2'. rew_fmap. applys~ fmap_union_single_write v w. } rewrite E1,E2,E1',E2'. rew_fmap. applys~ fmap_union_single_to_update v w. } { rewrite E2,E2'. auto. } { rewrite E2,E2'. auto. } { applys~ on_rw_sub_base. applys~ himpl_inst_prop (l ~~> w). split~. } { applys~ on_rw_sub_base. applys~ himpl_inst_prop (l ~~> w). split~. } Qed. Qed. ... ...
 ... @@ -105,7 +105,7 @@ Proof using. ... @@ -105,7 +105,7 @@ Proof using. { applys~ heap_ro_pred. } { applys~ heap_ro_pred. } { applys heap_eq. split. { applys heap_eq. split. { rew_heap~. fmap_eq. } (* todo clean *) { rew_heap~. fmap_eq. } (* todo clean *) { rewrite~ heap_union_r. rewrite~ fmap_union_idempotent. } } } } { rewrite~ heap_union_r. rewrite~ fmap_union_self. } } } } do 2 rewrite <- (hprop_star_comm_assoc (= heap_ro h2)) in K. do 2 rewrite <- (hprop_star_comm_assoc (= heap_ro h2)) in K. destruct K as (h2'&h1'&D'&P2'&P1'&EQ'). subst h2'. destruct K as (h2'&h1'&D'&P2'&P1'&EQ'). subst h2'. (* (* ... @@ -121,7 +121,7 @@ Proof using. ... @@ -121,7 +121,7 @@ Proof using. lets DH2: (heap_disjoint_components h2). lets DH2: (heap_disjoint_components h2). rew_heap in *. rewrite NH2 in *. clears NH2. rew_state. rew_heap in *. rewrite NH2 in *. clears NH2. rew_state. (* (* applys fmap_union_eq_inv E. rewrite heap_ro_r. applys fmap_union_eq_inv_of_disjoint E. rewrite heap_ro_r. rewrites (>> NH2 P2). destruct D' as (D1&D2).*) rewrites (>> NH2 P2). destruct D' as (D1&D2).*) admit. admit. } } ... @@ -274,9 +274,9 @@ Proof using. ... @@ -274,9 +274,9 @@ Proof using. { applys red_get. destruct N as (h1&h2&D&P1&P2&E). { applys red_get. destruct N as (h1&h2&D&P1&P2&E). destruct P1 as (h11&(Q1&Q2)&E1&E2). destruct P1 as (h11&(Q1&Q2)&E1&E2). subst h. rewrite heap_fmap_def. (* todo: cleanup *) subst h. rewrite heap_fmap_def. (* todo: cleanup *) rewrite fmap_union_comm_disjoint; [|rew_heap~]. rewrite fmap_union_comm_of_disjoint; [|rew_heap~]. rew_heap~. rewrite E1,E2,Q1,Q2. rew_state. rew_heap~. rewrite E1,E2,Q1,Q2. rew_state. applys~ fmap_union_single_read. } applys~ fmap_union_single_l_read. } { rewrite hprop_star_pure. split~. hhsimpl~. } { rewrite hprop_star_pure. split~. hhsimpl~. } Qed. Qed. ... @@ -296,7 +296,7 @@ Proof using. ... @@ -296,7 +296,7 @@ Proof using.