fin_map_dom.v 6.16 KB
Newer Older
1
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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 iris.prelude Require Export collections fin_maps.
7
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10

Class FinMapDom K M D `{FMap M,
     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,
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
     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.
36
  destruct Hss2; eauto. by simplify_map_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38 39
Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _)  .
Proof.
40
  intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43 44
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.
45
  rewrite E. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47 48 49
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)); set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
Qed.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
  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.
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. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  rewrite map_disjoint_spec, elem_of_disjoint.
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81
  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
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
83
Proof. apply map_disjoint_dom. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
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
85 86 87 88 89 90 91
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
92
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
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
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.
109 110 111 112 113
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
114 115 116 117 118 119 120 121 122 123

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