fin_map_dom.v 10.5 KB
Newer Older
1 2 3
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
4
From stdpp Require Export sets fin_maps.
5
Set Default Proof Using "Type*".
6

7
Class FinMapDom K M D `{ A, Dom (M A) D, FMap M,
8
     A, Lookup K A (M A),  A, Empty (M A),  A, PartialAlter K A (M A),
9
    OMap M, Merge M,  A, FinMapToList K A (M A), EqDecision K,
10
    ElemOf K D, Empty D, Singleton K D,
11
    Union D, Intersection D, Difference D} := {
12 13
  finmap_dom_map :> FinMap K M;
  finmap_dom_set :> Set_ K D;
14 15 16
  elem_of_dom {A} (m : M A) i : i  dom D m  is_Some (m !! i)
}.

17
Section fin_map_dom.
18 19
Context `{FinMapDom K M D}.

Dan Frumin's avatar
Dan Frumin committed
20 21 22 23
Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
  i  dom D m  m !! i = Some (m !!! i).
Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed.

24 25 26 27 28 29 30 31
Lemma dom_map_filter {A} (P : K * A  Prop) `{! x, Decision (P x)} (m : M A) X :
  ( i, i  X   x, m !! i = Some x  P (i, x)) 
  dom D (filter P m)  X.
Proof.
  intros HX i. rewrite elem_of_dom, HX.
  unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
Qed.
Lemma dom_map_filter_subseteq {A} (P : K * A  Prop) `{! x, Decision (P x)} (m : M A):
32 33 34 35 36 37
  dom D (filter P m)  dom D m.
Proof.
  intros ?. rewrite 2!elem_of_dom.
  destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists.
Qed.

38 39
Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x  i  dom D m.
Proof. rewrite elem_of_dom; eauto. Qed.
40
Lemma not_elem_of_dom {A} (m : M A) i : i  dom D m  m !! i = None.
41
Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
42
Lemma subseteq_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
43
Proof.
44 45
  rewrite map_subseteq_spec.
  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
46
Qed.
47
Lemma subset_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
48
Proof.
49 50 51
  intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
  contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
  specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
52
  destruct Hss2; eauto. by simplify_map_eq.
53 54 55
Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _)  .
Proof.
56
  intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
57
Qed.
58
Lemma dom_empty_inv {A} (m : M A) : dom D m    m = .
59 60
Proof.
  intros E. apply map_empty. intros. apply not_elem_of_dom.
61
  rewrite E. set_solver.
62
Qed.
63 64 65
Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m)  dom D m.
Proof.
  apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
66
  destruct (decide (i = j)); simplify_map_eq/=; eauto.
67 68
  destruct (m !! j); naive_solver.
Qed.
69
Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m)  {[ i ]}  dom D m.
70
Proof.
71 72
  apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_insert_Some.
73
  destruct (decide (i = j)); set_solver.
74
Qed.
75
Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m  dom D (<[i:=x]>m).
76
Proof. rewrite (dom_insert _). set_solver. Qed.
77
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
78
  X  dom D m  X  dom D (<[i:=x]>m).
79
Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
80
Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A)  {[ i ]}.
81
Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
82
Lemma dom_delete {A} (m : M A) i : dom D (delete i m)  dom D m  {[ i ]}.
83
Proof.
84
  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
85
  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
86 87 88 89 90 91 92
Qed.
Lemma delete_partial_alter_dom {A} (m : M A) i f :
  i  dom D m  delete i (partial_alter f i m) = m.
Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
Lemma delete_insert_dom {A} (m : M A) i x :
  i  dom D m  delete i (<[i:=x]>m) = m.
Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
93
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ## m2  dom D m1 ## dom D m2.
94
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  rewrite map_disjoint_spec, elem_of_disjoint.
96
  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
97
Qed.
98
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ## m2  dom D m1 ## dom D m2.
99
Proof. apply map_disjoint_dom. Qed.
100
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2  m1 ## m2.
101
Proof. apply map_disjoint_dom. Qed.
102
Lemma dom_union {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
103
Proof.
104 105 106
  apply elem_of_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_union_Some_raw.
  destruct (m1 !! i); naive_solver.
107
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1  m2)  dom D m1  dom D m2.
109
Proof.
110 111
  apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
112
Qed.
113
Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
114
Proof.
115 116 117
  apply elem_of_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_difference_Some.
  destruct (m2 !! i); naive_solver.
118
Qed.
119
Lemma dom_fmap {A B} (f : A  B) (m : M A) : dom D (f <$> m)  dom D m.
120 121 122 123 124
Proof.
  apply elem_of_equiv. intros i.
  rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
  destruct (m !! i); naive_solver.
Qed.
125 126 127
Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
Proof.
  induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
128 129
    eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
    (singleton_finite (C:=D)).
130
Qed.
Ralf Jung's avatar
Ralf Jung committed
131 132 133 134 135 136 137 138 139 140 141
Global Instance dom_proper `{!Equiv A} : Proper ((@{M A}) ==> ()) (dom D).
Proof.
  intros m1 m2 EQm. apply elem_of_equiv. intros i.
  rewrite !elem_of_dom, EQm. done.
Qed.
(** If [D] has Leibniz equality, we can show an even stronger result.  This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
  Proper ((@{M A}) ==> (=)) (dom D) | 0.
Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
142

143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
Section leibniz.
  Context `{!LeibnizEquiv D}.
  Lemma dom_map_filter_L {A} (P : K * A  Prop) `{! x, Decision (P x)} (m : M A) X :
    ( i, i  X   x, m !! i = Some x  P (i, x)) 
    dom D (filter P m) = X.
  Proof. unfold_leibniz. apply dom_map_filter. Qed.
  Lemma dom_empty_L {A} : dom D (@empty (M A) _) = .
  Proof. unfold_leibniz; apply dom_empty. Qed.
  Lemma dom_empty_inv_L {A} (m : M A) : dom D m =   m = .
  Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
  Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
  Proof. unfold_leibniz; apply dom_alter. Qed.
  Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]}  dom D m.
  Proof. unfold_leibniz; apply dom_insert. Qed.
  Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
  Proof. unfold_leibniz; apply dom_singleton. Qed.
  Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m  {[ i ]}.
  Proof. unfold_leibniz; apply dom_delete. Qed.
  Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1  m2) = dom D m1  dom D m2.
  Proof. unfold_leibniz; apply dom_union. Qed.
  Lemma dom_intersection_L {A} (m1 m2 : M A) :
    dom D (m1  m2) = dom D m1  dom D m2.
  Proof. unfold_leibniz; apply dom_intersection. Qed.
  Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1  m2) = dom D m1  dom D m2.
  Proof. unfold_leibniz; apply dom_difference. Qed.
  Lemma dom_fmap_L {A B} (f : A  B) (m : M A) : dom D (f <$> m) = dom D m.
  Proof. unfold_leibniz; apply dom_fmap. Qed.
End leibniz.
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220

(** * Set solver instances *)
Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom D (:M A)) False.
Proof. constructor. by rewrite dom_empty, elem_of_empty. Qed.
Global Instance set_unfold_dom_alter {A} f i j (m : M A) Q :
  SetUnfoldElemOf i (dom D m) Q 
  SetUnfoldElemOf i (dom D (alter f j m)) Q.
Proof. constructor. by rewrite dom_alter, (set_unfold_elem_of _ (dom _ _) _). Qed.
Global Instance set_unfold_dom_insert {A} i j x (m : M A) Q :
  SetUnfoldElemOf i (dom D m) Q 
  SetUnfoldElemOf i (dom D (<[j:=x]> m)) (i = j  Q).
Proof.
  constructor. by rewrite dom_insert, elem_of_union,
    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
Qed.
Global Instance set_unfold_dom_delete {A} i j (m : M A) Q :
  SetUnfoldElemOf i (dom D m) Q 
  SetUnfoldElemOf i (dom D (delete j m)) (Q  i  j).
Proof.
  constructor. by rewrite dom_delete, elem_of_difference,
    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
Qed.
Global Instance set_unfold_dom_singleton {A} i j :
  SetUnfoldElemOf i (dom D ({[ j := x ]} : M A)) (i = j).
Proof. constructor. by rewrite dom_singleton, elem_of_singleton. Qed.
Global Instance set_unfold_dom_union {A} i (m1 m2 : M A) Q1 Q2 :
  SetUnfoldElemOf i (dom D m1) Q1  SetUnfoldElemOf i (dom D m2) Q2 
  SetUnfoldElemOf i (dom D (m1  m2)) (Q1  Q2).
Proof.
  constructor. by rewrite dom_union, elem_of_union,
    !(set_unfold_elem_of _ (dom _ _) _).
Qed.
Global Instance set_unfold_dom_intersection {A} i (m1 m2 : M A) Q1 Q2 :
  SetUnfoldElemOf i (dom D m1) Q1  SetUnfoldElemOf i (dom D m2) Q2 
  SetUnfoldElemOf i (dom D (m1  m2)) (Q1  Q2).
Proof.
  constructor. by rewrite dom_intersection, elem_of_intersection,
    !(set_unfold_elem_of _ (dom _ _) _).
Qed.
Global Instance set_unfold_dom_difference {A} i (m1 m2 : M A) Q1 Q2 :
  SetUnfoldElemOf i (dom D m1) Q1  SetUnfoldElemOf i (dom D m2) Q2 
  SetUnfoldElemOf i (dom D (m1  m2)) (Q1  ¬Q2).
Proof.
  constructor. by rewrite dom_difference, elem_of_difference,
    !(set_unfold_elem_of _ (dom _ _) _).
Qed.
Global Instance set_unfold_dom_fmap {A B} (f : A  B) i (m : M A) Q :
  SetUnfoldElemOf i (dom D m) Q 
  SetUnfoldElemOf i (dom D (f <$> m)) Q.
Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _ _) _). Qed.
221
End fin_map_dom.
222 223

Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
224
  dom D (map_seq start (M:=M A) xs)  set_seq start (length xs).
225 226 227 228 229 230
Proof.
  revert start. induction xs as [|x xs IH]; intros start; simpl.
  - by rewrite dom_empty.
  - by rewrite dom_insert, IH.
Qed.
Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
231
  dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
232
Proof. unfold_leibniz. apply dom_seq. Qed.
233 234 235 236

Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
  SetUnfoldElemOf i (dom D (map_seq start (M:=M A) xs)) (start  i < start + length xs).
Proof. constructor. by rewrite dom_seq, elem_of_set_seq. Qed.