fin_map_dom.v 8.17 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2 3 4 5
(* This file is distributed under the terms of the BSD license. *)
(** 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. *)
6
From stdpp Require Export sets fin_maps.
7
Set Default Proof Using "Type*".
8

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

19
Section fin_map_dom.
20 21
Context `{FinMapDom K M D}.

Dan Frumin's avatar
Dan Frumin committed
22 23 24 25
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.

26 27 28 29 30 31 32 33
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):
34 35 36 37 38 39
  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.

40 41
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.
42
Lemma not_elem_of_dom {A} (m : M A) i : i  dom D m  m !! i = None.
43
Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
44
Lemma subseteq_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
45
Proof.
46 47
  rewrite map_subseteq_spec.
  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
48
Qed.
49
Lemma subset_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
50
Proof.
51 52 53
  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.
54
  destruct Hss2; eauto. by simplify_map_eq.
55 56 57
Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _)  .
Proof.
58
  intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
59
Qed.
60
Lemma dom_empty_inv {A} (m : M A) : dom D m    m = .
61 62
Proof.
  intros E. apply map_empty. intros. apply not_elem_of_dom.
63
  rewrite E. set_solver.
64
Qed.
65 66 67
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.
68
  destruct (decide (i = j)); simplify_map_eq/=; eauto.
69 70
  destruct (m !! j); naive_solver.
Qed.
71
Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m)  {[ i ]}  dom D m.
72
Proof.
73 74
  apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_insert_Some.
75
  destruct (decide (i = j)); set_solver.
76
Qed.
77
Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m  dom D (<[i:=x]>m).
78
Proof. rewrite (dom_insert _). set_solver. Qed.
79
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
80
  X  dom D m  X  dom D (<[i:=x]>m).
81
Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
82
Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A)  {[ i ]}.
83
Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
84
Lemma dom_delete {A} (m : M A) i : dom D (delete i m)  dom D m  {[ i ]}.
85
Proof.
86
  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
87
  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
88 89 90 91 92 93 94
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.
95
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ## m2  dom D m1 ## dom D m2.
96
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  rewrite map_disjoint_spec, elem_of_disjoint.
98
  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
99
Qed.
100
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ## m2  dom D m1 ## dom D m2.
101
Proof. apply map_disjoint_dom. Qed.
102
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2  m1 ## m2.
103
Proof. apply map_disjoint_dom. Qed.
104
Lemma dom_union {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
105
Proof.
106 107 108
  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.
109
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1  m2)  dom D m1  dom D m2.
111
Proof.
112 113
  apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
114
Qed.
115
Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
116
Proof.
117 118 119
  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.
120
Qed.
121
Lemma dom_fmap {A B} (f : A  B) (m : M A) : dom D (f <$> m)  dom D m.
122 123 124 125 126
Proof.
  apply elem_of_equiv. intros i.
  rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
  destruct (m !! i); naive_solver.
Qed.
127 128 129
Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
Proof.
  induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
130 131
    eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
    (singleton_finite (C:=D)).
132
Qed.
Ralf Jung's avatar
Ralf Jung committed
133 134 135 136 137 138 139 140 141 142 143
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.
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 171 172
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.
173
End fin_map_dom.
174 175

Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
176
  dom D (map_seq start (M:=M A) xs)  set_seq start (length xs).
177 178 179 180 181 182
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) :
183
  dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
184
Proof. unfold_leibniz. apply dom_seq. Qed.