fin_map_dom.v 6.21 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
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 collections fin_maps.
7

8 9 10 11 12
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} := {
13 14 15 16 17
  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)
}.

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

21 22
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.
23
Lemma not_elem_of_dom {A} (m : M A) i : i  dom D m  m !! i = None.
24
Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
25
Lemma subseteq_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
26
Proof.
27 28
  rewrite map_subseteq_spec.
  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
29
Qed.
30
Lemma subset_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
31
Proof.
32 33 34
  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.
36 37 38
Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _)  .
Proof.
39
  split; intro; [|set_solver].
40
  rewrite elem_of_dom, lookup_empty. by inversion 1.
41
Qed.
42
Lemma dom_empty_inv {A} (m : M A) : dom D m    m = .
43 44
Proof.
  intros E. apply map_empty. intros. apply not_elem_of_dom.
45
  rewrite E. set_solver.
46
Qed.
47 48 49
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.
51 52
  destruct (m !! j); naive_solver.
Qed.
53
Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m)  {[ i ]}  dom D m.
54
Proof.
55 56
  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)); set_solver.
58
Qed.
59
Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m  dom D (<[i:=x]>m).
60
Proof. rewrite (dom_insert _). set_solver. Qed.
61
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
62
  X  dom D m  X  dom D (<[i:=x]>m).
63
Proof. intros. trans (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; set_solver. Qed.
66
Lemma dom_delete {A} (m : M A) i : dom D (delete i m)  dom D m  {[ i ]}.
67
Proof.
68
  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
69
  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
70 71 72 73 74 75 76
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2  .
78
Proof.
79 80
  rewrite map_disjoint_spec, elem_of_equiv_empty.
  setoid_rewrite elem_of_intersection.
81
  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
82
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2  .
84
Proof. apply map_disjoint_dom. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1  dom D m2    m1  m2.
86
Proof. apply map_disjoint_dom. Qed.
87
Lemma dom_union {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
88
Proof.
89 90 91
  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.
92 93 94 95
Qed.
Lemma dom_intersection {A} (m1 m2 : M A) :
  dom D (m1  m2)  dom D m1  dom D m2.
Proof.
96 97
  apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
  unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
98
Qed.
99
Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
100
Proof.
101 102 103
  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.
104
Qed.
105 106 107 108 109 110
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.
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 ]}.
127 128 129 130 131 132 133 134 135 136 137 138
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.
139
End fin_map_dom.