fin_map_dom.v 4.42 KB
Newer Older
1 2 3 4 5 6 7 8
(* Copyright (c) 2012-2013, 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. *)
Require Export collections fin_maps.

Class FinMapDom K M D `{!FMap M}
9 10
    `{ A, Lookup K A (M A)} `{ A, Empty (M A)} `{ A, PartialAlter K A (M A)}
    `{!Merge M} `{ A, FinMapToList K A (M A)}
11
    `{ i j : K, Decision (i = j)}
12 13
    `{ A, Dom (M A) D} `{ElemOf K D} `{Empty D} `{Singleton K D}
    `{Union D}`{Intersection D} `{Difference D} := {
14 15 16 17 18
  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)
}.

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

22
Lemma not_elem_of_dom {A} (m : M A) i : i  dom D m  m !! i = None.
23 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 27 28 29
Proof.
  unfold subseteq, map_subseteq, collection_subseteq.
  intros ??. rewrite !elem_of_dom. inversion 1. eauto.
Qed.
30
Lemma subset_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
31 32 33 34 35
Proof.
  intros [Hss1 Hss2]. split.
  { by apply subseteq_dom. }
  intros Hdom. destruct Hss2. intros i x Hi.
  specialize (Hdom i). rewrite !elem_of_dom in Hdom.
36
  feed inversion Hdom. eauto. by erewrite (Hss1 i) in Hi by eauto.
37 38 39 40 41 42 43 44
Qed.

Lemma dom_empty {A} : dom D (@empty (M A) _)  .
Proof.
  split; intro.
  * rewrite elem_of_dom, lookup_empty. by inversion 1.
  * solve_elem_of.
Qed.
45
Lemma dom_empty_inv {A} (m : M A) : dom D m    m = .
46 47 48 49 50
Proof.
  intros E. apply map_empty. intros. apply not_elem_of_dom.
  rewrite E. solve_elem_of.
Qed.

51
Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m)  {[ i ]}  dom D m.
52 53 54 55 56 57
Proof.
  apply elem_of_equiv. intros j.
  rewrite elem_of_union, !elem_of_dom, !is_Some_alt.
  setoid_rewrite lookup_insert_Some.
  destruct (decide (i = j)); esolve_elem_of.
Qed.
58
Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m  dom D (<[i:=x]>m).
59 60
Proof. rewrite (dom_insert _). solve_elem_of. Qed.
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
61
  X  dom D m  X  dom D (<[i:=x]>m).
62 63
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 66 67 68 69
Proof.
  unfold singleton at 1, map_singleton.
  rewrite dom_insert, dom_empty. solve_elem_of.
Qed.

70
Lemma dom_delete {A} (m : M A) i : dom D (delete i m)  dom D m  {[ i ]}.
71 72 73 74 75 76 77 78 79 80 81 82 83
Proof.
  apply elem_of_equiv. intros j.
  rewrite elem_of_difference, !elem_of_dom, !is_Some_alt.
  setoid_rewrite lookup_delete_Some. esolve_elem_of.
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.

84
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2  .
85 86 87 88 89
Proof.
  unfold disjoint, map_disjoint, map_intersection_forall.
  rewrite elem_of_equiv_empty. setoid_rewrite elem_of_intersection.
  setoid_rewrite elem_of_dom. setoid_rewrite is_Some_alt. naive_solver.
Qed.
90
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2  .
91
Proof. apply map_disjoint_dom. Qed.
92
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1  dom D m2    m1  m2.
93 94
Proof. apply map_disjoint_dom. Qed.

95
Lemma dom_union {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
96 97 98
Proof.
  apply elem_of_equiv. intros i.
  rewrite elem_of_union, !elem_of_dom, !is_Some_alt.
99
  setoid_rewrite lookup_union_Some_raw. destruct (m1 !! i); naive_solver.
100 101 102 103 104 105 106 107 108 109 110
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, !is_Some_alt.
  setoid_rewrite lookup_intersection_Some.
  setoid_rewrite is_Some_alt. naive_solver.
Qed.

111
Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1  m2)  dom D m1  dom D m2.
112 113 114
Proof.
  apply elem_of_equiv. intros i.
  rewrite elem_of_difference, !elem_of_dom, !is_Some_alt.
115
  setoid_rewrite lookup_difference_Some. destruct (m2 !! i); naive_solver.
116
Qed.
117
End fin_map_dom.