LibSepFmapAppendix - Finite Maps

Set Implicit Arguments.
From SLF Require Import LibCore.

Representation of Finite Maps

This file provides a representation of finite maps, which may be used to represent the memory state of a program.
  • It implements basic operations such as creation of a singleton map, union of maps, read and update operations.
  • It includes predicates to assert disjointness of two maps (predicate disjoint), and coherence of two maps on the intersection of their domain (predicate agree).
  • It comes with a tactic for fmap_eq proving equalities modulo commutativity and associativity of map union.
The definition of the type fmap is slightly technical in that it involves a dependent pair to pack the partial function of type A option B that represents the map, together with a proof of finiteness of the domain of this map. One useful lemma established in this file is the existence of fresh keys: for any finite map whose keys are natural numbers, there exists a natural number that does not already belong to the domain of that map.

Representation of Potentially-Infinite Maps as Partial Functions

Representation

Type of partial functions from A to B
Definition map (A B : Type) : Type :=
  Aoption B.

Operations

Disjoint union of two partial functions
Definition map_union (A B : Type) (f1 f2 : map A B) : map A B :=
  fun (x:A) ⇒ match f1 x with
           | Some ySome y
           | Nonef2 x
           end.
Removal from a partial functions
Definition map_remove (A B : Type) (f : map A B) (k:A) : map A B :=
  fun (x:A) ⇒ If x = k then None else f x.
Finite domain of a partial function
Definition map_finite (A B : Type) (f : map A B) :=
   (L : list A), (x:A), f xNonemem x L.
Disjointness of domain of two partial functions
Definition map_disjoint (A B : Type) (f1 f2 : map A B) :=
   (x:A), f1 x = Nonef2 x = None.
Compatibility of two partial functions on the intersection of their domains (only for Separation Logic with RO-permissions)
Definition map_agree (A B : Type) (f1 f2 : map A B) :=
   x v1 v2,
  f1 x = Some v1
  f2 x = Some v2
  v1 = v2.
Domain of a map (as a predicate)
Definition map_indom (A B : Type) (f1 : map A B) : (AProp) :=
  fun (x:A) ⇒ f1 xNone.
Filter the bindings of a map
Definition map_filter A B (F:ABProp) (f:map A B) : map A B :=
  fun (x:A) ⇒ match f x with
    | NoneNone
    | Some yIf F x y then Some y else None
    end.
Map a function on the values of a map
Definition map_map A B1 B2 (F:AB1B2) (f:map A B1) : map A B2 :=
  fun (x:A) ⇒ match f x with
    | NoneNone
    | Some ySome (F x y)
    end.

Properties

Section MapOps.
Variables (A B : Type).
Implicit Types f : map A B.
Symmetry of disjointness
Lemma map_disjoint_sym :
  sym (@map_disjoint A B).
Proof using.
  introv H. unfolds map_disjoint. intros z. specializes H z. intuition.
Qed.
Commutativity of disjoint union
Lemma map_union_comm : f1 f2,
  map_disjoint f1 f2
  map_union f1 f2 = map_union f2 f1.
Proof using.
  introv H. unfold map.
  extens. intros x. unfolds map_disjoint, map_union.
  specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false.
Qed.
Finiteness of union
Lemma map_union_finite : f1 f2,
  map_finite f1
  map_finite f2
  map_finite (map_union f1 f2).
Proof using.
  introv [L1 F1] [L2 F2]. (L1 ++ L2). intros x M.
  specializes F1 x. specializes F2 x. unfold map_union in M.
  apply mem_app. destruct¬(f1 x).
Qed.
Finiteness of removal
Definition map_remove_finite : x f,
  map_finite f
  map_finite (map_remove f x).
Proof using.
  introv [L F]. L. intros x' M.
  specializes F x'. unfold map_remove in M. case_if¬.
Qed.
Finiteness of filter
Definition map_filter_finite : (F:ABProp) f,
  map_finite f
  map_finite (map_filter F f).
Proof using.
  introv [L N]. L. intros x' M.
  specializes N x'. unfold map_filter in M.
  destruct (f x'); tryfalse. case_if. applys N; auto_false.
Qed.
Finiteness of map
Definition map_map_finite : C (F:ABC) f,
  map_finite f
  map_finite (map_map F f).
Proof using.
  introv [L N]. L. intros x' M.
  specializes N x'. unfold map_map in M.
  destruct (f x'); tryfalse. applys N; auto_false.
Qed.

End MapOps.

Representation of Finite Maps as Dependent Pairs

Representation

Inductive fmap (A B : Type) : Type := make {
  fmap_data :> map A B;
  fmap_finite : map_finite fmap_data }.

Arguments make [A] [B].

Operations

Declare Scope fmap_scope.
Domain of a fmap (as a predicate)
Definition indom (A B: Type) (h:fmap A B) : (AProp) :=
  map_indom h.
Empty fmap
Program Definition empty (A B : Type) : fmap A B :=
  make (fun lNone) _.
Next Obligation. (@nil A). auto_false. Qed.

Arguments empty {A} {B}.
Singleton fmap
Program Definition single A B (x:A) (v:B) : fmap A B :=
  make (fun x'If x = x' then Some v else None) _.
Next Obligation.
   (x::nil). intros. case_if. subst¬.
Qed.
Union of fmaps
Program Definition union A B (h1 h2:fmap A B) : fmap A B :=
  make (map_union h1 h2) _.
Next Obligation. destruct h1. destruct h2. apply¬map_union_finite. Qed.

Notation "h1 \+ h2" := (union h1 h2)
   (at level 51, right associativity) : fmap_scope.

Open Scope fmap_scope.
Update of a fmap
Definition update A B (h:fmap A B) (x:A) (v:B) : fmap A B :=
  union (single x v) h.
  (* Note: the union operation first reads in the first argument. *)
Read in a fmap
Definition read (A B : Type) {IB:Inhab B} (h:fmap A B) (x:A) : B :=
  match fmap_data h x with
  | Some yy
  | Nonearbitrary
  end.
Removal from a fmap
Program Definition remove A B (h:fmap A B) (x:A) : fmap A B :=
  make (map_remove h x) _.
Next Obligation. destruct h. apply¬map_remove_finite. Qed.
Filter from a fmap
Program Definition filter A B (F:ABProp) (h:fmap A B) : fmap A B :=
  make (map_filter F h) _.
Next Obligation. destruct h. apply¬map_filter_finite. Qed.
Map a function onto the keys of a fmap
Program Definition map_ A B1 B2 (F:AB1B2) (h:fmap A B1) : fmap A B2 :=
  make (map_map F h) _.
Next Obligation. destruct h. apply¬map_map_finite. Qed.
Inhabited type fmap
Global Instance Inhab_fmap A B : Inhab (fmap A B).
Proof using. intros. applys Inhab_of_val (@empty A B). Qed.

Predicates on Finite Maps

Compatible fmaps (only for Separation Logic with RO-permissions)
Definition agree A B (h1 h2:fmap A B) :=
  map_agree h1 h2.
Disjoint fmaps
Definition disjoint A B (h1 h2 : fmap A B) : Prop :=
  map_disjoint h1 h2.
Three disjoint fmaps (not needed for basic separation logic)
Definition disjoint_3 A B (h1 h2 h3 : fmap A B) :=
     disjoint h1 h2
  ∧ disjoint h2 h3
  ∧ disjoint h1 h3.
Notation for disjointness
Module NotationForFmapDisjoint.

Notation "\# h1 h2" := (disjoint h1 h2)
  (at level 40, h1 at level 0, h2 at level 0, no associativity) : fmap_scope.

Notation "\# h1 h2 h3" := (disjoint_3 h1 h2 h3)
  (at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity)
  : fmap_scope.

End NotationForFmapDisjoint.

Import NotationForFmapDisjoint.

Poperties of Operations on Finite Maps

Section FmapProp.
Variables (A B : Type).
Implicit Types f g h : fmap A B.
Implicit Types x : A.
Implicit Types v : B.

Equality

Lemma make_eq : (f1 f2:map A B) F1 F2,
  ( x, f1 x = f2 x) →
  make f1 F1 = make f2 F2.
Proof using.
  introv H. asserts: (f1 = f2). { unfold map. extens¬. }
  subst. fequals. (* note: involves proof irrelevance *)
Qed.

Lemma eq_inv_fmap_data_eq : h1 h2,
  h1 = h2
   x, fmap_data h1 x = fmap_data h2 x.
Proof using. intros. fequals. Qed.

Lemma fmap_extens : h1 h2,
  ( x, fmap_data h1 x = fmap_data h2 x) →
  h1 = h2.
Proof using. intros [f1 F1] [f2 F2] M. simpls. applys¬make_eq. Qed.

Disjointness

Lemma disjoint_sym : h1 h2,
  \# h1 h2
  \# h2 h1.
Proof using. intros [f1 F1] [f2 F2]. apply map_disjoint_sym. Qed.

Lemma disjoint_comm : h1 h2,
  \# h1 h2 = \# h2 h1.
Proof using. lets: disjoint_sym. extens*. Qed.

Lemma disjoint_empty_l : h,
  \# empty h.
Proof using. intros [f F] x. simple¬. Qed.

Lemma disjoint_empty_r : h,
  \# h empty.
Proof using. intros [f F] x. simple¬. Qed.

Hint Resolve disjoint_sym disjoint_empty_l disjoint_empty_r.

Lemma disjoint_union_eq_r : h1 h2 h3,
  \# h1 (h2 \+ h3) =
  (\# h1 h2 ∧ \# h1 h3).
Proof using.
  intros [f1 F1] [f2 F2] [f3 F3].
  unfolds disjoint, union. simpls.
  unfolds map_disjoint, map_union. extens. iff M [M1 M2].
  split; intros x; specializes M x;
   destruct (f2 x); intuition; tryfalse.
  intros x. specializes M1 x. specializes M2 x.
   destruct (f2 x); intuition.
Qed.

Lemma disjoint_union_eq_l : h1 h2 h3,
  \# (h2 \+ h3) h1 =
  (\# h1 h2 ∧ \# h1 h3).
Proof using.
  intros. rewrite disjoint_comm.
  apply disjoint_union_eq_r.
Qed.

Lemma disjoint_single_single : (x1 x2:A) (v1 v2:B),
  x1x2
  \# (single x1 v1) (single x2 v2).
Proof using.
  introv N. intros x. simpls. do 2 case_if; auto.
Qed.

Lemma disjoint_single_single_same_inv : (x:A) (v1 v2:B),
  \# (single x v1) (single x v2) →
  False.
Proof using.
  introv D. specializes D x. simpls. case_if. destruct D; tryfalse.
Qed.

Lemma disjoint_3_unfold : h1 h2 h3,
  \# h1 h2 h3 = (\# h1 h2 ∧ \# h2 h3 ∧ \# h1 h3).
Proof using. auto. Qed.

Lemma disjoint_single_set : h l v1 v2,
  \# (single l v1) h
  \# (single l v2) h.
Proof using.
  introv M. unfolds disjoint, single, map_disjoint; simpls.
  intros l'. specializes M l'. case_if¬. destruct M; auto_false.
Qed.

Union

Lemma union_self : h,
  h \+ h = h.
Proof using.
  intros [f F]. apply¬make_eq. simpl. intros x.
  unfold map_union. cases¬(f x).
Qed.

Lemma union_empty_l : h,
  empty \+ h = h.
Proof using.
  intros [f F]. unfold union, map_union, empty. simpl.
  apply¬make_eq.
Qed.

Lemma union_empty_r : h,
  h \+ empty = h.
Proof using.
  intros [f F]. unfold union, map_union, empty. simpl.
  apply make_eq. intros x. destruct¬(f x).
Qed.

Lemma union_eq_empty_inv_l : h1 h2,
  h1 \+ h2 = empty
  h1 = empty.
Proof using.
  intros (f1&F1) (f2&F2) M. inverts M as M.
  applys make_eq. intros l.
  unfolds map_union.
  lets: fun_eq_1 l M.
  cases (f1 l); auto_false.
Qed.

Lemma union_eq_empty_inv_r : h1 h2,
  h1 \+ h2 = empty
  h2 = empty.
Proof using.
  intros (f1&F1) (f2&F2) M. inverts M as M.
  applys make_eq. intros l.
  unfolds map_union.
  lets: fun_eq_1 l M.
  cases (f1 l); auto_false.
Qed.

Lemma union_comm_of_disjoint : h1 h2,
  \# h1 h2
  h1 \+ h2 = h2 \+ h1.
Proof using.
  intros [f1 F1] [f2 F2] H. simpls. apply make_eq. simpl.
  intros. rewrite¬map_union_comm.
Qed.

Lemma union_comm_of_agree : h1 h2,
  agree h1 h2
  h1 \+ h2 = h2 \+ h1.
Proof using.
  intros [f1 F1] [f2 F2] H. simpls. apply make_eq. simpl.
  intros l. specializes H l. unfolds map_union. simpls.
  cases (f1 l); cases (f2 l); auto. fequals. applys* H.
Qed.

Lemma union_assoc : h1 h2 h3,
  (h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3).
Proof using.
  intros [f1 F1] [f2 F2] [f3 F3]. unfolds union. simpls.
  apply make_eq. intros x. unfold map_union. destruct¬(f1 x).
Qed.

Lemma union_eq_inv_of_disjoint : h2 h1 h1',
  \# h1 h2
  \# h1' h2
  h1 \+ h2 = h1' \+ h2
  h1 = h1'.
Proof using.
  intros [f2 F2] [f1' F1'] [f1 F1] D D' E.
  applys make_eq. intros x. specializes D x. specializes D' x.
  lets E': eq_inv_fmap_data_eq (rm E) x. simpls.
  unfolds map_union.
  cases (f1' x); cases (f1 x);
    destruct D; try congruence;
    destruct D'; try congruence.
Qed.

Compatibility

Lemma agree_refl : h,
  agree h h.
Proof using.
  intros h. introv M1 M2. congruence.
Qed.

Lemma agree_sym : f1 f2,
  agree f1 f2
  agree f2 f1.
Proof using.
  introv M. intros l v1 v2 E1 E2.
  specializes M l E1.
Qed.

Lemma agree_of_disjoint : h1 h2,
  disjoint h1 h2
  agree h1 h2.
Proof using.
  introv HD. intros l v1 v2 M1 M2. destruct (HD l); false.
Qed.

Lemma agree_empty_l : h,
  agree empty h.
Proof using. intros h l v1 v2 E1 E2. simpls. false. Qed.

Lemma agree_empty_r : h,
  agree h empty.
Proof using.
  hint agree_sym, agree_empty_l. eauto.
Qed.

Lemma agree_union_l : f1 f2 f3,
  agree f1 f3
  agree f2 f3
  agree (f1 \+ f2) f3.
Proof using.
  introv M1 M2. intros l v1 v2 E1 E2.
  specializes M1 l. specializes M2 l.
  simpls. unfolds map_union. cases (fmap_data f1 l).
  { inverts E1. applys* M1. }
  { applys* M2. }
Qed.

Lemma agree_union_r : f1 f2 f3,
  agree f1 f2
  agree f1 f3
  agree f1 (f2 \+ f3).
Proof using.
  hint agree_sym, agree_union_l. eauto.
Qed.

Lemma agree_union_lr : f1 g1 f2 g2,
  agree g1 g2
  \# f1 f2 (g1 \+ g2) →
  agree (f1 \+ g1) (f2 \+ g2).
Proof using.
  introv M1 (M2a&M2b&M2c).
  rewrite disjoint_union_eq_r in *.
  applys agree_union_l; applys agree_union_r;
    try solve [ applys* agree_of_disjoint ].
  auto.
Qed.

Lemma agree_union_ll_inv : f1 f2 f3,
  agree (f1 \+ f2) f3
  agree f1 f3.
Proof using.
  introv M. intros l v1 v2 E1 E2.
  specializes M l. simpls. unfolds map_union.
  rewrite E1 in M. applys* M.
Qed.

Lemma agree_union_rl_inv : f1 f2 f3,
  agree f1 (f2 \+ f3) →
  agree f1 f2.
Proof using.
  hint agree_union_ll_inv, agree_sym. eauto.
Qed.

Lemma agree_union_lr_inv_agree_agree : f1 f2 f3,
  agree (f1 \+ f2) f3
  agree f1 f2
  agree f2 f3.
Proof using.
  introv M D. rewrite¬(@union_comm_of_agree f1 f2) in M.
  applys* agree_union_ll_inv.
Qed.

Lemma agree_union_rr_inv_agree : f1 f2 f3,
  agree f1 (f2 \+ f3) →
  agree f2 f3
  agree f1 f3.
Proof using.
  hint agree_union_lr_inv_agree_agree, agree_sym. eauto.
Qed.

Lemma agree_union_l_inv : f1 f2 f3,
  agree (f1 \+ f2) f3
  agree f1 f2
     agree f1 f3
  ∧ agree f2 f3.
Proof using.
  introv M1 M2. split.
  { applys* agree_union_ll_inv. }
  { applys* agree_union_lr_inv_agree_agree. }
Qed.

Lemma agree_union_r_inv : f1 f2 f3,
  agree f1 (f2 \+ f3) →
  agree f2 f3
     agree f1 f2
  ∧ agree f1 f3.
Proof using.
  hint agree_sym.
  intros. forwards¬(M1&M2): agree_union_l_inv f2 f3 f1.
Qed.

Domain

Lemma indom_single : x v,
  indom (single x v) x.
Proof using.
  intros. hnf. simpl. case_if. auto_false.
Qed.

Lemma indom_union_l : h1 h2 x,
  indom h1 x
  indom (union h1 h2) x.
Proof using.
  intros. hnf. unfold union, map_union. simpl.
  case_eq (fmap_data h1 x); auto_false.
Qed.

Lemma indom_union_r : h1 h2 x,
  indom h2 x
  indom (union h1 h2) x.
Proof using.
  intros. hnf. unfold union, map_union. simpl.
  case_eq (fmap_data h1 x); auto_false.
Qed.

Disjoint and Domain

Lemma disjoint_eq_not_indom_both : h1 h2,
  disjoint h1 h2 = ( x, indom h1 xindom h2 xFalse).
Proof using.
  extens. iff D E.
  { introv M1 M2. destruct (D x); false*. }
  { intros x. specializes E x. unfolds indom, map_indom.
    applys not_not_inv. intros N. rew_logic in N. false*. }
Qed.

Lemma disjoint_of_not_indom_both : h1 h2,
  ( x, indom h1 xindom h2 xFalse) →
  disjoint h1 h2.
Proof using. introv M. rewrite¬disjoint_eq_not_indom_both. Qed.

Lemma disjoint_inv_not_indom_both : h1 h2 x,
  disjoint h1 h2
  indom h1 x
  indom h2 x
  False.
Proof using. introv. rewrite* disjoint_eq_not_indom_both. Qed.

Lemma disjoint_single_of_not_indom : h x v,
  ¬indom h x
  disjoint (single x v) h.
Proof using.
  introv N. unfolds disjoint, map_disjoint. unfolds single, indom, map_indom.
  simpl. rew_logic in N. intros l'. case_if; subst; autos*.
Qed.
Note that the reciprocal of the above lemma is a special instance of disjoint_inv_not_indom_both

Read

Lemma read_single : {IB:Inhab B} x v,
  read (single x v) x = v.
Proof using.
  intros. unfold read, single. simpl. case_if¬.
Qed.

Lemma read_union_l : {IB:Inhab B} h1 h2 x,
  indom h1 x
  read (union h1 h2) x = read h1 x.
Proof using.
  intros. unfold read, union, map_union. simpl.
  case_eq (fmap_data h1 x); auto_false.
Qed.

Lemma read_union_r : {IB:Inhab B} h1 h2 x,
  ¬indom h1 x
  read (union h1 h2) x = read h2 x.
Proof using.
  intros. unfold read, union, map_union. simpl.
  case_eq (fmap_data h1 x).
  { intros v Hv. false H. auto_false. }
  { auto_false. }
Qed.

Update

Lemma update_eq_union_single : h x v,
  update h x v = union (single x v) h.
Proof using. auto. Qed.

Lemma update_single : x v w,
  update (single x v) x w = single x w.
Proof using.
  intros. rewrite update_eq_union_single.
  applys make_eq. intros y.
  unfold map_union, single. simpl. case_if¬.
Qed.

Lemma update_union_l : h1 h2 x v,
  indom h1 x
  update (union h1 h2) x v = union (update h1 x v) h2.
Proof using.
  intros. do 2 rewrite update_eq_union_single.
  applys make_eq. intros y.
  unfold map_union, union, map_union. simpl. case_if¬.
Qed.

Lemma update_union_r : h1 h2 x v,
  ¬indom h1 x
  update (union h1 h2) x v = union h1 (update h2 x v).
Proof using.
  introv M. asserts IB: (Inhab B). { applys Inhab_of_val v. }
  do 2 rewrite update_eq_union_single.
  applys make_eq. intros y.
  unfold map_union, union, map_union. simpl. case_if¬.
  { subst. case_eq (fmap_data h1 y); auto_false.
    { intros w Hw. false M. auto_false. } }
Qed.

Removal

Lemma remove_union_single_l : h x v,
  ¬indom h x
  remove (union (single x v) h) x = h.
Proof using.
  introv M. applys fmap_extens. intros y.
  unfold remove, map_remove, union, map_union, single. simpls. case_if.
  { destruct h as [f F]. unfolds indom, map_indom. simpls. subst. rew_logic¬in M. }
  { case_if¬. }
Qed.

End FmapProp.
Fixing arguments
Arguments union_assoc [A] [B].
Arguments union_comm_of_disjoint [A] [B].
Arguments union_comm_of_agree [A] [B].

Tactics for Finite Maps

Tactic disjoint for proving disjointness results

disjoint proves goals of the form \# h1 h2 and \# h1 h2 h3 by expanding all hypotheses into binary forms \# h1 h2 and then exploiting symmetry and disjointness with empty.
Module Export DisjointHints.
Hint Resolve disjoint_sym disjoint_empty_l disjoint_empty_r.
End DisjointHints.

Hint Rewrite
  disjoint_union_eq_l
  disjoint_union_eq_r
  disjoint_3_unfold : rew_disjoint.

Tactic Notation "rew_disjoint" :=
  autorewrite with rew_disjoint in *.
Tactic Notation "rew_disjoint" "*" :=
  rew_disjoint; auto_star.

Ltac fmap_disjoint_pre tt :=
  subst; rew_disjoint; jauto_set.

Tactic Notation "fmap_disjoint" :=
  solve [ fmap_disjoint_pre tt; auto ].

Lemma disjoint_demo : A B (h1 h2 h3 h4 h5:fmap A B),
  h1 = h2 \+ h3
  \# h2 h3
  \# h1 h4 h5
  \# h3 h2 h5 ∧ \# h4 h5.
Proof using.
  intros. dup 2.
  { subst. rew_disjoint. jauto_set. auto. auto. auto. auto. }
  { fmap_disjoint. }
Qed.

Tactic rew_map for Normalizing Expressions

Hint Rewrite
  union_assoc
  union_empty_l
  union_empty_r : rew_fmap rew_fmap_for_fmap_eq.

Tactic Notation "rew_fmap" :=
  autorewrite with rew_fmap in *.

Tactic Notation "rew_fmap" "~" :=
  rew_fmap; auto_tilde.

Tactic Notation "rew_fmap" "*" :=
  rew_fmap; auto_star.

Tactic fmap_eq for Proving Equalities

Section StateEq.
Variables (A B : Type).
Implicit Types h : fmap A B.
eq proves equalities between unions of fmaps, of the form h1 \+ h2 \+ h3 \+ h4 = h1' \+ h2' \+ h3' \+ h4' It attempts to discharge the disjointness side-conditions. Disclaimer: it cancels heaps at depth up to 4, but no more.
Lemma union_eq_cancel_1 : h1 h2 h2',
  h2 = h2'
  h1 \+ h2 = h1 \+ h2'.
Proof using. intros. subst. auto. Qed.

Lemma union_eq_cancel_1' : h1,
  h1 = h1.
Proof using. intros. auto. Qed.

Lemma union_eq_cancel_2 : h1 h1' h2 h2',
  \# h1 h1'
  h2 = h1' \+ h2'
  h1 \+ h2 = h1' \+ h1 \+ h2'.
Proof using.
  intros. subst. rewrite <- union_assoc.
  rewrite (union_comm_of_disjoint h1 h1').
  rewrite¬union_assoc. auto.
Qed.

Lemma union_eq_cancel_2' : h1 h1' h2,
  \# h1 h1'
  h2 = h1'
  h1 \+ h2 = h1' \+ h1.
Proof using.
  intros. subst. apply¬union_comm_of_disjoint.
Qed.

Lemma union_eq_cancel_3 : h1 h1' h2 h2' h3',
  \# h1 (h1' \+ h2') →
  h2 = h1' \+ h2' \+ h3'
  h1 \+ h2 = h1' \+ h2' \+ h1 \+ h3'.
Proof using.
  intros. subst.
  rewrite <- (union_assoc h1' h2' h3').
  rewrite <- (union_assoc h1' h2' (h1 \+ h3')).
  apply¬union_eq_cancel_2.
Qed.

Lemma union_eq_cancel_3' : h1 h1' h2 h2',
  \# h1 (h1' \+ h2') →
  h2 = h1' \+ h2'
  h1 \+ h2 = h1' \+ h2' \+ h1.
Proof using.
  intros. subst.
  rewrite <- (union_assoc h1' h2' h1).
  apply¬union_eq_cancel_2'.
Qed.

Lemma union_eq_cancel_4 : h1 h1' h2 h2' h3' h4',
  \# h1 ((h1' \+ h2') \+ h3') →
  h2 = h1' \+ h2' \+ h3' \+ h4'
  h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1 \+ h4'.
Proof using.
  intros. subst.
  rewrite <- (union_assoc h1' h2' (h3' \+ h4')).
  rewrite <- (union_assoc h1' h2' (h3' \+ h1 \+ h4')).
  apply¬union_eq_cancel_3.
Qed.

Lemma union_eq_cancel_4' : h1 h1' h2 h2' h3',
  \# h1 (h1' \+ h2' \+ h3') →
  h2 = h1' \+ h2' \+ h3'
  h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1.
Proof using.
  intros. subst.
  rewrite <- (union_assoc h2' h3' h1).
  apply¬union_eq_cancel_3'.
Qed.

End StateEq.

Ltac fmap_eq_step tt :=
  match goal with | ⊢ ?Gmatch G with
  | ?h1 = ?h1apply union_eq_cancel_1'
  | ?h1 \+ ?h2 = ?h1 \+ ?h2'apply union_eq_cancel_1
  | ?h1 \+ ?h2 = ?h1' \+ ?h1apply union_eq_cancel_2'
  | ?h1 \+ ?h2 = ?h1' \+ ?h1 \+ ?h2'apply union_eq_cancel_2
  | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1apply union_eq_cancel_3'
  | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 \+ ?h3'apply union_eq_cancel_3
  | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1apply union_eq_cancel_4'
  | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 \+ ?h4'apply union_eq_cancel_4
  end end.

Tactic Notation "fmap_eq" :=
  subst;
  autorewrite with rew_fmap_for_fmap_eq;
  repeat (fmap_eq_step tt);
  try match goal with
  | ⊢ \# _ _fmap_disjoint
  | ⊢ \# _ _ _fmap_disjoint
  end.

Tactic Notation "fmap_eq" "~" :=
  fmap_eq; auto_tilde.

Tactic Notation "fmap_eq" "*" :=
  fmap_eq; auto_star.

Lemma fmap_eq_demo : A B (h1 h2 h3 h4 h5:fmap A B),
  \# h1 h2 h3
  \# (h1 \+ h2 \+ h3) h4 h5
  h1 = h2 \+ h3
  h4 \+ h1 \+ h5 = h2 \+ h5 \+ h4 \+ h3.
Proof using.
  intros. dup 2.
  { subst. rew_fmap.
    fmap_eq_step tt. fmap_disjoint.
    fmap_eq_step tt.
    fmap_eq_step tt. fmap_disjoint. auto. }
  { fmap_eq. }
Qed.

Existence of Fresh Locations

Consecutive Locations

The notion of "consecutive locations" is useful for reasoning about records and arrays.
Fixpoint conseq (B:Type) (vs:list B) (l:nat) : fmap nat B :=
  match vs with
  | nilempty
  | v::vs' ⇒ (single l v) \+ (conseq vs' (S l))
  end.

Lemma conseq_nil : B (l:nat),
  conseq (@nil B) l = empty.
Proof using. auto. Qed.

Lemma conseq_cons : B (l:nat) (v:B) (vs:list B),
  conseq (v::vs) l = (single l v) \+ (conseq vs (S l)).
Proof using. auto. Qed.

Lemma conseq_cons' : B (l:nat) (v:B) (vs:list B),
  conseq (v::vs) l = (single l v) \+ (conseq vs (l+1)).
Proof using. intros. math_rewrite (l+1 = S l)%nat. applys conseq_cons. Qed.

Global Opaque conseq.

Hint Rewrite conseq_nil conseq_cons : rew_listx.

Existence of Fresh Locations

Definition loc_fresh_gen (L : list nat) :=
  (1 + fold_right plus O L)%nat.

Lemma loc_fresh_ind : l L,
  mem l L
  (l < loc_fresh_gen L)%nat.
Proof using.
  intros l L. unfold loc_fresh_gen.
  induction L; introv M; inverts M; rew_listx.
  { math. }
  { forwards~: IHL. math. }
Qed.

Lemma loc_fresh_nat_ge : (L:list nat),
   (l:nat), (i:nat), ¬mem (l+i)%nat L.
Proof using.
  intros L. (loc_fresh_gen L). intros i M.
  lets: loc_fresh_ind M. math.
Qed.
For any finite list of locations (implemented as nat), there exists one location not in that list.
Lemma loc_fresh_nat : (L:list nat),
   (l:nat), ¬mem l L.
Proof using.
  intros L. forwards (l&P): loc_fresh_nat_ge L.
   l. intros M. applys (P 0%nat). applys_eq M. math.
Qed.

Section FmapFresh.
Variables (B : Type).
Implicit Types h : fmap nat B.
For any heap, there exists one (non-null) location not already in the domain of that heap.
Lemma exists_fresh : null h,
   l, ¬indom h llnull.
Proof using.
  intros null (m&(L&M)). unfold indom, map_indom. simpl.
  lets (l&F): (loc_fresh_nat (null::L)).
   l. split.
  { simpl. intros l'. forwards¬E: M l. }
  { intro_subst. applys¬F. }
Qed.
For any heap h, there exists one (non-null) location l such that the singleton map that binds l to a value v is disjoint from h.
Lemma single_fresh : null h v,
   l, \# (single l v) hlnull.
Proof using.
  intros. forwards (l&F&N): exists_fresh null h.
   l. split¬. applys* disjoint_single_of_not_indom.
Qed.

Lemma conseq_fresh : null h vs,
   l, \# (conseq vs l) hlnull.
Proof using.
  intros null (m&(L&M)) vs.
  unfold disjoint, map_disjoint. simpl.
  lets (l&F): (loc_fresh_nat_ge (null::L)).
   l. split.
  { intros l'. gen l. induction vs as [|v vs']; intros.
    { simple¬. }
    { rewrite conseq_cons. destruct (IHvs' (S l)%nat) as [E|?].
      { intros i N. applys F (S i). applys_eq N. math. }
      { simpl. unfold map_union. case_if¬.
        { subst. right. applys not_not_inv. intros H. applys F 0%nat.
          constructor. math_rewrite (l'+0 = l')%nat. applys¬M. } }
      { auto. } } }
  { intro_subst. applys¬F 0%nat. rew_nat. auto. }
Qed.

Lemma disjoint_single_conseq : B l l' L (v:B),
  (l < l')%nat ∨ (ll'+length L)%nat
  \# (single l v) (conseq L l').
Proof using.
  introv N. gen l'. induction L as [|L']; intros.
  { rewrite¬conseq_nil. }
  { rew_list in N. rewrite conseq_cons. rew_disjoint. split.
    { applys disjoint_single_single. destruct N; math. }
    { applys IHL. destruct N. { left. math. } { right. math. } } }
Qed.

Existence of a Smallest Fresh Locations

The notion of smallest fresh location is useful for setting up deterministic semantics.
Definition fresh (null:nat) (h:fmap nat B) (l:nat) : Prop :=
  ¬indom h llnull.

Definition smallest_fresh (null:nat) (h:fmap nat B) (l:nat) : Prop :=
  fresh null h l ∧ ( l', l' < l → ¬fresh null h l').

Lemma exists_smallest_fresh : null h,
   l, smallest_fresh null h l.
Proof using.
  intros.
  cuts M: ( l0, fresh null h l0
             l, fresh null h l
                   ∧ ( l', l' < l → ¬fresh null h l')).
  { lets (l0&F&N): exists_fresh null h. applys M l0. split*. }
  intros l0. induction_wf IH: wf_lt l0. intros F.
  tests C: ( l', l' < l0 → ¬fresh null h l').
  { * l0. }
  { destruct C as (l0'&K). rew_logic in K. destruct K as (L&F').
    applys* IH l0'. }
Qed.

Existence of Nonempty Heaps

The existence of nonempty (nat-indexed) finite maps is useful for constructing counterexamples.
Lemma exists_not_empty : `{IB:Inhab B},
   (h:fmap nat B), hempty.
Proof using.
  intros. sets l: 0%nat. sets h: (single l (arbitrary (A:=B))).
   h. intros N.
  sets h': (empty:fmap nat B).
  asserts M1: (indom h l).
  { applys indom_single. }
  asserts M2: (~ indom h' l).
  { unfolds @indom, map_indom, @empty. simpls. auto_false. }
  rewrite N in M1. false*.
Qed.

End FmapFresh.

(* 2021-01-25 13:22 *)