Commit d60affc0 authored by Robbert Krebbers's avatar Robbert Krebbers

Preparation to port the master branch

Major changes:
* A data structure to collect locked addresses in memory.
* Operations to lock and unlock addresses.
* Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This
  saves a lot of lines of code.
* Add a [void] value. This value cannot be typed, but will be used as a dummy
  return value for functions with return type [void].

Minor changes:
* Various deciders in preparation of the executable semantics.
* Improve naming and notations.
* Remove obsolete stuff.
parent 46799584
......@@ -9,11 +9,6 @@ Global Set Automatic Coercions Import.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
(** * General *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
Notation "(&&)" := andb (only parsing).
Notation "(||)" := orb (only parsing).
(** Zipping lists. *)
Definition zip_with {A B C} (f : A B C) : list A list B list C :=
fix go l1 l2 :=
......@@ -500,14 +495,6 @@ Class Merge (M : Type → Type) :=
Instance: Params (@merge) 4.
Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
(** We lift the insert and delete operation to lists of elements. *)
Definition insert_list `{Insert K A M} (l : list (K * A)) (m : M) : M :=
fold_right (λ p, <[p.1:=p.2]>) m l.
Instance: Params (@insert_list) 4.
Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
fold_right delete m l.
Instance: Params (@delete_list) 3.
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
and [m2] using the function [f] to combine values of members that are in
both [m1] and [m2]. *)
......@@ -724,8 +711,8 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C,
Elements A C, x y : A, Decision (x = y)} : Prop := {
fin_collection :>> Collection A C;
elements_spec X x : x X x elements X;
elements_nodup X : NoDup (elements X)
elem_of_elements X x : x elements X x X;
NoDup_elements X : NoDup (elements X)
}.
Class Size C := size: C nat.
Arguments size {_ _} !_ / : simpl nomatch.
......@@ -763,6 +750,20 @@ Class FreshSpec A C `{ElemOf A C,
is_fresh (X : C) : fresh X X
}.
(** * Booleans *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
Notation "(&&)" := andb (only parsing).
Notation "(||)" := orb (only parsing).
Infix "&&*" := (zip_with (&&)) (at level 40).
Infix "||*" := (zip_with (||)) (at level 50).
Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
Infix "=.>" := bool_le (at level 70).
Infix "=.>*" := (Forall2 bool_le) (at level 70).
Instance: PartialOrder bool_le.
Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
(** * Miscellaneous *)
Class Half A := half: A A.
Notation "½" := half : C_scope.
......@@ -823,14 +824,6 @@ Section prod_relation.
End prod_relation.
(** ** Other *)
Definition proj_eq {A B} (f : B A) : relation B := λ x y, f x = f y.
Global Instance proj_eq_equivalence `(f : B A) : Equivalence (proj_eq f).
Proof. unfold proj_eq. repeat split; red; intuition congruence. Qed.
Notation "x ~{ f } y" := (proj_eq f x y)
(at level 70, format "x ~{ f } y") : C_scope.
Hint Extern 0 (_ ~{_} _) => reflexivity.
Hint Extern 0 (_ ~{_} _) => symmetry; assumption.
Instance: A B (x : B), Commutative (=) (λ _ _ : A, x).
Proof. red. trivial. Qed.
Instance: A (x : A), Associative (=) (λ _ _ : A, x).
......
......@@ -18,10 +18,8 @@ Section simple_collection.
Proof. intros. apply elem_of_union. auto. Qed.
Lemma elem_of_union_r x X Y : x Y x X Y.
Proof. intros. apply elem_of_union. auto. Qed.
Global Instance: BoundedJoinSemiLattice C.
Proof. firstorder auto. Qed.
Lemma elem_of_subseteq X Y : X Y x, x X x Y.
Proof. done. Qed.
Lemma elem_of_equiv X Y : X Y x, x X x Y.
......@@ -31,7 +29,12 @@ Section simple_collection.
Proof. firstorder. Qed.
Lemma elem_of_equiv_empty X : X x, x X.
Proof. firstorder. Qed.
Lemma collection_positive_l X Y : X Y X .
Proof.
rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
Qed.
Lemma collection_positive_l_alt X Y : X X Y .
Proof. eauto using collection_positive_l. Qed.
Lemma elem_of_subseteq_singleton x X : x X {[ x ]} X.
Proof.
split.
......@@ -42,7 +45,6 @@ Section simple_collection.
Proof. by repeat intro; subst. Qed.
Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) () | 5.
Proof. intros ???; subst. firstorder. Qed.
Lemma elem_of_union_list Xs x : x Xs X, X Xs x X.
Proof.
split.
......@@ -51,7 +53,6 @@ Section simple_collection.
* intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
intros. apply elem_of_union_r; auto.
Qed.
Lemma non_empty_singleton x : {[ x ]} .
Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
Lemma not_elem_of_singleton x y : x {[ y ]} x y.
......@@ -68,6 +69,10 @@ Section simple_collection.
Proof. unfold_leibniz. apply elem_of_equiv_alt. Qed.
Lemma elem_of_equiv_empty_L X : X = x, x X.
Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
Lemma collection_positive_l_L X Y : X Y = X = .
Proof. unfold_leibniz. apply collection_positive_l. Qed.
Lemma collection_positive_l_alt_L X Y : X X Y .
Proof. unfold_leibniz. apply collection_positive_l_alt. Qed.
Lemma non_empty_singleton_L x : {[ x ]} .
Proof. unfold_leibniz. apply non_empty_singleton. Qed.
End leibniz.
......@@ -385,7 +390,7 @@ Section quantifiers.
End quantifiers.
Section more_quantifiers.
Context `{Collection A B}.
Context `{SimpleCollection A B}.
Lemma set_Forall_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
set_Forall P X set_Forall Q X.
......
......@@ -6,8 +6,6 @@ principles on finite collections . *)
Require Import Permutation ars listset.
Require Export numbers collections.
Definition collection_choose `{Elements A C} (X : C) : option A :=
head (elements X).
Instance collection_size `{Elements A C} : Size C := length elements.
Definition collection_fold `{Elements A C} {B}
(f : A B B) (b : B) : C B := foldr f b elements.
......@@ -18,76 +16,56 @@ Context `{FinCollection A C}.
Global Instance elements_proper: Proper (() ==> ()) elements.
Proof.
intros ?? E. apply NoDup_Permutation.
* apply elements_nodup.
* apply elements_nodup.
* intros. by rewrite <-!elements_spec, E.
* apply NoDup_elements.
* apply NoDup_elements.
* intros. by rewrite !elem_of_elements, E.
Qed.
Global Instance collection_size_proper: Proper (() ==> (=)) size.
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
Lemma size_empty : size ( : C) = 0.
Proof.
unfold size, collection_size. simpl.
rewrite (elem_of_nil_inv (elements )); [done |].
intro. rewrite <-elements_spec. solve_elem_of.
intro. rewrite elem_of_elements. solve_elem_of.
Qed.
Lemma size_empty_inv (X : C) : size X = 0 X .
Proof.
intros. apply equiv_empty. intro. rewrite elements_spec.
intros. apply equiv_empty. intro. rewrite <-elem_of_elements.
rewrite (nil_length_inv (elements X)). by rewrite elem_of_nil. done.
Qed.
Lemma size_empty_iff (X : C) : size X = 0 X .
Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
Lemma size_non_empty_iff (X : C) : size X 0 X .
Proof. by rewrite size_empty_iff. Qed.
Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof.
change (length (elements {[ x ]}) = length [x]).
apply Permutation_length, NoDup_Permutation.
* apply elements_nodup.
* apply NoDup_elements.
* apply NoDup_singleton.
* intros.
by rewrite <-elements_spec, elem_of_singleton, elem_of_list_singleton.
* intros. by rewrite elem_of_elements,
elem_of_singleton, elem_of_list_singleton.
Qed.
Lemma size_singleton_inv X x y : size X = 1 x X y X x = y.
Proof.
unfold size, collection_size. simpl. rewrite !elements_spec.
unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
generalize (elements X). intros [|? l]; intro; simplify_equality.
rewrite (nil_length_inv l), !elem_of_list_singleton by done. congruence.
Qed.
Lemma collection_choose_Some X x : collection_choose X = Some x x X.
Proof.
unfold collection_choose. destruct (elements X) eqn:E; intros;
simplify_equality. rewrite elements_spec, E. by left.
Qed.
Lemma collection_choose_None X : collection_choose X = None X .
Proof.
unfold collection_choose.
destruct (elements X) eqn:E; intros; simplify_equality.
apply equiv_empty. intros x. by rewrite elements_spec, E, elem_of_nil.
Qed.
Lemma elem_of_or_empty X : ( x, x X) X .
Proof.
destruct (collection_choose X) eqn:?;
eauto using collection_choose_Some, collection_choose_None.
Qed.
Lemma collection_choose_is_Some X : X is_Some (collection_choose X).
Proof.
destruct (collection_choose X) eqn:?.
* rewrite elem_of_equiv_empty. split; eauto using collection_choose_Some.
* split. intros []; eauto using collection_choose_None. by intros [??].
Qed.
Lemma not_elem_of_equiv_empty X : X ( x, x X).
Lemma collection_choose_or_empty X : ( x, x X) X .
Proof.
destruct (elem_of_or_empty X) as [?|E]; [esolve_elem_of |].
setoid_rewrite E. setoid_rewrite elem_of_empty. naive_solver.
destruct (elements X) as [|x l] eqn:HX; [right|left].
* apply equiv_empty. intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
* exists x. rewrite <-elem_of_elements, HX. by left.
Qed.
Lemma collection_choose X : X x, x X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
Lemma collection_choose_L `{!LeibnizEquiv C} X : X x, x X.
Proof. unfold_leibniz. apply collection_choose. Qed.
Lemma size_pos_elem_of X : 0 < size X x, x X.
Proof.
intros E1. apply not_elem_of_equiv_empty. intros E2.
rewrite E2, size_empty in E1. lia.
intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
contradict Hsz. rewrite HX, size_empty; lia.
Qed.
Lemma size_1_elem_of X : size X = 1 x, X {[ x ]}.
Proof.
......@@ -96,27 +74,24 @@ Proof.
* rewrite elem_of_singleton. eauto using size_singleton_inv.
* solve_elem_of.
Qed.
Lemma size_union X Y : X Y size (X Y) = size X + size Y.
Proof.
intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
* apply elements_nodup.
* apply NoDup_app; repeat split; try apply elements_nodup.
intros x. rewrite <-!elements_spec. esolve_elem_of.
* intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of.
* apply NoDup_elements.
* apply NoDup_app; repeat split; try apply NoDup_elements.
intros x. rewrite !elem_of_elements. esolve_elem_of.
* intros. rewrite elem_of_app, !elem_of_elements. solve_elem_of.
Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x X) | 100.
Proof.
refine (cast_if (decide_rel () x (elements X)));
by rewrite (elements_spec _).
by rewrite <-(elem_of_elements _).
Defined.
Global Program Instance collection_subseteq_dec_slow (X Y : C) :
Decision (X Y) | 100 :=
match decide_rel (=) (size (X Y)) 0 with
| left E1 => left _
| right E1 => right _
| left E1 => left _ | right E1 => right _
end.
Next Obligation.
intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
......@@ -126,14 +101,12 @@ Next Obligation.
intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
Qed.
Lemma size_union_alt X Y : size (X Y) = size X + size (Y X).
Proof.
rewrite <-size_union by solve_elem_of.
setoid_replace (Y X) with ((Y X) X) by esolve_elem_of.
rewrite <-union_difference, (commutative ()); solve_elem_of.
Qed.
Lemma subseteq_size X Y : X Y size X size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X Y size X < size Y.
......@@ -143,22 +116,19 @@ Proof.
cut (size (Y X) 0); [lia |].
by apply size_non_empty_iff, non_empty_difference.
Qed.
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C Prop) :
Proper (() ==> iff) P
P ( x X, x X P X P ({[ x ]} X)) X, P X.
Proof.
intros ? Hemp Hadd. apply well_founded_induction with ().
{ apply collection_wf. }
intros X IH. destruct (elem_of_or_empty X) as [[x ?]|HX].
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
* rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
* by rewrite HX.
Qed.
Lemma collection_fold_ind {B} (P : B C Prop) (f : A B B) (b : B) :
Proper ((=) ==> () ==> iff) P
P b ( x X r, x X P r X P (f x r) ({[ x ]} X))
......@@ -166,7 +136,8 @@ Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B)
Proof.
intros ? Hemp Hadd.
cut ( l, NoDup l X, ( x, x X x l) P (foldr f b l) X).
{ intros help ?. apply help. apply elements_nodup. apply elements_spec. }
{ intros help ?. apply help; [apply NoDup_elements|].
symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl.
* intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. esolve_elem_of.
......@@ -174,25 +145,23 @@ Proof.
rewrite (union_difference {[ x ]} X) by esolve_elem_of.
apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper (() ==> R) (collection_fold f b).
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
Global Instance set_Forall_dec `(P : A Prop)
`{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
Proof.
refine (cast_if (decide (Forall P (elements X))));
abstract (unfold set_Forall; setoid_rewrite elements_spec;
abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
by rewrite <-Forall_forall).
Defined.
Global Instance set_Exists_dec `(P : A Prop) `{ x, Decision (P x)} X :
Decision (set_Exists P X) | 100.
Proof.
refine (cast_if (decide (Exists P (elements X))));
abstract (unfold set_Exists; setoid_rewrite elements_spec;
abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
by rewrite <-Exists_exists).
Defined.
Global Instance rel_elem_of_dec `{ x y, Decision (R x y)} x X :
......
......@@ -35,7 +35,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
lookup_partial_alter_ne {A} f (m : M A) i j :
i j partial_alter f i m !! j = m !! j;
lookup_fmap {A B} (f : A B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
map_to_list_nodup {A} (m : M A) : NoDup (map_to_list m);
NoDup_map_to_list {A} (m : M A) : NoDup (map_to_list m);
elem_of_map_to_list {A} (m : M A) i x :
(i,x) map_to_list m m !! i = Some x;
lookup_omap {A B} (f : A option B) m i : omap f m !! i = m !! i = f;
......@@ -58,8 +58,8 @@ Instance map_delete `{PartialAlter K A M} : Delete K M :=
Instance map_singleton `{PartialAlter K A M, Empty M} :
Singleton (K * A) M := λ p, <[p.1:=p.2]> .
Definition map_of_list `{Insert K A M} `{Empty M}
(l : list (K * A)) : M := insert_list l .
Definition map_of_list `{Insert K A M} `{Empty M} : list (K * A) M :=
fold_right (λ p, <[p.1:=p.2]>) .
Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
λ f, merge (union_with f).
......@@ -81,11 +81,7 @@ Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
| None, Some y => Q y
| None, None => True
end.
(*
Definition map_intersection_Forall `{Lookup K A M}
(R : relation A) : relation M := λ m1 m2,
∀ i x1 x2, m1 !! i = Some x1 → m2 !! i = Some x2 → R x1 x2.
*)
Instance map_disjoint `{ A, Lookup K A (M A)} {A} : Disjoint (M A) :=
map_Forall2 (λ _ _, False) (λ _, True) (λ _, True).
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
......@@ -396,7 +392,7 @@ 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.
Proof. by rewrite lookup_singleton_None. Qed.
Lemma singleton_ne_empty {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.
......@@ -429,8 +425,8 @@ Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma map_to_list_unique {A} (m : M A) i x y :
(i,x) map_to_list m (i,y) map_to_list m x = y.
Proof. rewrite !elem_of_map_to_list. congruence. Qed.
Lemma map_to_list_key_nodup {A} (m : M A) : NoDup (fst <$> map_to_list m).
Proof. eauto using NoDup_fmap_fst, map_to_list_unique, map_to_list_nodup. Qed.
Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup (fst <$> map_to_list m).
Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
NoDup (fst <$> l) (i,x) l map_of_list l !! i = Some x.
Proof.
......@@ -477,23 +473,23 @@ Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
NoDup (fst <$> l1) NoDup (fst <$> l2)
map_of_list l1 = map_of_list l2 l1 l2.
Proof.
intros ?? Hl1l2. apply NoDup_Permutation; auto using (fmap_nodup_1 fst).
intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
Qed.
Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.
Proof.
apply map_eq. intros i. apply option_eq. intros x.
by rewrite <-elem_of_map_of_list, elem_of_map_to_list
by auto using map_to_list_key_nodup.
by auto using NoDup_fst_map_to_list.
Qed.
Lemma map_to_of_list {A} (l : list (K * A)) :
NoDup (fst <$> l) map_to_list (map_of_list l) l.
Proof. auto using map_of_list_inj, map_to_list_key_nodup, map_of_to_list. Qed.
Proof. auto using map_of_list_inj, NoDup_fst_map_to_list, map_of_to_list. Qed.
Lemma map_to_list_inj {A} (m1 m2 : M A) :
map_to_list m1 map_to_list m2 m1 = m2.
Proof.
intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
auto using map_of_list_proper, map_to_list_key_nodup.
auto using map_of_list_proper, NoDup_fst_map_to_list.
Qed.
Lemma map_to_list_empty {A} : map_to_list = @nil (K * A).
Proof.
......@@ -504,8 +500,8 @@ Lemma map_to_list_insert {A} (m : M A) i x :
m !! i = None map_to_list (<[i:=x]>m) (i,x) :: map_to_list m.
Proof.
intros. apply map_of_list_inj; simpl.
* apply map_to_list_key_nodup.
* constructor; auto using map_to_list_key_nodup.
* apply NoDup_fst_map_to_list.
* constructor; auto using NoDup_fst_map_to_list.
rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
rewrite elem_of_map_to_list in Hlookup. congruence.
* by rewrite !map_of_to_list.
......@@ -524,11 +520,17 @@ Lemma map_to_list_insert_inv {A} (m : M A) l i x :
Proof.
intros Hperm. apply map_to_list_inj.
assert (NoDup (fst <$> (i, x) :: l)) as Hnodup.
{ rewrite <-Hperm. auto using map_to_list_key_nodup. }
{ rewrite <-Hperm. auto using NoDup_fst_map_to_list. }
simpl in Hnodup. rewrite NoDup_cons in Hnodup. destruct Hnodup.
rewrite Hperm, map_to_list_insert, map_to_of_list;
auto using not_elem_of_map_of_list_1.
Qed.
Lemma map_choose {A} (m : M A) : m i x, m !! i = Some x.
Proof.
intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm.
{ destruct Hemp; eauto using map_to_list_empty_inv. }
exists i x. rewrite <-elem_of_map_to_list, Hm. by left.
Qed.
(** * Induction principles *)
Lemma map_ind {A} (P : M A Prop) :
......@@ -536,7 +538,7 @@ Lemma map_ind {A} (P : M A → Prop) :
Proof.
intros ? Hins. cut ( l, NoDup (fst <$> l) m, map_to_list m l P m).
{ intros help m.
apply (help (map_to_list m)); auto using map_to_list_key_nodup. }
apply (help (map_to_list m)); auto using NoDup_fst_map_to_list. }
induction l as [|[i x] l IH]; intros Hnodup m Hml.
{ apply map_to_list_empty_inv_alt in Hml. by subst. }
inversion_clear Hnodup.
......@@ -745,7 +747,7 @@ Lemma map_not_disjoint {A} (m1 m2 : M A) :
Proof.
unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
split; [|naive_solver].
* intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
Qed.
Global Instance: Symmetric (@disjoint (M A) _).
Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
......@@ -801,6 +803,15 @@ Context {A} (f : A → A → option A).
Lemma lookup_union_with m1 m2 i :
union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
Proof. by rewrite <-(lookup_merge _). Qed.
Lemma lookup_union_with_Some m1 m2 i z :
union_with f m1 m2 !! i = Some z
(m1 !! i = Some z m2 !! i = None)
(m1 !! i = None m2 !! i = Some z)
( x y, m1 !! i = Some x m2 !! i = Some y f x y = Some z).
Proof.
rewrite lookup_union_with.
destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
Global Instance: LeftId (@eq (M A)) (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.
Global Instance: RightId (@eq (M A)) (union_with f).
......@@ -847,9 +858,9 @@ Qed.
Lemma delete_union_with m1 m2 i :
delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
Proof. by apply (partial_alter_merge _). Qed.
Lemma delete_list_union_with (m1 m2 : M A) is :
delete_list is (union_with f m1 m2) =
union_with f (delete_list is m1) (delete_list is m2).
Lemma foldr_delete_union_with (m1 m2 : M A) is :
foldr delete (union_with f m1 m2) is =
union_with f (foldr delete m1 is) (foldr delete m2 is).
Proof. induction is; simpl. done. by rewrite IHis, delete_union_with. Qed.
Lemma insert_union_with m1 m2 i x :
( x, f x x = Some x)
......@@ -880,7 +891,6 @@ Proof.
Qed.
Global Instance: Idempotent (@eq (M A)) ().
Proof. intros A ?. by apply union_with_idempotent. Qed.
Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
(m1 m2) !! i = Some x
m1 !! i = Some x (m1 !! i = None m2 !! i = Some x).
......@@ -894,6 +904,13 @@ Proof.
unfold union, map_union, union_with, map_union_with. rewrite (lookup_merge _).
destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed.
Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = .
Proof.
intros Hm. apply map_empty. intros i. apply (f_equal (!! i)) in Hm.
rewrite lookup_empty, lookup_union_None in Hm; tauto.
Qed.
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 .
Proof. eauto using map_positive_l. Qed.
Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
m1 m2 (m1 m2) !! i = Some x m1 !! i = Some x m2 !! i = Some x.
Proof.
......@@ -1028,11 +1045,11 @@ Proof.
rewrite (map_union_commutative m1); [done |].
by apply map_disjoint_singleton_r.
Qed.
Lemma insert_list_union {A} (m : M A) l : insert_list l m = map_of_list l m.
Lemma foldr_insert_union {A} (m : M A) l :
foldr (λ p, <[p.1:=p.2]>) m l = map_of_list l m.
Proof.
induction l; simpl.
* by rewrite (left_id_L _ _).
* by rewrite IHl, insert_union_l.
induction l as [|i l IH]; simpl; [by rewrite (left_id_L _ _)|].
by rewrite IH, insert_union_l.
Qed.
Lemma delete_union {A} (m1 m2 : M A) i :
delete i (m1 m2) = delete i m1 delete i m2.
......@@ -1066,47 +1083,38 @@ Proof.
* apply map_union_preserving_l; auto.
Qed.
(** ** Properties of the [intersection] operation *)
Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
(m1 m2) !! i = Some x m1 !! i = Some x is_Some (m2 !! i).
Proof.
unfold intersection, map_intersection, intersection_with,
map_intersection_with. rewrite (lookup_merge _).
destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
(** ** Properties of the [delete_list] function *)
Lemma lookup_delete_list {A} (m : M A) is j :
j is delete_list is m !! j = None.
(** ** Properties of the folding the [delete] function *)
Lemma lookup_foldr_delete {A} (m : M A) is j :
j is foldr delete m is !! j = None.
Proof.
induction 1 as [|i j is]; simpl; [by rewrite lookup_delete|].
by destruct (decide (i = j)) as [->|?];
rewrite ?lookup_delete, ?lookup_delete_ne by done.
Qed.
Lemma lookup_delete_list_not_elem_of {A} (m : M A) is j :
j is delete_list is m !! j = m !! j.
Lemma lookup_foldr_delete_not_elem_of {A} (m : M A) is j :
j is foldr delete m is !! j = m !! j.
Proof.
induction is; simpl; [done |]. rewrite elem_of_cons; intros.
rewrite lookup_delete_ne; intuition.
Qed.
Lemma delete_list_notin {A} (m : M A) is :
Forall (λ i, m !! i = None) is delete_list is m = m.
Lemma foldr_delete_notin {A} (m : M A) is :
Forall (λ i, m !! i = None) is foldr delete m is = m.
Proof. induction 1; simpl; [done |]. rewrite delete_notin; congruence. Qed.
Lemma delete_list_insert_ne {A} (m : M A) is j x :
j is delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
Lemma foldr_delete_insert_ne {A} (m : M A) is j x :
j is foldr delete (<[j:=x]>m) is = <[j:=x]>(foldr delete m is).
Proof.
induction is; simpl; [done |]. rewrite elem_of_cons. intros.
rewrite IHis, delete_insert_ne; intuition.
Qed.
Lemma map_disjoint_delete_list_l {A} (m1 m2 : M A) is :
m1 m2 delete_list is m1 m2.
Lemma map_disjoint_foldr_delete_l {A} (m1 m2 : M A) is :
m1 m2 foldr delete m1 is m2.
Proof. induction is; simpl; auto using map_disjoint_delete_l. Qed.
Lemma map_disjoint_delete_list_r {A} (m1 m2 : M A) is :
m1 m2 m1 delete_list is m2.
Lemma map_disjoint_foldr_delete_r {A} (m1 m2 : M A) is :
m1 m2 m1 foldr delete m2 is.
Proof. induction is; simpl; auto using map_disjoint_delete_r. Qed.
Lemma delete_list_union {A} (m1 m2 : M A) is :
delete_list is (m1 m2) = delete_list is m1 delete_list is m2.
Proof. apply delete_list_union_with. Qed.
Lemma foldr_delete_union {A} (m1 m2 : M A) is :
foldr delete (m1 m2) is = foldr delete m1 is foldr delete m2 is.
Proof. apply foldr_delete_union_with. Qed.
(** ** Properties on disjointness of conversion to lists *)
Lemma map_disjoint_of_list_l {A} (m : M A) ixs :
......@@ -1144,9 +1152,8 @@ Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed.
Lemma union_delete_vec {A n} (ms : vec (M A) n) (i : fin n) :
ms ms !!! i delete (fin_to_nat i) (vec_to_list ms) = ms.