fin_map_dom.v 6.23 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* 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 prelude Require Export collections fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

Class FinMapDom K M D `{FMap M,
     A, Lookup K A (M A),  A, Empty (M A),  A, PartialAlter K A (M A),
    OMap M, Merge M,  A, FinMapToList K A (M A),  i j : K, Decision (i = j),
     A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
    Union D, Intersection D, Difference D} := {
  finmap_dom_map :>> FinMap K M;
  finmap_dom_collection :>> Collection K D;
  elem_of_dom {A} (m : M A) i : i  dom D m  is_Some (m !! i)
}.

Section fin_map_dom.
Context `{FinMapDom K M D}.

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

Context `{!LeibnizEquiv D}.
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.
126
Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i := x]} = {[ i ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
131
132
133
134
135
136
137
138
139
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 : dom D (f <$> m) = dom D m.
Proof. unfold_leibniz; apply dom_fmap. Qed.
End fin_map_dom.