diff --git a/theories/ars.v b/theories/ars.v index 57004f7ebb1669f179674ce8c42748d3fbe7ab4c..dd3484a4bb4ca59fda1bf896d493965b676b6cf7 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 b6bf6540c75bcf3884dee06f2c6496f55db695c6..709d29b590c78028cc6fd6cea87bf7318133f612 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 b96b6836cd89a3c643b5cd559c8e2f92c0b068ae..7d4c52dbd32858473e49a9f7ccc557269c90a4db 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 56a619e9625fa572d76793eaec885b7a0a8a1838..662d208416bf902650a42c9cd2405193eeb3cde1 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 35808597bc1ab411f30f29422ec9b88371ca8ad4..469696128a9750806f3c1ce484ff934889ca8363 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 0000000000000000000000000000000000000000..2ca9a5836e1127e08d14b8d0fe0276fb0b3c2725 --- /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 fd6e367503c49c2dbbb67f5be3c33cf5982db119..5c4acc4e76632214cc8a0647fe4cb1a056f6acbe 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 0be3b5577a06346374b738643ae9e64bba1a7070..84f0ec2c669bad6ba68dee21bacc8ddbfcef5e57 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 728aab8f327e8b3b59b9d560dc4c219bfd0b44ac..97509a7c394d78d6f6dfc24439ce17641754ff0e 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 21da87526f4ea6fd31167f0c7b3333f06e41c739..7738d9e90fd0b264876800c64af1be14a2f9238e 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 a63c969a5f1149fd13471c81502c4760b651b8ab..86b91d5b06efb8c8aa53e9ec41a4429ef657d56d 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 0000000000000000000000000000000000000000..25b7d40d9d6256910ed445e15f71d10ea4be5438 --- /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 312e9ee9b9e52fae96f934b56095504021691c21..8fac809aa29c49311780f2a41ca0859026374d50 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 e19e1019f9bcf9de216d421110408a4d922a0a4b..d08d8c3c3a8bcb84b112b52e40e0e4a37433e864 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 455d1a73ea7f084e84f3700a8936ab6d8a0c1434..22847c93c471d45ab69397a880c5d08aa5c10d3a 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 89c4554122d4f25206b541d0573c1f960c5d5b92..af0bec44511383fcd134db24e743f05fdb5ef16d 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 b7c04de4839d8bc00ff95769746e3d68059a237f..ee8d5550aee83f2eee2c32e539746e86a451f196 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 aa488b804e93688a7f929247d2ae4960f0ab0392..46dcf9b1b075a9450a0eddaf5d69d94a1de19055 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 4f7915e25b337e7cce9e504f4635565e009492f6..c55d57387359b0c4ffb28146c3b1d26d121d2e86 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 2051432340b439b00300c29546038048ccfb41c7..a7dd52ee60f51c35147e95f09e3b6071a094a300 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 :=