fin_map_dom.v 6.09 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 iris.prelude Require Export collections fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8 9 10
Class FinMapDom K M D `{FMap M, Lookup K M,  A, Empty (M A), PartialAlter K M,
    OMap M, Merge M, FinMapToList K M,  i j : K, Decision (i = j),
    Dom M D, ElemOf K D, Empty D, Singleton K D,
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
    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.
34
  destruct Hss2; eauto. by simplify_map_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36 37
Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _)  .
Proof.
38
  intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40 41 42
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.
43
  rewrite E. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47
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.
48
  destruct (decide (i = j)); simplify_map_eq/=; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51 52 53 54
  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.
55
  destruct (decide (i = j)); set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57
Qed.
Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m  dom D (<[i:=x]>m).
58
Proof. rewrite (dom_insert _). set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
  X  dom D m  X  dom D (<[i:=x]>m).
61
Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
62
Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]}  {[ i ]}.
63
Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66
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.
67
  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71 72 73 74
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
75
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  rewrite map_disjoint_spec, elem_of_disjoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
78 79
  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1  m2  dom D m1  dom D m2.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof. apply map_disjoint_dom. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1  dom D m2  m1  m2.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88 89
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1  m2)  dom D m1  dom D m2.
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
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.
107 108 109 110 111
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
112 113 114 115 116 117 118 119 120 121

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.
122
Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i := x]} = {[ i ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125 126 127 128 129 130 131 132 133 134 135
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.