Commit 9813f9b5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Separation type class for singleton maps.

parent 061604dd
......@@ -65,7 +65,7 @@ Proof.
by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done.
Qed.
Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
Timeless x Timeless ({[ i, x ]} : gmap K A) := _.
Timeless x Timeless ({[ i x ]} : gmap K A) := _.
Instance map_fmap_ne `{Dist A, Dist B} (f : A B) n :
Proper (dist n ==> dist n) f
Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
......@@ -172,7 +172,7 @@ Proof.
by specialize (Hm j); simplify_map_equality.
Qed.
Global Instance map_ra_singleton_valid_timeless `{Valid A, ValidN A} (i : K) x :
ValidTimeless x ValidTimeless ({[ i, x ]} : gmap K A).
ValidTimeless x ValidTimeless ({[ i x ]} : gmap K A).
Proof.
intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
by rewrite lookup_empty.
......
......@@ -146,10 +146,9 @@ Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
Lemma big_opM_insert (m : M A) i x :
m !! i = None big_opM (<[i:=x]> m) x big_opM m.
Proof. intros ?; unfold big_opM. by rewrite map_to_list_insert by done. Qed.
Lemma big_opM_singleton i x : big_opM ({[i,x]} : M A) x.
Lemma big_opM_singleton i x : big_opM ({[i x]} : M A) x.
Proof.
unfold singleton, map_singleton.
rewrite big_opM_insert by auto using lookup_empty; simpl.
rewrite <-insert_empty, big_opM_insert by auto using lookup_empty; simpl.
by rewrite big_opM_empty, (right_id _ _).
Qed.
Global Instance big_opM_proper : Proper (() ==> ()) (big_opM : M A _).
......
......@@ -468,6 +468,11 @@ Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
(** The singleton map *)
Class SingletonM K A M := singletonM: K A M.
Instance: Params (@singletonM) 5.
Notation "{[ x ↦ y ]}" := (singletonM x y) (at level 1) : C_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
Class Insert (K A M : Type) := insert: K A M M.
......
......@@ -61,11 +61,8 @@ 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.
Lemma dom_singleton {A} (i : K) (x : A) : dom D {[(i, x)]} {[ i ]}.
Proof.
unfold singleton at 1, map_singleton.
rewrite dom_insert, dom_empty. solve_elem_of.
Qed.
Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i x]} {[ i ]}.
Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed.
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.
......@@ -121,7 +118,7 @@ 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.
Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[(i, x)]} = {[ i ]}.
Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i x]} = {[ i ]}.
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.
......
......@@ -56,7 +56,7 @@ Instance map_alter `{PartialAlter K A M} : Alter K A M :=
Instance map_delete `{PartialAlter K A M} : Delete K M :=
partial_alter (λ _, None).
Instance map_singleton `{PartialAlter K A M, Empty M} :
Singleton (K * A) M := λ p, <[p.1:=p.2]> .
SingletonM K A M := λ i x, <[i:=x]> .
Definition map_of_list `{Insert K A M, Empty M} : list (K * A) M :=
fold_right (λ p, <[p.1:=p.2]>) .
......@@ -138,6 +138,9 @@ Section setoid.
Global Instance insert_proper (i : K) :
Proper (() ==> () ==> ()) (insert (M:=M A) i).
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
Global Instance singleton_proper k :
Proper (() ==> ()) (singletonM k : A M A).
Proof. by intros ???; apply insert_proper. Qed.
Global Instance delete_proper (i : K) :
Proper (() ==> ()) (delete (M:=M A) i).
Proof. by apply partial_alter_proper; [constructor|]. Qed.
......@@ -340,7 +343,7 @@ Proof.
Qed.
Lemma delete_empty {A} i : delete i ( : M A) = .
Proof. rewrite <-(partial_alter_self ) at 2. by rewrite lookup_empty. Qed.
Lemma delete_singleton {A} i (x : A) : delete i {[i, x]} = .
Lemma delete_singleton {A} i (x : A) : delete i {[i x]} = .
Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
Lemma delete_commute {A} (m : M A) i j :
delete i (delete j m) = delete j (delete i m).
......@@ -476,43 +479,39 @@ Proof.
* by rewrite lookup_fmap, !lookup_insert.
* by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
Lemma insert_empty {A} i (x : A) : <[i:=x]> = {[i,x]}.
Lemma insert_empty {A} i (x : A) : <[i:=x]> = {[i x]}.
Proof. done. Qed.
(** ** Properties of the singleton maps *)
Lemma lookup_singleton_Some {A} i j (x y : A) :
{[i, x]} !! j = Some y i = j x = y.
{[i x]} !! j = Some y i = j x = y.
Proof.
unfold singleton, map_singleton.
rewrite lookup_insert_Some, lookup_empty. simpl. intuition congruence.
rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence.
Qed.
Lemma lookup_singleton_None {A} i j (x : A) : {[i, x]} !! j = None i j.
Proof.
unfold singleton, map_singleton.
rewrite lookup_insert_None, lookup_empty. simpl. tauto.
Qed.
Lemma lookup_singleton {A} i (x : A) : {[i, x]} !! i = Some x.
Lemma lookup_singleton_None {A} i j (x : A) : {[i x]} !! j = None i j.
Proof. rewrite <-insert_empty,lookup_insert_None, lookup_empty; tauto. Qed.
Lemma lookup_singleton {A} i (x : A) : {[i x]} !! i = Some x.
Proof. by rewrite lookup_singleton_Some. Qed.
Lemma lookup_singleton_ne {A} i j (x : A) : i j {[i, x]} !! j = None.
Lemma lookup_singleton_ne {A} i j (x : A) : i j {[i x]} !! j = None.
Proof. by rewrite lookup_singleton_None. Qed.
Lemma map_non_empty_singleton {A} i (x : A) : {[i,x]} .
Lemma map_non_empty_singleton {A} i (x : A) : {[i x]} .
Proof.
intros Hix. apply (f_equal (!! i)) in Hix.
by rewrite lookup_empty, lookup_singleton in Hix.
Qed.
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i, x]} = {[i, y]}.
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i x]} = {[i y]}.
Proof.
unfold singleton, map_singleton, insert, map_insert.
unfold singletonM, map_singleton, insert, map_insert.
by rewrite <-partial_alter_compose.
Qed.
Lemma alter_singleton {A} (f : A A) i x : alter f i {[i,x]} = {[i, f x]}.
Lemma alter_singleton {A} (f : A A) i x : alter f i {[i x]} = {[i f x]}.
Proof.
intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?].
* by rewrite lookup_alter, !lookup_singleton.
* by rewrite lookup_alter_ne, !lookup_singleton_ne.
Qed.
Lemma alter_singleton_ne {A} (f : A A) i j x :
i j alter f i {[j,x]} = {[j,x]}.
i j alter f i {[j x]} = {[j x]}.
Proof.
intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
......@@ -524,7 +523,7 @@ Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
Lemma omap_empty {A B} (f : A option B) : omap f = .
Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma omap_singleton {A B} (f : A option B) i x y :
f x = Some y omap f {[ i,x ]} = {[ i,y ]}.
f x = Some y omap f {[ i x ]} = {[ i y ]}.
Proof.
intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|].
* by rewrite lookup_omap, !lookup_singleton.
......@@ -874,10 +873,9 @@ Lemma insert_merge m1 m2 i x y z :
<[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
Proof. by intros; apply partial_alter_merge. Qed.
Lemma merge_singleton i x y z :
f (Some y) (Some z) = Some x merge f {[i,y]} {[i,z]} = {[i,x]}.
f (Some y) (Some z) = Some x merge f {[i y]} {[i z]} = {[i x]}.
Proof.
intros. unfold singleton, map_singleton; simpl.
by erewrite <-insert_merge, merge_empty by eauto.
intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto.
Qed.
Lemma insert_merge_l m1 m2 i x y :
f (Some y) (m2 !! i) = Some x
......@@ -977,23 +975,23 @@ Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
m1 ⊥ₘ m2 m2 !! i = Some x m1 !! i = None.
Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i, x]} ⊥ₘ m m !! i = None.
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[ix]} ⊥ₘ m m !! i = None.
Proof.
split; [|rewrite !map_disjoint_spec].
* intro. apply (map_disjoint_Some_l {[i, x]} _ _ x);
* intro. apply (map_disjoint_Some_l {[i x]} _ _ x);
auto using lookup_singleton.
* intros ? j y1 y2. destruct (decide (i = j)) as [->|].
+ rewrite lookup_singleton. intuition congruence.
+ by rewrite lookup_singleton_ne.
Qed.
Lemma map_disjoint_singleton_r {A} (m : M A) i x :
m ⊥ₘ {[i, x]} m !! i = None.
m ⊥ₘ {[i x]} m !! i = None.
Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_singleton_l. Qed.
Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
m !! i = None {[i, x]} ⊥ₘ m.
m !! i = None {[i x]} ⊥ₘ m.
Proof. by rewrite map_disjoint_singleton_l. Qed.
Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
m !! i = None m ⊥ₘ {[i, x]}.
m !! i = None m ⊥ₘ {[i x]}.
Proof. by rewrite map_disjoint_singleton_r. Qed.
Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ⊥ₘ m2 delete i m1 ⊥ₘ m2.
Proof.
......@@ -1210,7 +1208,7 @@ Proof. by rewrite map_disjoint_union_l. Qed.
Lemma map_disjoint_union_r_2 {A} (m1 m2 m3 : M A) :
m1 ⊥ₘ m2 m1 ⊥ₘ m3 m1 ⊥ₘ m2 m3.
Proof. by rewrite map_disjoint_union_r. Qed.
Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i,x]} m.
Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i x]} m.
Proof.
apply map_eq. intros j. apply option_eq. intros y.
rewrite lookup_union_Some_raw.
......@@ -1219,7 +1217,7 @@ Proof.
* rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence.
Qed.
Lemma insert_union_singleton_r {A} (m : M A) i x :
m !! i = None <[i:=x]>m = m {[i,x]}.
m !! i = None <[i:=x]>m = m {[i x]}.
Proof.
intro. rewrite insert_union_singleton_l, map_union_commutative; [done |].
by apply map_disjoint_singleton_l.
......@@ -1423,15 +1421,15 @@ End theorems.
(** * Tactics *)
(** The tactic [decompose_map_disjoint] simplifies occurrences of [disjoint]
in the hypotheses that involve the empty map [], the union [()] or insert
[<[_:=_]>] operation, the singleton [{[ _ ]}] map, and disjointness of lists of
[<[_:=_]>] operation, the singleton [{[_ _]}] map, and disjointness of lists of
maps. This tactic does not yield any information loss as all simplifications
performed are reversible. *)
Ltac decompose_map_disjoint := repeat
match goal with
| H : _ _ ⊥ₘ _ |- _ => apply map_disjoint_union_l in H; destruct H
| H : _ ⊥ₘ _ _ |- _ => apply map_disjoint_union_r in H; destruct H
| H : {[ _ ]} ⊥ₘ _ |- _ => apply map_disjoint_singleton_l in H
| H : _ ⊥ₘ {[ _ ]} |- _ => apply map_disjoint_singleton_r in H
| H : {[ _ _ ]} ⊥ₘ _ |- _ => apply map_disjoint_singleton_l in H
| H : _ ⊥ₘ {[ _ _ ]} |- _ => apply map_disjoint_singleton_r in H
| H : <[_:=_]>_ ⊥ₘ _ |- _ => apply map_disjoint_insert_l in H; destruct H
| H : _ ⊥ₘ <[_:=_]>_ |- _ => apply map_disjoint_insert_r in H; destruct H
| H : _ ⊥ₘ _ |- _ => apply map_disjoint_union_list_l in H
......@@ -1455,9 +1453,9 @@ Ltac solve_map_disjoint :=
Hint Extern 1 (_ ⊥ₘ _) => done : map_disjoint.
Hint Extern 2 ( ⊥ₘ _) => apply map_disjoint_empty_l : map_disjoint.
Hint Extern 2 (_ ⊥ₘ ) => apply map_disjoint_empty_r : map_disjoint.
Hint Extern 2 ({[ _ ]} ⊥ₘ _) =>
Hint Extern 2 ({[ _ _ ]} ⊥ₘ _) =>
apply map_disjoint_singleton_l_2 : map_disjoint.
Hint Extern 2 (_ ⊥ₘ {[ _ ]}) =>
Hint Extern 2 (_ ⊥ₘ {[ _ _ ]}) =>
apply map_disjoint_singleton_r_2 : map_disjoint.
Hint Extern 2 (_ _ ⊥ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
Hint Extern 2 (_ ⊥ₘ _ _) => apply map_disjoint_union_r_2 : map_disjoint.
......@@ -1489,7 +1487,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
rewrite lookup_alter in H || rewrite lookup_alter_ne in H by tac
| H : context[ (delete _ _) !! _] |- _ =>
rewrite lookup_delete in H || rewrite lookup_delete_ne in H by tac
| H : context[ {[ _ ]} !! _ ] |- _ =>
| H : context[ {[ _ _ ]} !! _ ] |- _ =>
rewrite lookup_singleton in H || rewrite lookup_singleton_ne in H by tac
| H : context[ (_ <$> _) !! _ ] |- _ => rewrite lookup_fmap in H
| H : context[ (omap _ _) !! _ ] |- _ => rewrite lookup_omap in H
......@@ -1506,7 +1504,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
rewrite lookup_alter || rewrite lookup_alter_ne by tac
| |- context[ (delete _ _) !! _ ] =>
rewrite lookup_delete || rewrite lookup_delete_ne by tac
| |- context[ {[ _ ]} !! _ ] =>
| |- context[ {[ _ _ ]} !! _ ] =>
rewrite lookup_singleton || rewrite lookup_singleton_ne by tac
| |- context[ (_ <$> _) !! _ ] => rewrite lookup_fmap
| |- context[ (omap _ _) !! _ ] => rewrite lookup_omap
......@@ -1523,7 +1521,7 @@ Tactic Notation "simpl_map" := simpl_map by eauto with simpl_map map_disjoint.
Hint Extern 80 ((_ _) !! _ = Some _) => apply lookup_union_Some_l : simpl_map.
Hint Extern 81 ((_ _) !! _ = Some _) => apply lookup_union_Some_r : simpl_map.
Hint Extern 80 ({[ _ ]} !! _ = Some _) => apply lookup_singleton : simpl_map.
Hint Extern 80 ({[ __ ]} !! _ = Some _) => apply lookup_singleton : simpl_map.
Hint Extern 80 (<[_:=_]> _ !! _ = Some _) => apply lookup_insert : simpl_map.
(** Now we take everything together and also discharge conflicting look ups,
......@@ -1535,8 +1533,8 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
| _ => progress simpl_map by tac
| _ => progress simplify_equality
| _ => progress simpl_option_monad by tac
| H : {[ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
| H : {[ _ ]} !! _ = Some _ |- _ =>
| H : {[ _ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
| H : {[ _ _ ]} !! _ = Some _ |- _ =>
rewrite lookup_singleton_Some in H; destruct H
| H1 : ?m1 !! ?i = Some ?x, H2 : ?m2 !! ?i = Some ?y |- _ =>
let H3 := fresh in
......@@ -1549,8 +1547,8 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
apply map_union_cancel_l in H; [|by tac|by tac]
| H : _ ?m = _ ?m |- _ =>
apply map_union_cancel_r in H; [|by tac|by tac]
| H : {[?i,?x]} = |- _ => by destruct (map_non_empty_singleton i x)
| H : = {[?i,?x]} |- _ => by destruct (map_non_empty_singleton i x)
| H : {[?i ?x]} = |- _ => by destruct (map_non_empty_singleton i x)
| H : = {[?i ?x]} |- _ => by destruct (map_non_empty_singleton i x)
| H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ =>
unless (i j) by done;
assert (i j) by (by intros ?; simplify_equality)
......
......@@ -23,7 +23,7 @@ Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
Program Instance hashset_empty: Empty (hashset hash) := Hashset _.
Next Obligation. by intros n X; simpl_map. Qed.
Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
Hashset {[ hash x, [x] ]} _.
Hashset {[ hash x [x] ]} _.
Next Obligation.
intros n l. rewrite lookup_singleton_Some. intros [<- <-].
rewrite Forall_singleton; auto using NoDup_singleton.
......
......@@ -17,7 +17,7 @@ Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
mapset_car X !! x = Some ().
Instance mapset_empty: Empty (mapset M) := Mapset .
Instance mapset_singleton: Singleton K (mapset M) := λ x,
Mapset {[ (x,()) ]}.
Mapset {[ x () ]}.
Instance mapset_union: Union (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2).
Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment