From 415a4f1ca2bf510240bb6a2ec0366a04b17be36f Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 19 Feb 2013 13:32:10 +0100 Subject: [PATCH] Support sequence point, add permissions, and update prelude. Both the operational and axiomatic semantics are extended with sequence points and a permission system based on fractional permissions. In order to achieve this, the memory model has been completely revised, and is now built on top of an abstract interface for permissions. Apart from these changed, the library on lists and sets has been heavily extended, and minor changed have been made to other parts of the prelude. --- theories/ars.v | 2 +- theories/base.v | 163 ++- theories/collections.v | 224 ++- theories/decidable.v | 40 +- theories/fin_collections.v | 2 +- theories/fin_map_dom.v | 142 ++ theories/fin_maps.v | 2712 ++++++++++++++++++++---------------- theories/fresh_numbers.v | 2 +- theories/list.v | 328 ++++- theories/listset.v | 14 +- theories/listset_nodup.v | 22 +- theories/mapset.v | 151 ++ theories/nmap.v | 28 +- theories/numbers.v | 128 +- theories/option.v | 50 +- theories/orders.v | 277 +++- theories/pmap.v | 135 +- theories/prelude.v | 2 +- theories/tactics.v | 176 ++- theories/vector.v | 30 +- 20 files changed, 3035 insertions(+), 1593 deletions(-) create mode 100644 theories/fin_map_dom.v create mode 100644 theories/mapset.v diff --git a/theories/ars.v b/theories/ars.v index 57004f7e..dd3484a4 100644 --- a/theories/ars.v +++ b/theories/ars.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects definitions and theorems on abstract rewriting systems. These are particularly useful as we define the operational semantics as a diff --git a/theories/base.v b/theories/base.v index b6bf6540..709d29b5 100644 --- a/theories/base.v +++ b/theories/base.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects type class interfaces, notations, and general theorems that are used throughout the whole development. Most importantly it contains @@ -133,6 +133,27 @@ Notation "x ≢ y":= (¬x ≡ y) (at level 70, no associativity) : C_scope. Notation "( x ≢)" := (λ y, x ≢ y) (only parsing) : C_scope. Notation "(≢ x )" := (λ y, y ≢ x) (only parsing) : C_scope. +(** The type class [LeibnizEquiv] collects setoid equalities that coincide +with Leibniz equality. We provide the tactic [fold_leibniz] to transform such +setoid equalities into Leibniz equalities, and [unfold_leibniz] for the +reverse. *) +Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y ↔ x = y. + +Ltac fold_leibniz := repeat + match goal with + | H : context [ @equiv ?A _ _ _ ] |- _ => + setoid_rewrite (leibniz_equiv (A:=A)) in H + | |- context [ @equiv ?A _ _ _ ] => + setoid_rewrite (leibniz_equiv (A:=A)) + end. +Ltac unfold_leibniz := repeat + match goal with + | H : context [ @eq ?A _ _ ] |- _ => + setoid_rewrite <-(leibniz_equiv (A:=A)) in H + | |- context [ @eq ?A _ _ ] => + setoid_rewrite <-(leibniz_equiv (A:=A)) + end. + (** A [Params f n] instance forces the setoid rewriting mechanism not to rewrite in the first [n] arguments of the function [f]. We will declare such instances for all operational type classes in this development. *) @@ -227,23 +248,22 @@ Notation "(⊥)" := disjoint (only parsing) : C_scope. Notation "( X ⊥)" := (disjoint X) (only parsing) : C_scope. Notation "(⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope. -Inductive list_disjoint `{Disjoint A} : list A → Prop := +Inductive list_disjoint `{Empty A} `{Union A} + `{Disjoint A} : list A → Prop := | disjoint_nil : list_disjoint [] | disjoint_cons X Xs : - Forall (⊥ X) Xs → + X ⊥ ⋃ Xs → list_disjoint Xs → list_disjoint (X :: Xs). -Lemma list_disjoint_cons_inv `{Disjoint A} X Xs : +Lemma list_disjoint_cons_inv `{Empty A} `{Union A} `{Disjoint A} X Xs : list_disjoint (X :: Xs) → - Forall (⊥ X) Xs ∧ list_disjoint Xs. + X ⊥ ⋃ Xs ∧ list_disjoint Xs. Proof. inversion_clear 1; auto. Qed. -Instance generic_disjoint `{ElemOf A B} : Disjoint B | 100 := - λ X Y, ∀ x, x ∉ X ∨ x ∉ Y. - Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B. + (* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *) (** ** Monadic operations *) @@ -347,18 +367,16 @@ Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch. (** The function [dom C m] should yield the domain of [m]. That is a finite collection of type [C] that contains the keys that are a member of [m]. *) -Class Dom (K M : Type) := - dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C. -Instance: Params (@dom) 7. -Arguments dom _ _ _ _ _ _ _ !_ / : simpl nomatch. +Class Dom (M C : Type) := dom: M → C. +Instance: Params (@dom) 3. +Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits. (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by -constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)] -provided that [k] is a member of either [m1] or [m2].*) -Class Merge (A M : Type) := - merge: (option A → option A → option A) → M → M → M. -Instance: Params (@merge) 3. -Arguments merge _ _ _ _ !_ !_ / : simpl nomatch. +constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*) +Class Merge (M : Type → Type) := + merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C. +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 := @@ -379,14 +397,18 @@ both [m1] and [m2]. *) Class UnionWith (A M : Type) := union_with: (A → A → option A) → M → M → M. Instance: Params (@union_with) 3. +Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch. (** Similarly for intersection and difference. *) Class IntersectionWith (A M : Type) := intersection_with: (A → A → option A) → M → M → M. Instance: Params (@intersection_with) 3. +Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch. + Class DifferenceWith (A M : Type) := difference_with: (A → A → option A) → M → M → M. Instance: Params (@difference_with) 3. +Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch. Definition intersection_with_list `{IntersectionWith A M} (f : A → A → option A) : M → list M → M := fold_right (intersection_with f). @@ -396,25 +418,30 @@ Arguments intersection_with_list _ _ _ _ _ !_ /. (** These operational type classes allow us to refer to common mathematical properties in a generic way. For example, for injectivity of [(k ++)] it allows us to write [injective (k ++)] instead of [app_inv_head k]. *) -Class Injective {A B} R S (f : A → B) := +Class Injective {A B} (R : relation A) S (f : A → B) : Prop := injective: ∀ x y : A, S (f x) (f y) → R x y. -Class Idempotent {A} R (f : A → A → A) := +Class Idempotent {A} (R : relation A) (f : A → A → A) : Prop := idempotent: ∀ x, R (f x x) x. -Class Commutative {A B} R (f : B → B → A) := +Class Commutative {A B} (R : relation A) (f : B → B → A) : Prop := commutative: ∀ x y, R (f x y) (f y x). -Class LeftId {A} R (i : A) (f : A → A → A) := +Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop := left_id: ∀ x, R (f i x) x. -Class RightId {A} R (i : A) (f : A → A → A) := +Class RightId {A} (R : relation A) (i : A) (f : A → A → A) : Prop := right_id: ∀ x, R (f x i) x. -Class Associative {A} R (f : A → A → A) := +Class Associative {A} (R : relation A) (f : A → A → A) : Prop := associative: ∀ x y z, R (f x (f y z)) (f (f x y) z). -Class LeftAbsorb {A} R (i : A) (f : A → A → A) := +Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := left_absorb: ∀ x, R (f i x) i. -Class RightAbsorb {A} R (i : A) (f : A → A → A) := +Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := right_absorb: ∀ x, R (f x i) i. -Class AntiSymmetric {A} (R : A → A → Prop) := +Class LeftDistr {A} (R : relation A) (f g : A → A → A) : Prop := + left_distr: ∀ x y z, R (f x (g y z)) (g (f x y) (f x z)). +Class RightDistr {A} (R : relation A) (f g : A → A → A) : Prop := + right_distr: ∀ y z x, R (f (g y z) x) (g (f y x) (f z x)). +Class AntiSymmetric {A} (R : relation A) : Prop := anti_symmetric: ∀ x y, R x y → R y x → x = y. +Arguments irreflexivity {_} _ {_} _ _. Arguments injective {_ _ _ _} _ {_} _ _ _. Arguments idempotent {_ _} _ {_} _. Arguments commutative {_ _ _} _ {_} _ _. @@ -423,6 +450,8 @@ Arguments right_id {_ _} _ _ {_} _. Arguments associative {_ _} _ {_} _ _ _. Arguments left_absorb {_ _} _ _ {_} _. Arguments right_absorb {_ _} _ _ {_} _. +Arguments left_distr {_ _} _ _ {_} _ _ _. +Arguments right_distr {_ _} _ _ {_} _ _ _. Arguments anti_symmetric {_} _ {_} _ _ _ _. Instance: Commutative (↔) (@eq A). @@ -463,6 +492,14 @@ Instance: LeftId (↔) True impl. Proof. unfold impl. red. intuition. Qed. Instance: RightAbsorb (↔) True impl. Proof. unfold impl. red. intuition. Qed. +Instance: LeftDistr (↔) (∧) (∨). +Proof. red. intuition. Qed. +Instance: RightDistr (↔) (∧) (∨). +Proof. red. intuition. Qed. +Instance: LeftDistr (↔) (∨) (∧). +Proof. red. intuition. Qed. +Instance: RightDistr (↔) (∨) (∧). +Proof. red. intuition. Qed. (** The following lemmas are more specific versions of the projections of the above type classes. These lemmas allow us to enforce Coq not to use the setoid @@ -488,56 +525,76 @@ Proof. auto. Qed. Lemma right_absorb_eq {A} (i : A) (f : A → A → A) `{!RightAbsorb (=) i f} x : f x i = i. Proof. auto. Qed. +Lemma left_distr_eq {A} (f g : A → A → A) `{!LeftDistr (=) f g} x y z : + f x (g y z) = g (f x y) (f x z). +Proof. auto. Qed. +Lemma right_distr_eq {A} (f g : A → A → A) `{!RightDistr (=) f g} y z x : + f (g y z) x = g (f y x) (f z x). +Proof. auto. Qed. (** ** Axiomatization of ordered structures *) -(** A pre-order equiped with a smallest element. *) -Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := { +(** A pre-order equipped with a smallest element. *) +Class BoundedPreOrder A `{Empty A} `{SubsetEq A} : Prop := { bounded_preorder :>> PreOrder (⊆); subseteq_empty x : ∅ ⊆ x }. -Class PartialOrder A `{SubsetEq A} := { +Class PartialOrder A `{SubsetEq A} : Prop := { po_preorder :>> PreOrder (⊆); po_antisym :> AntiSymmetric (⊆) }. (** We do not include equality in the following interfaces so as to avoid the -need for proofs that the relations and operations respect setoid equality. +need for proofs that the relations and operations respect setoid equality. Instead, we will define setoid equality in a generic way as [λ X Y, X ⊆ Y ∧ Y ⊆ X]. *) -Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} := { +Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} : Prop := { bjsl_preorder :>> BoundedPreOrder A; - subseteq_union_l x y : x ⊆ x ∪ y; - subseteq_union_r x y : y ⊆ x ∪ y; + union_subseteq_l x y : x ⊆ x ∪ y; + union_subseteq_r x y : y ⊆ x ∪ y; union_least x y z : x ⊆ z → y ⊆ z → x ∪ y ⊆ z }. -Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} := { +Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} : Prop := { msl_preorder :>> BoundedPreOrder A; - subseteq_intersection_l x y : x ∩ y ⊆ x; - subseteq_intersection_r x y : x ∩ y ⊆ y; + intersection_subseteq_l x y : x ∩ y ⊆ x; + intersection_subseteq_r x y : x ∩ y ⊆ y; intersection_greatest x y z : z ⊆ x → z ⊆ y → z ⊆ x ∩ y }. + +(** A join distributive lattice with distributivity stated in the order +theoretic way. We will prove that distributivity of join, and distributivity +as an equality can be derived. *) Class LowerBoundedLattice A `{Empty A} `{SubsetEq A} - `{Union A} `{Intersection A} := { + `{Union A} `{Intersection A} : Prop := { lbl_bjsl :>> BoundedJoinSemiLattice A; - lbl_msl :>> MeetSemiLattice A + lbl_msl :>> MeetSemiLattice A; + lbl_distr x y z : (x ∪ y) ∩ (x ∪ z) ⊆ x ∪ (y ∩ z) }. + (** ** Axiomatization of collections *) (** The class [SimpleCollection A C] axiomatizes a collection of type [C] with elements of type [A]. *) Instance: Params (@map) 3. Class SimpleCollection A C `{ElemOf A C} - `{Empty C} `{Singleton A C} `{Union C} := { + `{Empty C} `{Singleton A C} `{Union C} : Prop := { not_elem_of_empty (x : A) : x ∉ ∅; elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y; elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y }. Class Collection A C `{ElemOf A C} `{Empty C} `{Singleton A C} - `{Union C} `{Intersection C} `{Difference C} `{IntersectionWith A C} := { + `{Union C} `{Intersection C} `{Difference C} : Prop := { collection_simple :>> SimpleCollection A C; elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y; - elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y; + elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y +}. +Class CollectionOps A C + `{ElemOf A C} `{Empty C} `{Singleton A C} + `{Union C} `{Intersection C} `{Difference C} + `{IntersectionWith A C} `{Filter A C} : Prop := { + collection_ops :>> Collection A C; elem_of_intersection_with (f : A → A → option A) X Y (x : A) : - x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x + x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x; + elem_of_filter X P `{∀ x, Decision (P x)} x : + x ∈ filter P X ↔ P x ∧ x ∈ X }. (** We axiomative a finite collection as a collection whose elements can be @@ -559,11 +616,9 @@ Inductive NoDup {A} : list A → Prop := (** Decidability of equality of the carrier set is admissible, but we add it anyway so as to avoid cycles in type class search. *) Class FinCollection A C `{ElemOf A C} `{Empty C} `{Singleton A C} - `{Union C} `{Intersection C} `{Difference C} `{IntersectionWith A C} - `{Filter A C} `{Elements A C} `{∀ x y : A, Decision (x = y)} := { + `{Union C} `{Intersection C} `{Difference C} + `{Elements A C} `{∀ x y : A, Decision (x = y)} : Prop := { fin_collection :>> Collection A C; - elem_of_filter X P `{∀ x, Decision (P x)} x : - x ∈ filter P X ↔ P x ∧ x ∈ X; elements_spec X x : x ∈ X ↔ x ∈ elements X; elements_nodup X : NoDup (elements X) }. @@ -581,7 +636,7 @@ decidability of equality, or a total order on the elements, which do not fit in a type constructor of type [Type → Type]. *) Class CollectionMonad M `{∀ A, ElemOf A (M A)} `{∀ A, Empty (M A)} `{∀ A, Singleton A (M A)} `{∀ A, Union (M A)} - `{!MBind M} `{!MRet M} `{!FMap M} `{!MJoin M} := { + `{!MBind M} `{!MRet M} `{!FMap M} `{!MJoin M} : Prop := { collection_monad_simple A :> SimpleCollection A (M A); elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) : x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X; @@ -599,7 +654,7 @@ equality on collections. *) Class Fresh A C := fresh: C → A. Instance: Params (@fresh) 3. Class FreshSpec A C `{ElemOf A C} - `{Empty C} `{Singleton A C} `{Union C} `{Fresh A C} := { + `{Empty C} `{Singleton A C} `{Union C} `{Fresh A C} : Prop := { fresh_collection_simple :>> SimpleCollection A C; fresh_proper_alt X Y : (∀ x, x ∈ X ↔ x ∈ Y) → fresh X = fresh Y; is_fresh (X : C) : fresh X ∉ X @@ -609,7 +664,9 @@ Class FreshSpec A C `{ElemOf A C} Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) : x↾Px = y↾Py → x = y. Proof. injection 1; trivial. Qed. - +Lemma not_symmetry `{R : relation A} `{!Symmetric R} (x y : A) : + ¬R x y → ¬R y x. +Proof. intuition. Qed. Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) : R x y ↔ R y x. Proof. intuition. Qed. @@ -701,6 +758,12 @@ Proof. red. trivial. Qed. Instance right_id_propholds {A} (R : relation A) i f : RightId R i f → ∀ x, PropHolds (R (f x i) x). Proof. red. trivial. Qed. +Instance left_absorb_propholds {A} (R : relation A) i f : + LeftAbsorb R i f → ∀ x, PropHolds (R (f i x) i). +Proof. red. trivial. Qed. +Instance right_absorb_propholds {A} (R : relation A) i f : + RightAbsorb R i f → ∀ x, PropHolds (R (f x i) i). +Proof. red. trivial. Qed. Instance idem_propholds {A} (R : relation A) f : Idempotent R f → ∀ x, PropHolds (R (f x x) x). Proof. red. trivial. Qed. diff --git a/theories/collections.v b/theories/collections.v index b96b6836..7d4c52db 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -1,11 +1,11 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects definitions and theorems on collections. Most importantly, it implements some tactics to automatically solve goals involving collections. *) Require Export base tactics orders. -(** * Theorems *) +(** * Basic theorems *) Section simple_collection. Context `{SimpleCollection A C}. @@ -28,6 +28,9 @@ Section simple_collection. Lemma elem_of_equiv_alt X Y : X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X). Proof. firstorder. Qed. + Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. + Proof. firstorder. Qed. + Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X. Proof. split. @@ -60,33 +63,92 @@ Section simple_collection. Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y. Proof. rewrite elem_of_union. tauto. Qed. - Context `{∀ X Y : C, Decision (X ⊆ Y)}. - - Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. - Proof. - refine (cast_if (decide_rel (⊆) {[ x ]} X)); - by rewrite elem_of_subseteq_singleton. - Defined. + Section leibniz. + Context `{!LeibnizEquiv C}. + + Lemma elem_of_equiv_L X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y. + Proof. unfold_leibniz. apply elem_of_equiv. Qed. + Lemma elem_of_equiv_alt_L X Y : + X = Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X). + 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 non_empty_singleton_L x : {[ x ]} ≠∅. + Proof. unfold_leibniz. apply non_empty_singleton. Qed. + End leibniz. + + Section dec. + Context `{∀ X Y : C, Decision (X ⊆ Y)}. + + Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. + Proof. + refine (cast_if (decide_rel (⊆) {[ x ]} X)); + by rewrite elem_of_subseteq_singleton. + Defined. + End dec. End simple_collection. +(** * Tactics *) +(** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will +recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *) +Tactic Notation "decompose_elem_of" hyp(H) := + let rec go H := + lazymatch type of H with + | _ ∈ ∅ => apply elem_of_empty in H; destruct H + | ?x ∈ {[ ?y ]} => + apply elem_of_singleton in H; try first [subst y | subst x] + | _ ∈ _ ∪ _ => + let H1 := fresh in let H2 := fresh in apply elem_of_union in H; + destruct H as [H1|H2]; [go H1 | go H2] + | _ ∈ _ ∩ _ => + let H1 := fresh in let H2 := fresh in apply elem_of_intersection in H; + destruct H as [H1 H2]; go H1; go H2 + | _ ∈ _ ∖ _ => + let H1 := fresh in let H2 := fresh in apply elem_of_difference in H; + destruct H as [H1 H2]; go H1; go H2 + | ?x ∈ _ <$> _ => + let H1 := fresh in apply elem_of_fmap in H; + destruct H as [? [? H1]]; try (subst x); go H1 + | _ ∈ _ ≫= _ => + let H1 := fresh in let H2 := fresh in apply elem_of_bind in H; + destruct H as [? [H1 H2]]; go H1; go H2 + | ?x ∈ mret ?y => + apply elem_of_ret in H; try first [subst y | subst x] + | _ ∈ mjoin _ ≫= _ => + let H1 := fresh in let H2 := fresh in apply elem_of_join in H; + destruct H as [? [H1 H2]]; go H1; go H2 + | _ => idtac + end in go H. +Tactic Notation "decompose_elem_of" := + repeat_on_hyps (fun H => decompose_elem_of H). + Ltac decompose_empty := repeat match goal with + | H : ∅ ≡ ∅ |- _ => clear H + | H : ∅ = ∅ |- _ => clear H + | H : ∅ ≡ _ |- _ => symmetry in H + | H : ∅ = _ |- _ => symmetry in H | H : _ ∪ _ ≡ ∅ |- _ => apply empty_union in H; destruct H | H : _ ∪ _ ≢ ∅ |- _ => apply non_empty_union in H; destruct H | H : {[ _ ]} ≡ ∅ |- _ => destruct (non_empty_singleton _ H) + | H : _ ∪ _ = ∅ |- _ => apply empty_union_L in H; destruct H + | H : _ ∪ _ ≠∅ |- _ => apply non_empty_union_L in H; destruct H + | H : {[ _ ]} = ∅ |- _ => destruct (non_empty_singleton_L _ H) end. -(** * Tactics *) -(** The first pass consists of eliminating all occurrences of [(∪)], [(∩)], -[(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into -logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into -[A → x ∈ X ∨ False]. *) +(** The first pass of our collection tactic consists of eliminating all +occurrences of [(∪)], [(∩)], [(∖)], [(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)], +by rewriting these into logically equivalent propositions. For example we +rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *) Ltac unfold_elem_of := repeat_on_hyps (fun H => repeat match type of H with | context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq in H | context [ _ ⊂ _ ] => setoid_rewrite subset_spec in H + | context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty in H | context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt in H + | context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L in H + | context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H | context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty in H | context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H | context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union in H @@ -100,7 +162,10 @@ Ltac unfold_elem_of := repeat match goal with | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq | |- context [ _ ⊂ _ ] => setoid_rewrite subset_spec + | |- context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt + | |- context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L + | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union @@ -117,6 +182,7 @@ For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is generally powerful enough. This tactic either fails or proves the goal. *) Tactic Notation "solve_elem_of" tactic3(tac) := simpl in *; + decompose_empty; unfold_elem_of; solve [intuition (simplify_equality; tac)]. Tactic Notation "solve_elem_of" := solve_elem_of auto. @@ -128,48 +194,22 @@ use the [naive_solver] tactic as a substitute. This tactic either fails or proves the goal. *) Tactic Notation "esolve_elem_of" tactic3(tac) := simpl in *; + decompose_empty; unfold_elem_of; naive_solver tac. Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. - -(** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will -recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *) -Tactic Notation "decompose_elem_of" hyp(H) := - let rec go H := - lazymatch type of H with - | _ ∈ ∅ => apply elem_of_empty in H; destruct H - | ?x ∈ {[ ?y ]} => - apply elem_of_singleton in H; try first [subst y | subst x] - | _ ∈ _ ∪ _ => - let H1 := fresh in let H2 := fresh in apply elem_of_union in H; - destruct H as [H1|H2]; [go H1 | go H2] - | _ ∈ _ ∩ _ => - let H1 := fresh in let H2 := fresh in apply elem_of_intersection in H; - destruct H as [H1 H2]; go H1; go H2 - | _ ∈ _ ∖ _ => - let H1 := fresh in let H2 := fresh in apply elem_of_difference in H; - destruct H as [H1 H2]; go H1; go H2 - | ?x ∈ _ <$> _ => - let H1 := fresh in apply elem_of_fmap in H; - destruct H as [? [? H1]]; try (subst x); go H1 - | _ ∈ _ ≫= _ => - let H1 := fresh in let H2 := fresh in apply elem_of_bind in H; - destruct H as [? [H1 H2]]; go H1; go H2 - | ?x ∈ mret ?y => - apply elem_of_ret in H; try first [subst y | subst x] - | _ ∈ mjoin _ ≫= _ => - let H1 := fresh in let H2 := fresh in apply elem_of_join in H; - destruct H as [? [H1 H2]]; go H1; go H2 - | _ => idtac - end in go H. -Tactic Notation "decompose_elem_of" := - repeat_on_hyps (fun H => decompose_elem_of H). - + +(** * More theorems *) Section collection. Context `{Collection A C}. Global Instance: LowerBoundedLattice C. - Proof. split. apply _. firstorder auto. Qed. + Proof. + split. + * apply _. + * firstorder auto. + * solve_elem_of. + Qed. Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}. Proof. esolve_elem_of. Qed. @@ -185,6 +225,62 @@ Section collection. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Proof. esolve_elem_of. Qed. + Section leibniz. + Context `{!LeibnizEquiv C}. + + Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = {[x]}. + Proof. unfold_leibniz. apply intersection_singletons. Qed. + Lemma difference_twice_L X Y : (X ∖ Y) ∖ Y = X ∖ Y. + Proof. unfold_leibniz. apply difference_twice. Qed. + + Lemma empty_difference_L X Y : X ⊆ Y → X ∖ Y = ∅. + Proof. unfold_leibniz. apply empty_difference. Qed. + Lemma difference_diag_L X : X ∖ X = ∅. + Proof. unfold_leibniz. apply difference_diag. Qed. + Lemma difference_union_distr_l_L X Y Z : (X ∪ Y) ∖ Z = X ∖ Z ∪ Y ∖ Z. + Proof. unfold_leibniz. apply difference_union_distr_l. Qed. + Lemma difference_intersection_distr_l_L X Y Z : + (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z. + Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. + End leibniz. + + Section dec. + Context `{∀ X Y : C, Decision (X ⊆ Y)}. + + Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y. + Proof. + rewrite elem_of_intersection. + destruct (decide (x ∈ X)); tauto. + Qed. + Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y. + Proof. + rewrite elem_of_difference. + destruct (decide (x ∈ Y)); tauto. + Qed. + Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X. + Proof. + split; intros x; rewrite !elem_of_union, elem_of_difference. + * destruct (decide (x ∈ X)); intuition. + * intuition. + Qed. + Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. + Proof. + intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. + destruct (decide (x ∈ X)); esolve_elem_of. + Qed. + + Context `{!LeibnizEquiv C}. + + Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. + Proof. unfold_leibniz. apply union_difference. Qed. + Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠∅. + Proof. unfold_leibniz. apply non_empty_difference. Qed. + End dec. +End collection. + +Section collection_ops. + Context `{CollectionOps A C}. + Lemma elem_of_intersection_with_list (f : A → A → option A) Xs Y x : x ∈ intersection_with_list f Y Xs ↔ ∃ xs y, Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x. @@ -212,31 +308,7 @@ Section collection. intros x Hx. rewrite elem_of_intersection_with in Hx. decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto. Qed. - - Context `{∀ X Y : C, Decision (X ⊆ Y)}. - - Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y. - Proof. - rewrite elem_of_intersection. - destruct (decide (x ∈ X)); tauto. - Qed. - Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y. - Proof. - rewrite elem_of_difference. - destruct (decide (x ∈ Y)); tauto. - Qed. - Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X. - Proof. - split; intros x; rewrite !elem_of_union, elem_of_difference. - * destruct (decide (x ∈ X)); intuition. - * intuition. - Qed. - Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. - Proof. - intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. - destruct (decide (x ∈ X)); esolve_elem_of. - Qed. -End collection. +End collection_ops. (** * Sets without duplicates up to an equivalence *) Section no_dup. @@ -378,6 +450,7 @@ Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C := | Some a => {[ a ]} end. +(** * Properties of implementations of collections that form a monad *) Section collection_monad. Context `{CollectionMonad M}. @@ -435,7 +508,8 @@ Section collection_monad. Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l. Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed. - Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P : B → C → Prop) l1 l2 k : + Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) + (P : B → C → Prop) l1 l2 k : l1 ∈ mapM f k → Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 → Forall2 P l1 l2. diff --git a/theories/decidable.v b/theories/decidable.v index 56a619e9..662d2084 100644 --- a/theories/decidable.v +++ b/theories/decidable.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects theorems, definitions, tactics, related to propositions with a decidable equality. Such propositions are collected by the [Decision] @@ -10,6 +10,9 @@ Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances. Lemma dec_stable `{Decision P} : ¬¬P → P. Proof. firstorder. Qed. +Lemma Is_true_reflect (b : bool) : reflect b b. +Proof. destruct b. by left. right. intros []. Qed. + (** We introduce [decide_rel] to avoid inefficienct computation due to eager evaluation of propositions by [vm_compute]. This inefficiency occurs if [(x = y) := (f x = f y)] as [decide (x = y)] evaluates to [decide (f x = f y)] @@ -21,18 +24,27 @@ Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y (x : A) (y : B) : decide_rel R x y = decide (R x y). Proof. done. Qed. +(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the +components is double negated, it will try to remove the double negation. *) +Ltac destruct_decide dec := + let H := fresh in + destruct dec as [H|H]; + try match type of H with + | ¬¬_ => apply dec_stable in H + end. + (** The tactic [case_decide] performs case analysis on an arbitrary occurrence of [decide] or [decide_rel] in the conclusion or hypotheses. *) Ltac case_decide := match goal with | H : context [@decide ?P ?dec] |- _ => - destruct (@decide P dec) + destruct_decide (@decide P dec) | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => - destruct (@decide_rel _ _ R x y dec) + destruct_decide (@decide_rel _ _ R x y dec) | |- context [@decide ?P ?dec] => - destruct (@decide P dec) + destruct_decide (@decide P dec) | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => - destruct (@decide_rel _ _ R x y dec) + destruct_decide (@decide_rel _ _ R x y dec) end. (** The tactic [solve_decision] uses Coq's [decide equality] tactic together @@ -61,6 +73,17 @@ Notation cast_if_not S := (if S then right _ else left _). Definition bool_decide (P : Prop) {dec : Decision P} : bool := if dec then true else false. +Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P). +Proof. unfold bool_decide. destruct dec. by left. by right. Qed. + +Ltac case_bool_decide := + match goal with + | H : context [@bool_decide ?P ?dec] |- _ => + destruct_decide (@bool_decide_reflect P dec) + | |- context [@bool_decide ?P ?dec] => + destruct_decide (@bool_decide_reflect P dec) + end. + Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P. Proof. unfold bool_decide. by destruct dec. Qed. Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P. @@ -70,9 +93,14 @@ Proof. unfold bool_decide. by destruct dec. Qed. (** Leibniz equality on Sigma types requires the equipped proofs to be equal as Coq does not support proof irrelevance. For decidable we propositions we define the type [dsig P] whose Leibniz equality is proof -irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *) +irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. Due to the absence of +universe polymorpic definitions we also define a variant [dsigS] for types +in [Set]. *) Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} := { x | bool_decide (P x) }. +Definition dsigS {A : Set} (P : A → Prop) `{∀ x : A, Decision (P x)} : Set := + { x | bool_decide (P x) }. + Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) := bool_decide_unpack _ (proj2_sig x). Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P := diff --git a/theories/fin_collections.v b/theories/fin_collections.v index 35808597..46969612 100644 --- a/theories/fin_collections.v +++ b/theories/fin_collections.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects definitions and theorems on finite collections. Most importantly, it implements a fold and size function and some useful induction diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v new file mode 100644 index 00000000..2ca9a583 --- /dev/null +++ b/theories/fin_map_dom.v @@ -0,0 +1,142 @@ +(* 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} + `{∀ A, Lookup K A (M A)} + `{∀ A, Empty (M A)} + `{∀ A, PartialAlter K A (M A)} + `{!Merge M} + `{∀ A, FinMapToList K A (M A)} + `{∀ i j : K, Decision (i = j)} + `{∀ 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 theorems. +Context `{FinMapDom K M D}. + +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. + unfold subseteq, map_subseteq, collection_subseteq. + 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. } + intros Hdom. destruct Hss2. intros i x Hi. + specialize (Hdom i). rewrite !elem_of_dom in Hdom. + feed inversion Hdom. eauto. + by erewrite (Hss1 i) in Hi by eauto. +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. +Lemma dom_empty_inv {A} (m : M A) : + dom D m ≡ ∅ → m = ∅. +Proof. + intros E. apply map_empty. intros. apply not_elem_of_dom. + rewrite E. solve_elem_of. +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, !is_Some_alt. + setoid_rewrite lookup_insert_Some. + destruct (decide (i = j)); esolve_elem_of. +Qed. +Lemma dom_insert_subseteq {A} (m : M A) i x : + dom D m ⊆ dom D (<[i:=x]>m). +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_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, !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. + +Lemma map_disjoint_dom {A} (m1 m2 : M A) : + m1 ⊥ m2 ↔ dom D m1 ∩ dom D m2 ≡ ∅. +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. +Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : + m1 ⊥ m2 → dom D m1 ∩ dom D m2 ≡ ∅. +Proof. apply map_disjoint_dom. Qed. +Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : + dom D m1 ∩ dom D m2 ≡ ∅ → m1 ⊥ m2. +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, !is_Some_alt. + setoid_rewrite lookup_union_Some_raw. + destruct (m1 !! i); naive_solver. +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. + +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, !is_Some_alt. + setoid_rewrite lookup_difference_Some. + destruct (m2 !! i); naive_solver. +Qed. +End theorems. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index fd6e3675..5c4acc4e 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1,11 +1,12 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** Finite maps associate data to keys. This file defines an interface for finite maps and collects some theory on it. Most importantly, it proves useful -induction principles for finite maps and implements the tactic [simplify_map] -to simplify goals involving finite maps. *) +induction principles for finite maps and implements the tactic +[simplify_map_equality] to simplify goals involving finite maps. *) Require Import Permutation. -Require Export prelude. +Require Export ars vector orders. + (** * Axiomatization of finite maps *) (** We require Leibniz equality to be extensional on finite maps. This of course limits the space of finite map implementations, but since we are mainly @@ -16,22 +17,22 @@ convenient use in the assertions of our axiomatic semantics. *) (** Finiteness is axiomatized by requiring that each map can be translated to an association list. The translation to association lists is used to -implement the [dom] function, and for well founded recursion on finite maps. *) +prove well founded recursion on finite maps. *) (** Finite map implementations are required to implement the [merge] function which enables us to give a generic implementation of [union_with], [intersection_with], and [difference_with]. *) -Class FinMapToList K A M := finmap_to_list: M → list (K * A). +Class FinMapToList K A M := map_to_list: M → list (K * A). Class FinMap K M `{!FMap M} `{∀ A, Lookup K A (M A)} `{∀ A, Empty (M A)} `{∀ A, PartialAlter K A (M A)} - `{∀ A, Merge A (M A)} + `{!Merge M} `{∀ A, FinMapToList K A (M A)} `{∀ i j : K, Decision (i = j)} := { - finmap_eq {A} (m1 m2 : M A) : + map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2; lookup_empty {A} i : (∅ : M A) !! i = None; @@ -41,12 +42,13 @@ Class FinMap K M `{!FMap M} 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; - finmap_to_list_nodup {A} (m : M A) : - NoDup (finmap_to_list m); - elem_of_finmap_to_list {A} (m : M A) i x : - (i,x) ∈ finmap_to_list m ↔ m !! i = Some x; - merge_spec {A} f `{!PropHolds (f None None = None)} - (m1 m2 : M A) i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i) + map_to_list_nodup {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_merge {A B C} (f : option A → option B → option C) + `{!PropHolds (f None None = None)} m1 m2 i : + merge f m1 m2 !! i = f (m1 !! i) (m2 !! i) }. (** * Derived operations *) @@ -54,431 +56,1504 @@ Class FinMap K M `{!FMap M} finite map implementations. These generic implementations do not cause a significant performance loss to make including them in the finite map interface worthwhile. *) -Instance finmap_insert `{PartialAlter K A M} : Insert K A M := λ i x, - partial_alter (λ _, Some x) i. -Instance finmap_alter `{PartialAlter K A M} : Alter K A M := λ f, - partial_alter (fmap f). -Instance finmap_delete `{PartialAlter K A M} : Delete K M := +Instance map_insert `{PartialAlter K A M} : Insert K A M := + λ i x, partial_alter (λ _, Some x) i. +Instance map_alter `{PartialAlter K A M} : Alter K A M := + λ f, partial_alter (fmap f). +Instance map_delete `{PartialAlter K A M} : Delete K M := partial_alter (λ _, None). -Instance finmap_singleton `{PartialAlter K A M} +Instance map_singleton `{PartialAlter K A M} `{Empty M} : Singleton (K * A) M := λ p, <[fst p:=snd p]>∅. -Definition finmap_of_list `{Insert K A M} `{Empty M} +Definition map_of_list `{Insert K A M} `{Empty M} (l : list (K * A)) : M := insert_list l ∅. -Instance finmap_dom `{FinMapToList K A M} : Dom K M := λ C _ _ _, - foldr ((∪) ∘ singleton ∘ fst) ∅ ∘ finmap_to_list. -Instance finmap_union_with `{Merge A M} : UnionWith A M := λ f, - merge (union_with f). -Instance finmap_intersection_with `{Merge A M} : IntersectionWith A M := λ f, - merge (intersection_with f). -Instance finmap_difference_with `{Merge A M} : DifferenceWith A M := λ f, - merge (difference_with f). +Instance map_union_with `{Merge M} {A} : UnionWith A (M A) := + λ f, merge (union_with f). +Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) := + λ f, merge (intersection_with f). +Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) := + λ f, merge (difference_with f). (** The relation [intersection_forall R] on finite maps describes that the relation [R] holds for each pair in the intersection. *) -Definition finmap_forall `{Lookup K A M} (P : K → A → Prop) : M → Prop := +Definition map_forall `{Lookup K A M} (P : K → A → Prop) : M → Prop := λ m, ∀ i x, m !! i = Some x → P i x. -Definition finmap_intersection_forall `{Lookup K A M} +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 finmap_disjoint `{∀ A, Lookup K A (M A)} : Disjoint (M A) := λ A, - finmap_intersection_forall (λ _ _, False). +Instance map_disjoint `{∀ A, Lookup K A (M A)} : Disjoint (M A) := + λ A, map_intersection_forall (λ _ _, False). (** The union of two finite maps only has a meaningful definition for maps that are disjoint. However, as working with partial functions is inconvenient in Coq, we define the union as a total function. In case both finite maps have a value at the same index, we take the value of the first map. *) -Instance finmap_union `{Merge A M} : Union M := - union_with (λ x _, Some x). -Instance finmap_intersection `{Merge A M} : Intersection M := +Instance map_union `{Merge M} {A} : Union (M A) := union_with (λ x _, Some x). +Instance map_intersection `{Merge M} {A} : Intersection (M A) := + intersection_with (λ x _, Some x). + (** The difference operation removes all values from the first map whose index contains a value in the second map as well. *) -Instance finmap_difference `{Merge A M} : Difference M := +Instance map_difference `{Merge M} {A} : Difference (M A) := difference_with (λ _ _, None). -(** * General theorems *) -Section finmap_common. - Context `{FinMap K M} {A : Type}. - - Global Instance finmap_subseteq: SubsetEq (M A) := λ m n, - ∀ i x, m !! i = Some x → n !! i = Some x. - Global Instance: BoundedPreOrder (M A). - Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed. - - Lemma lookup_weaken (m1 m2 : M A) i x : - m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x. - Proof. auto. Qed. - Lemma lookup_weaken_is_Some (m1 m2 : M A) i : - is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i). - Proof. inversion 1. eauto using lookup_weaken. Qed. - Lemma lookup_weaken_None (m1 m2 : M A) i : - m2 !! i = None → m1 ⊆ m2 → m1 !! i = None. - Proof. - rewrite eq_None_not_Some. intros Hm2 Hm1m2. - specialize (Hm1m2 i). destruct (m1 !! i); naive_solver. - Qed. - - Lemma lookup_weaken_inv (m1 m2 : M A) i x y : - m1 !! i = Some x → - m1 ⊆ m2 → - m2 !! i = Some y → - x = y. - Proof. - intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. - congruence. - Qed. - - Lemma lookup_ne (m : M A) i j : m !! i ≠m !! j → i ≠j. - Proof. congruence. Qed. - Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅. - Proof. intros Hm. apply finmap_eq. intros. by rewrite Hm, lookup_empty. Qed. - Lemma lookup_empty_is_Some i : ¬is_Some ((∅ : M A) !! i). - Proof. rewrite lookup_empty. by inversion 1. Qed. - Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x. - Proof. by rewrite lookup_empty. Qed. - - Lemma partial_alter_compose (m : M A) i f g : - partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m). - Proof. - intros. apply finmap_eq. intros ii. case (decide (i = ii)). - * intros. subst. by rewrite !lookup_partial_alter. - * intros. by rewrite !lookup_partial_alter_ne. - Qed. - Lemma partial_alter_comm (m : M A) i j f g : - i ≠j → - partial_alter f i (partial_alter g j m) = - partial_alter g j (partial_alter f i m). - Proof. - intros. apply finmap_eq. intros jj. - destruct (decide (jj = j)). - * subst. by rewrite lookup_partial_alter_ne, - !lookup_partial_alter, lookup_partial_alter_ne. - * destruct (decide (jj = i)). - + subst. by rewrite lookup_partial_alter, - !lookup_partial_alter_ne, lookup_partial_alter by congruence. - + by rewrite !lookup_partial_alter_ne by congruence. - Qed. - Lemma partial_alter_self_alt (m : M A) i x : - x = m !! i → partial_alter (λ _, x) i m = m. - Proof. - intros. apply finmap_eq. intros ii. - destruct (decide (i = ii)). - * subst. by rewrite lookup_partial_alter. - * by rewrite lookup_partial_alter_ne. - Qed. - Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m. - Proof. by apply partial_alter_self_alt. Qed. - - Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x. - Proof. unfold insert. apply lookup_partial_alter. Qed. - Lemma lookup_insert_rev (m : M A) i x y : <[i:= x ]>m !! i = Some y → x = y. - Proof. rewrite lookup_insert. congruence. Qed. - Lemma lookup_insert_ne (m : M A) i j x : i ≠j → <[i:=x]>m !! j = m !! j. - Proof. unfold insert. apply lookup_partial_alter_ne. Qed. - Lemma insert_comm (m : M A) i j x y : - i ≠j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m). - Proof. apply partial_alter_comm. Qed. - - Lemma lookup_insert_Some (m : M A) i j x y : - <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠j ∧ m !! j = Some y). - Proof. - split. - * destruct (decide (i = j)); subst; - rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. - * intros [[??]|[??]]. - + subst. apply lookup_insert. - + by rewrite lookup_insert_ne. - Qed. - Lemma lookup_insert_None (m : M A) i j x : - <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠j. - Proof. - split. - * destruct (decide (i = j)); subst; - rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. - * intros [??]. by rewrite lookup_insert_ne. - Qed. - - Lemma lookup_singleton_Some i j (x y : A) : - {[(i, x)]} !! j = Some y ↔ i = j ∧ x = y. - Proof. - unfold singleton, finmap_singleton. - rewrite lookup_insert_Some, lookup_empty. simpl. - intuition congruence. - Qed. - Lemma lookup_singleton_None i j (x : A) : - {[(i, x)]} !! j = None ↔ i ≠j. - Proof. - unfold singleton, finmap_singleton. - rewrite lookup_insert_None, lookup_empty. simpl. tauto. - Qed. - Lemma insert_singleton i (x y : A) : <[i:=y]>{[(i, x)]} = {[(i, y)]}. - Proof. - unfold singleton, finmap_singleton, insert, finmap_insert. - by rewrite <-partial_alter_compose. - Qed. - - Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x. - Proof. by rewrite lookup_singleton_Some. Qed. - Lemma lookup_singleton_ne i j (x : A) : i ≠j → {[(i, x)]} !! j = None. - Proof. by rewrite lookup_singleton_None. Qed. - - Lemma lookup_delete (m : M A) i : delete i m !! i = None. - Proof. apply lookup_partial_alter. Qed. - Lemma lookup_delete_ne (m : M A) i j : i ≠j → delete i m !! j = m !! j. - Proof. apply lookup_partial_alter_ne. Qed. - - Lemma lookup_delete_Some (m : M A) i j y : - delete i m !! j = Some y ↔ i ≠j ∧ m !! j = Some y. - Proof. - split. - * destruct (decide (i = j)); subst; - rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence. - * intros [??]. by rewrite lookup_delete_ne. - Qed. - Lemma lookup_delete_None (m : M A) i j : - delete i m !! j = None ↔ i = j ∨ m !! j = None. - Proof. - destruct (decide (i = j)). - * subst. rewrite lookup_delete. tauto. - * rewrite lookup_delete_ne; tauto. - Qed. - - Lemma delete_empty i : delete i (∅ : M A) = ∅. - Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed. - Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅. - Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed. - Lemma delete_comm (m : M A) i j : - delete i (delete j m) = delete j (delete i m). - Proof. destruct (decide (i = j)). by subst. by apply partial_alter_comm. Qed. - Lemma delete_insert_comm (m : M A) i j x : - i ≠j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m). - Proof. intro. by apply partial_alter_comm. Qed. - - Lemma delete_notin (m : M A) i : - m !! i = None → delete i m = m. - Proof. - intros. apply finmap_eq. intros j. - destruct (decide (i = j)). - * subst. by rewrite lookup_delete. - * by apply lookup_delete_ne. - Qed. - - Lemma delete_partial_alter (m : M A) i f : - m !! i = None → delete i (partial_alter f i m) = m. - Proof. - intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose. - rapply partial_alter_self_alt. congruence. - Qed. - Lemma delete_insert (m : M A) i x : - m !! i = None → delete i (<[i:=x]>m) = m. - Proof. apply delete_partial_alter. Qed. - Lemma insert_delete (m : M A) i x : - m !! i = Some x → <[i:=x]>(delete i m) = m. - Proof. - intros Hmi. unfold delete, finmap_delete, insert, finmap_insert. - rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi. - by apply partial_alter_self_alt. - Qed. - - Lemma lookup_delete_list (m : M A) is j : - j ∈ is → delete_list is m !! j = None. - Proof. - induction 1 as [|i j is]; simpl. - * by rewrite lookup_delete. - * destruct (decide (i = j)). - + subst. by rewrite lookup_delete. - + rewrite lookup_delete_ne; auto. - Qed. - Lemma lookup_delete_list_not_elem_of (m : M A) is j : - j ∉ is → delete_list is m !! j = m !! j. - Proof. - induction is; simpl; [done |]. - rewrite elem_of_cons. intros. - intros. rewrite lookup_delete_ne; intuition. - Qed. - Lemma delete_list_notin (m : M A) is : - Forall (λ i, m !! i = None) is → delete_list is m = m. - Proof. - induction 1; simpl; [done |]. - rewrite delete_notin; congruence. - Qed. - - Lemma delete_list_insert_comm (m : M A) is j x : - j ∉ is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m). - Proof. - induction is; simpl; [done |]. - rewrite elem_of_cons. intros. - rewrite IHis, delete_insert_comm; intuition. - Qed. - - Lemma elem_of_dom C `{SimpleCollection K C} (m : M A) i : - i ∈ dom C m ↔ is_Some (m !! i). - Proof. - unfold dom, finmap_dom. simpl. rewrite is_Some_alt. - setoid_rewrite <-elem_of_finmap_to_list. - induction (finmap_to_list m) as [|[j x] l IH]; simpl. - * rewrite elem_of_empty. - setoid_rewrite elem_of_nil. naive_solver. - * rewrite elem_of_union, elem_of_singleton. - setoid_rewrite elem_of_cons. naive_solver. - Qed. - Lemma not_elem_of_dom C `{SimpleCollection K C} (m : M A) i : - i ∉ dom C m ↔ m !! i = None. - Proof. by rewrite (elem_of_dom C), eq_None_not_Some. Qed. - - Lemma dom_empty C `{SimpleCollection K C} : dom C (∅ : M A) ≡ ∅. - Proof. - split; intro. - * rewrite (elem_of_dom C), lookup_empty. by inversion 1. - * solve_elem_of. - Qed. - Lemma dom_empty_inv C `{SimpleCollection K C} (m : M A) : - dom C m ≡ ∅ → m = ∅. - Proof. - intros E. apply finmap_empty. intros. apply (not_elem_of_dom C). - rewrite E. solve_elem_of. - Qed. - - Lemma delete_partial_alter_dom C `{SimpleCollection K C} (m : M A) i f : - i ∉ dom C m → delete i (partial_alter f i m) = m. - Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed. - Lemma delete_insert_dom C `{SimpleCollection K C} (m : M A) i x : - i ∉ dom C m → delete i (<[i:=x]>m) = m. - Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed. - Lemma elem_of_dom_delete C `{SimpleCollection K C} (m : M A) i j : - i ∈ dom C (delete j m) ↔ i ≠j ∧ i ∈ dom C m. - Proof. - rewrite !(elem_of_dom C), <-!not_eq_None_Some. - rewrite lookup_delete_None. intuition. - Qed. - Lemma not_elem_of_dom_delete C `{SimpleCollection K C} (m : M A) i : - i ∉ dom C (delete i m). - Proof. apply (not_elem_of_dom C), lookup_delete. Qed. - - Lemma subseteq_dom C `{SimpleCollection K C} (m1 m2 : M A) : - m1 ⊆ m2 → dom C m1 ⊆ dom C m2. - Proof. - unfold subseteq, finmap_subseteq, collection_subseteq. - intros ??. rewrite !(elem_of_dom C). inversion 1. eauto. - Qed. - Lemma subset_dom C `{SimpleCollection K C} (m1 m2 : M A) : - m1 ⊂ m2 → dom C m1 ⊂ dom C m2. - Proof. - intros [Hss1 Hss2]. split. - * by apply subseteq_dom. - * intros Hdom. destruct Hss2. intros i x Hi. - specialize (Hdom i). rewrite !(elem_of_dom C) in Hdom. - feed inversion Hdom. eauto. - by erewrite (Hss1 i) in Hi by eauto. - Qed. - Lemma finmap_wf : wf (@subset (M A) _). - Proof. - apply (wf_projected (⊂) (dom (listset K))). - * by apply (subset_dom _). - * by apply collection_wf. - Qed. - - Lemma partial_alter_subseteq (m : M A) i f : - m !! i = None → - m ⊆ partial_alter f i m. - Proof. - intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. - Qed. - Lemma partial_alter_subset (m : M A) i f : - m !! i = None → - is_Some (f (m !! i)) → - m ⊂ partial_alter f i m. - Proof. - intros Hi Hfi. split. - * by apply partial_alter_subseteq. - * inversion Hfi as [x Hx]. intros Hm. - apply (Some_ne_None x). rewrite <-(Hm i x); [done|]. - by rewrite lookup_partial_alter. - Qed. - Lemma insert_subseteq (m : M A) i x : - m !! i = None → - m ⊆ <[i:=x]>m. - Proof. apply partial_alter_subseteq. Qed. - Lemma insert_subset (m : M A) i x : - m !! i = None → - m ⊂ <[i:=x]>m. - Proof. intro. apply partial_alter_subset; eauto. Qed. - - Lemma delete_subseteq (m : M A) i : - delete i m ⊆ m. - Proof. intros j x. rewrite lookup_delete_Some. tauto. Qed. - Lemma delete_subseteq_compat (m1 m2 : M A) i : - m1 ⊆ m2 → - delete i m1 ⊆ delete i m2. - Proof. intros ? j x. rewrite !lookup_delete_Some. intuition eauto. Qed. - Lemma delete_subset_alt (m : M A) i x : - m !! i = Some x → delete i m ⊂ m. - Proof. - split. - * apply delete_subseteq. - * intros Hi. apply (None_ne_Some x). - by rewrite <-(lookup_delete m i), (Hi i x). - Qed. - Lemma delete_subset (m : M A) i : - is_Some (m !! i) → delete i m ⊂ m. - Proof. inversion 1. eauto using delete_subset_alt. Qed. - - (** * Induction principles *) - (** We use the induction principle on finite collections to prove the - following induction principle on finite maps. *) - Lemma finmap_ind_alt C (P : M A → Prop) `{FinCollection K C} : - P ∅ → - (∀ i x m, i ∉ dom C m → P m → P (<[i:=x]>m)) → - ∀ m, P m. - Proof. - intros Hemp Hinsert m. - apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m). - * solve_proper. - * clear m. intros m Hm. rewrite finmap_empty. - + done. - + intros. rewrite <-(not_elem_of_dom C), Hm. - by solve_elem_of. - * clear m. intros i X Hi IH m Hdom. - assert (∃ x, m !! i = Some x) as [x ?]. - { apply is_Some_alt, (elem_of_dom C). - rewrite Hdom. clear Hdom. - by solve_elem_of. } - rewrite <-(insert_delete m i x) by done. - apply Hinsert. - { by apply (not_elem_of_dom_delete C). } - apply IH. apply elem_of_equiv. intros. - rewrite (elem_of_dom_delete C). - esolve_elem_of. - * done. - Qed. - - (** We use the [listset] implementation to prove an induction principle that - does not use the map's domain. *) - Lemma finmap_ind (P : M A → Prop) : - P ∅ → - (∀ i x m, m !! i = None → P m → P (<[i:=x]>m)) → - ∀ m, P m. - Proof. - setoid_rewrite <-(not_elem_of_dom (listset _)). - apply (finmap_ind_alt (listset _) P). - Qed. -End finmap_common. - -(** * The finite map tactic *) -(** The tactic [simplify_map by tac] simplifies finite map expressions -occuring in the conclusion and hypotheses. It uses [tac] to discharge generated -inequalities. *) +(** * Theorems *) +Section theorems. +Context `{FinMap K M}. + +Global Instance map_subseteq {A} : SubsetEq (M A) := λ m1 m2, + ∀ i x, m1 !! i = Some x → m2 !! i = Some x. +Global Instance: BoundedPreOrder (M A). +Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed. +Global Instance : PartialOrder (M A). +Proof. + split; [apply _ |]. + intros ????. apply map_eq. intros i. apply option_eq. naive_solver. +Qed. + +Lemma lookup_weaken {A} (m1 m2 : M A) i x : + m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x. +Proof. auto. Qed. +Lemma lookup_weaken_is_Some {A} (m1 m2 : M A) i : + is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i). +Proof. inversion 1. eauto using lookup_weaken. Qed. +Lemma lookup_weaken_None {A} (m1 m2 : M A) i : + m2 !! i = None → m1 ⊆ m2 → m1 !! i = None. +Proof. + rewrite eq_None_not_Some. intros Hm2 Hm1m2. + specialize (Hm1m2 i). destruct (m1 !! i); naive_solver. +Qed. + +Lemma lookup_weaken_inv {A} (m1 m2 : M A) i x y : + m1 !! i = Some x → + m1 ⊆ m2 → + m2 !! i = Some y → + x = y. +Proof. + intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. + congruence. +Qed. + +Lemma lookup_ne {A} (m : M A) i j : m !! i ≠m !! j → i ≠j. +Proof. congruence. Qed. +Lemma map_empty {A} (m : M A) : (∀ i, m !! i = None) → m = ∅. +Proof. intros Hm. apply map_eq. intros. by rewrite Hm, lookup_empty. Qed. +Lemma lookup_empty_is_Some {A} i : ¬is_Some ((∅ : M A) !! i). +Proof. rewrite lookup_empty. by inversion 1. Qed. +Lemma lookup_empty_Some {A} i (x : A) : ¬∅ !! i = Some x. +Proof. by rewrite lookup_empty. Qed. + +Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅. +Proof. intros [? []]. intros i x. by rewrite lookup_empty. Qed. + +(** ** Properties of the [partial_alter] operation *) +Lemma partial_alter_compose {A} (m : M A) i f g : + partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m). +Proof. + intros. apply map_eq. intros ii. case (decide (i = ii)). + * intros. subst. by rewrite !lookup_partial_alter. + * intros. by rewrite !lookup_partial_alter_ne. +Qed. +Lemma partial_alter_commute {A} (m : M A) i j f g : + i ≠j → + partial_alter f i (partial_alter g j m) = + partial_alter g j (partial_alter f i m). +Proof. + intros. apply map_eq. intros jj. + destruct (decide (jj = j)). + * subst. by rewrite lookup_partial_alter_ne, + !lookup_partial_alter, lookup_partial_alter_ne. + * destruct (decide (jj = i)). + + subst. by rewrite lookup_partial_alter, + !lookup_partial_alter_ne, lookup_partial_alter by congruence. + + by rewrite !lookup_partial_alter_ne by congruence. +Qed. +Lemma partial_alter_self_alt {A} (m : M A) i x : + x = m !! i → partial_alter (λ _, x) i m = m. +Proof. + intros. apply map_eq. intros ii. + destruct (decide (i = ii)). + * subst. by rewrite lookup_partial_alter. + * by rewrite lookup_partial_alter_ne. +Qed. +Lemma partial_alter_self {A} (m : M A) i : + partial_alter (λ _, m !! i) i m = m. +Proof. by apply partial_alter_self_alt. Qed. + +Lemma partial_alter_subseteq {A} (m : M A) i f : + m !! i = None → + m ⊆ partial_alter f i m. +Proof. + intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. +Qed. +Lemma partial_alter_subset {A} (m : M A) i f : + m !! i = None → + is_Some (f (m !! i)) → + m ⊂ partial_alter f i m. +Proof. + intros Hi Hfi. split. + * by apply partial_alter_subseteq. + * inversion Hfi as [x Hx]. intros Hm. + apply (Some_ne_None x). rewrite <-(Hm i x); [done|]. + by rewrite lookup_partial_alter. +Qed. + +(** ** Properties of the [alter] operation *) +Lemma lookup_alter {A} (f : A → A) m i : + alter f i m !! i = f <$> m !! i. +Proof. apply lookup_partial_alter. Qed. +Lemma lookup_alter_ne {A} (f : A → A) m i j : + i ≠j → alter f i m !! j = m !! j. +Proof. apply lookup_partial_alter_ne. Qed. + +Lemma lookup_alter_Some {A} (f : A → A) m i j y : + alter f i m !! j = Some y ↔ + (i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠j ∧ m !! j = Some y). +Proof. + destruct (decide (i = j)); subst. + * rewrite lookup_alter. naive_solver (simplify_option_equality; eauto). + * rewrite lookup_alter_ne by done. naive_solver. +Qed. +Lemma lookup_alter_None {A} (f : A → A) m i j : + alter f i m !! j = None ↔ m !! j = None. +Proof. + destruct (decide (i = j)); subst. + * by rewrite lookup_alter, fmap_None. + * by rewrite lookup_alter_ne. +Qed. + +Lemma alter_None {A} (f : A → A) m i : + m !! i = None → alter f i m = m. +Proof. + intros Hi. apply map_eq. intros j. destruct (decide (i = j)); subst. + * by rewrite lookup_alter, !Hi. + * by rewrite lookup_alter_ne. +Qed. + +(** ** Properties of the [delete] operation *) +Lemma lookup_delete {A} (m : M A) i : delete i m !! i = None. +Proof. apply lookup_partial_alter. Qed. +Lemma lookup_delete_ne {A} (m : M A) i j : i ≠j → delete i m !! j = m !! j. +Proof. apply lookup_partial_alter_ne. Qed. + +Lemma lookup_delete_Some {A} (m : M A) i j y : + delete i m !! j = Some y ↔ i ≠j ∧ m !! j = Some y. +Proof. + split. + * destruct (decide (i = j)); subst; + rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence. + * intros [??]. by rewrite lookup_delete_ne. +Qed. +Lemma lookup_delete_None {A} (m : M A) i j : + delete i m !! j = None ↔ i = j ∨ m !! j = None. +Proof. + destruct (decide (i = j)). + * subst. rewrite lookup_delete. tauto. + * rewrite lookup_delete_ne; tauto. +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)]} = ∅. +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). +Proof. destruct (decide (i = j)). by subst. by apply partial_alter_commute. Qed. +Lemma delete_insert_ne {A} (m : M A) i j x : + i ≠j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m). +Proof. intro. by apply partial_alter_commute. Qed. + +Lemma delete_notin {A} (m : M A) i : + m !! i = None → delete i m = m. +Proof. + intros. apply map_eq. intros j. + destruct (decide (i = j)). + * subst. by rewrite lookup_delete. + * by apply lookup_delete_ne. +Qed. + +Lemma delete_partial_alter {A} (m : M A) i f : + m !! i = None → delete i (partial_alter f i m) = m. +Proof. + intros. unfold delete, map_delete. rewrite <-partial_alter_compose. + unfold compose. by apply partial_alter_self_alt. +Qed. +Lemma delete_insert {A} (m : M A) i x : + m !! i = None → delete i (<[i:=x]>m) = m. +Proof. apply delete_partial_alter. Qed. +Lemma insert_delete {A} (m : M A) i x : + m !! i = Some x → <[i:=x]>(delete i m) = m. +Proof. + intros Hmi. unfold delete, map_delete, insert, map_insert. + rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi. + by apply partial_alter_self_alt. +Qed. + +Lemma delete_subseteq {A} (m : M A) i : + delete i m ⊆ m. +Proof. intros j x. rewrite lookup_delete_Some. tauto. Qed. +Lemma delete_subseteq_compat {A} (m1 m2 : M A) i : + m1 ⊆ m2 → + delete i m1 ⊆ delete i m2. +Proof. intros ? j x. rewrite !lookup_delete_Some. intuition eauto. Qed. +Lemma delete_subset_alt {A} (m : M A) i x : + m !! i = Some x → + delete i m ⊂ m. +Proof. + split. + * apply delete_subseteq. + * intros Hi. apply (None_ne_Some x). + by rewrite <-(lookup_delete m i), (Hi i x). +Qed. +Lemma delete_subset {A} (m : M A) i : + is_Some (m !! i) → + delete i m ⊂ m. +Proof. inversion 1. eauto using delete_subset_alt. Qed. + +(** ** Properties of the [insert] operation *) +Lemma lookup_insert {A} (m : M A) i x : <[i:=x]>m !! i = Some x. +Proof. unfold insert. apply lookup_partial_alter. Qed. +Lemma lookup_insert_rev {A} (m : M A) i x y : + <[i:=x]>m !! i = Some y → x = y. +Proof. rewrite lookup_insert. congruence. Qed. +Lemma lookup_insert_ne {A} (m : M A) i j x : + i ≠j → <[i:=x]>m !! j = m !! j. +Proof. unfold insert. apply lookup_partial_alter_ne. Qed. +Lemma insert_commute {A} (m : M A) i j x y : + i ≠j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m). +Proof. apply partial_alter_commute. Qed. + +Lemma lookup_insert_Some {A} (m : M A) i j x y : + <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠j ∧ m !! j = Some y). +Proof. + split. + * destruct (decide (i = j)); subst; + rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. + * intros [[??]|[??]]. + + subst. apply lookup_insert. + + by rewrite lookup_insert_ne. +Qed. +Lemma lookup_insert_None {A} (m : M A) i j x : + <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠j. +Proof. + split. + * destruct (decide (i = j)); subst; + rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. + * intros [??]. by rewrite lookup_insert_ne. +Qed. + +Lemma insert_subseteq {A} (m : M A) i x : + m !! i = None → + m ⊆ <[i:=x]>m. +Proof. apply partial_alter_subseteq. Qed. +Lemma insert_subset {A} (m : M A) i x : + m !! i = None → + m ⊂ <[i:=x]>m. +Proof. intro. apply partial_alter_subset; eauto. Qed. +Lemma insert_subseteq_r {A} (m1 m2 : M A) i x : + m1 !! i = None → + m1 ⊆ m2 → + m1 ⊆ <[i:=x]>m2. +Proof. + intros ?? j ?. destruct (decide (j = i)); subst. + * congruence. + * rewrite lookup_insert_ne; auto. +Qed. + +Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x : + m1 !! i = None → + <[i:=x]> m1 ⊆ m2 → + m1 ⊆ delete i m2. +Proof. + intros Hi Hix j y Hj. destruct (decide (i = j)); subst. + * congruence. + * rewrite lookup_delete_ne by done. apply Hix. + by rewrite lookup_insert_ne by done. +Qed. +Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x : + m1 !! i = Some x → + delete i m1 ⊆ m2 → + m1 ⊆ <[i:=x]> m2. +Proof. + intros Hix Hi j y Hj. destruct (decide (i = j)); subst. + * rewrite lookup_insert. congruence. + * rewrite lookup_insert_ne by done. apply Hi. + by rewrite lookup_delete_ne. +Qed. + +Lemma insert_delete_subset {A} (m1 m2 : M A) i x : + m1 !! i = None → + <[i:=x]> m1 ⊂ m2 → + m1 ⊂ delete i m2. +Proof. + intros ? [Hm12 Hm21]. split. + * eauto using insert_delete_subseteq. + * contradict Hm21. apply delete_insert_subseteq; auto. + apply Hm12. by rewrite lookup_insert. +Qed. + +Lemma insert_subset_inv {A} (m1 m2 : M A) i x : + m1 !! i = None → + <[i:=x]> m1 ⊂ m2 → + ∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None. +Proof. + intros Hi Hm1m2. exists (delete i m2). split_ands. + * rewrite insert_delete. done. + eapply lookup_weaken, subset_subseteq; eauto. + by rewrite lookup_insert. + * eauto using insert_delete_subset. + * by rewrite lookup_delete. +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. +Proof. + unfold singleton, map_singleton. + rewrite lookup_insert_Some, lookup_empty. simpl. + 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. +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 insert_singleton {A} i (x y : A) : <[i:=y]>{[(i, x)]} = {[(i, y)]}. +Proof. + unfold singleton, 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) ]}. +Proof. + intros. apply map_eq. intros i'. destruct (decide (i = i')); subst. + * 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) ]}. +Proof. + intros. apply map_eq. intros i'. destruct (decide (i = i')); subst. + * by rewrite lookup_alter, lookup_singleton_ne. + * by rewrite lookup_alter_ne. +Qed. + +(** ** Properties of conversion to lists *) +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 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. + induction l as [|[j y] l IH]; simpl. + { by rewrite elem_of_nil. } + rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap. + intros [Hl ?] [?|?]; simplify_equality. + { by rewrite lookup_insert. } + destruct (decide (i = j)); simplify_equality. + * destruct Hl. by exists (j,x). + * rewrite lookup_insert_ne; auto. +Qed. +Lemma elem_of_map_of_list_2 {A} (l : list (K * A)) i x : + map_of_list l !! i = Some x → + (i,x) ∈ l. +Proof. + induction l as [|[j y] l IH]; simpl. + { by rewrite lookup_empty. } + rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality. + * rewrite lookup_insert; intuition congruence. + * rewrite lookup_insert_ne; intuition congruence. +Qed. +Lemma elem_of_map_of_list {A} (l : list (K * A)) i x : + NoDup (fst <$> l) → + (i,x) ∈ l ↔ map_of_list l !! i = Some x. +Proof. + split; auto using elem_of_map_of_list_1, elem_of_map_of_list_2. +Qed. + +Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i : + i ∉ fst <$> l → + map_of_list l !! i = None. +Proof. + rewrite elem_of_list_fmap, eq_None_not_Some, is_Some_alt. + intros Hi [x ?]. destruct Hi. exists (i,x). simpl. + auto using elem_of_map_of_list_2. +Qed. +Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i : + map_of_list l !! i = None → + i ∉ fst <$> l. +Proof. + induction l as [|[j y] l IH]; simpl. + { rewrite elem_of_nil. tauto. } + rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality. + * by rewrite lookup_insert. + * by rewrite lookup_insert_ne; intuition. +Qed. +Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i : + i ∉ fst <$> l ↔ map_of_list l !! i = None. +Proof. + split; auto using not_elem_of_map_of_list_1, + not_elem_of_map_of_list_2. +Qed. + +Lemma map_of_list_proper {A} (l1 l2 : list (K * A)) : + NoDup (fst <$> l1) → + Permutation l1 l2 → + map_of_list l1 = map_of_list l2. +Proof. + intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x. + by rewrite <-!elem_of_map_of_list; rewrite <-?Hperm. +Qed. +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 → + Permutation l1 l2. +Proof. + 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. +Qed. +Lemma map_to_of_list {A} (l : list (K * A)) : + NoDup (fst <$> l) → + Permutation (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. +Lemma map_to_list_inj {A} (m1 m2 : M A) : + Permutation (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. +Qed. + +Lemma map_to_list_empty {A} : + map_to_list ∅ = @nil (K * A). +Proof. + apply elem_of_nil_inv. intros [i x]. + rewrite elem_of_map_to_list. apply lookup_empty_Some. +Qed. +Lemma map_to_list_insert {A} (m : M A) i x : + m !! i = None → + Permutation (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. + 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. +Qed. + +Lemma map_of_list_nil {A} : + map_of_list (@nil (K * A)) = ∅. +Proof. done. Qed. +Lemma map_of_list_cons {A} (l : list (K * A)) i x : + map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l). +Proof. done. Qed. + +Lemma map_to_list_empty_inv_alt {A} (m : M A) : + Permutation (map_to_list m) [] → m = ∅. +Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed. +Lemma map_to_list_empty_inv {A} (m : M A) : + map_to_list m = [] → m = ∅. +Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed. + +Lemma map_to_list_insert_inv {A} (m : M A) l i x : + Permutation (map_to_list m) ((i,x) :: l) → + m = <[i:=x]>(map_of_list l). +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. } + 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. + +(** * Induction principles *) +Lemma map_ind {A} (P : M A → Prop) : + P ∅ → + (∀ i x m, m !! i = None → P m → P (<[i:=x]>m)) → + ∀ m, P m. +Proof. + intros Hemp Hins. + cut (∀ l, NoDup (fst <$> l) → ∀ m, Permutation (map_to_list m) l → P m). + { intros help m. + apply (help (map_to_list m)); auto using map_to_list_key_nodup. } + 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. + apply map_to_list_insert_inv in Hml. subst. apply Hins. + * by apply not_elem_of_map_of_list_1. + * apply IH; auto using map_to_of_list. +Qed. + +Lemma map_to_list_length {A} (m1 m2 : M A) : + m1 ⊂ m2 → + length (map_to_list m1) < length (map_to_list m2). +Proof. + revert m2. induction m1 as [|i x m ? IH] using map_ind. + { intros m2 Hm2. rewrite map_to_list_empty. simpl. + apply neq_0_lt. intros Hlen. symmetry in Hlen. + apply nil_length, map_to_list_empty_inv in Hlen. + rewrite Hlen in Hm2. destruct (irreflexivity (⊂) ∅ Hm2). } + intros m2 Hm2. + destruct (insert_subset_inv m m2 i x) as (m2'&?&?&?); auto; subst. + rewrite !map_to_list_insert; simpl; auto with arith. +Qed. + +Lemma map_wf {A} : wf (@subset (M A) _). +Proof. + apply (wf_projected (<) (length ∘ map_to_list)). + * by apply map_to_list_length. + * by apply lt_wf. +Qed. + +(** ** Properties of the [map_forall] predicate *) +Section map_forall. +Context {A} (P : K → A → Prop). + +Lemma map_forall_to_list m : + map_forall P m ↔ Forall (curry P) (map_to_list m). +Proof. + rewrite Forall_forall. split. + * intros Hforall [i x]. + rewrite elem_of_map_to_list. by apply (Hforall i x). + * intros Hforall i x. + rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)). +Qed. + +Context `{∀ i x, Decision (P i x)}. +Global Instance map_forall_dec m : Decision (map_forall P m). +Proof. + refine (cast_if (decide (Forall (curry P) (map_to_list m)))); + by rewrite map_forall_to_list. +Defined. + +Lemma map_not_forall (m : M A) : + ¬map_forall P m ↔ ∃ i x, m !! i = Some x ∧ ¬P i x. +Proof. + split. + * rewrite map_forall_to_list. intros Hm. + apply (not_Forall_Exists _), Exists_exists in Hm. + destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list. + * intros (i&x&?&?) Hm. specialize (Hm i x). tauto. +Qed. +End map_forall. + +(** ** Properties of the [merge] operation *) +Lemma merge_Some {A B C} (f : option A → option B → option C) + `{!PropHolds (f None None = None)} m1 m2 m : + (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m. +Proof. + split; [| intro; subst; apply (lookup_merge _) ]. + intros Hlookup. apply map_eq. intros. rewrite Hlookup. + apply (lookup_merge _). +Qed. + +Section merge. +Context {A} (f : option A → option A → option A). + +Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f). +Proof. + intros ??. apply map_eq. intros. + by rewrite !(lookup_merge f), lookup_empty, (left_id None f). +Qed. +Global Instance: RightId (=) None f → RightId (=) ∅ (merge f). +Proof. + intros ??. apply map_eq. intros. + by rewrite !(lookup_merge f), lookup_empty, (right_id None f). +Qed. + +Context `{!PropHolds (f None None = None)}. + +Lemma merge_commutative m1 m2 : + (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → + merge f m1 m2 = merge f m2 m1. +Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. +Global Instance: Commutative (=) f → Commutative (=) (merge f). +Proof. + intros ???. apply merge_commutative. intros. by apply (commutative f). +Qed. +Lemma merge_associative m1 m2 m3 : + (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = + f (f (m1 !! i) (m2 !! i)) (m3 !! i)) → + merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3. +Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. +Global Instance: Associative (=) f → Associative (=) (merge f). +Proof. + intros ????. apply merge_associative. intros. by apply (associative f). +Qed. +Lemma merge_idempotent m1 : + (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → + merge f m1 m1 = m1. +Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. +Global Instance: Idempotent (=) f → Idempotent (=) (merge f). +Proof. + intros ??. apply merge_idempotent. intros. by apply (idempotent f). +Qed. + +Lemma partial_alter_merge (g g1 g2 : option A → option A) m1 m2 i : + g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (g2 (m2 !! i)) → + partial_alter g i (merge f m1 m2) = + merge f (partial_alter g1 i m1) (partial_alter g2 i m2). +Proof. + intro. apply map_eq. intros j. destruct (decide (i = j)); subst. + * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _). + * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _). +Qed. +Lemma partial_alter_merge_l (g g1 : option A → option A) m1 m2 i : + g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) → + partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2. +Proof. + intro. apply map_eq. intros j. destruct (decide (i = j)); subst. + * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _). + * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _). +Qed. +Lemma partial_alter_merge_r (g g2 : option A → option A) m1 m2 i : + g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) → + partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2). +Proof. + intro. apply map_eq. intros j. destruct (decide (i = j)); subst. + * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _). + * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _). +Qed. + +Lemma insert_merge_l m1 m2 i x : + f (Some x) (m2 !! i) = Some x → + <[i:=x]>(merge f m1 m2) = merge f (<[i:=x]>m1) m2. +Proof. + intros. unfold insert, map_insert, alter, map_alter. + by apply partial_alter_merge_l. +Qed. +Lemma insert_merge_r m1 m2 i x : + f (m1 !! i) (Some x) = Some x → + <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=x]>m2). +Proof. + intros. unfold insert, map_insert, alter, map_alter. + by apply partial_alter_merge_r. +Qed. +End merge. + +(** ** Properties on the [map_intersection_forall] relation *) +Section intersection_forall. +Context {A} (R : relation A). + +Global Instance map_intersection_forall_sym: + Symmetric R → Symmetric (map_intersection_forall R). +Proof. firstorder auto. Qed. +Lemma map_intersection_forall_empty_l (m : M A) : + map_intersection_forall R ∅ m. +Proof. intros ???. by rewrite lookup_empty. Qed. +Lemma map_intersection_forall_empty_r (m : M A) : + map_intersection_forall R m ∅. +Proof. intros ???. by rewrite lookup_empty. Qed. + +Lemma map_intersection_forall_alt (m1 m2 : M A) : + map_intersection_forall R m1 m2 ↔ + map_forall (λ _, curry R) (merge (λ x y, + match x, y with + | Some x, Some y => Some (x,y) + | _, _ => None + end) m1 m2). +Proof. + split. + * intros Hm12 i [x y]. rewrite lookup_merge by done. intros. + destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simplify_equality. + eapply Hm12; eauto. + * intros Hm12 i x y ??. apply (Hm12 i (x,y)). + rewrite lookup_merge by done. by simplify_option_equality. +Qed. + +(** Due to the finiteness of finite maps, we can extract a witness if the +relation does not hold. *) +Lemma map_not_intersection_forall `{∀ x y, Decision (R x y)} (m1 m2 : M A) : + ¬map_intersection_forall R m1 m2 + ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ ¬R x1 x2. +Proof. + split. + * rewrite map_intersection_forall_alt, (map_not_forall _). + intros (i & [x y] & Hm12 & ?). rewrite lookup_merge in Hm12 by done. + exists i x y. by destruct (m1 !! i), (m2 !! i); simplify_equality. + * intros (i & x1 & x2 & Hx1 & Hx2 & Hx1x2) Hm12. + by apply Hx1x2, (Hm12 i x1 x2). +Qed. +End intersection_forall. + +(** ** Properties on the disjoint maps *) +Lemma map_disjoint_alt {A} (m1 m2 : M A) : + m1 ⊥ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None. +Proof. + split; intros Hm1m2 i; specialize (Hm1m2 i); + destruct (m1 !! i), (m2 !! i); naive_solver. +Qed. +Lemma map_not_disjoint {A} (m1 m2 : M A) : + ¬m1 ⊥ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2. +Proof. + unfold disjoint, map_disjoint. + rewrite map_not_intersection_forall. + * naive_solver. + * right. auto. +Qed. + +Global Instance: Symmetric (@disjoint (M A) _). +Proof. intro. apply map_intersection_forall_sym. auto. Qed. +Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ⊥ m. +Proof. apply map_intersection_forall_empty_l. Qed. +Lemma map_disjoint_empty_r {A} (m : M A) : m ⊥ ∅. +Proof. apply map_intersection_forall_empty_r. Qed. + +Lemma map_disjoint_weaken {A} (m1 m1' m2 m2' : M A) : + m1' ⊥ m2' → + m1 ⊆ m1' → m2 ⊆ m2' → + m1 ⊥ m2. +Proof. + intros Hdisjoint Hm1 Hm2 i x1 x2 Hx1 Hx2. + destruct (Hdisjoint i x1 x2); auto. +Qed. +Lemma map_disjoint_weaken_l {A} (m1 m1' m2 : M A) : + m1' ⊥ m2 → m1 ⊆ m1' → m1 ⊥ m2. +Proof. eauto using map_disjoint_weaken. Qed. +Lemma map_disjoint_weaken_r {A} (m1 m2 m2' : M A) : + m1 ⊥ m2' → m2 ⊆ m2' → m1 ⊥ m2. +Proof. eauto using map_disjoint_weaken. Qed. + +Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x: + m1 ⊥ m2 → + m1 !! i = Some x → + m2 !! i = None. +Proof. + intros Hdisjoint ?. rewrite eq_None_not_Some, is_Some_alt. + intros [x2 ?]. by apply (Hdisjoint i x x2). +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 (⊥)). apply map_disjoint_Some_l. Qed. + +Lemma map_disjoint_singleton_l {A} (m : M A) i x : + {[(i, x)]} ⊥ m ↔ m !! i = None. +Proof. + split. + * intro. apply (map_disjoint_Some_l {[(i, x)]} _ _ x); + auto using lookup_singleton. + * intros ? j y1 y2. destruct (decide (i = j)); subst. + + 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. +Proof. by rewrite (symmetry_iff (⊥)), map_disjoint_singleton_l. Qed. + +Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x : + 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)]}. +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. + rewrite !map_disjoint_alt. + intros Hdisjoint j. destruct (Hdisjoint j); auto. + rewrite lookup_delete_None. tauto. +Qed. +Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : + m1 ⊥ m2 → m1 ⊥ delete i m2. +Proof. symmetry. by apply map_disjoint_delete_l. Qed. + +(** ** Properties of the [union_with] operation *) +Section union_with. +Context {A} (f : A → A → option A). + +Lemma lookup_union_with m1 m2 i z : + union_with f m1 m2 !! i = z ↔ + (m1 !! i = None ∧ m2 !! i = None ∧ z = None) ∨ + (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ z = Some x) ∨ + (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ z = Some y) ∨ + (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ z = f x y). +Proof. + unfold union_with, map_union_with. rewrite (lookup_merge _). + destruct (m1 !! i), (m2 !! i); compute; naive_solver. +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. naive_solver. Qed. +Lemma lookup_union_with_None m1 m2 i : + union_with f m1 m2 !! i = None ↔ + (m1 !! i = None ∧ m2 !! i = None) ∨ + (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = None). +Proof. rewrite lookup_union_with. naive_solver. Qed. + +Lemma lookup_union_with_Some_lr m1 m2 i x y z : + m1 !! i = Some x → + m2 !! i = Some y → + f x y = Some z → + union_with f m1 m2 !! i = Some z. +Proof. rewrite lookup_union_with. naive_solver. Qed. +Lemma lookup_union_with_Some_l m1 m2 i x : + m1 !! i = Some x → + m2 !! i = None → + union_with f m1 m2 !! i = Some x. +Proof. rewrite lookup_union_with. naive_solver. Qed. +Lemma lookup_union_with_Some_r m1 m2 i y : + m1 !! i = None → + m2 !! i = Some y → + union_with f m1 m2 !! i = Some y. +Proof. rewrite lookup_union_with. 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). +Proof. unfold union_with, map_union_with. apply _. Qed. + +Lemma union_with_commutative m1 m2 : + (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) → + union_with f m1 m2 = union_with f m2 m1. +Proof. + intros. apply (merge_commutative _). intros i. + destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto. +Qed. +Global Instance: Commutative (=) f → Commutative (@eq (M A)) (union_with f). +Proof. intros ???. apply union_with_commutative. eauto. Qed. + +Lemma union_with_idempotent m : + (∀ i x, m !! i = Some x → f x x = Some x) → + union_with f m m = m. +Proof. + intros. apply (merge_idempotent _). intros i. + destruct (m !! i) eqn:?; simpl; eauto. +Qed. + +Lemma alter_union_with (g : A → A) m1 m2 i : + (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) (g y)) → + alter g i (union_with f m1 m2) = + union_with f (alter g i m1) (alter g i m2). +Proof. + intros. apply (partial_alter_merge _). + destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto. +Qed. +Lemma alter_union_with_l (g : A → A) m1 m2 i : + (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) y) → + (∀ y, m1 !! i = None → m2 !! i = Some y → g y = y) → + alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2. +Proof. + intros. apply (partial_alter_merge_l _). + destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto using f_equal. +Qed. +Lemma alter_union_with_r (g : A → A) m1 m2 i : + (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f x (g y)) → + (∀ x, m1 !! i = Some x → m2 !! i = None → g x = x) → + alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2). +Proof. + intros. apply (partial_alter_merge_r _). + destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto using f_equal. +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). +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) → + <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=x]>m2). +Proof. intros. apply (partial_alter_merge _). simpl. auto. Qed. +Lemma insert_union_with_l m1 m2 i x : + m2 !! i = None → + <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) m2. +Proof. + intros Hm2. unfold union_with, map_union_with. + rewrite (insert_merge_l _). done. by rewrite Hm2. +Qed. +Lemma insert_union_with_r m1 m2 i x : + m1 !! i = None → + <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2). +Proof. + intros Hm1. unfold union_with, map_union_with. + rewrite (insert_merge_r _). done. by rewrite Hm1. +Qed. +End union_with. + +(** ** Properties of the [union] operation *) +Global Instance: LeftId (@eq (M A)) ∅ (∪) := _. +Global Instance: RightId (@eq (M A)) ∅ (∪) := _. +Global Instance: Associative (@eq (M A)) (∪). +Proof. + intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with. + apply (merge_associative _). intros i. + by destruct (m1 !! i), (m2 !! i), (m3 !! i). +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). +Proof. + unfold union, map_union, union_with, map_union_with. + rewrite (lookup_merge _). + destruct (m1 !! i), (m2 !! i); compute; intuition congruence. +Qed. +Lemma lookup_union_None {A} (m1 m2 : M A) i : + (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None. +Proof. + unfold union, map_union, union_with, map_union_with. + rewrite (lookup_merge _). + destruct (m1 !! i), (m2 !! i); compute; intuition congruence. +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. + intros Hdisjoint. rewrite lookup_union_Some_raw. + intuition eauto using map_disjoint_Some_r. +Qed. + +Lemma lookup_union_Some_l {A} (m1 m2 : M A) i x : + m1 !! i = Some x → + (m1 ∪ m2) !! i = Some x. +Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed. +Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x : + m1 ⊥ m2 → + m2 !! i = Some x → + (m1 ∪ m2) !! i = Some x. +Proof. intro. rewrite lookup_union_Some; intuition. Qed. + +Lemma map_union_commutative {A} (m1 m2 : M A) : + m1 ⊥ m2 → + m1 ∪ m2 = m2 ∪ m1. +Proof. + intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))). + intros i. specialize (Hdisjoint i). + destruct (m1 !! i), (m2 !! i); compute; naive_solver. +Qed. + +Lemma map_subseteq_union {A} (m1 m2 : M A) : + m1 ⊆ m2 → + m1 ∪ m2 = m2. +Proof. + intros Hm1m2. + apply map_eq. intros i. apply option_eq. intros x. + rewrite lookup_union_Some_raw. split; [by intuition |]. + intros Hm2. specialize (Hm1m2 i). + destruct (m1 !! i) as [y|]; [| by auto]. + rewrite (Hm1m2 y eq_refl) in Hm2. intuition congruence. +Qed. + +Lemma map_union_subseteq_l {A} (m1 m2 : M A) : + m1 ⊆ m1 ∪ m2. +Proof. intros ? i x. rewrite lookup_union_Some_raw. intuition. Qed. +Lemma map_union_subseteq_r {A} (m1 m2 : M A) : + m1 ⊥ m2 → + m2 ⊆ m1 ∪ m2. +Proof. + intros. rewrite map_union_commutative by done. + by apply map_union_subseteq_l. +Qed. + +Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : + m1 ⊆ m2 → + m1 ⊆ m2 ∪ m3. +Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed. +Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) : + m2 ⊥ m3 → + m1 ⊆ m3 → + m1 ⊆ m2 ∪ m3. +Proof. intros. transitivity m3; auto using map_union_subseteq_r. Qed. + +Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : + m1 ⊆ m2 → + m3 ∪ m1 ⊆ m3 ∪ m2. +Proof. intros ???. rewrite !lookup_union_Some_raw. naive_solver. Qed. +Lemma map_union_preserving_r {A} (m1 m2 m3 : M A) : + m2 ⊥ m3 → + m1 ⊆ m2 → + m1 ∪ m3 ⊆ m2 ∪ m3. +Proof. + intros. rewrite !(map_union_commutative _ m3) + by eauto using map_disjoint_weaken_l. + by apply map_union_preserving_l. +Qed. + +Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) : + m3 ⊥ m1 → + m3 ⊥ m2 → + m3 ∪ m1 ⊆ m3 ∪ m2 → + m1 ⊆ m2. +Proof. + intros Hm3m1 Hm3m2 E b x ?. + specialize (E b x). rewrite !lookup_union_Some in E by done. + destruct E; auto. by destruct (Hm3m1 b x x). +Qed. +Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) : + m1 ⊥ m3 → + m2 ⊥ m3 → + m1 ∪ m3 ⊆ m2 ∪ m3 → + m1 ⊆ m2. +Proof. + intros ??. rewrite !(map_union_commutative _ m3) by done. + by apply map_union_reflecting_l. +Qed. + +Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) : + m1 ⊥ m3 → + m2 ⊥ m3 → + m3 ∪ m1 = m3 ∪ m2 → + m1 = m2. +Proof. + intros. by apply (anti_symmetric _); + apply map_union_reflecting_l with m3; auto with congruence. +Qed. +Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) : + m1 ⊥ m3 → + m2 ⊥ m3 → + m1 ∪ m3 = m2 ∪ m3 → + m1 = m2. +Proof. + intros. apply (anti_symmetric _); + apply map_union_reflecting_r with m3; auto with congruence. +Qed. + +Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) : + m1 ∪ m2 ⊥ m3 ↔ m1 ⊥ m3 ∧ m2 ⊥ m3. +Proof. + rewrite !map_disjoint_alt. + setoid_rewrite lookup_union_None. naive_solver. +Qed. +Lemma map_disjoint_union_r {A} (m1 m2 m3 : M A) : + m1 ⊥ m2 ∪ m3 ↔ m1 ⊥ m2 ∧ m1 ⊥ m3. +Proof. + rewrite !map_disjoint_alt. + setoid_rewrite lookup_union_None. naive_solver. +Qed. +Lemma map_disjoint_union_l_2 {A} (m1 m2 m3 : M A) : + m1 ⊥ m3 → m2 ⊥ m3 → m1 ∪ m2 ⊥ m3. +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. +Proof. + apply map_eq. intros j. apply option_eq. intros y. + rewrite lookup_union_Some_raw. + destruct (decide (i = j)); subst. + * rewrite !lookup_singleton, lookup_insert. intuition congruence. + * 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)]}. +Proof. + intro. rewrite insert_union_singleton_l, map_union_commutative; [done |]. + by apply map_disjoint_singleton_l. +Qed. + +Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x : + <[i:=x]>m1 ⊥ m2 ↔ m2 !! i = None ∧ m1 ⊥ m2. +Proof. + rewrite insert_union_singleton_l. + by rewrite map_disjoint_union_l, map_disjoint_singleton_l. +Qed. +Lemma map_disjoint_insert_r {A} (m1 m2 : M A) i x : + m1 ⊥ <[i:=x]>m2 ↔ m1 !! i = None ∧ m1 ⊥ m2. +Proof. + rewrite insert_union_singleton_l. + by rewrite map_disjoint_union_r, map_disjoint_singleton_r. +Qed. + +Lemma map_disjoint_insert_l_2 {A} (m1 m2 : M A) i x : + m2 !! i = None → m1 ⊥ m2 → <[i:=x]>m1 ⊥ m2. +Proof. by rewrite map_disjoint_insert_l. Qed. +Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x : + m1 !! i = None → m1 ⊥ m2 → m1 ⊥ <[i:=x]>m2. +Proof. by rewrite map_disjoint_insert_r. Qed. + +Lemma insert_union_l {A} (m1 m2 : M A) i x : + <[i:=x]>(m1 ∪ m2) = <[i:=x]>m1 ∪ m2. +Proof. by rewrite !insert_union_singleton_l, (associative (∪)). Qed. +Lemma insert_union_r {A} (m1 m2 : M A) i x : + m1 !! i = None → + <[i:=x]>(m1 ∪ m2) = m1 ∪ <[i:=x]>m2. +Proof. + intro. rewrite !insert_union_singleton_l, !(associative (∪)). + 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. +Proof. + induction l; simpl. + * by rewrite (left_id _ _). + * by rewrite IHl, insert_union_l. +Qed. + +Lemma delete_union {A} (m1 m2 : M A) i : + delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2. +Proof. apply delete_union_with. Qed. + +(** ** Properties of the [union_list] operation *) +Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) : + ⋃ ms ⊥ m ↔ Forall (⊥ m) ms. +Proof. + split. + * induction ms; simpl; rewrite ?map_disjoint_union_l; intuition. + * induction 1; simpl. + + apply map_disjoint_empty_l. + + by rewrite map_disjoint_union_l. +Qed. +Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) : + m ⊥ ⋃ ms ↔ Forall (⊥ m) ms. +Proof. by rewrite (symmetry_iff (⊥)), map_disjoint_union_list_l. Qed. + +Lemma map_disjoint_union_list_l_2 {A} (ms : list (M A)) (m : M A) : + Forall (⊥ m) ms → ⋃ ms ⊥ m. +Proof. by rewrite map_disjoint_union_list_l. Qed. +Lemma map_disjoint_union_list_r_2 {A} (ms : list (M A)) (m : M A) : + Forall (⊥ m) ms → m ⊥ ⋃ ms. +Proof. by rewrite map_disjoint_union_list_r. Qed. + +Lemma map_union_sublist {A} (ms1 ms2 : list (M A)) : + list_disjoint ms2 → + sublist ms1 ms2 → + ⋃ ms1 ⊆ ⋃ ms2. +Proof. + intros Hms2. revert ms1. + induction Hms2 as [|m2 ms2]; intros ms1; [by inversion 1|]. + rewrite sublist_cons_r. intros [?|(ms1' &?&?)]; subst; simpl. + * transitivity (⋃ ms2); auto. by apply map_union_subseteq_r. + * 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 _). + rewrite is_Some_alt. + 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. +Proof. + induction 1 as [|i j is]; simpl. + * by rewrite lookup_delete. + * destruct (decide (i = j)). + + subst. by rewrite lookup_delete. + + rewrite lookup_delete_ne; auto. +Qed. +Lemma lookup_delete_list_not_elem_of {A} (m : M A) is j : + j ∉ is → delete_list is m !! j = m !! j. +Proof. + induction is; simpl; [done |]. + rewrite elem_of_cons. intros. + 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. +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). +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. +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. +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. + +(** ** Properties on disjointness of conversion to lists *) +Lemma map_disjoint_of_list_l {A} (m : M A) ixs : + map_of_list ixs ⊥ m ↔ Forall (λ ix, m !! fst ix = None) ixs. +Proof. + split. + * induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition. + * induction 1; simpl. + + apply map_disjoint_empty_l. + + rewrite map_disjoint_insert_l. auto. +Qed. +Lemma map_disjoint_of_list_r {A} (m : M A) ixs : + m ⊥ map_of_list ixs ↔ Forall (λ ix, m !! fst ix = None) ixs. +Proof. by rewrite (symmetry_iff (⊥)), map_disjoint_of_list_l. Qed. + +Lemma map_disjoint_of_list_zip_l {A} (m : M A) is xs : + same_length is xs → + map_of_list (zip is xs) ⊥ m ↔ Forall (λ i, m !! i = None) is. +Proof. + intro. rewrite map_disjoint_of_list_l. + rewrite <-(zip_fst is xs) at 2 by done. + by rewrite Forall_fmap. +Qed. +Lemma map_disjoint_of_list_zip_r {A} (m : M A) is xs : + same_length is xs → + m ⊥ map_of_list (zip is xs) ↔ Forall (λ i, m !! i = None) is. +Proof. + intro. by rewrite (symmetry_iff (⊥)), map_disjoint_of_list_zip_l. +Qed. +Lemma map_disjoint_of_list_zip_l_2 {A} (m : M A) is xs : + same_length is xs → + Forall (λ i, m !! i = None) is → + map_of_list (zip is xs) ⊥ m. +Proof. intro. by rewrite map_disjoint_of_list_zip_l. Qed. +Lemma map_disjoint_of_list_zip_r_2 {A} (m : M A) is xs : + same_length is xs → + Forall (λ i, m !! i = None) is → + m ⊥ map_of_list (zip is xs). +Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed. + +(** ** Properties with respect to vectors *) +Lemma union_delete_vec {A n} (ms : vec (M A) n) (i : fin n) : + list_disjoint ms → + ms !!! i ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms) = ⋃ ms. +Proof. + induction ms as [|m ? ms]; inversion_clear 1; + inv_fin i; simpl; [done | intros i]. + rewrite (map_union_commutative m), (associative_eq _ _), IHms. + * by rewrite map_union_commutative. + * done. + * apply map_disjoint_weaken_r with (⋃ ms); [done |]. + apply map_union_sublist; auto using sublist_delete. +Qed. + +Lemma union_insert_vec {A n} (ms : vec (M A) n) (i : fin n) m : + m ⊥ ⋃ delete (fin_to_nat i) (vec_to_list ms) → + ⋃ vinsert i m ms = m ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms). +Proof. + induction ms as [|m' ? ms IH]; + inv_fin i; simpl; [done | intros i Hdisjoint]. + rewrite map_disjoint_union_r in Hdisjoint. + rewrite IH, !(associative_eq (∪)), (map_union_commutative m); intuition. +Qed. + +(** ** Properties of the [difference_with] operation *) +Section difference_with. +Context {A} (f : A → A → option A). + +Lemma lookup_difference_with m1 m2 i z : + difference_with f m1 m2 !! i = z ↔ + (m1 !! i = None ∧ z = None) ∨ + (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ z = Some x) ∨ + (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ z = f x y). +Proof. + unfold difference_with, map_difference_with. rewrite (lookup_merge _). + destruct (m1 !! i), (m2 !! i); compute; naive_solver. +Qed. +Lemma lookup_difference_with_Some m1 m2 i z : + difference_with f m1 m2 !! i = Some z ↔ + (m1 !! i = Some z ∧ m2 !! i = None) ∨ + (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z). +Proof. rewrite lookup_difference_with. naive_solver. Qed. +Lemma lookup_difference_with_None m1 m2 i : + difference_with f m1 m2 !! i = None ↔ + (m1 !! i = None) ∨ + (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = None). +Proof. rewrite lookup_difference_with. naive_solver. Qed. + +Lemma lookup_difference_with_Some_lr m1 m2 i x y z : + m1 !! i = Some x → + m2 !! i = Some y → + f x y = Some z → + difference_with f m1 m2 !! i = Some z. +Proof. rewrite lookup_difference_with. naive_solver. Qed. +Lemma lookup_difference_with_None_lr m1 m2 i x y : + m1 !! i = Some x → + m2 !! i = Some y → + f x y = None → + difference_with f m1 m2 !! i = None. +Proof. rewrite lookup_difference_with. naive_solver. Qed. +Lemma lookup_difference_with_Some_l m1 m2 i x : + m1 !! i = Some x → + m2 !! i = None → + difference_with f m1 m2 !! i = Some x. +Proof. rewrite lookup_difference_with. naive_solver. Qed. +End difference_with. + +(** ** Properties of the [difference] operation *) +Lemma lookup_difference_Some {A} (m1 m2 : M A) i x : + (m1 ∖ m2) !! i = Some x ↔ m1 !! i = Some x ∧ m2 !! i = None. +Proof. + unfold difference, map_difference, difference_with, map_difference_with. + rewrite (lookup_merge _). + destruct (m1 !! i), (m2 !! i); compute; intuition congruence. +Qed. + +Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : + m1 ⊆ m2 → + m2 ∖ m1 ⊥ m1. +Proof. + intros E i. specialize (E i). + unfold difference, map_difference. intros x1 x2. + rewrite lookup_difference_with_Some. intros [?| (?&?&?&?&?)] ?. + * specialize (E x2). intuition congruence. + * done. +Qed. +Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : + m1 ⊆ m2 → + m1 ⊥ m2 ∖ m1. +Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed. + +Lemma map_difference_union {A} (m1 m2 : M A) : + m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2. +Proof. + intro Hm1m2. apply map_eq. intros i. + apply option_eq. intros v. specialize (Hm1m2 i). + unfold difference, map_difference, + difference_with, map_difference_with. + rewrite lookup_union_Some_raw, (lookup_merge _). + destruct (m1 !! i) as [v'|], (m2 !! i); + try specialize (Hm1m2 v'); compute; intuition congruence. +Qed. +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 +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_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 + | H : _ ⊥ ⋃ _ |- _ => apply map_disjoint_union_list_r in H + | H : ∅ ⊥ _ |- _ => clear H + | H : _ ⊥ ∅ |- _ => clear H + | H : list_disjoint [] |- _ => clear H + | H : list_disjoint [_] |- _ => clear H + | H : list_disjoint (_ :: _) |- _ => + apply list_disjoint_cons_inv in H; destruct H + | H : Forall (⊥ _) _ |- _ => rewrite Forall_vlookup in H + | H : Forall (⊥ _) [] |- _ => clear H + | H : Forall (⊥ _) (_ :: _) |- _ => + rewrite Forall_cons in H; destruct H + | H : Forall (⊥ _) (_ :: _) |- _ => + rewrite Forall_app in H; destruct H + end. + +(** To prove a disjointness property, we first decompose all hypotheses, and +then use an auto database to prove the required property. *) +Create HintDb map_disjoint. +Ltac solve_map_disjoint := + solve [decompose_map_disjoint; auto with map_disjoint]. + +(** We declare these hints using [Hint Extern] instead of [Hint Resolve] as +[eauto] works badly with hints parametrized by type class constraints. *) +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 ({[ _ ]} ⊥ _) => + apply map_disjoint_singleton_l_2 : map_disjoint. +Hint Extern 2 (_ ⊥ {[ _ ]}) => + apply map_disjoint_singleton_r_2 : map_disjoint. +Hint Extern 2 (list_disjoint []) => apply disjoint_nil : map_disjoint. +Hint Extern 2 (list_disjoint (_ :: _)) => apply disjoint_cons : map_disjoint. +Hint Extern 2 (_ ∪ _ ⊥ _) => apply map_disjoint_union_l_2 : map_disjoint. +Hint Extern 2 (_ ⊥ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint. +Hint Extern 2 (<[_:=_]>_ ⊥ _) => apply map_disjoint_insert_l_2 : map_disjoint. +Hint Extern 2 (_ ⊥ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint. +Hint Extern 2 (delete _ _ ⊥ _) => apply map_disjoint_delete_l : map_disjoint. +Hint Extern 2 (_ ⊥ delete _ _) => apply map_disjoint_delete_r : map_disjoint. +Hint Extern 2 (map_of_list _ ⊥ _) => + apply map_disjoint_of_list_zip_l_2 : mem_disjoint. +Hint Extern 2 (_ ⊥ map_of_list _) => + apply map_disjoint_of_list_zip_r_2 : mem_disjoint. +Hint Extern 2 (⋃ _ ⊥ _) => apply map_disjoint_union_list_l_2 : mem_disjoint. +Hint Extern 2 (_ ⊥ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint. +Hint Extern 2 (delete_list _ _ ⊥ _) => + apply map_disjoint_delete_list_l : map_disjoint. +Hint Extern 2 (_ ⊥ delete_list _ _) => + apply map_disjoint_delete_list_r : map_disjoint. + +(** The tactic [simpl_map by tac] simplifies occurrences of finite map look +ups. It uses [tac] to discharge generated inequalities. Look ups in unions do +not have nice equational properties, hence it invokes [tac] to prove that such +look ups yield [Some]. *) Tactic Notation "simpl_map" "by" tactic3(tac) := repeat match goal with | H : context[ ∅ !! _ ] |- _ => rewrite lookup_empty in H | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H - | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by tac + | H : context[ (<[_:=_]>_) !! _ ] |- _ => + rewrite lookup_insert_ne in H by tac | H : context[ (delete _ _) !! _] |- _ => rewrite lookup_delete in H - | H : context[ (delete _ _) !! _] |- _ => rewrite lookup_delete_ne in H by tac + | H : context[ (delete _ _) !! _] |- _ => + rewrite lookup_delete_ne in H by tac | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton in H - | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by tac + | H : context[ {[ _ ]} !! _ ] |- _ => + rewrite lookup_singleton_ne in H by tac + | H : context[ lookup (A:=?A) ?i (?m1 ∪ ?m2) ] |- _ => + let x := fresh in evar (x:A); + let x' := eval unfold x in x in clear x; + let E := fresh in + assert ((m1 ∪ m2) !! i = Some x') as E by (clear H; by tac); + rewrite E in H; clear E | |- context[ ∅ !! _ ] => rewrite lookup_empty | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert_ne by tac @@ -487,23 +1562,35 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by tac | |- context [ lookup (A:=?A) ?i ?m ] => - let x := fresh in evar (x:A); - let x' := eval unfold x in x in clear x; - let E := fresh in - assert (m !! i = Some x') as E by tac; - rewrite E; clear E + let x := fresh in evar (x:A); + let x' := eval unfold x in x in clear x; + let E := fresh in + assert (m !! i = Some x') as E by tac; + rewrite E; clear E end. Create HintDb simpl_map. -Tactic Notation "simpl_map" := simpl_map by eauto with simpl_map. +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_insert : simpl_map. + +(** Now we take everything together and also discharge conflicting look ups, +simplify overlapping look ups, and perform cancellations of equalities +involving unions. *) Tactic Notation "simplify_map_equality" "by" tactic3(tac) := repeat match goal with | _ => progress simpl_map by tac | _ => progress simplify_equality | H : {[ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H | H : {[ _ ]} !! _ = Some _ |- _ => - rewrite lookup_singleton_Some in H; destruct H + rewrite lookup_singleton_Some in H; destruct H | H1 : ?m1 !! ?i = Some ?x, H2 : ?m2 !! ?i = Some ?y |- _ => let H3 := fresh in feed pose proof (lookup_weaken_inv m1 m2 i x y) as H3; @@ -513,786 +1600,11 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) := repeat let H3 := fresh in assert (m1 ⊆ m2) as H3 by tac; apply H3 in H1; congruence + | H : ?m ∪ _ = ?m ∪ _ |- _ => + apply map_union_cancel_l in H; [| solve[tac] | solve [tac]] + | H : _ ∪ ?m = _ ∪ ?m |- _ => + apply map_union_cancel_r in H; [| solve[tac] | solve [tac]] end. Tactic Notation "simplify_map_equality" := - simplify_map_equality by eauto with simpl_map. - -(** * More theorems on finite maps *) -Section finmap_more. - Context `{FinMap K M} {A : Type}. - - (** ** Properties of conversion to lists *) - Lemma finmap_to_list_unique (m : M A) i x y : - (i,x) ∈ finmap_to_list m → - (i,y) ∈ finmap_to_list m → - x = y. - Proof. rewrite !elem_of_finmap_to_list. congruence. Qed. - Lemma finmap_to_list_key_nodup (m : M A) : - NoDup (fst <$> finmap_to_list m). - Proof. - eauto using NoDup_fmap_fst, finmap_to_list_unique, finmap_to_list_nodup. - Qed. - - Lemma elem_of_finmap_of_list_1 (l : list (K * A)) i x : - NoDup (fst <$> l) → (i,x) ∈ l → finmap_of_list l !! i = Some x. - Proof. - induction l as [|[j y] l IH]; simpl. - * by rewrite elem_of_nil. - * rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap. - intros [Hl ?] [?|?]; simplify_map_equality; [done |]. - destruct (decide (i = j)); simplify_map_equality; [|done]. - destruct Hl. by exists (j,x). - Qed. - Lemma elem_of_finmap_of_list_2 (l : list (K * A)) i x : - finmap_of_list l !! i = Some x → (i,x) ∈ l. - Proof. - induction l as [|[j y] l IH]; simpl. - * by rewrite lookup_empty. - * rewrite elem_of_cons. destruct (decide (i = j)); - simplify_map_equality; intuition congruence. - Qed. - Lemma elem_of_finmap_of_list (l : list (K * A)) i x : - NoDup (fst <$> l) → - (i,x) ∈ l ↔ finmap_of_list l !! i = Some x. - Proof. - split; auto using elem_of_finmap_of_list_1, elem_of_finmap_of_list_2. - Qed. - - Lemma not_elem_of_finmap_of_list_1 (l : list (K * A)) i : - i ∉ fst <$> l → finmap_of_list l !! i = None. - Proof. - rewrite elem_of_list_fmap, eq_None_not_Some, is_Some_alt. - intros Hi [x ?]. destruct Hi. exists (i,x). simpl. - auto using elem_of_finmap_of_list_2. - Qed. - Lemma not_elem_of_finmap_of_list_2 (l : list (K * A)) i : - finmap_of_list l !! i = None → i ∉ fst <$> l. - Proof. - induction l as [|[j y] l IH]; simpl. - * rewrite elem_of_nil. tauto. - * rewrite elem_of_cons. - destruct (decide (i = j)); simplify_map_equality; by intuition. - Qed. - Lemma not_elem_of_finmap_of_list (l : list (K * A)) i : - i ∉ fst <$> l ↔ finmap_of_list l !! i = None. - Proof. - split; auto using not_elem_of_finmap_of_list_1, - not_elem_of_finmap_of_list_2. - Qed. - - Lemma finmap_of_list_proper (l1 l2 : list (K * A)) : - NoDup (fst <$> l1) → - Permutation l1 l2 → - finmap_of_list l1 = finmap_of_list l2. - Proof. - intros ? Hperm. apply finmap_eq. intros i. apply option_eq. intros x. - by rewrite <-!elem_of_finmap_of_list; rewrite <-?Hperm. - Qed. - Lemma finmap_of_list_inj (l1 l2 : list (K * A)) : - NoDup (fst <$> l1) → - NoDup (fst <$> l2) → - finmap_of_list l1 = finmap_of_list l2 → - Permutation l1 l2. - Proof. - intros ?? Hl1l2. - apply NoDup_Permutation; auto using (NoDup_fmap_1 fst). - intros [i x]. by rewrite !elem_of_finmap_of_list, Hl1l2. - Qed. - Lemma finmap_of_to_list (m : M A) : - finmap_of_list (finmap_to_list m) = m. - Proof. - apply finmap_eq. intros i. apply option_eq. intros x. - by rewrite <-elem_of_finmap_of_list, elem_of_finmap_to_list - by auto using finmap_to_list_key_nodup. - Qed. - Lemma finmap_to_of_list (l : list (K * A)) : - NoDup (fst <$> l) → - Permutation (finmap_to_list (finmap_of_list l)) l. - Proof. - auto using finmap_of_list_inj, - finmap_to_list_key_nodup, finmap_of_to_list. - Qed. - Lemma finmap_to_list_inj (m1 m2 : M A) : - Permutation (finmap_to_list m1) (finmap_to_list m2) → - m1 = m2. - Proof. - intros. - rewrite <-(finmap_of_to_list m1), <-(finmap_of_to_list m2). - auto using finmap_of_list_proper, finmap_to_list_key_nodup. - Qed. - - Lemma finmap_to_list_empty : - finmap_to_list ∅ = @nil (K * A). - Proof. - apply elem_of_nil_inv. intros [i x]. - rewrite elem_of_finmap_to_list. apply lookup_empty_Some. - Qed. - Lemma finmap_to_list_insert (m : M A) i x : - m !! i = None → - Permutation (finmap_to_list (<[i:=x]>m)) ((i,x) :: finmap_to_list m). - Proof. - intros. apply finmap_of_list_inj; simpl. - * apply finmap_to_list_key_nodup. - * constructor; auto using finmap_to_list_key_nodup. - rewrite elem_of_list_fmap. - intros [[??] [? Hlookup]]; subst; simpl in *. - rewrite elem_of_finmap_to_list in Hlookup. congruence. - * by rewrite !finmap_of_to_list. - Qed. - - Lemma finmap_of_list_nil : - finmap_of_list (@nil (K * A)) = ∅. - Proof. done. Qed. - Lemma finmap_of_list_cons (l : list (K * A)) i x : - finmap_of_list ((i, x) :: l) = <[i:=x]>(finmap_of_list l). - Proof. done. Qed. - - Lemma finmap_to_list_empty_inv (m : M A) : - Permutation (finmap_to_list m) [] → m = ∅. - Proof. rewrite <-finmap_to_list_empty. apply finmap_to_list_inj. Qed. - Lemma finmap_to_list_insert_inv (m : M A) l i x : - Permutation (finmap_to_list m) ((i,x) :: l) → - m = <[i:=x]>(finmap_of_list l). - Proof. - intros Hperm. apply finmap_to_list_inj. - assert (NoDup (fst <$> (i, x) :: l)) as Hnodup. - { rewrite <-Hperm. auto using finmap_to_list_key_nodup. } - simpl in Hnodup. rewrite NoDup_cons in Hnodup. - destruct Hnodup. - rewrite Hperm, finmap_to_list_insert, finmap_to_of_list; - auto using not_elem_of_finmap_of_list_1. - Qed. - - (** ** Properties of the forall predicate *) - Section finmap_forall. - Context (P : K → A → Prop). - - Lemma finmap_forall_to_list m : - finmap_forall P m ↔ Forall (curry P) (finmap_to_list m). - Proof. - rewrite Forall_forall. split. - * intros Hforall [i x]. - rewrite elem_of_finmap_to_list. by apply (Hforall i x). - * intros Hforall i x. - rewrite <-elem_of_finmap_to_list. by apply (Hforall (i,x)). - Qed. - - Global Instance finmap_forall_dec - `{∀ i x, Decision (P i x)} m : Decision (finmap_forall P m). - Proof. - refine (cast_if (decide (Forall (curry P) (finmap_to_list m)))); - by rewrite finmap_forall_to_list. - Defined. - End finmap_forall. - - (** ** Properties of the merge operation *) - Section merge_with. - Context (f : option A → option A → option A). - - Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f). - Proof. - intros ??. apply finmap_eq. intros. - by rewrite !(merge_spec f), lookup_empty, (left_id None f). - Qed. - Global Instance: RightId (=) None f → RightId (=) ∅ (merge f). - Proof. - intros ??. apply finmap_eq. intros. - by rewrite !(merge_spec f), lookup_empty, (right_id None f). - Qed. - - Context `{!PropHolds (f None None = None)}. - - Lemma merge_spec_alt m1 m2 m : - (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m. - Proof. - split; [| intro; subst; apply (merge_spec _) ]. - intros Hlookup. apply finmap_eq. intros. rewrite Hlookup. - apply (merge_spec _). - Qed. - - Lemma merge_commutative m1 m2 : - (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → - merge f m1 m2 = merge f m2 m1. - Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed. - Global Instance: Commutative (=) f → Commutative (=) (merge f). - Proof. - intros ???. apply merge_commutative. intros. by apply (commutative f). - Qed. - - Lemma merge_associative m1 m2 m3 : - (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = - f (f (m1 !! i) (m2 !! i)) (m3 !! i)) → - merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3. - Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed. - Global Instance: Associative (=) f → Associative (=) (merge f). - Proof. - intros ????. apply merge_associative. intros. by apply (associative f). - Qed. - - Lemma merge_idempotent m1 : - (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → - merge f m1 m1 = m1. - Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed. - Global Instance: Idempotent (=) f → Idempotent (=) (merge f). - Proof. - intros ??. apply merge_idempotent. intros. by apply (idempotent f). - Qed. - End merge_with. - - (** ** Properties on the intersection forall relation *) - Section intersection_forall. - Context (R : relation A). - - Global Instance finmap_intersection_forall_sym: - Symmetric R → Symmetric (finmap_intersection_forall R). - Proof. firstorder auto. Qed. - Lemma finmap_intersection_forall_empty_l (m : M A) : - finmap_intersection_forall R ∅ m. - Proof. intros ???. by simpl_map. Qed. - Lemma finmap_intersection_forall_empty_r (m : M A) : - finmap_intersection_forall R m ∅. - Proof. intros ???. by simpl_map. Qed. - - (** Due to the finiteness of finite maps, we can extract a witness are - property does not hold for the intersection. *) - Lemma finmap_not_intersection_forall `{∀ x y, Decision (R x y)} (m1 m2 : M A) : - ¬finmap_intersection_forall R m1 m2 - ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ ¬R x1 x2. - Proof. - split. - * intros Hdisjoint. - set (Pi i := ∀ x1 x2, m1 !! i = Some x1 → m2 !! i = Some x2 → ¬R x1 x2). - assert (∀ i, Decision (Pi i)). - { intros i. unfold Decision, Pi. - destruct (m1 !! i) as [x1|], (m2 !! i) as [x2|]; try (by left). - destruct (decide (R x1 x2)). - * naive_solver. - * intuition congruence. } - destruct (decide (cexists Pi (dom (listset _) m1 ∩ dom (listset _) m2))) - as [[i [Hdom Hi]] | Hi]. - + rewrite elem_of_intersection in Hdom. - rewrite !(elem_of_dom (listset _)), !is_Some_alt in Hdom. - destruct Hdom as [[x1 ?] [x2 ?]]. exists i x1 x2; auto. - + destruct Hdisjoint. intros i x1 x2 Hx1 Hx2. - apply dec_stable. intros HP. - destruct Hi. exists i. - rewrite elem_of_intersection, !(elem_of_dom (listset _)). - intuition eauto; congruence. - * intros (i & x1 & x2 & Hx1 & Hx2 & Hx1x2) Hdisjoint. - by apply Hx1x2, (Hdisjoint i x1 x2). - Qed. - End intersection_forall. - - (** ** Properties on the disjoint maps *) - Lemma finmap_disjoint_alt (m1 m2 : M A) : - m1 ⊥ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None. - Proof. - split; intros Hm1m2 i; specialize (Hm1m2 i); - destruct (m1 !! i), (m2 !! i); naive_solver. - Qed. - Lemma finmap_not_disjoint (m1 m2 : M A) : - ¬m1 ⊥ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2. - Proof. - unfold disjoint, finmap_disjoint. - rewrite finmap_not_intersection_forall. - * naive_solver. - * right. auto. - Qed. - - Global Instance: Symmetric (@disjoint (M A) _). - Proof. apply finmap_intersection_forall_sym. auto. Qed. - Lemma finmap_disjoint_empty_l (m : M A) : ∅ ⊥ m. - Proof. apply finmap_intersection_forall_empty_l. Qed. - Lemma finmap_disjoint_empty_r (m : M A) : m ⊥ ∅. - Proof. apply finmap_intersection_forall_empty_r. Qed. - - Lemma finmap_disjoint_weaken (m1 m1' m2 m2' : M A) : - m1' ⊥ m2' → - m1 ⊆ m1' → m2 ⊆ m2' → - m1 ⊥ m2. - Proof. - intros Hdisjoint Hm1 Hm2 i x1 x2 Hx1 Hx2. - destruct (Hdisjoint i x1 x2); auto. - Qed. - Lemma finmap_disjoint_weaken_l (m1 m1' m2 : M A) : - m1' ⊥ m2 → m1 ⊆ m1' → m1 ⊥ m2. - Proof. eauto using finmap_disjoint_weaken. Qed. - Lemma finmap_disjoint_weaken_r (m1 m2 m2' : M A) : - m1 ⊥ m2' → m2 ⊆ m2' → m1 ⊥ m2. - Proof. eauto using finmap_disjoint_weaken. Qed. - - Lemma finmap_disjoint_Some_l (m1 m2 : M A) i x: - m1 ⊥ m2 → - m1 !! i = Some x → - m2 !! i = None. - Proof. - intros Hdisjoint ?. rewrite eq_None_not_Some, is_Some_alt. - intros [x2 ?]. by apply (Hdisjoint i x x2). - Qed. - Lemma finmap_disjoint_Some_r (m1 m2 : M A) i x: - m1 ⊥ m2 → - m2 !! i = Some x → - m1 !! i = None. - Proof. rewrite (symmetry_iff (⊥)). apply finmap_disjoint_Some_l. Qed. - - Lemma finmap_disjoint_singleton_l (m : M A) i x : - {[(i, x)]} ⊥ m ↔ m !! i = None. - Proof. - split. - * intro. apply (finmap_disjoint_Some_l {[(i, x)]} _ _ x); by simpl_map. - * intros ? j y1 y2 ??. - destruct (decide (i = j)); simplify_map_equality; congruence. - Qed. - Lemma finmap_disjoint_singleton_r (m : M A) i x : - m ⊥ {[(i, x)]} ↔ m !! i = None. - Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_singleton_l. Qed. - - Lemma finmap_disjoint_singleton_l_2 (m : M A) i x : - m !! i = None → {[(i, x)]} ⊥ m. - Proof. by rewrite finmap_disjoint_singleton_l. Qed. - Lemma finmap_disjoint_singleton_r_2 (m : M A) i x : - m !! i = None → m ⊥ {[(i, x)]}. - Proof. by rewrite finmap_disjoint_singleton_r. Qed. - - (** ** Properties of the union and intersection operation *) - Section union_intersection_with. - Context (f : A → A → option A). - - Lemma finmap_union_with_Some m1 m2 i x y : - m1 !! i = Some x → - m2 !! i = Some y → - union_with f m1 m2 !! i = f x y. - Proof. - intros Hx Hy. unfold union_with, finmap_union_with. - by rewrite (merge_spec _), Hx, Hy. - Qed. - Lemma finmap_union_with_Some_l m1 m2 i x : - m1 !! i = Some x → - m2 !! i = None → - union_with f m1 m2 !! i = Some x. - Proof. - intros Hx Hy. unfold union_with, finmap_union_with. - by rewrite (merge_spec _), Hx, Hy. - Qed. - Lemma finmap_union_with_Some_r m1 m2 i y : - m1 !! i = None → - m2 !! i = Some y → - union_with f m1 m2 !! i = Some y. - Proof. - intros Hx Hy. unfold union_with, finmap_union_with. - by rewrite (merge_spec _), Hx, Hy. - Qed. - - Global Instance: LeftId (=) ∅ (@union_with _ (M A) _ f). - Proof. unfold union_with, finmap_union_with. apply _. Qed. - Global Instance: RightId (=) ∅ (@union_with _ (M A) _ f). - Proof. unfold union_with, finmap_union_with. apply _. Qed. - Global Instance: - Commutative (=) f → Commutative (=) (@union_with _ (M A) _ f). - Proof. unfold union_with, finmap_union_with. apply _. Qed. - End union_intersection_with. - - Global Instance: LeftId (=) ∅ (@union (M A) _) := _. - Global Instance: RightId (=) ∅ (@union (M A) _) := _. - Global Instance: Associative (=) (@union (M A) _). - Proof. - intros m1 m2 m3. unfold union, finmap_union, union_with, finmap_union_with. - apply (merge_associative _). intros i. - by destruct (m1 !! i), (m2 !! i), (m3 !! i). - Qed. - Global Instance: Idempotent (=) (@union (M A) _). - intros m. unfold union, finmap_union, union_with, finmap_union_with. - apply (merge_idempotent _). intros i. by destruct (m !! i). - Qed. - - Lemma lookup_union_Some_raw (m1 m2 : M A) i x : - (m1 ∪ m2) !! i = Some x ↔ - m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x). - Proof. - unfold union, finmap_union, union_with, finmap_union_with. - rewrite (merge_spec _). - destruct (m1 !! i), (m2 !! i); compute; intuition congruence. - Qed. - Lemma lookup_union_None (m1 m2 : M A) i : - (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None. - Proof. - unfold union, finmap_union, union_with, finmap_union_with. - rewrite (merge_spec _). - destruct (m1 !! i), (m2 !! i); compute; intuition congruence. - Qed. - - Lemma lookup_union_Some (m1 m2 : M A) i x : - m1 ⊥ m2 → - (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x. - Proof. - intros Hdisjoint. rewrite lookup_union_Some_raw. - intuition eauto using finmap_disjoint_Some_r. - Qed. - - Lemma lookup_union_Some_l (m1 m2 : M A) i x : - m1 !! i = Some x → - (m1 ∪ m2) !! i = Some x. - Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed. - Lemma lookup_union_Some_r (m1 m2 : M A) i x : - m1 ⊥ m2 → - m2 !! i = Some x → - (m1 ∪ m2) !! i = Some x. - Proof. intro. rewrite lookup_union_Some; intuition. Qed. - - Lemma finmap_union_comm (m1 m2 : M A) : - m1 ⊥ m2 → - m1 ∪ m2 = m2 ∪ m1. - Proof. - intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))). - intros i. specialize (Hdisjoint i). - destruct (m1 !! i), (m2 !! i); compute; naive_solver. - Qed. - - Lemma finmap_subseteq_union (m1 m2 : M A) : - m1 ⊆ m2 → - m1 ∪ m2 = m2. - Proof. - intros Hm1m2. - apply finmap_eq. intros i. apply option_eq. intros x. - rewrite lookup_union_Some_raw. split; [by intuition |]. - intros Hm2. specialize (Hm1m2 i). - destruct (m1 !! i) as [y|]; [| by auto]. - rewrite (Hm1m2 y eq_refl) in Hm2. intuition congruence. - Qed. - Lemma finmap_subseteq_union_l (m1 m2 : M A) : - m1 ⊆ m1 ∪ m2. - Proof. intros ? i x. rewrite lookup_union_Some_raw. intuition. Qed. - Lemma finmap_subseteq_union_r (m1 m2 : M A) : - m1 ⊥ m2 → - m2 ⊆ m1 ∪ m2. - Proof. - intros. rewrite finmap_union_comm by done. - by apply finmap_subseteq_union_l. - Qed. - - Lemma finmap_disjoint_union_l (m1 m2 m3 : M A) : - m1 ∪ m2 ⊥ m3 ↔ m1 ⊥ m3 ∧ m2 ⊥ m3. - Proof. - rewrite !finmap_disjoint_alt. - setoid_rewrite lookup_union_None. naive_solver. - Qed. - Lemma finmap_disjoint_union_r (m1 m2 m3 : M A) : - m1 ⊥ m2 ∪ m3 ↔ m1 ⊥ m2 ∧ m1 ⊥ m3. - Proof. - rewrite !finmap_disjoint_alt. - setoid_rewrite lookup_union_None. naive_solver. - Qed. - Lemma finmap_disjoint_union_l_2 (m1 m2 m3 : M A) : - m1 ⊥ m3 → m2 ⊥ m3 → m1 ∪ m2 ⊥ m3. - Proof. by rewrite finmap_disjoint_union_l. Qed. - Lemma finmap_disjoint_union_r_2 (m1 m2 m3 : M A) : - m1 ⊥ m2 → m1 ⊥ m3 → m1 ⊥ m2 ∪ m3. - Proof. by rewrite finmap_disjoint_union_r. Qed. - Lemma finmap_union_cancel_l (m1 m2 m3 : M A) : - m1 ⊥ m3 → - m2 ⊥ m3 → - m1 ∪ m3 = m2 ∪ m3 → - m1 = m2. - Proof. - revert m1 m2 m3. - cut (∀ (m1 m2 m3 : M A) i x, - m1 ⊥ m3 → - m2 ⊥ m3 → - m1 ∪ m3 = m2 ∪ m3 → - m1 !! i = Some x → m2 !! i = Some x). - { intros. apply finmap_eq. intros i. - apply option_eq. naive_solver. } - intros m1 m2 m3 b v Hm1m3 Hm2m3 E ?. - destruct (proj1 (lookup_union_Some m2 m3 b v Hm2m3)) as [E2|E2]. - * rewrite <-E. by apply lookup_union_Some_l. - * done. - * contradict E2. by apply eq_None_ne_Some, finmap_disjoint_Some_l with m1 v. - Qed. - Lemma finmap_union_cancel_r (m1 m2 m3 : M A) : - m1 ⊥ m3 → - m2 ⊥ m3 → - m3 ∪ m1 = m3 ∪ m2 → - m1 = m2. - Proof. - intros ??. rewrite !(finmap_union_comm m3) by done. - by apply finmap_union_cancel_l. - Qed. - - Lemma insert_union_singleton_l (m : M A) i x : - <[i:=x]>m = {[(i,x)]} ∪ m. - Proof. - apply finmap_eq. intros j. apply option_eq. intros y. - rewrite lookup_union_Some_raw. - destruct (decide (i = j)); simplify_map_equality; intuition congruence. - Qed. - Lemma insert_union_singleton_r (m : M A) i x : - m !! i = None → - <[i:=x]>m = m ∪ {[(i,x)]}. - Proof. - intro. rewrite insert_union_singleton_l, finmap_union_comm; [done |]. - by apply finmap_disjoint_singleton_l. - Qed. - - Lemma finmap_disjoint_insert_l (m1 m2 : M A) i x : - <[i:=x]>m1 ⊥ m2 ↔ m2 !! i = None ∧ m1 ⊥ m2. - Proof. - rewrite insert_union_singleton_l. - by rewrite finmap_disjoint_union_l, finmap_disjoint_singleton_l. - Qed. - Lemma finmap_disjoint_insert_r (m1 m2 : M A) i x : - m1 ⊥ <[i:=x]>m2 ↔ m1 !! i = None ∧ m1 ⊥ m2. - Proof. - rewrite insert_union_singleton_l. - by rewrite finmap_disjoint_union_r, finmap_disjoint_singleton_r. - Qed. - - Lemma finmap_disjoint_insert_l_2 (m1 m2 : M A) i x : - m2 !! i = None → m1 ⊥ m2 → <[i:=x]>m1 ⊥ m2. - Proof. by rewrite finmap_disjoint_insert_l. Qed. - Lemma finmap_disjoint_insert_r_2 (m1 m2 : M A) i x : - m1 !! i = None → m1 ⊥ m2 → m1 ⊥ <[i:=x]>m2. - Proof. by rewrite finmap_disjoint_insert_r. Qed. - - Lemma insert_union_l (m1 m2 : M A) i x : - <[i:=x]>(m1 ∪ m2) = <[i:=x]>m1 ∪ m2. - Proof. by rewrite !insert_union_singleton_l, (associative (∪)). Qed. - Lemma insert_union_r (m1 m2 : M A) i x : - m1 !! i = None → - <[i:=x]>(m1 ∪ m2) = m1 ∪ <[i:=x]>m2. - Proof. - intro. rewrite !insert_union_singleton_l, !(associative (∪)). - rewrite (finmap_union_comm m1); [done |]. - by apply finmap_disjoint_singleton_r. - Qed. - - Lemma insert_list_union l (m : M A) : - insert_list l m = finmap_of_list l ∪ m. - Proof. - induction l; simpl. - * by rewrite (left_id _ _). - * by rewrite IHl, insert_union_l. - Qed. - - Lemma insert_subseteq_r (m1 m2 : M A) i x : - m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]>m2. - Proof. - intros ?? j. by destruct (decide (j = i)); intros; simplify_map_equality. - Qed. - - (** ** Properties of the delete operation *) - Lemma finmap_disjoint_delete_l (m1 m2 : M A) i : - m1 ⊥ m2 → delete i m1 ⊥ m2. - Proof. - rewrite !finmap_disjoint_alt. - intros Hdisjoint j. destruct (Hdisjoint j); auto. - rewrite lookup_delete_None. tauto. - Qed. - Lemma finmap_disjoint_delete_r (m1 m2 : M A) i : - m1 ⊥ m2 → m1 ⊥ delete i m2. - Proof. symmetry. by apply finmap_disjoint_delete_l. Qed. - - Lemma finmap_disjoint_delete_list_l (m1 m2 : M A) is : - m1 ⊥ m2 → delete_list is m1 ⊥ m2. - Proof. induction is; simpl; auto using finmap_disjoint_delete_l. Qed. - Lemma finmap_disjoint_delete_list_r (m1 m2 : M A) is : - m1 ⊥ m2 → m1 ⊥ delete_list is m2. - Proof. induction is; simpl; auto using finmap_disjoint_delete_r. Qed. - - Lemma finmap_union_delete (m1 m2 : M A) i : - delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2. - Proof. - intros. apply finmap_eq. intros j. apply option_eq. intros y. - destruct (decide (i = j)); simplify_map_equality; - rewrite ?lookup_union_Some_raw; simpl_map; intuition congruence. - Qed. - Lemma finmap_union_delete_list (m1 m2 : M A) is : - delete_list is (m1 ∪ m2) = delete_list is m1 ∪ delete_list is m2. - Proof. - induction is; simpl; [done |]. - by rewrite IHis, finmap_union_delete. - Qed. - - Lemma finmap_disjoint_union_list_l (ms : list (M A)) (m : M A) : - ⋃ ms ⊥ m ↔ Forall (⊥ m) ms. - Proof. - split. - * induction ms; simpl; rewrite ?finmap_disjoint_union_l; intuition. - * induction 1; simpl. - + apply finmap_disjoint_empty_l. - + by rewrite finmap_disjoint_union_l. - Qed. - Lemma finmap_disjoint_union_list_r (ms : list (M A)) (m : M A) : - m ⊥ ⋃ ms ↔ Forall (⊥ m) ms. - Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_union_list_l. Qed. - - Lemma finmap_disjoint_union_list_l_2 (ms : list (M A)) (m : M A) : - Forall (⊥ m) ms → ⋃ ms ⊥ m. - Proof. by rewrite finmap_disjoint_union_list_l. Qed. - Lemma finmap_disjoint_union_list_r_2 (ms : list (M A)) (m : M A) : - Forall (⊥ m) ms → m ⊥ ⋃ ms. - Proof. by rewrite finmap_disjoint_union_list_r. Qed. - - (** ** Properties of the conversion from lists to maps *) - Lemma finmap_disjoint_of_list_l (m : M A) ixs : - finmap_of_list ixs ⊥ m ↔ Forall (λ ix, m !! fst ix = None) ixs. - Proof. - split. - * induction ixs; simpl; rewrite ?finmap_disjoint_insert_l in *; intuition. - * induction 1; simpl. - + apply finmap_disjoint_empty_l. - + rewrite finmap_disjoint_insert_l. auto. - Qed. - Lemma finmap_disjoint_of_list_r (m : M A) ixs : - m ⊥ finmap_of_list ixs ↔ Forall (λ ix, m !! fst ix = None) ixs. - Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_of_list_l. Qed. - - Lemma finmap_disjoint_of_list_zip_l (m : M A) is xs : - same_length is xs → - finmap_of_list (zip is xs) ⊥ m ↔ Forall (λ i, m !! i = None) is. - Proof. - intro. rewrite finmap_disjoint_of_list_l. - rewrite <-(zip_fst is xs) at 2 by done. - by rewrite Forall_fmap. - Qed. - Lemma finmap_disjoint_of_list_zip_r (m : M A) is xs : - same_length is xs → - m ⊥ finmap_of_list (zip is xs) ↔ Forall (λ i, m !! i = None) is. - Proof. - intro. by rewrite (symmetry_iff (⊥)), finmap_disjoint_of_list_zip_l. - Qed. - Lemma finmap_disjoint_of_list_zip_l_2 (m : M A) is xs : - same_length is xs → - Forall (λ i, m !! i = None) is → - finmap_of_list (zip is xs) ⊥ m. - Proof. intro. by rewrite finmap_disjoint_of_list_zip_l. Qed. - Lemma finmap_disjoint_of_list_zip_r_2 (m : M A) is xs : - same_length is xs → - Forall (λ i, m !! i = None) is → - m ⊥ finmap_of_list (zip is xs). - Proof. intro. by rewrite finmap_disjoint_of_list_zip_r. Qed. - - (** ** Properties with respect to vectors *) - Lemma union_delete_vec {n} (ms : vec (M A) n) (i : fin n) : - list_disjoint ms → - ms !!! i ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms) = ⋃ ms. - Proof. - induction ms as [|m ? ms]; inversion_clear 1; - inv_fin i; simpl; [done | intros i]. - rewrite (finmap_union_comm m), (associative_eq _ _), IHms. - * by apply finmap_union_comm, finmap_disjoint_union_list_l. - * done. - * by apply finmap_disjoint_union_list_r, Forall_delete. - Qed. - - Lemma union_insert_vec {n} (ms : vec (M A) n) (i : fin n) m : - m ⊥ ⋃ delete (fin_to_nat i) (vec_to_list ms) → - ⋃ vinsert i m ms = m ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms). - Proof. - induction ms as [|m' ? ms IH]; - inv_fin i; simpl; [done | intros i Hdisjoint]. - rewrite finmap_disjoint_union_r in Hdisjoint. - rewrite IH, !(associative_eq (∪)), (finmap_union_comm m); intuition. - Qed. - - Lemma finmap_list_disjoint_delete_vec {n} (ms : vec (M A) n) (i : fin n) : - list_disjoint ms → - Forall (⊥ ms !!! i) (delete (fin_to_nat i) (vec_to_list ms)). - Proof. - induction ms; inversion_clear 1; inv_fin i; simpl. - * done. - * constructor. symmetry. by apply Forall_vlookup. auto. - Qed. - - Lemma finmap_list_disjoint_insert_vec {n} (ms : vec (M A) n) (i : fin n) m : - list_disjoint ms → - Forall (⊥ m) (delete (fin_to_nat i) (vec_to_list ms)) → - list_disjoint (vinsert i m ms). - Proof. - induction ms as [|m' ? ms]; inversion_clear 1; inv_fin i; simpl. - { constructor; auto. } - intros i. inversion_clear 1. constructor; [| by auto]. - apply Forall_vlookup_2. intros j. - destruct (decide (i = j)); subst; - rewrite ?vlookup_insert, ?vlookup_insert_ne by done. - * done. - * by apply Forall_vlookup. - Qed. - - (** ** Properties of the difference operation *) - Lemma finmap_difference_Some (m1 m2 : M A) i x : - (m1 ∖ m2) !! i = Some x ↔ m1 !! i = Some x ∧ m2 !! i = None. - Proof. - unfold difference, finmap_difference, - difference_with, finmap_difference_with. - rewrite (merge_spec _). - destruct (m1 !! i), (m2 !! i); compute; intuition congruence. - Qed. - - Lemma finmap_disjoint_difference_l (m1 m2 m3 : M A) : - m2 ⊆ m3 → m1 ∖ m3 ⊥ m2. - Proof. - intros E i. specialize (E i). - unfold difference, finmap_difference, - difference_with, finmap_difference_with. - rewrite (merge_spec _). - destruct (m1 !! i), (m2 !! i), (m3 !! i); compute; - try intuition congruence. - ediscriminate E; eauto. - Qed. - Lemma finmap_disjoint_difference_r (m1 m2 m3 : M A) : - m2 ⊆ m3 → m2 ⊥ m1 ∖ m3. - Proof. intros. symmetry. by apply finmap_disjoint_difference_l. Qed. - - Lemma finmap_union_difference (m1 m2 : M A) : - m1 ⊆ m2 → m2 = m1 ∪ m2 ∖ m1. - Proof. - intro Hm1m2. apply finmap_eq. intros i. - apply option_eq. intros v. specialize (Hm1m2 i). - unfold difference, finmap_difference, - difference_with, finmap_difference_with. - rewrite lookup_union_Some_raw, (merge_spec _). - destruct (m1 !! i) as [v'|], (m2 !! i); - try specialize (Hm1m2 v'); compute; intuition congruence. - Qed. -End finmap_more. - -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_insert : simpl_map. - -(** * Tactic to decompose disjoint assumptions *) -(** The tactic [decompose_map_disjoint] simplifies occurences of [disjoint] -in the conclusion and hypotheses that involve the union, insert, or singleton -operation. *) -Ltac decompose_map_disjoint := repeat - match goal with - | H : _ ∪ _ ⊥ _ |- _ => - apply finmap_disjoint_union_l in H; destruct H - | H : _ ⊥ _ ∪ _ |- _ => - apply finmap_disjoint_union_r in H; destruct H - | H : {[ _ ]} ⊥ _ |- _ => apply finmap_disjoint_singleton_l in H - | H : _ ⊥ {[ _ ]} |- _ => apply finmap_disjoint_singleton_r in H - | H : <[_:=_]>_ ⊥ _ |- _ => - apply finmap_disjoint_insert_l in H; destruct H - | H : _ ⊥ <[_:=_]>_ |- _ => - apply finmap_disjoint_insert_r in H; destruct H - | H : ⋃ _ ⊥ _ |- _ => apply finmap_disjoint_union_list_l in H - | H : _ ⊥ ⋃ _ |- _ => apply finmap_disjoint_union_list_r in H - | H : ∅ ⊥_ |- _ => clear H - | H : _ ⊥ ∅ |- _ => clear H - | H : list_disjoint [] |- _ => clear H - | H : list_disjoint [_] |- _ => clear H - | H : list_disjoint (_ :: _) |- _ => - apply list_disjoint_cons_inv in H; destruct H - | H : Forall (⊥ _) _ |- _ => rewrite Forall_vlookup in H - | H : Forall (⊥ _) [] |- _ => clear H - | H : Forall (⊥ _) (_ :: _) |- _ => - rewrite Forall_cons in H; destruct H - | H : Forall (⊥ _) (_ :: _) |- _ => - rewrite Forall_app in H; destruct H - end. + decompose_map_disjoint; + simplify_map_equality by eauto with simpl_map map_disjoint. diff --git a/theories/fresh_numbers.v b/theories/fresh_numbers.v index 0be3b557..84f0ec2c 100644 --- a/theories/fresh_numbers.v +++ b/theories/fresh_numbers.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** Given a finite set of binary naturals [N], we generate a fresh element by taking the maximum, and adding one to it. We declare this operation as an diff --git a/theories/list.v b/theories/list.v index 728aab8f..97509a7c 100644 --- a/theories/list.v +++ b/theories/list.v @@ -1,10 +1,10 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects general purpose definitions and theorems on lists that are not in the Coq standard library. *) Require Import Permutation. -Require Export base decidable option numbers. +Require Export numbers base decidable option. Arguments length {_} _. Arguments cons {_} _ _. @@ -65,7 +65,7 @@ Instance list_insert {A} : Insert nat A (list A) := λ i x, alter (λ _, x) i. (** The function [option_list] converts an element of the option type into -a list. *) +the empty list or a singleton list. *) Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) []. (** The function [filter P l] returns the list of elements of [l] that @@ -107,32 +107,42 @@ Arguments resize {_} !_ _ !_. (** The predicate [suffix_of] holds if the first list is a suffix of the second. The predicate [prefix_of] holds if the first list is a prefix of the second. *) -Definition suffix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1. -Definition prefix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k. -Definition max_prefix_of `{∀ x y : A, Decision (x = y)} : - list A → list A → list A * list A * list A := - fix go l1 l2 := - match l1, l2 with - | [], l2 => ([], l2, []) - | l1, [] => (l1, [], []) - | x1 :: l1, x2 :: l2 => - if decide_rel (=) x1 x2 - then snd_map (x1 ::) (go l1 l2) - else (x1 :: l1, x2 :: l2, []) - end. -Definition max_suffix_of `{∀ x y : A, Decision (x = y)} (l1 l2 : list A) : - list A * list A * list A := - match max_prefix_of (reverse l1) (reverse l2) with - | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3) - end. +Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1. +Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k. -(** * Tactics on lists *) -Lemma cons_inv {A} (l1 l2 : list A) x1 x2 : - x1 :: l1 = x2 :: l2 → x1 = x2 ∧ l1 = l2. -Proof. by injection 1. Qed. +Section prefix_suffix_ops. + Context `{∀ x y : A, Decision (x = y)}. + + Definition max_prefix_of : list A → list A → list A * list A * list A := + fix go l1 l2 := + match l1, l2 with + | [], l2 => ([], l2, []) + | l1, [] => (l1, [], []) + | x1 :: l1, x2 :: l2 => + if decide_rel (=) x1 x2 + then snd_map (x1 ::) (go l1 l2) + else (x1 :: l1, x2 :: l2, []) + end. + Definition max_suffix_of (l1 l2 : list A) : list A * list A * list A := + match max_prefix_of (reverse l1) (reverse l2) with + | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3) + end. + + Definition strip_prefix (l1 l2 : list A) := snd $ fst $ max_prefix_of l1 l2. + Definition strip_suffix (l1 l2 : list A) := snd $ fst $ max_suffix_of l1 l2. +End prefix_suffix_ops. -(** The tactic [discriminate_list_equality] discharges goals containing -invalid list equalities as an assumption. *) +(** A list [l1] is a sub list of [l2] if [l2] is obtained by removing elements +from [l1] without changing the order. *) +Inductive sublist {A} : relation (list A) := + | sublist_nil : sublist [] [] + | sublist_cons x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2) + | sublist_cons_skip x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2). + +(** * Tactics on lists *) +(** The tactic [discriminate_list_equality] discharges a goal if it contains +a list equality involving [(::)] and [(++)] of two lists that have a different +length as one of its hypotheses. *) Tactic Notation "discriminate_list_equality" hyp(H) := apply (f_equal length) in H; repeat (simpl in H || rewrite app_length in H); @@ -140,8 +150,13 @@ Tactic Notation "discriminate_list_equality" hyp(H) := Tactic Notation "discriminate_list_equality" := solve [repeat_on_hyps (fun H => discriminate_list_equality H)]. -(** The tactic [simplify_list_equality] simplifies assumptions involving -equalities on lists. *) +(** The tactic [simplify_list_equality] simplifies hypotheses involving +equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies +lookups in singleton lists. *) +Lemma cons_inv {A} (l1 l2 : list A) x1 x2 : + x1 :: l1 = x2 :: l2 → x1 = x2 ∧ l1 = l2. +Proof. by injection 1. Qed. + Ltac simplify_list_equality := repeat match goal with | H : _ :: _ = _ :: _ |- _ => @@ -181,7 +196,7 @@ Lemma app_inj (l1 k1 l2 k2 : list A) : l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2. Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed. -Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2. +Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i)%C → l1 = l2. Proof. revert l2. induction l1; intros [|??] H. * done. @@ -195,7 +210,8 @@ Proof. intros. by apply list_eq. Qed. Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k, Decision (l = k) := list_eq_dec dec. -Definition list_singleton_dec (l : list A) : { x | l = [x] } + { length l ≠1 }. +Definition list_singleton_dec (l : list A) : + { x | l = [x] } + { length l ≠1 }. Proof. by refine ( match l with @@ -204,6 +220,9 @@ Proof. end). Defined. +Global Instance: Proper (Permutation ==> (=)) (@length A). +Proof. induction 1; simpl; auto with lia. Qed. + Lemma nil_or_length_pos (l : list A) : l = [] ∨ length l ≠0. Proof. destruct l; simpl; auto with lia. Qed. Lemma nil_length (l : list A) : length l = 0 → l = []. @@ -375,6 +394,10 @@ Lemma insert_consecutive_length (l : list A) i k : length (insert_consecutive i k l) = length l. Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed. +Lemma delete_middle (l1 l2 : list A) x : + delete (length l1) (l1 ++ x :: l2) = l1 ++ l2. +Proof. induction l1; simpl; f_equal; auto. Qed. + Lemma not_elem_of_nil (x : A) : x ∉ []. Proof. by inversion 1. Qed. Lemma elem_of_nil (x : A) : x ∈ [] ↔ False. @@ -566,7 +589,7 @@ Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed. Lemma reverse_length (l : list A) : length (reverse l) = length l. Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed. Lemma reverse_involutive (l : list A) : reverse (reverse l) = l. -Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. +Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. Lemma take_nil n : take n (@nil A) = []. @@ -840,6 +863,136 @@ Lemma drop_resize_plus (l : list A) n m x : drop n (resize (n + m) x l) = resize m x (drop n l). Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed. +Lemma delete_take_drop (l : list A) i : + delete i l = take i l ++ drop (S i) l. +Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed. + +Lemma sublist_nil_l (l : list A) : + sublist [] l. +Proof. induction l; try constructor; auto. Qed. +Lemma sublist_nil_r (l : list A) : + sublist l [] ↔ l = []. +Proof. split. by inversion 1. intros. subst. constructor. Qed. + +Lemma sublist_app_skip_l (k : list A) l1 l2 : + sublist l1 l2 → + sublist l1 (k ++ l2). +Proof. induction k; try constructor; auto. Qed. +Lemma sublist_app_skip_r (k : list A) l1 l2 : + sublist l1 l2 → + sublist l1 (l2 ++ k). +Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed. + +Lemma sublist_cons_r (x : A) l k : + sublist l (x :: k) ↔ sublist l k ∨ ∃ l', l = x :: l' ∧ sublist l' k. +Proof. + split. + * inversion 1; eauto. + * intros [?|(?&?&?)]; subst; constructor; auto. +Qed. +Lemma sublist_cons_l (x : A) l k : + sublist (x :: l) k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ sublist l k2. +Proof. + split. + * intros Hlk. induction k as [|y k IH]; inversion Hlk. + + eexists [], k. by repeat constructor. + + destruct IH as (k1 & k2 & ? & ?); subst; auto. + by exists (y :: k1) k2. + * intros (k1 & k2 & ? & ?). subst. + by apply sublist_app_skip_l, sublist_cons. +Qed. + +Lemma sublist_app_compat (l1 l2 k1 k2 : list A) : + sublist l1 l2 → sublist k1 k2 → + sublist (l1 ++ k1) (l2 ++ k2). +Proof. induction 1; simpl; try constructor; auto. Qed. + +Lemma sublist_app_r (l k1 k2 : list A) : + sublist l (k1 ++ k2) ↔ ∃ l1 l2, + l = l1 ++ l2 ∧ sublist l1 k1 ∧ sublist l2 k2. +Proof. + split. + * revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl. + { eexists [], l. by repeat constructor. } + rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst. + + destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst. + exists l1 l2. auto using sublist_cons_skip. + + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst. + exists (y :: l1) l2. auto using sublist_cons. + * intros (?&?&?&?&?); subst. auto using sublist_app_compat. +Qed. +Lemma sublist_app_l (l1 l2 k : list A) : + sublist (l1 ++ l2) k ↔ ∃ k1 k2, + k = k1 ++ k2 ∧ sublist l1 k1 ∧ sublist l2 k2. +Proof. + split. + * revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl. + { eexists [], k. by repeat constructor. } + rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst. + destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst. + exists (k1 ++ x :: h1) h2. rewrite <-(associative (++)). + auto using sublist_app_skip_l, sublist_cons. + * intros (?&?&?&?&?); subst. auto using sublist_app_compat. +Qed. + +Global Instance: PreOrder (@sublist A). +Proof. + split. + * intros l. induction l; constructor; auto. + * intros l1 l2 l3 Hl12. revert l3. induction Hl12. + + auto using sublist_nil_l. + + intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst. + eauto using sublist_app_skip_l, sublist_cons. + + intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst. + eauto using sublist_app_skip_l, sublist_cons_skip. +Qed. + +Lemma sublist_length (l1 l2 : list A) : + sublist l1 l2 → length l1 ≤ length l2. +Proof. induction 1; simpl; auto with arith. Qed. + +Lemma sublist_take (l : list A) i : + sublist (take i l) l. +Proof. rewrite <-(take_drop i l) at 2. by apply sublist_app_skip_r. Qed. +Lemma sublist_drop (l : list A) i : + sublist (drop i l) l. +Proof. rewrite <-(take_drop i l) at 2. by apply sublist_app_skip_l. Qed. +Lemma sublist_delete (l : list A) i : + sublist (delete i l) l. +Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed. +Lemma sublist_delete_list (l : list A) is : + sublist (delete_list is l) l. +Proof. + induction is as [|i is IH]; simpl; [done |]. + transitivity (delete_list is l); auto using sublist_delete. +Qed. + +Lemma sublist_alt (l1 l2 : list A) : + sublist l1 l2 ↔ ∃ is, l1 = delete_list is l2. +Proof. + split. + * intros Hl12. + cut (∀ k, ∃ is, k ++ l1 = delete_list is (k ++ l2)). + { intros help. apply (help []). } + induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k. + + by eexists []. + + destruct (IH (k ++ [x])) as [is His]. exists is. + by rewrite <-!(associative (++)) in His. + + destruct (IH k) as [is His]. exists (is ++ [length k]). + unfold delete_list. rewrite fold_right_app. simpl. + by rewrite delete_middle. + * intros [is ?]. subst. apply sublist_delete_list. +Qed. + +Global Instance: AntiSymmetric (@sublist A). +Proof. + intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21. + induction Hl12; simpl in *. + * done. + * f_equal. auto with arith. + * apply sublist_length in Hl12. lia. +Qed. + Section Forall_Exists. Context (P : A → Prop). @@ -873,6 +1026,15 @@ Section Forall_Exists. Forall P l → (∀ x, P x → Q x) → Forall Q l. Proof. intros H ?. induction H; auto. Defined. + Global Instance Forall_proper: + Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A). + Proof. split; subst; induction 1; constructor; firstorder. Qed. + + Lemma Forall_iff l (Q : A → Prop) : + (∀ x, P x ↔ Q x) → + Forall P l ↔ Forall Q l. + Proof. intros H. apply Forall_proper. red. apply H. done. Qed. + Lemma Forall_delete l i : Forall P l → Forall P (delete i l). Proof. intros H. revert i. @@ -910,7 +1072,7 @@ Section Forall_Exists. split. * induction 1 as [x|y ?? IH]. + exists x. split. constructor. done. - + destruct IH as [x [??]]. exists x. split. by constructor. done. + + destruct IH as [x [??]]. exists x. split. by constructor. done. * intros [x [Hin ?]]. induction l. + by destruct (not_elem_of_nil x). + inversion Hin; subst. by left. right; auto. @@ -923,9 +1085,13 @@ Section Forall_Exists. * induction l1; inversion 1; intuition. * intros [H|H]. + induction H; simpl; intuition. - + induction l1; simpl; intuition. + + induction l1; simpl; intuition. Qed. + Global Instance Exists_proper: + Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A). + Proof. split; subst; (induction 1; [left|right]; firstorder auto). Qed. + Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l. Proof. induction 1; inversion_clear 1; contradiction. Qed. Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l. @@ -1085,6 +1251,14 @@ Section Forall2. induction Hl; simpl; intros [|i]; constructor; auto. Qed. + Lemma Forall2_delete l1 l2 i : + Forall2 P l1 l2 → + Forall2 P (delete i l1) (delete i l2). + Proof. + intros Hl12. revert i. + induction Hl12; intros [|i]; simpl; intuition. + Qed. + Lemma Forall2_replicate_l l n x : Forall (P x) l → length l = n → @@ -1301,7 +1475,7 @@ Section prefix_postfix. end end. - Section max_prefix_of. + Section prefix_ops. Context `{∀ x y : A, Decision (x = y)}. Lemma max_prefix_of_fst (l1 l2 : list A) : @@ -1372,7 +1546,7 @@ Section prefix_postfix. * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl). apply prefix_of_app, prefix_of_cons, prefix_of_nil. Qed. - End max_prefix_of. + End prefix_ops. Lemma prefix_suffix_reverse (l1 l2 : list A) : prefix_of l1 l2 ↔ suffix_of (reverse l1) (reverse l2). @@ -1397,7 +1571,7 @@ Section prefix_postfix. Lemma suffix_of_snoc_alt x y (l1 l2 : list A) : x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]). Proof. intro. subst. apply suffix_of_snoc. Qed. - + Lemma suffix_of_app (l1 l2 k : list A) : suffix_of l1 l2 → suffix_of (l1 ++ k) (l2 ++ k). Proof. intros [k' E]. exists k'. subst. by rewrite (associative (++)). Qed. @@ -1666,12 +1840,18 @@ Section list_fmap. f <$> k = [] → k = []. Proof. by destruct k. Qed. Lemma fmap_cons_inv y l k : - f <$> l = y :: k → ∃ x l', - y = f x ∧ k = f <$> l' ∧ l = x :: l'. + f <$> l = y :: k → + ∃ x l', + y = f x ∧ + k = f <$> l' ∧ + l = x :: l'. Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed. Lemma fmap_app_inv l k1 k2 : - f <$> l = k1 ++ k2 → ∃ l1 l2, - k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2. + f <$> l = k1 ++ k2 → + ∃ l1 l2, + k1 = f <$> l1 ∧ + k2 = f <$> l2 ∧ + l = l1 ++ l2. Proof. revert l. induction k1 as [|y k1 IH]; simpl. * intros l ?. by eexists [], l. @@ -1699,7 +1879,7 @@ Section list_fmap. intros Hi. rewrite list_lookup_fmap in Hi. destruct (l !! i) eqn:?; simplify_equality; eauto. Qed. - + Lemma list_alter_fmap (g : A → A) (h : B → B) l i : Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l). @@ -1931,10 +2111,10 @@ Ltac simplify_list_fmap_equality := repeat | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H | H : _ <$> _ = _ :: _ |- _ => - apply fmap_cons_inv in H; destruct H as (?&?&?&?&?) + apply fmap_cons_inv in H; destruct H as (?&?&?&?&?) | H : _ :: _ = _ <$> _ |- _ => symmetry in H | H : _ <$> _ = _ ++ _ |- _ => - apply fmap_app_inv in H; destruct H as (?&?&?&?&?) + apply fmap_app_inv in H; destruct H as (?&?&?&?&?) | H : _ ++ _ = _ <$> _ |- _ => symmetry in H end. @@ -2036,6 +2216,47 @@ Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C : Section zip_with. Context {A B C : Type} (f : A → B → C). + Lemma zip_with_nil_inv l1 l2 : + zip_with f l1 l2 = [] → l1 = [] ∨ l2 = []. + Proof. destruct l1, l2; simpl; auto with congruence. Qed. + Lemma zip_with_cons_inv y l1 l2 k : + zip_with f l1 l2 = y :: k → + ∃ x1 x2 l1' l2', + y = f x1 x2 ∧ + k = zip_with f l1' l2' ∧ + l1 = x1 :: l1' ∧ + l2 = x2 :: l2'. + Proof. + intros. destruct l1, l2; simpl; simplify_equality; repeat eexists. + Qed. + Lemma zip_with_app_inv l1 l2 k' k'' : + zip_with f l1 l2 = k' ++ k'' → + ∃ l1' l1'' l2' l2'', + k' = zip_with f l1' l2' ∧ + k'' = zip_with f l1'' l2'' ∧ + l1 = l1' ++ l1'' ∧ + l2 = l2' ++ l2''. + Proof. + revert l1 l2. induction k' as [|y k' IH]; simpl. + * intros l1 l2 ?. by eexists [], l1, [], l2. + * intros [|x1 l1] [|x2 l2] ?; simpl; simplify_equality. + destruct (IH l1 l2) as (l1' & l1'' & l2' & l2'' &?&?&?&?); + subst; [done |]. + by exists (x1 :: l1') l1'' (x2 :: l2') l2''. + Qed. + + Lemma zip_with_inj l1 l2 k1 k2 : + (∀ x1 x2 y1 y2, f x1 x2 = f y1 y2 → x1 = y1 ∧ x2 = y2) → + same_length l1 l2 → + same_length k1 k2 → + zip_with f l1 l2 = zip_with f k1 k2 → + l1 = k1 ∧ l2 = k2. + Proof. + intros ? Hl. revert k1 k2. + induction Hl; intros ?? [] ?; simpl; + simplify_equality; f_equal; naive_solver. + Qed. + Lemma zip_with_length l1 l2 : length l1 ≤ length l2 → length (zip_with f l1 l2) = length l1. @@ -2117,6 +2338,21 @@ Section zip. Proof. by apply zip_with_fmap_snd. Qed. End zip. +Ltac simplify_zip_equality := repeat + match goal with + | _ => progress simplify_equality + | H : zip_with _ _ _ = [] |- _ => + apply zip_with_nil_inv in H; destruct H + | H : [] = zip_with _ _ _ |- _ => + symmetry in H + | H : zip_with _ _ _ = _ :: _ |- _ => + apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?) + | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H + | H : zip_with _ _ _ = _ ++ _ |- _ => + apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?) + | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H + end. + Definition zipped_map {A B} (f : list A → list A → A → B) : list A → list A → list B := fix go l k := @@ -2208,14 +2444,14 @@ Section permutations. * by apply elem_of_list_singleton. * apply elem_of_list_bind. eauto using interleave_cons. Qed. - Lemma permutations_skip (x : A) (l l' : list A) : + Lemma permutations_skip (x : A) (l l' : list A) : l ∈ permutations l' → x :: l ∈ permutations (x :: l'). Proof. intros Hl. simpl. apply elem_of_list_bind. eauto using interleave_cons. Qed. - Lemma permutations_swap (x y : A) (l : list A) : + Lemma permutations_swap (x y : A) (l : list A) : y :: x :: l ∈ permutations (x :: y :: l). Proof. simpl. apply elem_of_list_bind. diff --git a/theories/listset.v b/theories/listset.v index 21da8752..7738d9e9 100644 --- a/theories/listset.v +++ b/theories/listset.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file implements finite as unordered lists without duplicates removed. This implementation forms a monad. *) @@ -51,13 +51,12 @@ Instance listset_filter: Filter A (listset A) := λ P _ l, | Listset l' => Listset (filter P l') end. -Global Instance: Collection A (listset A). +Instance: Collection A (listset A). Proof. split. * apply _. * intros [?] [?]. apply elem_of_list_intersection. * intros [?] [?]. apply elem_of_list_difference. - * intros ? [?] [?]. apply elem_of_list_intersection_with. Qed. Instance listset_elems: Elements A (listset A) := @@ -67,10 +66,17 @@ Global Instance: FinCollection A (listset A). Proof. split. * apply _. - * intros [?] ??. apply elem_of_list_filter. * symmetry. apply elem_of_remove_dups. * intros. apply remove_dups_nodup. Qed. + +Global Instance: CollectionOps A (listset A). +Proof. + split. + * apply _. + * intros ? [?] [?]. apply elem_of_list_intersection_with. + * intros [?] ??. apply elem_of_list_filter. +Qed. End listset. (** These instances are declared using [Hint Extern] to avoid too diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v index a63c969a..86b91d5b 100644 --- a/theories/listset_nodup.v +++ b/theories/listset_nodup.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file implements finite as unordered lists without duplicates. Although this implementation is slow, it is very useful as decidable equality @@ -59,18 +59,14 @@ Instance listset_nodup_intersection_with: Instance listset_nodup_filter: Filter A C := λ P _ l, LS _ (filter_nodup P _ (listset_nodup_prf l)). -Global Instance: Collection A C. +Instance: Collection A C. Proof. - split; [split | | |]. + split; [split | | ]. * by apply not_elem_of_nil. * by apply elem_of_list_singleton. * intros. apply elem_of_listset_nodup_union_raw. * intros. apply elem_of_list_intersection. * intros. apply elem_of_list_difference. - * intros. unfold intersection_with, listset_nodup_intersection_with, - elem_of, listset_nodup_elem_of. simpl. - rewrite elem_of_remove_dups. - by apply elem_of_list_intersection_with. Qed. Global Instance listset_nodup_elems: Elements A C := listset_nodup_car. @@ -79,10 +75,20 @@ Global Instance: FinCollection A C. Proof. split. * apply _. - * intros. apply elem_of_list_filter. * done. * by intros [??]. Qed. + +Global Instance: CollectionOps A C. +Proof. + split. + * apply _. + * intros. unfold intersection_with, listset_nodup_intersection_with, + elem_of, listset_nodup_elem_of. simpl. + rewrite elem_of_remove_dups. + by apply elem_of_list_intersection_with. + * intros. apply elem_of_list_filter. +Qed. End list_collection. Hint Extern 1 (ElemOf _ (listset_nodup _)) => diff --git a/theories/mapset.v b/theories/mapset.v new file mode 100644 index 00000000..25b7d40d --- /dev/null +++ b/theories/mapset.v @@ -0,0 +1,151 @@ +(* Copyright (c) 2012-2013, Robbert Krebbers. *) +(* This file is distributed under the terms of the BSD license. *) +(** This files gives an implementation of finite sets using finite maps with +elements of the unit type. Since maps enjoy extensional equality, the +constructed finite sets do so as well. *) + +Require Export fin_map_dom. + +Record mapset (M : Type → Type) := Mapset { + mapset_car: M unit +}. +Arguments Mapset {_} _. +Arguments mapset_car {_} _. + +Section mapset. +Context `{FinMap K M}. + +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,()) ]}. +Instance mapset_union: Union (mapset M) := λ X1 X2, + match X1, X2 with + | Mapset m1, Mapset m2 => Mapset (m1 ∪ m2) + end. +Instance mapset_intersection: Intersection (mapset M) := λ X1 X2, + match X1, X2 with + | Mapset m1, Mapset m2 => Mapset (m1 ∩ m2) + end. +Instance mapset_difference: Difference (mapset M) := λ X1 X2, + match X1, X2 with + | Mapset m1, Mapset m2 => Mapset (m1 ∖ m2) + end. +Instance mapset_elems: Elements K (mapset M) := λ X, + match X with + | Mapset m => fst <$> map_to_list m + end. + +Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2. +Proof. + split. + * intros. by subst. + * destruct X1 as [m1], X2 as [m2]. simpl. intros E. + f_equal. apply map_eq. intros i. + apply option_eq. intros []. by apply E. +Qed. + +Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)} : + ∀ X1 X2 : mapset M, Decision (X1 = X2) | 1. +Proof. solve_decision. Defined. +Global Instance mapset_elem_of_dec x (X : mapset M) : + Decision (x ∈ X) | 1. +Proof. solve_decision. Defined. + +Instance: Collection K (mapset M). +Proof. + split; [split | | ]. + * unfold empty, elem_of, mapset_empty, mapset_elem_of. + simpl. intros. by simpl_map. + * unfold singleton, elem_of, mapset_singleton, mapset_elem_of. + simpl. by split; intros; simplify_map_equality. + * unfold union, elem_of, mapset_union, mapset_elem_of. + intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw. + destruct (m1 !! x) as [[]|]; tauto. + * unfold intersection, elem_of, mapset_intersection, mapset_elem_of. + intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some. + setoid_replace (is_Some (m2 !! x)) with (m2 !! x = Some ()); [done |]. + rewrite is_Some_alt. split; eauto. by intros [[] ?]. + * unfold difference, elem_of, mapset_difference, mapset_elem_of. + intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some. + destruct (m2 !! x) as [[]|]; intuition congruence. +Qed. + +Global Instance: PartialOrder (mapset M). +Proof. + split; try apply _. + intros ????. apply mapset_eq. intuition. +Qed. + +Global Instance: FinCollection K (mapset M). +Proof. + split. + * apply _. + * unfold elements, elem_of at 1, mapset_elems, mapset_elem_of. + intros [m] x. simpl. rewrite elem_of_list_fmap. split. + + intros. exists (x, ()). by rewrite elem_of_map_to_list. + + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list. + * unfold elements, mapset_elems. intros [m]. simpl. + apply map_to_list_key_nodup. +Qed. + +Definition mapset_map_with `(f : bool → A → B) (X : mapset M) : M A → M B := + match X with + | Mapset m => merge (λ x y, + match x, y with + | Some _, Some a => Some (f true a) + | None, Some a => Some (f false a) + | _, None => None + end) m + end. +Definition mapset_dom_with `(f : A → bool) (m : M A) : mapset M := + Mapset $ merge (λ x _, + match x with + | Some a => if f a then Some () else None + | None => None + end) m (@empty (M A) _). + +Lemma lookup_mapset_map_with `(f : bool → A → B) X m i : + mapset_map_with f X m !! i = f (bool_decide (i ∈ X)) <$> m !! i. +Proof. + destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of. + rewrite lookup_merge by done. simpl. + by case_bool_decide; destruct (mX !! i) as [[]|], (m !! i). +Qed. +Lemma elem_of_mapset_dom_with `(f : A → bool) m i : + i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x. +Proof. + unfold mapset_dom_with, elem_of, mapset_elem_of. + simpl. rewrite lookup_merge by done. + destruct (m !! i) as [a|]. + * destruct (Is_true_reflect (f a)); naive_solver. + * naive_solver. +Qed. + +Instance mapset_dom {A} : Dom (M A) (mapset M) := + mapset_dom_with (λ _, true). +Instance mapset_dom_spec: FinMapDom K M (mapset M). +Proof. + split; try apply _. intros. unfold dom, mapset_dom. + rewrite is_Some_alt, elem_of_mapset_dom_with. naive_solver. +Qed. +End mapset. + +(** These instances are declared using [Hint Extern] to avoid too +eager type class search. *) +Hint Extern 1 (ElemOf _ (mapset _)) => + eapply @mapset_elem_of : typeclass_instances. +Hint Extern 1 (Empty (mapset _)) => + eapply @mapset_empty : typeclass_instances. +Hint Extern 1 (Singleton _ (mapset _)) => + eapply @mapset_singleton : typeclass_instances. +Hint Extern 1 (Union (mapset _)) => + eapply @mapset_union : typeclass_instances. +Hint Extern 1 (Intersection (mapset _)) => + eapply @mapset_intersection : typeclass_instances. +Hint Extern 1 (Difference (mapset _)) => + eapply @mapset_difference : typeclass_instances. +Hint Extern 1 (Elements _ (mapset _)) => + eapply @mapset_elems : typeclass_instances. diff --git a/theories/nmap.v b/theories/nmap.v index 312e9ee9..8fac809a 100644 --- a/theories/nmap.v +++ b/theories/nmap.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This files extends the implementation of finite over [positive] to finite maps whose keys range over Coq's data type of binary naturals [N]. *) @@ -30,9 +30,9 @@ Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t, Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t, match t with | NMap o t => option_case (λ x, [(0,x)]) [] o ++ - (fst_map Npos <$> finmap_to_list t) + (fst_map Npos <$> map_to_list t) end. -Instance Nmerge {A} : Merge A (Nmap A) := λ f t1 t2, +Instance Nmerge: Merge Nmap := λ A B C f t1 t2, match t1, t2 with | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2) end. @@ -46,7 +46,7 @@ Proof. split. * intros ? [??] [??] H. f_equal. + apply (H 0). - + apply finmap_eq. intros i. apply (H (Npos i)). + + apply map_eq. intros i. apply (H (Npos i)). * by intros ? [|?]. * intros ? f [? t] [|i]; simpl. + done. @@ -54,27 +54,27 @@ Proof. * intros ? f [? t] [|i] [|j]; simpl; try intuition congruence. intros. apply lookup_partial_alter_ne. congruence. * intros ??? [??] []; simpl. done. apply lookup_fmap. - * intros ? [[x|] t]; unfold finmap_to_list; simpl. + * intros ? [[x|] t]; unfold map_to_list; simpl. + constructor. - rewrite elem_of_list_fmap. by intros [[??] [??]]. - - rewrite (NoDup_fmap _). apply finmap_to_list_nodup. - + rewrite (NoDup_fmap _). apply finmap_to_list_nodup. - * intros ? t i x. unfold finmap_to_list. split. + - rewrite (NoDup_fmap _). apply map_to_list_nodup. + + rewrite (NoDup_fmap _). apply map_to_list_nodup. + * intros ? t i x. unfold map_to_list. split. + destruct t as [[y|] t]; simpl. - rewrite elem_of_cons, elem_of_list_fmap. intros [? | [[??] [??]]]; simplify_equality; simpl; [done |]. - by apply elem_of_finmap_to_list. + by apply elem_of_map_to_list. - rewrite elem_of_list_fmap. intros [[??] [??]]; simplify_equality; simpl. - by apply elem_of_finmap_to_list. + by apply elem_of_map_to_list. + destruct t as [[y|] t]; simpl. - rewrite elem_of_cons, elem_of_list_fmap. destruct i as [|i]; simpl; [intuition congruence |]. - intros. right. exists (i, x). by rewrite elem_of_finmap_to_list. + intros. right. exists (i, x). by rewrite elem_of_map_to_list. - rewrite elem_of_list_fmap. destruct i as [|i]; simpl; [done |]. - intros. exists (i, x). by rewrite elem_of_finmap_to_list. - * intros ? f ? [o1 t1] [o2 t2] [|?]; simpl. + intros. exists (i, x). by rewrite elem_of_map_to_list. + * intros ??? f ? [o1 t1] [o2 t2] [|?]; simpl. + done. - + apply (merge_spec f t1 t2). + + apply (lookup_merge f t1 t2). Qed. diff --git a/theories/numbers.v b/theories/numbers.v index e19e1019..d08d8c3c 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -1,13 +1,16 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects some trivial facts on the Coq types [nat] and [N] for natural numbers, and the type [Z] for integers. It also declares some useful notations. *) Require Export PArith NArith ZArith. +Require Import Qcanon. Require Export base decidable. +Open Scope nat_scope. Coercion Z.of_nat : nat >-> Z. +(** * Notations and properties of [nat] *) Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level). Reserved Notation "x ≤ y < z" (at level 70, y at next level). Reserved Notation "x < y < z" (at level 70, y at next level). @@ -42,17 +45,86 @@ Definition sum_list_with {A} (f : A → nat) : list A → nat := end. Notation sum_list := (sum_list_with id). +(** * Notations and properties of [positive] *) +Open Scope positive_scope. + Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec. -Instance positive_inhabited: Inhabited positive := populate 1%positive. +Instance positive_inhabited: Inhabited positive := populate 1. Notation "(~0)" := xO (only parsing) : positive_scope. Notation "(~1)" := xI (only parsing) : positive_scope. -Instance: Injective (=) (=) xO. +Instance: Injective (=) (=) (~0). Proof. by injection 1. Qed. -Instance: Injective (=) (=) xI. +Instance: Injective (=) (=) (~1). Proof. by injection 1. Qed. +(** Since [positive] represents lists of bits, we define list operations +on it. These operations are in reverse, as positives are treated as snoc +lists instead of cons lists. *) +Fixpoint Papp (p1 p2 : positive) : positive := + match p2 with + | 1 => p1 + | p2~0 => (Papp p1 p2)~0 + | p2~1 => (Papp p1 p2)~1 + end. +Infix "++" := Papp : positive_scope. +Notation "(++)" := Papp (only parsing) : positive_scope. +Notation "( p ++)" := (Papp p) (only parsing) : positive_scope. +Notation "(++ q )" := (λ p, Papp p q) (only parsing) : positive_scope. + +Fixpoint Preverse_go (p1 p2 : positive) : positive := + match p2 with + | 1 => p1 + | p2~0 => Preverse_go (p1~0) p2 + | p2~1 => Preverse_go (p1~1) p2 + end. +Definition Preverse : positive → positive := Preverse_go 1. + +Global Instance: LeftId (=) 1 (++). +Proof. intros p. induction p; simpl; intros; f_equal; auto. Qed. +Global Instance: RightId (=) 1 (++). +Proof. done. Qed. +Global Instance: Associative (=) (++). +Proof. intros ?? p. induction p; simpl; intros; f_equal; auto. Qed. +Global Instance: ∀ p : positive, Injective (=) (=) (++ p). +Proof. intros p ???. induction p; simplify_equality; auto. Qed. + +Lemma Preverse_go_app_cont p1 p2 p3 : + Preverse_go (p2 ++ p1) p3 = p2 ++ Preverse_go p1 p3. +Proof. + revert p1. induction p3; simpl; intros. + * apply (IHp3 (_~1)). + * apply (IHp3 (_~0)). + * done. +Qed. +Lemma Preverse_go_app p1 p2 p3 : + Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2. +Proof. + revert p1. induction p3; intros p1; simpl; auto. + by rewrite <-Preverse_go_app_cont. +Qed. +Lemma Preverse_app p1 p2 : + Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1. +Proof. unfold Preverse. by rewrite Preverse_go_app. Qed. + +Lemma Preverse_xO p : Preverse (p~0) = (1~0) ++ Preverse p. +Proof Preverse_app p (1~0). +Lemma Preverse_xI p : Preverse (p~1) = (1~1) ++ Preverse p. +Proof Preverse_app p (1~1). + +Fixpoint Plength (p : positive) : nat := + match p with + | 1 => 0%nat + | p~0 | p~1 => S (Plength p) + end. +Lemma Papp_length p1 p2 : + Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat. +Proof. induction p2; simpl; f_equal; auto. Qed. + +Close Scope positive_scope. + +(** * Notations and properties of [N] *) Infix "≤" := N.le : N_scope. Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope. Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%N : N_scope. @@ -82,6 +154,7 @@ Program Instance N_lt_dec (x y : N) : Decision (x < y)%N := Next Obligation. congruence. Qed. Instance N_inhabited: Inhabited N := populate 1%N. +(** * Notations and properties of [Z] *) Infix "≤" := Z.le : Z_scope. Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Z : Z_scope. Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Z : Z_scope. @@ -98,6 +171,53 @@ Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec. Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec. Instance Z_inhabited: Inhabited Z := populate 1%Z. +(** * Notations and properties of [Qc] *) +Notation "2" := (1+1)%Qc : Qc_scope. +Infix "≤" := Qcle : Qc_scope. +Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Qc : Qc_scope. +Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Qc : Qc_scope. +Notation "x < y < z" := (x < y ∧ y < z)%Qc : Qc_scope. +Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Qc : Qc_scope. +Notation "(≤)" := Qcle (only parsing) : Qc_scope. +Notation "(<)" := Qclt (only parsing) : Qc_scope. + +Instance Qc_eq_dec: ∀ x y : Qc, Decision (x = y) := Qc_eq_dec. +Program Instance Qc_le_dec (x y : Qc) : Decision (x ≤ y)%Qc := + if Qclt_le_dec y x then right _ else left _. +Next Obligation. by apply Qclt_not_le. Qed. +Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y)%Qc := + if Qclt_le_dec x y then left _ else right _. +Next Obligation. by apply Qcle_not_lt. Qed. + +Instance: Reflexive Qcle. +Proof. red. apply Qcle_refl. Qed. +Instance: Transitive Qcle. +Proof. red. apply Qcle_trans. Qed. + +Lemma Qcle_ngt (x y : Qc) : (x ≤ y ↔ ¬y < x)%Qc. +Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed. +Lemma Qclt_nge (x y : Qc) : (x < y ↔ ¬y ≤ x)%Qc. +Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed. + +Lemma Qcplus_le_mono_l (x y z : Qc) : + (x ≤ y ↔ z + x ≤ z + y)%Qc. +Proof. + split; intros. + * by apply Qcplus_le_compat. + * replace x with ((0 - z) + (z + x))%Qc by ring. + replace y with ((0 - z) + (z + y))%Qc by ring. + by apply Qcplus_le_compat. +Qed. +Lemma Qcplus_le_mono_r (x y z : Qc) : + (x ≤ y ↔ x + z ≤ y + z)%Qc. +Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed. +Lemma Qcplus_lt_mono_l (x y z : Qc) : + (x < y ↔ z + x < z + y)%Qc. +Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed. +Lemma Qcplus_lt_mono_r (x y z : Qc) : + (x < y ↔ x + z < y + z)%Qc. +Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed. + (** * Conversions *) (** The function [Z_to_option_N] converts an integer [x] into a natural number by giving [None] in case [x] is negative. *) diff --git a/theories/option.v b/theories/option.v index 455d1a73..22847c93 100644 --- a/theories/option.v +++ b/theories/option.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects general purpose definitions and theorems on the option data type that are not in the Coq standard library. *) @@ -95,21 +95,15 @@ Proof. destruct 1. intros. f_equal. auto. Qed. (** Equality on [option] is decidable. *) Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) : Decision (x = y) := - match x with - | Some a => - match y with - | Some b => - match dec a b with - | left H => left (f_equal _ H) - | right H => right (H ∘ injective Some _ _) - end - | None => right (Some_ne_None _) - end - | None => - match y with - | Some _ => right (None_ne_Some _) - | None => left eq_refl + match x, y with + | Some a, Some b => + match dec a b with + | left H => left (f_equal _ H) + | right H => right (H ∘ injective Some _ _) end + | Some _, None => right (Some_ne_None _) + | None, Some _ => right (None_ne_Some _) + | None, None => left eq_refl end. (** * Monadic operations *) @@ -128,13 +122,19 @@ Instance option_fmap: FMap option := @option_map. Instance option_guard: MGuard option := λ P dec A x, if dec then x else None. -Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : - is_Some x ↔ is_Some (f <$> x). -Proof. split; inversion 1. done. by destruct x. Qed. -Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : - x = None ↔ f <$> x = None. +Lemma fmap_is_Some {A B} (f : A → B) (x : option A) : + is_Some (f <$> x) ↔ is_Some x. +Proof. split; inversion 1. by destruct x. done. Qed. +Lemma fmap_Some {A B} (f : A → B) (x : option A) y : + f <$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'. +Proof. unfold fmap, option_fmap. destruct x; naive_solver. Qed. +Lemma fmap_None {A B} (f : A → B) (x : option A) : + f <$> x = None ↔ x = None. Proof. unfold fmap, option_fmap. by destruct x. Qed. +Lemma option_fmap_id {A} (x : option A) : + id <$> x = x. +Proof. by destruct x. Qed. Lemma option_bind_assoc {A B C} (f : A → option B) (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f). Proof. by destruct x; simpl. Qed. @@ -214,10 +214,10 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat end | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ => let X := context C [ if dec then x else None ] in - change X in H; destruct dec + change X in H; destruct_decide dec | |- context C [@mguard option _ ?P ?dec _ ?x] => let X := context C [ if dec then x else None ] in - change X; destruct dec + change X; destruct_decide dec | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ => assert (y = x) by congruence; clear H2 | H1 : ?o = Some ?x, H2 : ?o = None |- _ => @@ -259,8 +259,14 @@ Section option_union_intersection_difference. Proof. by intros [?|]. Qed. Global Instance: Commutative (=) f → Commutative (=) (union_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. + + Global Instance: LeftAbsorb (=) None (intersection_with f). + Proof. by intros [?|]. Qed. + Global Instance: RightAbsorb (=) None (intersection_with f). + Proof. by intros [?|]. Qed. Global Instance: Commutative (=) f → Commutative (=) (intersection_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. + Global Instance: RightId (=) None (difference_with f). Proof. by intros [?|]. Qed. End option_union_intersection_difference. diff --git a/theories/orders.v b/theories/orders.v index 89c45541..af0bec44 100644 --- a/theories/orders.v +++ b/theories/orders.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects common properties of pre-orders and semi lattices. This theory will mainly be used for the theory on collections and finite maps. *) @@ -31,20 +31,26 @@ Section preorder. Global Instance preorder_subset: Subset A := λ X Y, X ⊆ Y ∧ Y ⊈ X. Lemma subset_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X. Proof. done. Qed. + Lemma subset_spec_alt X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y. + Proof. + split. + * intros [? HYX]. split. done. contradict HYX. by rewrite HYX. + * intros [? HXY]. split. done. by contradict HXY. + Qed. Lemma subset_subseteq X Y : X ⊂ Y → X ⊆ Y. Proof. by intros [? _]. Qed. Lemma subset_trans_l X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z. Proof. - intros [? Hxy] ?. split. + intros [? HXY] ?. split. * by transitivity Y. - * contradict Hxy. by transitivity Z. + * contradict HXY. by transitivity Z. Qed. Lemma subset_trans_r X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z. Proof. - intros ? [? Hyz]. split. + intros ? [? HYZ]. split. * by transitivity Y. - * contradict Hyz. by transitivity X. + * contradict HYZ. by transitivity X. Qed. Global Instance: StrictOrder (⊂). @@ -56,42 +62,81 @@ Section preorder. Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊂). Proof. unfold subset, preorder_subset. solve_proper. Qed. - Context `{∀ X Y : A, Decision (X ⊆ Y)}. - Global Instance preorder_equiv_dec_slow (X Y : A) : - Decision (X ≡ Y) | 100 := _. - Global Instance preorder_subset_dec_slow (X Y : A) : - Decision (X ⊂ Y) | 100 := _. + Section leibniz. + Context `{!LeibnizEquiv A}. - Lemma subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y. - Proof. - destruct (decide (Y ⊆ X)). - * by right. - * by left. - Qed. + Lemma subset_spec_alt_L X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠Y. + Proof. unfold_leibniz. apply subset_spec_alt. Qed. + End leibniz. + + Section dec. + Context `{∀ X Y : A, Decision (X ⊆ Y)}. + + Global Instance preorder_equiv_dec_slow (X Y : A) : + Decision (X ≡ Y) | 100 := _. + Global Instance preorder_subset_dec_slow (X Y : A) : + Decision (X ⊂ Y) | 100 := _. + + Lemma subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y. + Proof. rewrite subset_spec_alt. destruct (decide (X ≡ Y)); tauto. Qed. + Lemma not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y. + Proof. rewrite subset_spec_alt. destruct (decide (X ≡ Y)); tauto. Qed. + + Context `{!LeibnizEquiv A}. + + Lemma subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y. + Proof. unfold_leibniz. apply subseteq_inv. Qed. + Lemma not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y. + Proof. unfold_leibniz. apply not_subset_inv. Qed. + End dec. End preorder. Typeclasses Opaque preorder_equiv. +Typeclasses Opaque preorder_subset. Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances. +(** * Partial orders *) +Section partialorder. + Context `{PartialOrder A}. + + Global Instance: LeibnizEquiv A. + Proof. + split. + * intros [??]. by apply (anti_symmetric _). + * intros. by subst. + Qed. +End partialorder. + (** * Join semi lattices *) (** General purpose theorems on join semi lattices. *) Section bounded_join_sl. Context `{BoundedJoinSemiLattice A}. - Hint Resolve subseteq_empty subseteq_union_l subseteq_union_r union_least. + Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least. - Lemma union_compat_l x1 x2 y : x1 ⊆ x2 → x1 ⊆ x2 ∪ y. + Lemma union_subseteq_l_alt x1 x2 y : x1 ⊆ x2 → x1 ⊆ x2 ∪ y. Proof. intros. transitivity x2; auto. Qed. - Lemma union_compat_r x1 x2 y : x1 ⊆ x2 → x1 ⊆ y ∪ x2. + Lemma union_subseteq_r_alt x1 x2 y : x1 ⊆ x2 → x1 ⊆ y ∪ x2. Proof. intros. transitivity x2; auto. Qed. - Hint Resolve union_compat_l union_compat_r. + Hint Resolve union_subseteq_l_alt union_subseteq_r_alt. - Lemma union_compat x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∪ y1 ⊆ x2 ∪ y2. + Lemma union_preserving_l x y1 y2 : + y1 ⊆ y2 → + x ∪ y1 ⊆ x ∪ y2. + Proof. auto. Qed. + Lemma union_preserving_r x1 x2 y : + x1 ⊆ x2 → + x1 ∪ y ⊆ x2 ∪ y. + Proof. auto. Qed. + Lemma union_preserving x1 x2 y1 y2 : + x1 ⊆ x2 → y1 ⊆ y2 → + x1 ∪ y1 ⊆ x2 ∪ y2. Proof. auto. Qed. + Lemma union_empty x : x ∪ ∅ ⊆ x. Proof. by apply union_least. Qed. - Lemma union_comm x y : x ∪ y ⊆ y ∪ x. + Lemma union_comm_1 x y : x ∪ y ⊆ y ∪ x. Proof. auto. Qed. Lemma union_assoc_1 x y z : (x ∪ y) ∪ z ⊆ x ∪ (y ∪ z). Proof. auto. Qed. @@ -100,7 +145,8 @@ Section bounded_join_sl. Global Instance union_proper: Proper ((≡) ==> (≡) ==> (≡)) (∪). Proof. - unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. + unfold equiv, preorder_equiv. + split; apply union_preserving; simpl in *; tauto. Qed. Global Instance: Idempotent (≡) (∪). Proof. split; eauto. Qed. @@ -109,7 +155,7 @@ Section bounded_join_sl. Global Instance: RightId (≡) ∅ (∪). Proof. split; eauto. Qed. Global Instance: Commutative (≡) (∪). - Proof. split; apply union_comm. Qed. + Proof. split; apply union_comm_1. Qed. Global Instance: Associative (≡) (∪). Proof. split. apply union_assoc_2. apply union_assoc_1. Qed. @@ -123,13 +169,39 @@ Section bounded_join_sl. Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅. Proof. split; eauto. Qed. - Global Instance: Proper (eqlistA (≡) ==> (≡)) union_list. + Global Instance union_list_proper: + Proper (eqlistA (≡) ==> (≡)) union_list. Proof. induction 1; simpl. * done. * by apply union_proper. Qed. + Lemma union_list_nil : ⋃ @nil A = ∅. + Proof. done. Qed. + Lemma union_list_cons (X : A) (Xs : list A) : ⋃ (X :: Xs) = X ∪ ⋃ Xs. + Proof. done. Qed. + Lemma union_list_singleton (X : A) : ⋃ [X] ≡ X. + Proof. simpl. by rewrite (right_id ∅ _). Qed. + Lemma union_list_app (Xs1 Xs2 : list A) : ⋃ (Xs1 ++ Xs2) ≡ ⋃ Xs1 ∪ ⋃ Xs2. + Proof. + induction Xs1 as [|X Xs1 IH]; simpl. + * by rewrite (left_id ∅ _). + * by rewrite IH, (associative _). + Qed. + Lemma union_list_reverse (Xs : list A) : + ⋃ (reverse Xs) ≡ ⋃ Xs. + Proof. + induction Xs as [|X Xs IH]; simpl; [done |]. + by rewrite reverse_cons, union_list_app, + union_list_singleton, (commutative _), IH. + Qed. + + Lemma union_list_preserving (Xs Ys : list A) : + Forall2 (⊆) Xs Ys → + ⋃ Xs ⊆ ⋃ Ys. + Proof. induction 1; simpl; auto using union_preserving. Qed. + Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅. Proof. split. @@ -144,11 +216,56 @@ Section bounded_join_sl. * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union. Qed. - Context `{∀ X Y : A, Decision (X ⊆ Y)}. - Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅. - Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed. - Lemma non_empty_list_union Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs. - Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed. + Section leibniz. + Context `{!LeibnizEquiv A}. + + Global Instance: Idempotent (=) (∪). + Proof. intros ?. unfold_leibniz. apply (idempotent _). Qed. + Global Instance: LeftId (=) ∅ (∪). + Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed. + Global Instance: RightId (=) ∅ (∪). + Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed. + Global Instance: Commutative (=) (∪). + Proof. intros ??. unfold_leibniz. apply (commutative _). Qed. + Global Instance: Associative (=) (∪). + Proof. intros ???. unfold_leibniz. apply (associative _). Qed. + + Lemma subseteq_union_L X Y : X ⊆ Y ↔ X ∪ Y = Y. + Proof. unfold_leibniz. apply subseteq_union. Qed. + Lemma subseteq_union_1_L X Y : X ⊆ Y → X ∪ Y = Y. + Proof. unfold_leibniz. apply subseteq_union_1. Qed. + Lemma subseteq_union_2_L X Y : X ∪ Y = Y → X ⊆ Y. + Proof. unfold_leibniz. apply subseteq_union_2. Qed. + + Lemma equiv_empty_L X : X ⊆ ∅ → X = ∅. + Proof. unfold_leibniz. apply equiv_empty. Qed. + Lemma union_list_singleton_L (X : A) : ⋃ [X] = X. + Proof. unfold_leibniz. apply union_list_singleton. Qed. + Lemma union_list_app_L (Xs1 Xs2 : list A) : ⋃ (Xs1 ++ Xs2) = ⋃ Xs1 ∪ ⋃ Xs2. + Proof. unfold_leibniz. apply union_list_app. Qed. + Lemma union_list_reverse_L (Xs : list A) : ⋃ (reverse Xs) = ⋃ Xs. + Proof. unfold_leibniz. apply union_list_reverse. Qed. + + Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅. + Proof. unfold_leibniz. apply empty_union. Qed. + Lemma empty_list_union_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs. + Proof. unfold_leibniz. apply empty_list_union. Qed. + End leibniz. + + Section dec. + Context `{∀ X Y : A, Decision (X ⊆ Y)}. + + Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅. + Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed. + Lemma non_empty_list_union Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs. + Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed. + + Context `{!LeibnizEquiv A}. + Lemma non_empty_union_L X Y : X ∪ Y ≠∅ → X ≠∅ ∨ Y ≠∅. + Proof. unfold_leibniz. apply non_empty_union. Qed. + Lemma non_empty_list_union_L Xs : ⋃ Xs ≠∅ → Exists (≠∅) Xs. + Proof. unfold_leibniz. apply non_empty_list_union. Qed. + End dec. End bounded_join_sl. (** * Meet semi lattices *) @@ -156,19 +273,29 @@ End bounded_join_sl. Section meet_sl. Context `{MeetSemiLattice A}. - Hint Resolve subseteq_intersection_l subseteq_intersection_r + Hint Resolve intersection_subseteq_l intersection_subseteq_r intersection_greatest. - Lemma intersection_compat_l x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2. + Lemma intersection_subseteq_l_alt x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2. Proof. intros. transitivity x1; auto. Qed. - Lemma intersection_compat_r x1 x2 y : x1 ⊆ x2 → y ∩ x1 ⊆ x2. + Lemma intersection_subseteq_r_alt x1 x2 y : x1 ⊆ x2 → y ∩ x1 ⊆ x2. Proof. intros. transitivity x1; auto. Qed. - Hint Resolve intersection_compat_l intersection_compat_r. + Hint Resolve intersection_subseteq_l_alt intersection_subseteq_r_alt. - Lemma intersection_compat x1 x2 y1 y2 : - x1 ⊆ x2 → y1 ⊆ y2 → x1 ∩ y1 ⊆ x2 ∩ y2. + Lemma intersection_preserving_l x y1 y2 : + y1 ⊆ y2 → + x ∩ y1 ⊆ x ∩ y2. + Proof. auto. Qed. + Lemma intersection_preserving_r x1 x2 y : + x1 ⊆ x2 → + x1 ∩ y ⊆ x2 ∩ y. + Proof. auto. Qed. + Lemma intersection_preserving x1 x2 y1 y2 : + x1 ⊆ x2 → y1 ⊆ y2 → + x1 ∩ y1 ⊆ x2 ∩ y2. Proof. auto. Qed. - Lemma intersection_comm x y : x ∩ y ⊆ y ∩ x. + + Lemma intersection_comm_1 x y : x ∩ y ⊆ y ∩ x. Proof. auto. Qed. Lemma intersection_assoc_1 x y z : (x ∩ y) ∩ z ⊆ x ∩ (y ∩ z). Proof. auto. Qed. @@ -178,12 +305,12 @@ Section meet_sl. Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∩). Proof. unfold equiv, preorder_equiv. split; - apply intersection_compat; simpl in *; tauto. + apply intersection_preserving; simpl in *; tauto. Qed. Global Instance: Idempotent (≡) (∩). Proof. split; eauto. Qed. Global Instance: Commutative (≡) (∩). - Proof. split; apply intersection_comm. Qed. + Proof. split; apply intersection_comm_1. Qed. Global Instance: Associative (≡) (∩). Proof. split. apply intersection_assoc_2. apply intersection_assoc_1. Qed. @@ -193,6 +320,24 @@ Section meet_sl. Proof. apply subseteq_intersection. Qed. Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y. Proof. apply subseteq_intersection. Qed. + + Section leibniz. + Context `{!LeibnizEquiv A}. + + Global Instance: Idempotent (=) (∩). + Proof. intros ?. unfold_leibniz. apply (idempotent _). Qed. + Global Instance: Commutative (=) (∩). + Proof. intros ??. unfold_leibniz. apply (commutative _). Qed. + Global Instance: Associative (=) (∩). + Proof. intros ???. unfold_leibniz. apply (associative _). Qed. + + Lemma subseteq_intersection_L X Y : X ⊆ Y ↔ X ∩ Y = X. + Proof. unfold_leibniz. apply subseteq_intersection. Qed. + Lemma subseteq_intersection_1_L X Y : X ⊆ Y → X ∩ Y = X. + Proof. unfold_leibniz. apply subseteq_intersection_1. Qed. + Lemma subseteq_intersection_2_L X Y : X ∩ Y = X → X ⊆ Y. + Proof. unfold_leibniz. apply subseteq_intersection_2. Qed. + End leibniz. End meet_sl. (** * Lower bounded lattices *) @@ -202,9 +347,61 @@ Section lower_bounded_lattice. Global Instance: LeftAbsorb (≡) ∅ (∩). Proof. split. - * by apply subseteq_intersection_l. + * by apply intersection_subseteq_l. * by apply subseteq_empty. Qed. Global Instance: RightAbsorb (≡) ∅ (∩). Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed. + + Global Instance: LeftDistr (≡) (∪) (∩). + Proof. + intros x y z. split. + * apply union_least. + { apply intersection_greatest; auto using union_subseteq_l. } + apply intersection_greatest. + + apply union_subseteq_r_alt, intersection_subseteq_l. + + apply union_subseteq_r_alt, intersection_subseteq_r. + * apply lbl_distr. + Qed. + Global Instance: RightDistr (≡) (∪) (∩). + Proof. intros x y z. by rewrite !(commutative _ _ z), (left_distr _ _). Qed. + + Global Instance: LeftDistr (≡) (∩) (∪). + Proof. + intros x y z. split. + * rewrite (left_distr (∪) (∩)). + apply intersection_greatest. + { apply union_subseteq_r_alt, intersection_subseteq_l. } + rewrite (right_distr (∪) (∩)). apply intersection_preserving. + + apply union_subseteq_l. + + done. + * apply intersection_greatest. + { apply union_least; auto using intersection_subseteq_l. } + apply union_least. + + apply intersection_subseteq_r_alt, union_subseteq_l. + + apply intersection_subseteq_r_alt, union_subseteq_r. + Qed. + Global Instance: RightDistr (≡) (∩) (∪). + Proof. + intros x y z. by rewrite !(commutative _ _ z), (left_distr _ _). + Qed. + + Section leibniz. + Context `{!LeibnizEquiv A}. + + Global Instance: LeftAbsorb (=) ∅ (∩). + Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed. + Global Instance: RightAbsorb (=) ∅ (∩). + Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed. + + Global Instance: LeftDistr (=) (∪) (∩). + Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed. + Global Instance: RightDistr (=) (∪) (∩). + Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. + + Global Instance: LeftDistr (=) (∩) (∪). + Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed. + Global Instance: RightDistr (=) (∩) (∪). + Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. + End leibniz. End lower_bounded_lattice. diff --git a/theories/pmap.v b/theories/pmap.v index b7c04de4..ee8d5550 100644 --- a/theories/pmap.v +++ b/theories/pmap.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This files implements an efficient implementation of finite maps whose keys range over Coq's data type of positive binary naturals [positive]. The @@ -29,7 +29,7 @@ Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) : Decision (x = y). Proof. solve_decision. Defined. -(** The following predicate describes non empty trees. *) +(** The following decidable predicate describes non empty trees. *) Inductive Pmap_ne {A} : Pmap_raw A → Prop := | Pmap_ne_val l x r : Pmap_ne (Pnode l (Some x) r) | Pmap_ne_l l r : Pmap_ne l → Pmap_ne (Pnode l None r) @@ -64,8 +64,9 @@ Proof. right; inversion_clear 1; intuition. Qed. -(** Now we restrict the data type of trees to those that are well formed. *) -Definition Pmap A := @dsig (Pmap_raw A) Pmap_wf _. +(** Now we restrict the data type of trees to those that are well formed and +thereby obtain a data type that ensures canonicity. *) +Definition Pmap A := dsig (@Pmap_wf A). (** * Operations on the data structure *) Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) : @@ -257,63 +258,79 @@ Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i : fmap f t !! i = fmap f (t !! i). Proof. revert i. induction t. done. by intros [?|?|]; simpl. Qed. -(** The [finmap_to_list] function is rather inefficient, but since we do not -use it for computation at this moment, we do not care. *) -Fixpoint Pto_list_raw {A} (t : Pmap_raw A) : list (positive * A) := +Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A) : + list (positive * A) := match t with | Pleaf => [] - | Pnode l o r => - option_case (λ x, [(1,x)]) [] o ++ - (fst_map (~0) <$> Pto_list_raw l) ++ - (fst_map (~1) <$> Pto_list_raw r) - end. + | Pnode l o r => option_case (λ x, [(Preverse j, x)]) [] o ++ + Pto_list_raw (j~0) l ++ Pto_list_raw (j~1) r + end%list. -Lemma Pto_list_raw_nodup {A} (t : Pmap_raw A) : NoDup (Pto_list_raw t). -Proof. - induction t as [|? IHl [?|] ? IHr]; simpl. - * constructor. - * rewrite NoDup_cons, NoDup_app, !(NoDup_fmap _). - repeat split; trivial. - + rewrite elem_of_app, !elem_of_list_fmap. - intros [[[??] [??]] | [[??] [??]]]; simpl in *; simplify_equality. - + intro. rewrite !elem_of_list_fmap. - intros [[??] [??]] [[??] [??]]; simpl in *; simplify_equality. - * rewrite NoDup_app, !(NoDup_fmap _). - repeat split; trivial. - intro. rewrite !elem_of_list_fmap. - intros [[??] [??]] [[??] [??]]; simpl in *; simplify_equality. -Qed. - -Lemma Pelem_of_to_list_raw {A} (t : Pmap_raw A) i x : - (i,x) ∈ Pto_list_raw t ↔ t !! i = Some x. +Lemma Pelem_of_to_list_raw_aux {A} (t : Pmap_raw A) j i x : + (i,x) ∈ Pto_list_raw j t ↔ ∃ i', i = i' ++ Preverse j ∧ t !! i' = Some x. Proof. split. - * revert i. induction t as [|? IHl [?|] ? IHr]; intros i; simpl. + * revert j. induction t as [|? IHl [?|] ? IHr]; intros j; simpl. + by rewrite ?elem_of_nil. - + rewrite elem_of_cons, !elem_of_app, !elem_of_list_fmap. - intros [? | [[[??] [??]] | [[??] [??]]]]; naive_solver. - + rewrite !elem_of_app, !elem_of_list_fmap. - intros [[[??] [??]] | [[??] [??]]]; naive_solver. - * revert i. induction t as [|? IHl [?|] ? IHr]; simpl. + + rewrite elem_of_cons, !elem_of_app. intros [?|[?|?]]. + - simplify_equality. exists 1. by rewrite (left_id 1 (++))%positive. + - destruct (IHl (j~0)) as (i' &?&?); trivial; subst. + exists (i' ~ 0). by rewrite Preverse_xO, (associative _). + - destruct (IHr (j~1)) as (i' &?&?); trivial; subst. + exists (i' ~ 1). by rewrite Preverse_xI, (associative _). + + rewrite !elem_of_app. intros [?|?]. + - destruct (IHl (j~0)) as (i' &?&?); trivial; subst. + exists (i' ~ 0). by rewrite Preverse_xO, (associative _). + - destruct (IHr (j~1)) as (i' &?&?); trivial; subst. + exists (i' ~ 1). by rewrite Preverse_xI, (associative _). + * intros (i' & ?& Hi'); subst. revert i' j Hi'. + induction t as [|? IHl [?|] ? IHr]; intros i j; simpl. + done. - + intros i. rewrite elem_of_cons, elem_of_app. - destruct i as [i|i|]; simpl. - - right. right. rewrite elem_of_list_fmap. - exists (i,x); simpl; auto. - - right. left. rewrite elem_of_list_fmap. - exists (i,x); simpl; auto. - - left. congruence. - + intros i. rewrite elem_of_app. - destruct i as [i|i|]; simpl. - - right. rewrite elem_of_list_fmap. - exists (i,x); simpl; auto. - - left. rewrite elem_of_list_fmap. - exists (i,x); simpl; auto. + + rewrite elem_of_cons, elem_of_app. destruct i as [i|i|]; simpl in *. + - right. right. specialize (IHr i (j~1)). + rewrite Preverse_xI, (associative_eq _) in IHr. auto. + - right. left. specialize (IHl i (j~0)). + rewrite Preverse_xO, (associative_eq _) in IHl. auto. + - left. simplify_equality. by rewrite (left_id_eq 1 (++))%positive. + + rewrite elem_of_app. destruct i as [i|i|]; simpl in *. + - right. specialize (IHr i (j~1)). + rewrite Preverse_xI, (associative_eq _) in IHr. auto. + - left. specialize (IHl i (j~0)). + rewrite Preverse_xO, (associative_eq _) in IHl. auto. - done. Qed. +Lemma Pelem_of_to_list_raw {A} (t : Pmap_raw A) i x : + (i,x) ∈ Pto_list_raw 1 t ↔ t !! i = Some x. +Proof. + rewrite Pelem_of_to_list_raw_aux. split. + * by intros (i' &?&?); subst. + * intros. by exists i. +Qed. + +Lemma Pto_list_raw_nodup {A} j (t : Pmap_raw A) : NoDup (Pto_list_raw j t). +Proof. + revert j. induction t as [|? IHl [?|] ? IHr]; simpl. + * constructor. + * intros. rewrite NoDup_cons, NoDup_app. split_ands; trivial. + + rewrite elem_of_app, !Pelem_of_to_list_raw_aux. + intros [(i&Hi&?)|(i&Hi&?)]. + - rewrite Preverse_xO in Hi. apply (f_equal Plength) in Hi. + rewrite !Papp_length in Hi. simpl in Hi. lia. + - rewrite Preverse_xI in Hi. apply (f_equal Plength) in Hi. + rewrite !Papp_length in Hi. simpl in Hi. lia. + + intros [??]. rewrite !Pelem_of_to_list_raw_aux. + intros (i1&?&?) (i2&Hi&?); subst. + rewrite Preverse_xO, Preverse_xI, !(associative_eq _) in Hi. + by apply (injective (++ _)) in Hi. + * intros. rewrite NoDup_app. split_ands; trivial. + intros [??]. rewrite !Pelem_of_to_list_raw_aux. + intros (i1&?&?) (i2&Hi&?); subst. + rewrite Preverse_xO, Preverse_xI, !(associative_eq _) in Hi. + by apply (injective (++ _)) in Hi. +Qed. Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := - λ t, Pto_list_raw (`t). + λ t, Pto_list_raw 1 (`t). Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B := match t with @@ -334,25 +351,26 @@ Proof. intros [?|?|]; simpl; Pnode_canon_rewrite; auto. Qed. -Global Instance Pmerge_raw {A} : Merge A (Pmap_raw A) := - fix Pmerge_raw f (t1 t2 : Pmap_raw A) : Pmap_raw A := +Global Instance Pmerge_raw : Merge Pmap_raw := + fix Pmerge_raw A B C f t1 t2 : Pmap_raw C := match t1, t2 with | Pleaf, t2 => Pmerge_aux (f None) t2 | t1, Pleaf => Pmerge_aux (flip f None) t1 | Pnode l1 o1 r1, Pnode l2 o2 r2 => - Pnode_canon (@merge _ _ Pmerge_raw f l1 l2) - (f o1 o2) (@merge _ _ Pmerge_raw f r1 r2) + Pnode_canon (@merge _ Pmerge_raw A B C f l1 l2) + (f o1 o2) (@merge _ Pmerge_raw A B C f r1 r2) end. Local Arguments Pmerge_aux _ _ _ _ : simpl never. -Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) : +Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 : Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2). Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed. -Global Instance Pmerge {A} : Merge A (Pmap A) := λ f t1 t2, +Global Instance Pmerge: Merge Pmap := λ A B C f t1 t2, dexist (merge f (`t1) (`t2)) (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)). -Lemma Pmerge_raw_spec {A} f (Hf : f None None = None) (t1 t2 : Pmap_raw A) i : +Lemma Pmerge_raw_spec {A B C} (f : option A → option B → option C) + (Hf : f None None = None) (t1 : Pmap_raw A) t2 i : merge f t1 t2 !! i = f (t1 !! i) (t2 !! i). Proof. revert t2 i. induction t1 as [| l1 IHl1 o1 r1 IHr1 ]. @@ -362,6 +380,7 @@ Proof. + intros [?|?|]; simpl; by Pnode_canon_rewrite. Qed. +(** * Instantiation of the finite map interface *) Global Instance: FinMap positive Pmap. Proof. split. @@ -373,5 +392,5 @@ Proof. * intros ??? [??]. by apply Plookup_raw_fmap. * intros ? [??]. apply Pto_list_raw_nodup. * intros ? [??]. apply Pelem_of_to_list_raw. - * intros ??? [??] [??] ?. by apply Pmerge_raw_spec. + * intros ??? ?? [??] [??] ?. by apply Pmerge_raw_spec. Qed. diff --git a/theories/prelude.v b/theories/prelude.v index aa488b80..46dcf9b1 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) Require Export base diff --git a/theories/tactics.v b/theories/tactics.v index 4f7915e2..c55d5738 100644 --- a/theories/tactics.v +++ b/theories/tactics.v @@ -1,6 +1,6 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) -(** This file collects some general purpose tactics that are used throughout +(** This file collects general purpose tactics that are used throughout the development. *) Require Export Psatz. Require Export base. @@ -18,9 +18,10 @@ declarations as the above. *) Tactic Notation "intuition" := intuition auto. (** A slightly modified version of Ssreflect's finishing tactic [done]. It -also performs [reflexivity] and does not compute the goal's [hnf] so as to -avoid unfolding setoid equalities. Note that this tactic performs much better -than Coq's [easy] as it does not perform [inversion]. *) +also performs [reflexivity] and uses symmetry of negated equalities. Compared +to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid +unfolding setoid equalities. Note that this tactic performs much better than +Coq's [easy] tactic as it does not perform [inversion]. *) Ltac done := trivial; intros; solve [ repeat first @@ -29,6 +30,7 @@ Ltac done := | reflexivity | discriminate | contradiction + | solve [apply not_symmetry; trivial] | split ] | match goal with H : ¬_ |- _ => solve [destruct H; trivial] @@ -36,12 +38,37 @@ Ltac done := Tactic Notation "by" tactic(tac) := tac; done. +(** Whereas the [split] tactic splits any inductive with one constructor, the +tactic [split_and] only splits a conjunction. *) +Ltac split_and := + match goal with + | |- _ ∧ _ => split + end. +Ltac split_ands := repeat split_and. + +(** The tactic [case_match] destructs an arbitrary match in the conclusion or +assumptions, and generates a corresponding equality. This tactic is best used +together with the [repeat] tactical. *) Ltac case_match := match goal with | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:? | |- context [ match ?x with _ => _ end ] => destruct x eqn:? end. +(** The tactic [assert T unless tac_fail by tac_success] is used to assert +[T] only if it is not provable by [tac_fail]. This is useful to build other +tactics where only propositions that are not trivially provable are being +asserted. *) +Tactic Notation "assert" constr(T) + "unless" tactic3(tac_fail) "by" tactic3(tac_success) := first + [ assert T by tac_fail; fail 1 + | assert T by tac_success ]. + +(** The tactic [repeat_on_hyps tac] repeatedly applies [tac] in unspecified +order on all hypotheses until it cannot be applied to any hypothesis anymore. *) +Tactic Notation "repeat_on_hyps" tactic3(tac) := + repeat match goal with H : _ |- _ => progress tac H end. + (** The tactic [clear dependent H1 ... Hn] clears the hypotheses [Hi] and their dependencies. *) Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) := @@ -66,25 +93,42 @@ Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5) hyp (H6) hyp(H7) hyp(H8) hyp(H9) hyp(H10) := clear dependent H1 H2 H3 H4 H5 H6 H7 H8 H9; clear dependent H10. -(** The tactic [first_of tac1 tac2] calls [tac1] and then calls [tac2] on the -first subgoal generated by [tac1] *) -Tactic Notation "first_of" tactic3(tac1) "by" tactic3(tac2) := - (tac1; [ tac2 ]) - || (tac1; [ tac2 |]) - || (tac1; [ tac2 | | ]) - || (tac1; [ tac2 | | | ]) - || (tac1; [ tac2 | | | | ]) - || (tac1; [ tac2 | | | | | ]) - || (tac1; [ tac2 | | | | | |]) - || (tac1; [ tac2 | | | | | | |]) - || (tac1; [ tac2 | | | | | | | |]) - || (tac1; [ tac2 | | | | | | | | |]) - || (tac1; [ tac2 | | | | | | | | | |]) - || (tac1; [ tac2 | | | | | | | | | | |]) - || (tac1; [ tac2 | | | | | | | | | | | |]). +(** The tactic [first_of t ft ot] calls [t] and then calls [ft] on the first +subgoal generated by [t], and [ot] on the other subgoals. *) +Ltac first_of t ft ot := + solve [t] + || (t; [ ft ]) + || (t; [ ft | ot ]) + || (t; [ ft | ot | ot ]) + || (t; [ ft | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot ]) + || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot ]). + +Ltac last_of t ot lt := + solve [t] + || (t; [ lt ]) + || (t; [ ot | lt ]) + || (t; [ ot | ot | lt ]) + || (t; [ ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ]) + || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ]). (** The tactic [is_non_dependent H] determines whether the goal's conclusion or -assumptions depend on [H]. *) +hypotheses depend on [H]. *) Tactic Notation "is_non_dependent" constr(H) := match goal with | _ : context [ H ] |- _ => fail 1 @@ -92,12 +136,16 @@ Tactic Notation "is_non_dependent" constr(H) := | _ => idtac end. -(* The tactic [var_eq x y] fails if [x] and [y] are unequal. *) +(** The tactic [var_eq x y] fails if [x] and [y] are unequal, and [var_neq] +does the converse. *) Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end. Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end. -Tactic Notation "repeat_on_hyps" tactic3(tac) := - repeat match goal with H : _ |- _ => progress tac H end. +(** The tactics [block_hyps] and [unblock_hyps] can be used to temporarily mark +certain hypothesis as being blocked. The tactic changes all hypothesis [H: T] +into [H: blocked T], where [blocked] is the identity function. If a hypothesis +is already blocked, it will not be blocked again. The tactic [unblock_hyps] +removes [blocked] everywhere. *) Ltac block_hyps := repeat_on_hyps (fun H => match type of H with @@ -163,19 +211,21 @@ Tactic Notation "feed" tactic(tac) constr(H) := (** The tactic [efeed tac H] is similar to [feed], but it also instantiates dependent premises of [H] with evars. *) -Tactic Notation "efeed" tactic(tac) constr(H) := +Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) := let rec go H := let T := type of H in lazymatch eval hnf in T with | ?T1 → ?T2 => let HT1 := fresh "feed" in assert T1 as HT1; - [| go (H HT1); clear HT1 ] + [bytac | go (H HT1); clear HT1 ] | ?T1 → _ => let e := fresh "feed" in evar (e:T1); let e' := eval unfold e in e in clear e; go (H e') | ?T1 => tac H end in go H. +Tactic Notation "efeed" constr(H) "using" tactic3(tac) := + efeed H using tac by idtac. (** The following variants of [pose proof], [specialize], [inversion], and [destruct], use the [feed] tactic before invoking the actual tactic. *) @@ -185,14 +235,14 @@ Tactic Notation "feed" "pose" "proof" constr(H) := feed (fun p => pose proof p) H. Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') := - efeed (fun p => pose proof p as H') H. + efeed H using (fun p => pose proof p as H'). Tactic Notation "efeed" "pose" "proof" constr(H) := - efeed (fun p => pose proof p) H. + efeed H using (fun p => pose proof p). Tactic Notation "feed" "specialize" hyp(H) := feed (fun p => specialize p) H. Tactic Notation "efeed" "specialize" hyp(H) := - efeed (fun p => specialize p) H. + efeed H using (fun p => specialize p). Tactic Notation "feed" "inversion" constr(H) := feed (fun p => let H':=fresh in pose proof p as H'; inversion H') H. @@ -220,7 +270,7 @@ for the purposes of this development. This tactic either fails or proves the goal. *) Tactic Notation "naive_solver" tactic(tac) := unfold iff, not in *; - let rec go := + let rec go n := repeat match goal with (**i intros *) | |- ∀ _, _ => intro @@ -232,36 +282,48 @@ Tactic Notation "naive_solver" tactic(tac) := | |- _ => progress simpl in * | |- _ => progress simplify_equality (**i solve the goal *) - | |- _ => solve [ eassumption | symmetry; eassumption | reflexivity ] + | |- _ => solve + [ eassumption + | symmetry; eassumption + | apply not_symmetry; eassumption + | reflexivity ] (**i operations that generate more subgoals *) | |- _ ∧ _ => split | H : _ ∨ _ |- _ => destruct H (**i solve the goal using the user supplied tactic *) | |- _ => solve [tac] end; - (**i use recursion to enable backtracking on the following clauses *) - match goal with - (**i instantiations of assumptions *) - | H : _ → _ |- _ => - is_non_dependent H; eapply H; clear H; go - | H : _ → _ |- _ => - is_non_dependent H; - (**i create subgoals for all premises *) - efeed (fun p => - match type of p with - | _ ∧ _ => - let H' := fresh in pose proof p as H'; destruct H' - | ∃ _, _ => - let H' := fresh in pose proof p as H'; destruct H' - | _ ∨ _ => - let H' := fresh in pose proof p as H'; destruct H' - | False => - let H' := fresh in pose proof p as H'; destruct H' - end) H; - (**i solve these subgoals, but clear [H] to avoid loops *) - clear H; go - (**i instantiation of the conclusion *) - | |- ∃ x, _ => eexists; go - | |- _ ∨ _ => first [left; go | right; go] - end in go. + (**i use recursion to enable backtracking on the following clauses. We use + a counter to minimize the number of instantiations, and thus to reduce the + number of potentially unresolved meta variables. *) + first + [ iter (fun n' => + match goal with + (**i instantiations of assumptions *) + | H : _ → _ |- _ => + is_non_dependent H; + eapply H; clear H; go n' + | H : _ → _ |- _ => + is_non_dependent H; + (**i create subgoals for all premises *) + efeed H using (fun p => + match type of p with + | _ ∧ _ => + let H' := fresh in pose proof p as H'; destruct H' + | ∃ _, _ => + let H' := fresh in pose proof p as H'; destruct H' + | _ ∨ _ => + let H' := fresh in pose proof p as H'; destruct H' + | False => + let H' := fresh in pose proof p as H'; destruct H' + end) by (clear H; go n'); + (**i solve these subgoals, but clear [H] to avoid loops *) + clear H; go n + end) (eval compute in (seq 0 n)) + | match goal with + (**i instantiation of the conclusion *) + | |- ∃ x, _ => eexists; go n + | |- _ ∨ _ => first [left; go n | right; go n] + end] + in go 10. Tactic Notation "naive_solver" := naive_solver eauto. diff --git a/theories/vector.v b/theories/vector.v index 20514323..a7dd52ee 100644 --- a/theories/vector.v +++ b/theories/vector.v @@ -1,4 +1,4 @@ -(* Copyright (c) 2012, Robbert Krebbers. *) +(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects general purpose definitions and theorems on vectors (lists of fixed length) and the fin type (bounded naturals). It uses the @@ -132,6 +132,14 @@ Proof. apply vcons_inj. Qed. Lemma vcons_inj_2 {A n} x y (v w : vec A n) : x ::: v = y ::: w → v = w. Proof. apply vcons_inj. Qed. +Lemma vec_eq {A n} (v w : vec A n) : + (∀ i, v !!! i = w !!! i) → v = w. +Proof. + vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal. + * apply (Hi 0%fin). + * apply IH. intros i. apply (Hi (FS i)). +Qed. + Instance vec_dec {A} {dec : ∀ x y : A, Decision (x = y)} {n} : ∀ v w : vec A n, Decision (v = w). Proof. @@ -204,6 +212,9 @@ Proof. by induction l; simpl; f_equal. Qed. Lemma vec_to_list_length {A n} (v : vec A n) : length (vec_to_list v) = n. Proof. induction v; simpl; by f_equal. Qed. +Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) : + same_length v w. +Proof. apply same_length_length. by rewrite !vec_to_list_length. Qed. Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) : vec_to_list v = vec_to_list w → n = m. @@ -234,8 +245,7 @@ Proof. rewrite <-(vec_to_list_of_list l), <-(vec_to_list_of_list k) in H. rewrite <-vec_to_list_cons, <-vec_to_list_app in H. pose proof (vec_to_list_inj1 _ _ H); subst. - apply vec_to_list_inj2 in H; subst. - induction l. simpl. + apply vec_to_list_inj2 in H; subst. induction l. simpl. * eexists 0%fin. simpl. by rewrite vec_to_list_of_list. * destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence. Qed. @@ -300,7 +310,7 @@ Proof. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)). Qed. -(** The function [vmap f v] applies a function [f] element wise to [v]. *) +(** The function [vmap f v] applies a funlocks (mem_unlock (⋃ Ωs) (⋃ ms)) ≡ ∅ction [f] element wise to [v]. *) Notation vmap := Vector.map. Lemma vlookup_map `(f : A → B) {n} (v : vec A n) i : @@ -315,10 +325,20 @@ Proof. induction v; simpl. done. by rewrite IHv. Qed. wise using the function [f]. *) Notation vzip_with := Vector.map2. -Lemma vzip_with_lookup `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i : +Lemma vlookup_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i : vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i). Proof. by apply Vector.nth_map2. Qed. +Lemma vec_to_list_zip_with `(f : A → B → C) {n} + (v1 : vec A n) (v2 : vec B n) : + vec_to_list (vzip_with f v1 v2) = + zip_with f (vec_to_list v1) (vec_to_list v2). +Proof. + revert v2. induction v1; intros v2; inv_vec v2; intros; simpl. + * done. + * by rewrite IHv1. +Qed. + (** Similar to vlookup, we cannot define [vinsert] as an instance of the [Insert] type class, as it has a dependent type. *) Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n → vec A n := -- GitLab