fin_map_dom.v 8.09 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

Context `{!LeibnizEquiv D}.
146 147 148 149
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.
150 151 152 153 154 155 156 157
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.
158
Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
159 160 161 162 163 164 165 166 167 168
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.
169
Lemma dom_fmap_L {A B} (f : A  B) (m : M A) : dom D (f <$> m) = dom D m.
170
Proof. unfold_leibniz; apply dom_fmap. Qed.
171
End fin_map_dom.
172 173

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