diff --git a/theories/base.v b/theories/base.v index 323dd30d14e43c84bb6540f63f5ba17ccc7ceb56..fb129db3dda95ff55f794e2deaa66b9d210dfd6f 100644 --- a/theories/base.v +++ b/theories/base.v @@ -94,6 +94,9 @@ Proof. split; repeat intro; congruence. Qed. (** We define an operational type class for setoid equality. This is based on (Spitters/van der Weegen, 2011). *) Class Equiv A := equiv: relation A. +(* No Hint Mode set because of Coq bug #5735 +Hint Mode Equiv ! : typeclass_instances. *) + Infix "≡" := equiv (at level 70, no associativity) : C_scope. Notation "(≡)" := equiv (only parsing) : C_scope. Notation "( X ≡)" := (equiv X) (only parsing) : C_scope. @@ -108,10 +111,12 @@ 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. +Hint Mode LeibnizEquiv ! - : typeclass_instances. + Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) : x ≡ y ↔ x = y. Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed. - + Ltac fold_leibniz := repeat match goal with | H : context [ @equiv ?A _ _ _ ] |- _ => @@ -149,12 +154,14 @@ propositions. For example to declare a parameter expressing decidable equality on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing [decide (x = y)]. *) Class Decision (P : Prop) := decide : {P} + {¬P}. +Hint Mode Decision ! : typeclass_instances. Arguments decide _ {_} : assert. Notation EqDecision A := (∀ x y : A, Decision (x = y)). (** ** Inhabited types *) (** This type class collects types that are inhabited. *) Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Hint Mode Inhabited ! : typeclass_instances. Arguments populate {_} _ : assert. (** ** Proof irrelevant types *) @@ -162,6 +169,7 @@ Arguments populate {_} _ : assert. elements of the type are equal. We use this notion only used for propositions, but by universe polymorphism we can generalize it. *) Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y. +Hint Mode ProofIrrel ! : typeclass_instances. (** ** Common properties *) (** These operational type classes allow us to refer to common mathematical @@ -625,14 +633,17 @@ relations on collections: the empty collection [∅], the union [(∪)], intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset [(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *) Class Empty A := empty: A. +Hint Mode Empty ! : typeclass_instances. Notation "∅" := empty : C_scope. Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅. Class Top A := top : A. +Hint Mode Top ! : typeclass_instances. Notation "⊤" := top : C_scope. Class Union A := union: A → A → A. +Hint Mode Union ! : typeclass_instances. Instance: Params (@union) 2. Infix "∪" := union (at level 50, left associativity) : C_scope. Notation "(∪)" := union (only parsing) : C_scope. @@ -650,6 +661,7 @@ Arguments union_list _ _ _ !_ / : assert. Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : C_scope. Class Intersection A := intersection: A → A → A. +Hint Mode Intersection ! : typeclass_instances. Instance: Params (@intersection) 2. Infix "∩" := intersection (at level 40) : C_scope. Notation "(∩)" := intersection (only parsing) : C_scope. @@ -657,6 +669,7 @@ Notation "( x ∩)" := (intersection x) (only parsing) : C_scope. Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope. Class Difference A := difference: A → A → A. +Hint Mode Difference ! : typeclass_instances. Instance: Params (@difference) 2. Infix "∖" := difference (at level 40, left associativity) : C_scope. Notation "(∖)" := difference (only parsing) : C_scope. @@ -670,6 +683,7 @@ Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*))) (at level 50, left associativity) : C_scope. Class Singleton A B := singleton: A → B. +Hint Mode Singleton - ! : typeclass_instances. Instance: Params (@singleton) 3. Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope. Notation "{[ x ; y ; .. ; z ]}" := @@ -681,6 +695,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z)) (at level 1, y at next level, z at next level) : C_scope. Class SubsetEq A := subseteq: relation A. +Hint Mode SubsetEq ! : typeclass_instances. Instance: Params (@subseteq) 2. Infix "⊆" := subseteq (at level 70) : C_scope. Notation "(⊆)" := subseteq (only parsing) : C_scope. @@ -720,8 +735,10 @@ Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) is used to create finite maps, finite sets, etc, and is typically different from the order [(⊆)]. *) Class Lexico A := lexico: relation A. +Hint Mode Lexico ! : typeclass_instances. Class ElemOf A B := elem_of: A → B → Prop. +Hint Mode ElemOf - ! : typeclass_instances. Instance: Params (@elem_of) 3. Infix "∈" := elem_of (at level 70) : C_scope. Notation "(∈)" := elem_of (only parsing) : C_scope. @@ -733,6 +750,7 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope. Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope. Class Disjoint A := disjoint : A → A → Prop. +Hint Mode Disjoint ! : typeclass_instances. Instance: Params (@disjoint) 2. Infix "⊥" := disjoint (at level 70) : C_scope. Notation "(⊥)" := disjoint (only parsing) : C_scope. @@ -749,6 +767,7 @@ Hint Extern 0 (_ ⊥ _) => symmetry; eassumption. Hint Extern 0 (_ ⊥* _) => symmetry; eassumption. Class DisjointE E A := disjointE : E → A → A → Prop. +Hint Mode DisjointE - ! : typeclass_instances. Instance: Params (@disjointE) 4. Notation "X ⊥{ Γ } Y" := (disjointE Γ X Y) (at level 70, format "X ⊥{ Γ } Y") : C_scope. @@ -765,11 +784,14 @@ Notation "Xs ⊥{ Γ1 , Γ2 , .. , Γ3 }* Ys" := Hint Extern 0 (_ ⊥{_} _) => symmetry; eassumption. Class DisjointList A := disjoint_list : list A → Prop. +Hint Mode DisjointList ! : typeclass_instances. Instance: Params (@disjoint_list) 2. Notation "⊥ Xs" := (disjoint_list Xs) (at level 20, format "⊥ Xs") : C_scope. Section disjoint_list. Context `{Disjoint A, Union A, Empty A}. + Implicit Types X : A. + Inductive disjoint_list_default : DisjointList A := | disjoint_nil_2 : ⊥ (@nil A) | disjoint_cons_2 (X : A) (Xs : list A) : X ⊥ ⋃ Xs → ⊥ Xs → ⊥ (X :: Xs). @@ -782,8 +804,10 @@ Section disjoint_list. End disjoint_list. Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B. +Hint Mode Filter - ! : typeclass_instances. Class UpClose A B := up_close : A → B. +Hint Mode UpClose - ! : typeclass_instances. Notation "↑ x" := (up_close x) (at level 20, format "↑ x"). (** * Monadic operations *) @@ -850,6 +874,7 @@ Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o)) on maps. In the file [fin_maps] we will axiomatize finite maps. The function look up [m !! k] should yield the element at key [k] in [m]. *) Class Lookup (K A M : Type) := lookup: K → M → option A. +Hint Mode Lookup - - ! : typeclass_instances. Instance: Params (@lookup) 4. Notation "m !! i" := (lookup i m) (at level 20) : C_scope. Notation "(!!)" := lookup (only parsing) : C_scope. @@ -859,12 +884,14 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert. (** The singleton map *) Class SingletonM K A M := singletonM: K → A → M. +Hint Mode SingletonM - - ! : typeclass_instances. Instance: Params (@singletonM) 5. Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope. (** The function insert [<[k:=a]>m] should update the element at key [k] with value [a] in [m]. *) Class Insert (K A M : Type) := insert: K → A → M → M. +Hint Mode Insert - - ! : typeclass_instances. Instance: Params (@insert) 5. Notation "<[ k := a ]>" := (insert k a) (at level 5, right associativity, format "<[ k := a ]>") : C_scope. @@ -874,12 +901,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert. [m]. If the key [k] is not a member of [m], the original map should be returned. *) Class Delete (K M : Type) := delete: K → M → M. +Hint Mode Delete - ! : typeclass_instances. Instance: Params (@delete) 4. Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert. (** The function [alter f k m] should update the value at key [k] using the function [f], which is called with the original value. *) Class Alter (K A M : Type) := alter: (A → A) → K → M → M. +Hint Mode Alter - - ! : typeclass_instances. Instance: Params (@alter) 5. Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert. @@ -889,12 +918,14 @@ if [k] is not a member of [m]. The value at [k] should be deleted if [f] yields [None]. *) Class PartialAlter (K A M : Type) := partial_alter: (option A → option A) → K → M → M. +Hint Mode PartialAlter - - ! : typeclass_instances. Instance: Params (@partial_alter) 4. Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert. (** 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 (M C : Type) := dom: M → C. +Hint Mode Dom ! ! : typeclass_instances. Instance: Params (@dom) 3. Arguments dom : clear implicits. Arguments dom {_} _ {_} !_ / : simpl nomatch, assert. @@ -903,6 +934,7 @@ Arguments dom {_} _ {_} !_ / : simpl nomatch, assert. 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. +Hint Mode Merge ! : typeclass_instances. Instance: Params (@merge) 4. Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert. @@ -911,17 +943,20 @@ and [m2] using the function [f] to combine values of members that are in both [m1] and [m2]. *) Class UnionWith (A M : Type) := union_with: (A → A → option A) → M → M → M. +Hint Mode UnionWith - ! : typeclass_instances. Instance: Params (@union_with) 3. Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. (** Similarly for intersection and difference. *) Class IntersectionWith (A M : Type) := intersection_with: (A → A → option A) → M → M → M. +Hint Mode IntersectionWith - ! : typeclass_instances. Instance: Params (@intersection_with) 3. Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. Class DifferenceWith (A M : Type) := difference_with: (A → A → option A) → M → M → M. +Hint Mode DifferenceWith - ! : typeclass_instances. Instance: Params (@difference_with) 3. Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. @@ -930,6 +965,7 @@ Definition intersection_with_list `{IntersectionWith A M} Arguments intersection_with_list _ _ _ _ _ !_ / : assert. Class LookupE (E K A M : Type) := lookupE: E → K → M → option A. +Hint Mode LookupE - - - ! : typeclass_instances. Instance: Params (@lookupE) 6. Notation "m !!{ Γ } i" := (lookupE Γ i m) (at level 20, format "m !!{ Γ } i") : C_scope. @@ -937,6 +973,7 @@ Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope. Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert. Class InsertE (E K A M : Type) := insertE: E → K → A → M → M. +Hint Mode InsertE - - - ! : typeclass_instances. Instance: Params (@insertE) 6. Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a) (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope. @@ -963,6 +1000,7 @@ Class Collection A C `{ElemOf A C, Empty C, Singleton A C, enumerated as a list. These elements, given by the [elements] function, may be in any order and should not contain duplicates. *) Class Elements A C := elements: C → list A. +Hint Mode Elements - ! : typeclass_instances. Instance: Params (@elements) 3. (** We redefine the standard library's [In] and [NoDup] using type classes. *) @@ -998,6 +1036,7 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C, NoDup_elements X : NoDup (elements X) }. Class Size C := size: C → nat. +Hint Mode Size ! : typeclass_instances. Arguments size {_ _} !_ / : simpl nomatch, assert. Instance: Params (@size) 2. @@ -1025,6 +1064,7 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A), will later prove that [fresh] is [Proper] with respect to the induced setoid equality on collections. *) Class Fresh A C := fresh: C → A. +Hint Mode Fresh - ! : typeclass_instances. Instance: Params (@fresh) 3. Class FreshSpec A C `{ElemOf A C, Empty C, Singleton A C, Union C, Fresh A C} : Prop := { @@ -1035,5 +1075,6 @@ Class FreshSpec A C `{ElemOf A C, (** * Miscellaneous *) Class Half A := half: A → A. +Hint Mode Half ! : typeclass_instances. Notation "½" := half : C_scope. Notation "½*" := (fmap (M:=list) half) : C_scope. diff --git a/theories/coPset.v b/theories/coPset.v index 68b8466fea08fbbc555e05fac3fd95339e275e7e..4af9f0233e92a20b4d420be0b68ec9d769b87a0d 100644 --- a/theories/coPset.v +++ b/theories/coPset.v @@ -427,7 +427,7 @@ Proof. rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht. induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto. Qed. -Lemma coPset_split X : +Lemma coPset_split (X : coPset) : ¬set_finite X → ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ ¬set_finite X1 ∧ ¬set_finite X2. Proof. diff --git a/theories/collections.v b/theories/collections.v index bb6c4b5fcaff5d76ffc8deb361b0922ac5b6a773..134af648961b502059787fe706048e0cb79dcfd7 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -145,9 +145,9 @@ Section set_unfold_simple. Implicit Types x y : A. Implicit Types X Y : C. - Global Instance set_unfold_empty x : SetUnfold (x ∈ ∅) False. + Global Instance set_unfold_empty x : SetUnfold (x ∈ (∅ : C)) False. Proof. constructor. split. apply not_elem_of_empty. done. Qed. - Global Instance set_unfold_singleton x y : SetUnfold (x ∈ {[ y ]}) (x = y). + Global Instance set_unfold_singleton x y : SetUnfold (x ∈ ({[ y ]} : C)) (x = y). Proof. constructor; apply elem_of_singleton. Qed. Global Instance set_unfold_union x X Y P Q : SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ∪ Y) (P ∨ Q). @@ -161,30 +161,30 @@ Section set_unfold_simple. (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5. Proof. intros ?; constructor. unfold equiv, collection_equiv. - pose proof not_elem_of_empty; naive_solver. + pose proof (not_elem_of_empty (C:=C)); naive_solver. Qed. - Global Instance set_unfold_equiv_empty_r (P : A → Prop) : + Global Instance set_unfold_equiv_empty_r (P : A → Prop) X : (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5. Proof. intros ?; constructor. unfold equiv, collection_equiv. - pose proof not_elem_of_empty; naive_solver. + pose proof (not_elem_of_empty (C:=C)); naive_solver. Qed. - Global Instance set_unfold_equiv (P Q : A → Prop) : + Global Instance set_unfold_equiv (P Q : A → Prop) X : (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ≡ Y) (∀ x, P x ↔ Q x) | 10. Proof. constructor. apply forall_proper; naive_solver. Qed. - Global Instance set_unfold_subseteq (P Q : A → Prop) : + Global Instance set_unfold_subseteq (P Q : A → Prop) X Y : (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊆ Y) (∀ x, P x → Q x). Proof. constructor. apply forall_proper; naive_solver. Qed. - Global Instance set_unfold_subset (P Q : A → Prop) : + Global Instance set_unfold_subset (P Q : A → Prop) X : (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊂ Y) ((∀ x, P x → Q x) ∧ ¬∀ x, Q x → P x). Proof. constructor. unfold strict. repeat f_equiv; apply forall_proper; naive_solver. Qed. - Global Instance set_unfold_disjoint (P Q : A → Prop) : + Global Instance set_unfold_disjoint (P Q : A → Prop) X Y : (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊥ Y) (∀ x, P x → Q x → False). Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed. @@ -195,10 +195,10 @@ Section set_unfold_simple. Global Instance set_unfold_equiv_empty_l_L X (P : A → Prop) : (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ = X) (∀ x, ¬P x) | 5. Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_l. Qed. - Global Instance set_unfold_equiv_empty_r_L (P : A → Prop) : + Global Instance set_unfold_equiv_empty_r_L (P : A → Prop) X : (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X = ∅) (∀ x, ¬P x) | 5. Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_r. Qed. - Global Instance set_unfold_equiv_L (P Q : A → Prop) : + Global Instance set_unfold_equiv_L (P Q : A → Prop) X Y : (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X = Y) (∀ x, P x ↔ Q x) | 10. Proof. constructor. unfold_leibniz. by apply set_unfold_equiv. Qed. @@ -224,20 +224,20 @@ Section set_unfold. End set_unfold. Section set_unfold_monad. - Context `{CollectionMonad M} {A : Type}. - Implicit Types x y : A. + Context `{CollectionMonad M}. - Global Instance set_unfold_ret x y : SetUnfold (x ∈ mret y) (x = y). + Global Instance set_unfold_ret {A} (x y : A) : + SetUnfold (x ∈ mret (M:=M) y) (x = y). Proof. constructor; apply elem_of_ret. Qed. - Global Instance set_unfold_bind {B} (f : A → M B) X (P Q : A → Prop) : + Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) : (∀ y, SetUnfold (y ∈ X) (P y)) → (∀ y, SetUnfold (x ∈ f y) (Q y)) → SetUnfold (x ∈ X ≫= f) (∃ y, Q y ∧ P y). Proof. constructor. rewrite elem_of_bind; naive_solver. Qed. - Global Instance set_unfold_fmap {B} (f : A → B) X (P : A → Prop) : + Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) : (∀ y, SetUnfold (y ∈ X) (P y)) → SetUnfold (x ∈ f <\$> X) (∃ y, x = f y ∧ P y). Proof. constructor. rewrite elem_of_fmap; naive_solver. Qed. - Global Instance set_unfold_join (X : M (M A)) (P : M A → Prop) : + Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) : (∀ Y, SetUnfold (Y ∈ X) (P Y)) → SetUnfold (x ∈ mjoin X) (∃ Y, x ∈ Y ∧ P Y). Proof. constructor. rewrite elem_of_join; naive_solver. Qed. End set_unfold_monad. @@ -381,7 +381,7 @@ Section simple_collection. Proof. set_solver. Qed. Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. Proof. set_solver. Qed. - Lemma elem_of_empty x : x ∈ ∅ ↔ False. + Lemma elem_of_empty x : x ∈ (∅ : C) ↔ False. Proof. set_solver. Qed. Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅. Proof. set_solver. Qed. @@ -393,15 +393,15 @@ Section simple_collection. Proof. set_solver. Qed. (** Singleton *) - Lemma elem_of_singleton_1 x y : x ∈ {[y]} → x = y. + Lemma elem_of_singleton_1 x y : x ∈ ({[y]} : C) → x = y. Proof. by rewrite elem_of_singleton. Qed. - Lemma elem_of_singleton_2 x y : x = y → x ∈ {[y]}. + Lemma elem_of_singleton_2 x y : x = y → x ∈ ({[y]} : C). Proof. by rewrite elem_of_singleton. Qed. Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X. Proof. set_solver. Qed. Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅. Proof. set_solver. Qed. - Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y. + Lemma not_elem_of_singleton x y : x ∉ ({[ y ]} : C) ↔ x ≠ y. Proof. by rewrite elem_of_singleton. Qed. (** Disjointness *) @@ -512,7 +512,7 @@ Section simple_collection. Proof. unfold_leibniz. apply non_empty_inhabited. Qed. (** Singleton *) - Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅. + Lemma non_empty_singleton_L x : {[ x ]} ≠ (∅ : C). Proof. unfold_leibniz. apply non_empty_singleton. Qed. (** Big unions *) @@ -554,6 +554,7 @@ End simple_collection. (** * Collections with [∪], [∩], [∖], [∅] and [{[_]}] *) Section collection. Context `{Collection A C}. + Implicit Types x y : A. Implicit Types X Y : C. (** Intersection *) @@ -654,7 +655,7 @@ Section collection. Global Instance intersection_empty_r_L: RightAbsorb ((=) : relation C) ∅ (∩). Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed. - Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = {[x]}. + Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = ({[x]} : C). Proof. unfold_leibniz. apply intersection_singletons. Qed. Lemma union_intersection_l_L X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z). @@ -719,7 +720,7 @@ Section collection. {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}). Proof. intro y; split; intros Hy; [ set_solver | ]. - destruct (decide (y ∈ {[x]})); set_solver. + destruct (decide (y ∈ ({[x]} : C))); set_solver. Qed. Context `{!LeibnizEquiv C}. @@ -736,7 +737,6 @@ Section collection. Lemma singleton_union_difference_L X Y x : {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}). Proof. unfold_leibniz. apply singleton_union_difference. Qed. - End dec. End collection. @@ -751,26 +751,26 @@ Section of_option_list. Context `{SimpleCollection A C}. Implicit Types l : list A. - Lemma elem_of_of_option (x : A) mx: x ∈ of_option mx ↔ mx = Some x. + Lemma elem_of_of_option (x : A) mx: x ∈ of_option (C:=C) mx ↔ mx = Some x. Proof. destruct mx; set_solver. Qed. - Lemma not_elem_of_of_option (x : A) mx: x ∉ of_option mx ↔ mx ≠ Some x. + Lemma not_elem_of_of_option (x : A) mx: x ∉ of_option (C:=C) mx ↔ mx ≠ Some x. Proof. by rewrite elem_of_of_option. Qed. - Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l. + Lemma elem_of_of_list (x : A) l : x ∈ of_list (C:=C) l ↔ x ∈ l. Proof. split. - induction l; simpl; [by rewrite elem_of_empty|]. rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto. - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto. Qed. - Lemma not_elem_of_of_list (x : A) l : x ∉ of_list l ↔ x ∉ l. + Lemma not_elem_of_of_list (x : A) l : x ∉ of_list (C:=C) l ↔ x ∉ l. Proof. by rewrite elem_of_of_list. Qed. Global Instance set_unfold_of_option (mx : option A) x : - SetUnfold (x ∈ of_option mx) (mx = Some x). + SetUnfold (x ∈ of_option (C:=C) mx) (mx = Some x). Proof. constructor; apply elem_of_of_option. Qed. Global Instance set_unfold_of_list (l : list A) x P : - SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list l) P. + SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list (C:=C) l) P. Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x ∈ l) P). Qed. Lemma of_list_nil : of_list (C:=C) [] = ∅. @@ -810,7 +810,7 @@ Section collection_monad_base. rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard. destruct (decide P); naive_solver. Qed. - Global Instance set_unfold_guard `{Decision P} {A} (x : A) X Q : + Global Instance set_unfold_guard `{Decision P} {A} (x : A) (X : M A) Q : SetUnfold (x ∈ X) Q → SetUnfold (x ∈ guard P; X) (P ∧ Q). Proof. constructor. by rewrite elem_of_guard, (set_unfold (x ∈ X) Q). Qed. Lemma bind_empty {A B} (f : A → M B) X : @@ -824,11 +824,12 @@ Definition set_Forall `{ElemOf A C} (P : A → Prop) (X : C) := ∀ x, x ∈ X Definition set_Exists `{ElemOf A C} (P : A → Prop) (X : C) := ∃ x, x ∈ X ∧ P x. Section quantifiers. - Context `{SimpleCollection A B} (P : A → Prop). + Context `{SimpleCollection A C} (P : A → Prop). + Implicit Types X Y : C. - Lemma set_Forall_empty : set_Forall P ∅. + Lemma set_Forall_empty : set_Forall P (∅ : C). Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Forall_singleton x : set_Forall P {[ x ]} ↔ P x. + Lemma set_Forall_singleton x : set_Forall P ({[ x ]} : C) ↔ P x. Proof. unfold set_Forall. set_solver. Qed. Lemma set_Forall_union X Y : set_Forall P X → set_Forall P Y → set_Forall P (X ∪ Y). @@ -838,9 +839,9 @@ Section quantifiers. Lemma set_Forall_union_inv_2 X Y : set_Forall P (X ∪ Y) → set_Forall P Y. Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Exists_empty : ¬set_Exists P ∅. + Lemma set_Exists_empty : ¬set_Exists P (∅ : C). Proof. unfold set_Exists. set_solver. Qed. - Lemma set_Exists_singleton x : set_Exists P {[ x ]} ↔ P x. + Lemma set_Exists_singleton x : set_Exists P ({[ x ]} : C) ↔ P x. Proof. unfold set_Exists. set_solver. Qed. Lemma set_Exists_union_1 X Y : set_Exists P X → set_Exists P (X ∪ Y). Proof. unfold set_Exists. set_solver. Qed. @@ -852,7 +853,8 @@ Section quantifiers. End quantifiers. Section more_quantifiers. - Context `{SimpleCollection A B}. + Context `{SimpleCollection A C}. + Implicit Types X : C. Lemma set_Forall_impl (P Q : A → Prop) X : set_Forall P X → (∀ x, P x → Q x) → set_Forall Q X. @@ -987,15 +989,17 @@ End collection_monad. Definition set_finite `{ElemOf A B} (X : B) := ∃ l : list A, ∀ x, x ∈ X → x ∈ l. Section finite. - Context `{SimpleCollection A B}. + Context `{SimpleCollection A C}. + Implicit Types X Y : C. + Global Instance set_finite_subseteq : - Proper (flip (⊆) ==> impl) (@set_finite A B _). + Proper (flip (⊆) ==> impl) (@set_finite A C _). Proof. intros X Y HX [l Hl]; exists l; set_solver. Qed. - Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A B _). + Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A C _). Proof. intros X Y HX; apply exist_proper. by setoid_rewrite HX. Qed. - Lemma empty_finite : set_finite ∅. + Lemma empty_finite : set_finite (∅ : C). Proof. by exists []; intros ?; rewrite elem_of_empty. Qed. - Lemma singleton_finite (x : A) : set_finite {[ x ]}. + Lemma singleton_finite (x : A) : set_finite ({[ x ]} : C). Proof. exists [x]; intros y ->%elem_of_singleton; left. Qed. Lemma union_finite X Y : set_finite X → set_finite Y → set_finite (X ∪ Y). Proof. @@ -1009,7 +1013,9 @@ Section finite. End finite. Section more_finite. - Context `{Collection A B}. + Context `{Collection A C}. + Implicit Types X Y : C. + Lemma intersection_finite_l X Y : set_finite X → set_finite (X ∩ Y). Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed. Lemma intersection_finite_r X Y : set_finite Y → set_finite (X ∩ Y). @@ -1038,14 +1044,15 @@ Section seq_set. Implicit Types start len x : nat. Lemma elem_of_seq_set start len x : - x ∈ seq_set start len ↔ start ≤ x < start + len. + x ∈ seq_set (C:=C) start len ↔ start ≤ x < start + len. Proof. revert start. induction len as [|len IH]; intros start; simpl. - rewrite elem_of_empty. omega. - rewrite elem_of_union, elem_of_singleton, IH. omega. Qed. - Lemma seq_set_S_disjoint start len : {[ start + len ]} ⊥ seq_set start len. + Lemma seq_set_S_disjoint start len : + {[ start + len ]} ⊥ seq_set (C:=C) start len. Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed. Lemma seq_set_S_union start len : @@ -1055,7 +1062,7 @@ Section seq_set. Qed. Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len : - seq_set start (S len) = {[ start + len ]} ∪ seq_set start len. + seq_set start (C:=C) (S len) = {[ start + len ]} ∪ seq_set start len. Proof. unfold_leibniz. apply seq_set_S_union. Qed. End seq_set. @@ -1067,6 +1074,7 @@ Typeclasses Opaque minimal. Section minimal. Context `{SimpleCollection A C} {R : relation A}. + Implicit Types X Y : C. Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x). Proof. intros X X' y; unfold minimal; set_solver. Qed. @@ -1085,11 +1093,11 @@ Section minimal. minimal R x X ↔ ∀ y, y ∈ X → ¬R y x. Proof. unfold minimal; split; [eauto using minimal_strict_1|naive_solver]. Qed. - Lemma empty_minimal x : minimal R x ∅. + Lemma empty_minimal x : minimal R x (∅ : C). Proof. unfold minimal; set_solver. Qed. - Lemma singleton_minimal x : minimal R x {[ x ]}. + Lemma singleton_minimal x : minimal R x ({[ x ]} : C). Proof. unfold minimal; set_solver. Qed. - Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x {[ y ]}. + Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x ({[ y ]} : C). Proof. unfold minimal; set_solver. Qed. Lemma union_minimal X Y x : minimal R x X → minimal R x Y → minimal R x (X ∪ Y). diff --git a/theories/fin_collections.v b/theories/fin_collections.v index f5061160adb40a3743f397add31630fca38578ea..ddb1220c05c4c63ee3f8eab8b0905dfcc5c7a040 100644 --- a/theories/fin_collections.v +++ b/theories/fin_collections.v @@ -63,14 +63,14 @@ Proof. intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton. by rewrite elem_of_cons, elem_of_elements. Qed. -Lemma elements_singleton x : elements {[ x ]} = [x]. +Lemma elements_singleton x : elements ({[ x ]} : C) = [x]. Proof. apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}), elements_union_singleton, elements_empty by set_solver. Qed. Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y. Proof. - intros; apply NoDup_submseteq; auto using NoDup_elements. + intros; apply NoDup_submseteq; eauto using NoDup_elements. intros x. rewrite !elem_of_elements; auto. Qed. @@ -106,7 +106,7 @@ Proof. contradict Hsz. rewrite HX, size_empty; lia. Qed. -Lemma size_singleton (x : A) : size {[ x ]} = 1. +Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1. Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed. Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. Proof. @@ -200,9 +200,9 @@ Proof. { destruct IH as (x' & Hx' & Hmin); [set_solver|]. destruct (decide (R x x')). - exists x; split; [set_solver|]. - eauto using union_minimal, singleton_minimal, minimal_weaken. + eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken. - exists x'; split; [set_solver|]. - auto using union_minimal, singleton_minimal_not_above. } + eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). } exists x; split; [set_solver|]. rewrite HX, (right_id _ (∪)). apply singleton_minimal. Qed. diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v index 5be84036978123a40071174129d392b25eda7022..68632ad6c64daad09798be1d4cd5545e9eff520c 100644 --- a/theories/fin_map_dom.v +++ b/theories/fin_map_dom.v @@ -61,7 +61,7 @@ Proof. rewrite (dom_insert _). set_solver. 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. trans (dom D m); eauto using dom_insert_subseteq. Qed. -Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} ≡ {[ i ]}. +Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A) ≡ {[ i ]}. Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed. Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}. Proof. @@ -100,7 +100,7 @@ Proof. unfold is_Some. setoid_rewrite lookup_difference_Some. destruct (m2 !! i); naive_solver. Qed. -Lemma dom_fmap {A B} (f : A → B) m : dom D (f <\$> m) ≡ dom D m. +Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom D (f <\$> m) ≡ dom D m. Proof. apply elem_of_equiv. intros i. rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some. @@ -109,7 +109,8 @@ Qed. Lemma dom_finite {A} (m : M A) : set_finite (dom D m). Proof. induction m using map_ind; rewrite ?dom_empty, ?dom_insert; - eauto using empty_finite, union_finite, singleton_finite. + eauto using (empty_finite (C:=D)), (union_finite (C:=D)), + (singleton_finite (C:=D)). Qed. Context `{!LeibnizEquiv D}. @@ -121,7 +122,7 @@ Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m. Proof. unfold_leibniz; apply dom_alter. Qed. Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m. Proof. unfold_leibniz; apply dom_insert. Qed. -Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i := x]} = {[ i ]}. +Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}. Proof. unfold_leibniz; apply dom_singleton. Qed. Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}. Proof. unfold_leibniz; apply dom_delete. Qed. @@ -132,6 +133,6 @@ Lemma dom_intersection_L {A} (m1 m2 : M A) : Proof. unfold_leibniz; apply dom_intersection. Qed. Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2. Proof. unfold_leibniz; apply dom_difference. Qed. -Lemma dom_fmap_L {A B} (f : A → B) m : dom D (f <\$> m) = dom D m. +Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <\$> m) = dom D m. Proof. unfold_leibniz; apply dom_fmap. Qed. End fin_map_dom. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index e9607aeffd30e960c7e03a85c268882b44da9356..fcaba6ce290f1c215813c8dbad6536d1a3eb3b6c 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -26,6 +26,8 @@ which enables us to give a generic implementation of [union_with], [intersection_with], and [difference_with]. *) Class FinMapToList K A M := map_to_list: M → list (K * A). +Hint Mode FinMapToList ! - - : typeclass_instances. +Hint Mode FinMapToList - - ! : typeclass_instances. Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A), @@ -213,7 +215,7 @@ Proof. specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver. Qed. Global Instance map_included_preorder {A} (R : relation A) : - PreOrder R → PreOrder (map_included R). + PreOrder R → PreOrder (map_included R : relation (M A)). Proof. split; [intros m i; by destruct (m !! i); simpl|]. intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i). @@ -247,7 +249,7 @@ 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. +Lemma lookup_empty_Some {A} i (x : A) : ¬(∅ : M A) !! i = Some x. Proof. by rewrite lookup_empty. Qed. Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅. Proof. @@ -319,9 +321,10 @@ Proof. Qed. (** ** Properties of the [alter] operation *) -Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <\$> m !! i. +Lemma lookup_alter {A} (f : A → A) (m : M A) i : alter f i m !! i = f <\$> m !! i. Proof. unfold alter. 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. +Lemma lookup_alter_ne {A} (f : A → A) (m : M A) i j : + i ≠ j → alter f i m !! j = m !! j. Proof. unfold alter. apply lookup_partial_alter_ne. Qed. Lemma alter_ext {A} (f g : A → A) (m : M A) i : (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m. @@ -335,7 +338,7 @@ Qed. Lemma alter_commute {A} (f g : A → A) (m : M A) i j : i ≠ j → alter f i (alter g j m) = alter g j (alter f i m). Proof. apply partial_alter_commute. Qed. -Lemma lookup_alter_Some {A} (f : A → A) m i j y : +Lemma lookup_alter_Some {A} (f : A → A) (m : M A) 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. @@ -343,16 +346,16 @@ Proof. - rewrite lookup_alter. naive_solver (simplify_option_eq; eauto). - rewrite lookup_alter_ne by done. naive_solver. Qed. -Lemma lookup_alter_None {A} (f : A → A) m i j : +Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j : alter f i m !! j = None ↔ m !! j = None. Proof. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_alter, ?fmap_None, ?lookup_alter_ne. Qed. -Lemma lookup_alter_is_Some {A} (f : A → A) m i j : +Lemma lookup_alter_is_Some {A} (f : A → A) (m : M A) i j : is_Some (alter f i m !! j) ↔ is_Some (m !! j). Proof. by rewrite <-!not_eq_None_Some, lookup_alter_None. Qed. -Lemma alter_id {A} (f : A → A) m i : +Lemma alter_id {A} (f : A → A) (m : M A) i : (∀ x, m !! i = Some x → f x = x) → alter f i m = m. Proof. intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?]. @@ -484,7 +487,7 @@ Proof. - rewrite lookup_insert. destruct (m !! j); simpl; eauto. - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl. Qed. -Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}. +Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}. Proof. done. Qed. Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅. Proof. @@ -542,44 +545,47 @@ Qed. (** ** Properties of the singleton maps *) Lemma lookup_singleton_Some {A} i j (x y : A) : - {[i := x]} !! j = Some y ↔ i = j ∧ x = y. + ({[i := x]} : M A) !! j = Some y ↔ i = j ∧ x = y. Proof. rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence. Qed. -Lemma lookup_singleton_None {A} i j (x : A) : {[i := x]} !! j = None ↔ i ≠ j. +Lemma lookup_singleton_None {A} i j (x : A) : + ({[i := x]} : M A) !! j = None ↔ i ≠ j. Proof. rewrite <-insert_empty,lookup_insert_None, lookup_empty; tauto. Qed. -Lemma lookup_singleton {A} i (x : A) : {[i := x]} !! i = Some x. +Lemma lookup_singleton {A} i (x : A) : ({[i := x]} : M A) !! i = Some x. Proof. by rewrite lookup_singleton_Some. Qed. -Lemma lookup_singleton_ne {A} i j (x : A) : i ≠ j → {[i := x]} !! j = None. +Lemma lookup_singleton_ne {A} i j (x : A) : + i ≠ j → ({[i := x]} : M A) !! j = None. Proof. by rewrite lookup_singleton_None. Qed. -Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ ∅. +Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ (∅ : M A). Proof. intros Hix. apply (f_equal (!! i)) in Hix. by rewrite lookup_empty, lookup_singleton in Hix. Qed. -Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i := x]} = {[i := y]}. +Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}. Proof. unfold singletonM, map_singleton, insert, map_insert. by rewrite <-partial_alter_compose. Qed. -Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i := x]} = {[i := f x]}. +Lemma alter_singleton {A} (f : A → A) i x : + alter f i ({[i := x]} : M A) = {[i := f x]}. Proof. intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?]. - by rewrite lookup_alter, !lookup_singleton. - by rewrite lookup_alter_ne, !lookup_singleton_ne. Qed. Lemma alter_singleton_ne {A} (f : A → A) i j x : - i ≠ j → alter f i {[j := x]} = {[j := x]}. + i ≠ j → alter f i ({[j := x]} : M A) = {[j := x]}. Proof. intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?]; rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done. Qed. -Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ ∅. +Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ (∅ : M A). Proof. apply insert_non_empty. Qed. -Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = ∅. +Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = (∅ : M A). Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed. Lemma delete_singleton_ne {A} i j (x : A) : - i ≠ j → delete i {[j := x]} = {[j := x]}. + i ≠ j → delete i ({[j := x]} : M A) = {[j := x]}. Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed. (** ** Properties of the map operations *) @@ -621,19 +627,19 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed. Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) : g ∘ f <\$> m = g <\$> f <\$> m. Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed. -Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m : +Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) (m : M A) : (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <\$> m ≡ f2 <\$> m. Proof. intros Hi i; rewrite !lookup_fmap. destruct (m !! i) eqn:?; constructor; eauto. Qed. -Lemma map_fmap_ext {A B} (f1 f2 : A → B) m : +Lemma map_fmap_ext {A B} (f1 f2 : A → B) (m : M A) : (∀ i x, m !! i = Some x → f1 x = f2 x) → f1 <\$> m = f2 <\$> m. Proof. intros Hi; apply map_eq; intros i; rewrite !lookup_fmap. by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto. Qed. -Lemma omap_ext {A B} (f1 f2 : A → option B) m : +Lemma omap_ext {A B} (f1 f2 : A → option B) (m : M A) : (∀ i x, m !! i = Some x → f1 x = f2 x) → omap f1 m = omap f2 m. Proof. intros Hi; apply map_eq; intros i; rewrite !lookup_omap. @@ -670,7 +676,7 @@ Proof. rewrite !elem_of_map_to_list. congruence. Qed. Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup ((map_to_list m).*1). Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed. Lemma elem_of_map_of_list_1' {A} (l : list (K * A)) i x : - (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → map_of_list l !! i = Some x. + (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → (map_of_list l : M A) !! i = Some x. Proof. induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|]. setoid_rewrite elem_of_cons. @@ -680,7 +686,7 @@ Proof. - rewrite lookup_insert_ne by done; eauto. Qed. Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x : - NoDup (l.*1) → (i,x) ∈ l → map_of_list l !! i = Some x. + NoDup (l.*1) → (i,x) ∈ l → (map_of_list l : M A) !! i = Some x. Proof. intros ? Hx; apply elem_of_map_of_list_1'; eauto using NoDup_fmap_fst. intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj']. @@ -688,7 +694,7 @@ Proof. by rewrite ?list_lookup_fmap, ?Hi', ?Hj'. 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. + (map_of_list l : M A) !! 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)) as [->|]; @@ -696,20 +702,20 @@ Proof. Qed. Lemma elem_of_map_of_list' {A} (l : list (K * A)) i x : (∀ x', (i,x) ∈ l → (i,x') ∈ l → x = x') → - (i,x) ∈ l ↔ map_of_list l !! i = Some x. + (i,x) ∈ l ↔ (map_of_list l : M A) !! i = Some x. Proof. split; auto using elem_of_map_of_list_1', elem_of_map_of_list_2. Qed. Lemma elem_of_map_of_list {A} (l : list (K * A)) i x : - NoDup (l.*1) → (i,x) ∈ l ↔ map_of_list l !! i = Some x. + NoDup (l.*1) → (i,x) ∈ l ↔ (map_of_list l : M A) !! 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 ∉ l.*1 → map_of_list l !! i = None. + i ∉ l.*1 → (map_of_list l : M A) !! i = None. Proof. rewrite elem_of_list_fmap, eq_None_not_Some. 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 ∉ l.*1. + (map_of_list l : M A) !! i = None → i ∉ l.*1. Proof. induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|]. rewrite elem_of_cons. destruct (decide (i = j)); simplify_eq. @@ -717,16 +723,17 @@ Proof. - by rewrite lookup_insert_ne; intuition. Qed. Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i : - i ∉ l.*1 ↔ map_of_list l !! i = None. + i ∉ l.*1 ↔ (map_of_list l : M A) !! i = None. Proof. red; 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 (l1.*1) → l1 ≡ₚ l2 → map_of_list l1 = map_of_list l2. + NoDup (l1.*1) → l1 ≡ₚ l2 → (map_of_list l1 : M A) = 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 (l1.*1) → NoDup (l2.*1) → map_of_list l1 = map_of_list l2 → l1 ≡ₚ l2. + NoDup (l1.*1) → NoDup (l2.*1) → + (map_of_list l1 : M A) = map_of_list l2 → 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. @@ -753,13 +760,13 @@ Proof. auto using map_of_list_proper, NoDup_fst_map_to_list. Qed. -Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅. +Lemma map_of_list_nil {A} : map_of_list [] = (∅ : M 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). + map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l : M A). Proof. done. Qed. Lemma map_of_list_fmap {A B} (f : A → B) l : - map_of_list (prod_map id f <\$> l) = f <\$> map_of_list l. + map_of_list (prod_map id f <\$> l) = f <\$> (map_of_list l : M A). Proof. induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto. rewrite <-map_of_list_cons; simpl. by rewrite IH, <-fmap_insert. @@ -780,7 +787,8 @@ Proof. rewrite elem_of_map_to_list in Hlookup. congruence. - by rewrite !map_of_to_list. Qed. -Lemma map_to_list_singleton {A} i (x : A) : map_to_list {[i:=x]} = [(i,x)]. +Lemma map_to_list_singleton {A} i (x : A) : + map_to_list ({[i:=x]} : M A) = [(i,x)]. Proof. apply Permutation_singleton. unfold singletonM, map_singleton. by rewrite map_to_list_insert, map_to_list_empty by auto using lookup_empty. @@ -792,7 +800,7 @@ Proof. intros; apply NoDup_submseteq; auto using NoDup_map_to_list. intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken. Qed. -Lemma map_to_list_fmap {A B} (f : A → B) m : +Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) : map_to_list (f <\$> m) ≡ₚ prod_map id f <\$> map_to_list m. Proof. assert (NoDup ((prod_map id f <\$> map_to_list m).*1)). @@ -836,7 +844,7 @@ Proof. Defined. (** Properties of the imap function *) -Lemma lookup_imap {A B} (f : K → A → option B) m i : +Lemma lookup_imap {A B} (f : K → A → option B) (m : M A) i : map_imap f m !! i = m !! i ≫= f i. Proof. unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl. @@ -856,9 +864,9 @@ Qed. Section map_of_to_collection. Context {A : Type} `{FinCollection B C}. - Lemma lookup_map_of_collection (f : B → K * A) Y i x : + Lemma lookup_map_of_collection (f : B → K * A) (Y : C) i x : (∀ y y', y ∈ Y → y' ∈ Y → (f y).1 = (f y').1 → y = y') → - map_of_collection f Y !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x). + (map_of_collection f Y : M A) !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x). Proof. intros Hinj. assert (∀ x', (i, x) ∈ f <\$> elements Y → (i, x') ∈ f <\$> elements Y → x = x'). @@ -870,14 +878,15 @@ Section map_of_to_collection. Qed. Lemma elem_of_map_to_collection (f : K → A → B) (m : M A) (y : B) : - y ∈ map_to_collection f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y. + y ∈ map_to_collection (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y. Proof. unfold map_to_collection; simpl. rewrite elem_of_of_list, elem_of_list_fmap. split. - intros ([i x] & ? & ?%elem_of_map_to_list); eauto. - intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list. Qed. - Lemma map_to_collection_empty (f : K → A → B) : map_to_collection f ∅ = ∅. + Lemma map_to_collection_empty (f : K → A → B) : + map_to_collection f (∅ : M A) = (∅ : C). Proof. unfold map_to_collection; simpl. by rewrite map_to_list_empty. Qed. Lemma map_to_collection_insert (f : K → A → B)(m : M A) i x : m !! i = None → @@ -885,7 +894,7 @@ Section map_of_to_collection. Proof. intros. unfold map_to_collection; simpl. by rewrite map_to_list_insert. Qed. - Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) m i x : + Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x : m !! i = None → map_to_collection (C:=C) f (<[i:=x]>m) = {[f i x]} ∪ map_to_collection f m. Proof. unfold_leibniz. apply map_to_collection_insert. Qed. @@ -893,7 +902,7 @@ End map_of_to_collection. Lemma lookup_map_of_collection_id `{FinCollection (K * A) C} (X : C) i x : (∀ i y y', (i,y) ∈ X → (i,y') ∈ X → y = y') → - map_of_collection id X !! i = Some x ↔ (i,x) ∈ X. + (map_of_collection id X : M A) !! i = Some x ↔ (i,x) ∈ X. Proof. intros. etrans; [apply lookup_map_of_collection|naive_solver]. intros [] [] ???; simplify_eq/=; eauto with f_equal. @@ -996,6 +1005,7 @@ Qed. (** ** Properties of the [map_Forall] predicate *) Section map_Forall. Context {A} (P : K → A → Prop). +Implicit Types m : M A. Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m). Proof. @@ -1003,7 +1013,7 @@ Proof. - 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. -Lemma map_Forall_empty : map_Forall P ∅. +Lemma map_Forall_empty : map_Forall P (∅ : M A). Proof. intros i x. by rewrite lookup_empty. Qed. Lemma map_Forall_impl (Q : K → A → Prop) m : map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m. @@ -1052,12 +1062,14 @@ End map_Forall. (** ** Properties of the [merge] operation *) Section merge. Context {A} (f : option A → option A → option A) `{!DiagNone f}. -Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f). +Implicit Types m : M A. + +Global Instance: LeftId (=) None f → LeftId (=) (∅ : M A) (merge f). Proof. intros ??. apply map_eq. intros. by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f). Qed. -Global Instance: RightId (=) None f → RightId (=) ∅ (merge f). +Global Instance: RightId (=) None f → RightId (=) (∅ : M A) (merge f). Proof. intros ??. apply map_eq. intros. by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f). @@ -1066,34 +1078,34 @@ Lemma merge_comm 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 merge_comm' : Comm (=) f → Comm (=) (merge f). +Global Instance merge_comm' : Comm (=) f → Comm (=) (merge (M:=M) f). Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed. Lemma merge_assoc 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 merge_assoc' : Assoc (=) f → Assoc (=) (merge f). +Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge (M:=M) f). Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed. Lemma merge_idemp 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 merge_idemp' : IdemP (=) f → IdemP (=) (merge f). +Global Instance merge_idemp' : IdemP (=) f → IdemP (=) (merge (M:=M) f). Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed. End merge. Section more_merge. Context {A B C} (f : option A → option B → option C) `{!DiagNone f}. -Lemma merge_Some m1 m2 m : +Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) : (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m. Proof. split; [|intros <-; apply (lookup_merge _) ]. intros Hlookup. apply map_eq; intros. rewrite Hlookup. apply (lookup_merge _). Qed. -Lemma merge_empty : merge f ∅ ∅ = ∅. +Lemma merge_empty : merge f (∅ : M A) (∅ : M B) = ∅. Proof. apply map_eq. intros. by rewrite !(lookup_merge f), !lookup_empty. Qed. -Lemma partial_alter_merge g g1 g2 m1 m2 i : +Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) 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). @@ -1102,7 +1114,7 @@ Proof. - 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 m1 m2 i : +Lemma partial_alter_merge_l g g1 (m1 : M A) (m2 : M B) 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. @@ -1110,7 +1122,7 @@ Proof. - 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 m1 m2 i : +Lemma partial_alter_merge_r g g2 (m1 : M A) (m2 : M B) 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. @@ -1118,37 +1130,39 @@ Proof. - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _). - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _). Qed. -Lemma insert_merge m1 m2 i x y z : +Lemma insert_merge (m1 : M A) (m2 : M B) i x y z : f (Some y) (Some z) = Some x → <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2). Proof. by intros; apply partial_alter_merge. Qed. Lemma merge_singleton i x y z : - f (Some y) (Some z) = Some x → merge f {[i := y]} {[i := z]} = {[i := x]}. + f (Some y) (Some z) = Some x → + merge f ({[i := y]} : M A) ({[i := z]} : M B) = {[i := x]}. Proof. intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto. Qed. -Lemma insert_merge_l m1 m2 i x y : +Lemma insert_merge_l (m1 : M A) (m2 : M B) i x y : f (Some y) (m2 !! i) = Some x → <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) m2. Proof. by intros; apply partial_alter_merge_l. Qed. -Lemma insert_merge_r m1 m2 i x z : +Lemma insert_merge_r (m1 : M A) (m2 : M B) i x z : f (m1 !! i) (Some z) = Some x → <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2). Proof. by intros; apply partial_alter_merge_r. Qed. End more_merge. (** Properties of the zip_with function *) -Lemma map_lookup_zip_with {A B C} (f : A → B → C) m1 m2 i : +Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i : map_zip_with f m1 m2 !! i = x ← m1 !! i; y ← m2 !! i; Some (f x y). Proof. unfold map_zip_with. rewrite lookup_merge by done. by destruct (m1 !! i), (m2 !! i). Qed. -Lemma map_zip_with_empty {A B C} (f : A → B → C) : map_zip_with f ∅ ∅ = ∅. +Lemma map_zip_with_empty {A B C} (f : A → B → C) : + map_zip_with f (∅ : M A) (∅ : M B) = ∅. Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed. -Lemma map_insert_zip_with {A B C} (f : A → B → C) m1 m2 i x y z : +Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i x y z : f y z = x → <[i:=x]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2). Proof. @@ -1157,7 +1171,7 @@ Proof. Qed. Lemma map_zip_with_fmap {A' A B' B C} (f : A → B → C) - (g1 : A' → A) (g2 : B' → B) m1 m2 : + (g1 : A' → A) (g2 : B' → B) (m1 : M A') (m2 : M B') : map_zip_with f (g1 <\$> m1) (g2 <\$> m2) = map_zip_with (λ x y, f (g1 x) (g2 y)) m1 m2. Proof. apply map_eq; intro i. rewrite !map_lookup_zip_with, !lookup_fmap. @@ -1165,13 +1179,14 @@ Proof. Qed. Lemma map_zip_with_fmap_1 {A' A B C} (f : A → B → C) - (g : A' → A) m1 m2 : + (g : A' → A) (m1 : M A') (m2 : M B) : map_zip_with f (g <\$> m1) m2 = map_zip_with (λ x y, f (g x) y) m1 m2. Proof. rewrite <- (map_fmap_id m2) at 1. by rewrite map_zip_with_fmap. Qed. -Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C) (g : B' → B) m1 m2 : +Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C) + (g : B' → B) (m1 : M A) (m2 : M B') : map_zip_with f m1 (g <\$> m2) = map_zip_with (λ x y, f x (g y)) m1 m2. Proof. rewrite <- (map_fmap_id m1) at 1. by rewrite map_zip_with_fmap. @@ -1184,14 +1199,15 @@ Proof. by destruct (m1 !! i), (m2 !! i). Qed. -Lemma map_zip_with_map_zip {A B C} (f : A → B → C) m1 m2 : +Lemma map_zip_with_map_zip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) : map_zip_with f m1 m2 = curry f <\$> map_zip m1 m2. Proof. apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with. by destruct (m1 !! i), (m2 !! i). Qed. -Lemma map_fmap_zip {A' A B' B} (g1 : A' → A) (g2 : B' → B) m1 m2 : +Lemma map_fmap_zip {A' A B' B} (g1 : A' → A) + (g2 : B' → B) (m1 : M A') (m2 : M B') : map_zip (fmap g1 m1) (fmap g2 m2) = prod_map g1 g2 <\$> map_zip m1 m2. Proof. rewrite map_zip_with_fmap, map_zip_with_map_zip. @@ -1223,7 +1239,7 @@ Proof. by eapply bool_decide_unpack, Hm. Qed. Global Instance map_relation_dec `{∀ x y, Decision (R x y), ∀ x, Decision (P x), - ∀ y, Decision (Q y)} m1 m2 : Decision (map_relation R P Q m1 m2). + ∀ y, Decision (Q y)} (m1 : M A) (m2 : M B) : Decision (map_relation R P Q m1 m2). Proof. refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2)))); abstract by rewrite map_relation_alt. @@ -1316,6 +1332,7 @@ 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). +Implicit Types m : M A. Lemma lookup_union_with m1 m2 i : union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i). @@ -1659,10 +1676,10 @@ Lemma map_disjoint_of_list_zip_r_2 {A} (m : M A) is xs : Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed. (** ** Properties of the [intersection_with] operation *) -Lemma lookup_intersection_with {A} (f : A → A → option A) m1 m2 i : +Lemma lookup_intersection_with {A} (f : A → A → option A) (m1 m2 : M A) i : intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i). Proof. by rewrite <-(lookup_merge _). Qed. -Lemma lookup_intersection_with_Some {A} (f : A → A → option A) m1 m2 i z : +Lemma lookup_intersection_with_Some {A} (f : A → A → option A) (m1 m2 : M A) i z : intersection_with f m1 m2 !! i = Some z ↔ (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z). Proof. @@ -1685,10 +1702,10 @@ Proof. Qed. (** ** Properties of the [difference_with] operation *) -Lemma lookup_difference_with {A} (f : A → A → option A) m1 m2 i : +Lemma lookup_difference_with {A} (f : A → A → option A) (m1 m2 : M A) i : difference_with f m1 m2 !! i = difference_with f (m1 !! i) (m2 !! i). Proof. by rewrite <-lookup_merge by done. Qed. -Lemma lookup_difference_with_Some {A} (f : A → A → option A) m1 m2 i z : +Lemma lookup_difference_with_Some {A} (f : A → A → option A) (m1 m2 : M A) 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). diff --git a/theories/gmap.v b/theories/gmap.v index fe7ddf772f5a9a8590c9210a543d6064d110f154..874fff964215e31b974a8444de62534ff9c12d3b 100644 --- a/theories/gmap.v +++ b/theories/gmap.v @@ -136,8 +136,10 @@ Definition gmap_uncurry `{Countable K1, Countable K2} {A} : Section curry_uncurry. Context `{Countable K1, Countable K2} {A : Type}. + (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are + a consequence of Coq bug #5735 *) Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j : - gmap_curry m !! (i,j) = m !! i ≫= (!! j). + gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (!! j). Proof. apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (!! j))). { by rewrite !lookup_empty. } @@ -154,7 +156,7 @@ Section curry_uncurry. Qed. Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j : - gmap_uncurry m !! i ≫= (!! j) = m !! (i, j). + (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (!! j) = m !! (i, j). Proof. apply (map_fold_ind (λ mr m, mr !! i ≫= (!! j) = m !! (i, j))). { by rewrite !lookup_empty. } @@ -229,7 +231,7 @@ Qed. (* This is pretty ad-hoc and just for the case of [gset positive]. We need a notion of countable non-finite types to generalize this. *) Instance gset_positive_fresh : Fresh positive (gset positive) := λ X, - let 'Mapset (GMap m _) := X in fresh (dom _ m). + let 'Mapset (GMap m _) := X in fresh (dom Pset m). Instance gset_positive_fresh_spec : FreshSpec positive (gset positive). Proof. split. diff --git a/theories/gmultiset.v b/theories/gmultiset.v index 084dfdca5b609518591529f7fa862744c284cdec..f61416e9627f0953bcdbdb3f6b78942a2991b04b 100644 --- a/theories/gmultiset.v +++ b/theories/gmultiset.v @@ -25,27 +25,27 @@ Section definitions. Definition multiplicity (x : A) (X : gmultiset A) : nat := match gmultiset_car X !! x with Some n => S n | None => 0 end. - Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X, + Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X, 0 < multiplicity x X. - Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x, + Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x, multiplicity x X ≤ multiplicity x Y. - Instance gmultiset_elements : Elements A (gmultiset A) := λ X, + Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X, let (X) := X in '(x,n) ← map_to_list X; replicate (S n) x. - Instance gmultiset_size : Size (gmultiset A) := length ∘ elements. + Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements. - Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅. - Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x, + Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅. + Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x, GMultiSet {[ x := 0 ]}. - Instance gmultiset_union : Union (gmultiset A) := λ X Y, + Global Instance gmultiset_union : Union (gmultiset A) := λ X Y, let (X) := X in let (Y) := Y in GMultiSet \$ union_with (λ x y, Some (S (x + y))) X Y. - Instance gmultiset_difference : Difference (gmultiset A) := λ X Y, + Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y, let (X) := X in let (Y) := Y in GMultiSet \$ difference_with (λ x y, let z := x - y in guard (0 < z); Some (pred z)) X Y. - Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X, + Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X, let (X) := X in dom _ X. End definitions. @@ -54,27 +54,6 @@ Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty. Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference. Typeclasses Opaque gmultiset_dom. -(** These instances are declared using [Hint Extern] to avoid too -eager type class search. *) -Hint Extern 1 (ElemOf _ (gmultiset _)) => - eapply @gmultiset_elem_of : typeclass_instances. -Hint Extern 1 (SubsetEq (gmultiset _)) => - eapply @gmultiset_subseteq : typeclass_instances. -Hint Extern 1 (Empty (gmultiset _)) => - eapply @gmultiset_empty : typeclass_instances. -Hint Extern 1 (Singleton _ (gmultiset _)) => - eapply @gmultiset_singleton : typeclass_instances. -Hint Extern 1 (Union (gmultiset _)) => - eapply @gmultiset_union : typeclass_instances. -Hint Extern 1 (Difference (gmultiset _)) => - eapply @gmultiset_difference : typeclass_instances. -Hint Extern 1 (Elements _ (gmultiset _)) => - eapply @gmultiset_elements : typeclass_instances. -Hint Extern 1 (Size (gmultiset _)) => - eapply @gmultiset_size : typeclass_instances. -Hint Extern 1 (Dom (gmultiset _) _) => - eapply @gmultiset_dom : typeclass_instances. - Section lemmas. Context `{Countable A}. Implicit Types x y : A. diff --git a/theories/hashset.v b/theories/hashset.v index 59c5506ba5c5527585b551223a16c46cb5f8029c..20a7d4ae07c1507310e459cdfa5cd8c0ebc53d52 100644 --- a/theories/hashset.v +++ b/theories/hashset.v @@ -18,18 +18,18 @@ Arguments hashset_car {_ _} _ : assert. Section hashset. Context `{EqDecision A} (hash : A → Z). -Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l, +Global Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l, hashset_car m !! hash x = Some l ∧ x ∈ l. -Program Instance hashset_empty: Empty (hashset hash) := Hashset ∅ _. +Global Program Instance hashset_empty: Empty (hashset hash) := Hashset ∅ _. Next Obligation. by intros n X; simpl_map. Qed. -Program Instance hashset_singleton: Singleton A (hashset hash) := λ x, +Global Program Instance hashset_singleton: Singleton A (hashset hash) := λ x, Hashset {[ hash x := [x] ]} _. Next Obligation. intros x n l [<- <-]%lookup_singleton_Some. rewrite Forall_singleton; auto using NoDup_singleton. Qed. -Program Instance hashset_union: Union (hashset hash) := λ m1 m2, +Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2, let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. Next Obligation. @@ -38,7 +38,7 @@ Next Obligation. split; [apply Forall_list_union|apply NoDup_list_union]; first [by eapply Hm1; eauto | by eapply Hm2; eauto]. Qed. -Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2, +Global Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2, let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in Hashset (intersection_with (λ l k, let l' := list_intersection l k in guard (l' ≠ []); Some l') m1 m2) _. @@ -48,7 +48,7 @@ Next Obligation. split; [apply Forall_list_intersection|apply NoDup_list_intersection]; first [by eapply Hm1; eauto | by eapply Hm2; eauto]. Qed. -Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2, +Global Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2, let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in Hashset (difference_with (λ l k, let l' := list_difference l k in guard (l' ≠ []); Some l') m1 m2) _. @@ -58,10 +58,10 @@ Next Obligation. split; [apply Forall_list_difference|apply NoDup_list_difference]; first [by eapply Hm1; eauto | by eapply Hm2; eauto]. Qed. -Instance hashset_elems: Elements A (hashset hash) := λ m, +Global Instance hashset_elements: Elements A (hashset hash) := λ m, map_to_list (hashset_car m) ≫= snd. -Global Instance: FinCollection A (hashset hash). +Global Instance hashset_fin_collection : FinCollection A (hashset hash). Proof. split; [split; [split| |]| |]. - intros ? (?&?&?); simplify_map_eq/=. @@ -98,13 +98,13 @@ Proof. assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference). exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto. by rewrite option_guard_True by eauto using elem_of_not_nil. - - unfold elem_of at 2, hashset_elem_of, elements, hashset_elems. + - unfold elem_of at 2, hashset_elem_of, elements, hashset_elements. intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split. { intros ([n l]&Hx&Hn); simpl in *; rewrite elem_of_map_to_list in Hn. cut (hash x = n); [intros <-; eauto|]. eapply (Forall_forall (λ x, hash x = n) l); eauto. eapply Hm; eauto. } intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list. - - unfold elements, hashset_elems. intros [m Hm]; simpl. + - unfold elements, hashset_elements. intros [m Hm]; simpl. rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m). induction Hm as [|[n l] m' [??]]; csimpl; inversion_clear 1 as [|?? Hn]; [constructor|]. @@ -120,23 +120,6 @@ End hashset. Typeclasses Opaque hashset_elem_of. -(** These instances are declared using [Hint Extern] to avoid too -eager type class search. *) -Hint Extern 1 (ElemOf _ (hashset _)) => - eapply @hashset_elem_of : typeclass_instances. -Hint Extern 1 (Empty (hashset _)) => - eapply @hashset_empty : typeclass_instances. -Hint Extern 1 (Singleton _ (hashset _)) => - eapply @hashset_singleton : typeclass_instances. -Hint Extern 1 (Union (hashset _)) => - eapply @hashset_union : typeclass_instances. -Hint Extern 1 (Intersection (hashset _)) => - eapply @hashset_intersection : typeclass_instances. -Hint Extern 1 (Difference (hashset _)) => - eapply @hashset_difference : typeclass_instances. -Hint Extern 1 (Elements _ (hashset _)) => - eapply @hashset_elems : typeclass_instances. - Section remove_duplicates. Context `{EqDecision A} (hash : A → Z). diff --git a/theories/list.v b/theories/list.v index 5f3bf7840e3ac26ab2cba52be7be27b8e0a30fc1..a258bea8e2959d1c4d7010aeb01aa51a708dcef4 100644 --- a/theories/list.v +++ b/theories/list.v @@ -311,7 +311,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → Section list_set. Context `{dec : EqDecision A}. - Global Instance elem_of_list_dec (x : A) : ∀ l, Decision (x ∈ l). + Global Instance elem_of_list_dec (x : A) : ∀ l : list A, Decision (x ∈ l). Proof. refine ( fix go l := @@ -2857,6 +2857,7 @@ Proof. induction l; f_equal/=; auto. Qed. Section fmap. Context {A B : Type} (f : A → B). + Implicit Types l : list A. Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <\$> l = g <\$> f <\$> l. Proof. induction l; f_equal/=; auto. Qed. @@ -2975,24 +2976,24 @@ Section fmap. Lemma Exists_fmap (P : B → Prop) l : Exists P (f <\$> l) ↔ Exists (P ∘ f) l. Proof. split; induction l; inversion 1; constructor; by auto. Qed. - Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 : - Forall2 P (f <\$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2. + Lemma Forall2_fmap_l {C} (P : B → C → Prop) l k : + Forall2 P (f <\$> l) k ↔ Forall2 (P ∘ f) l k. Proof. - split; revert l2; induction l1; inversion_clear 1; constructor; auto. + split; revert k; induction l; inversion_clear 1; constructor; auto. Qed. - Lemma Forall2_fmap_r {C} (P : C → B → Prop) l1 l2 : - Forall2 P l1 (f <\$> l2) ↔ Forall2 (λ x, P x ∘ f) l1 l2. + Lemma Forall2_fmap_r {C} (P : C → B → Prop) k l : + Forall2 P k (f <\$> l) ↔ Forall2 (λ x, P x ∘ f) k l. Proof. - split; revert l1; induction l2; inversion_clear 1; constructor; auto. + split; revert k; induction l; inversion_clear 1; constructor; auto. Qed. - Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l1 l2 : - Forall2 P (f <\$> l1) (g <\$> l2) → Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2. - Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed. - Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l1 l2 : - Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 → Forall2 P (f <\$> l1) (g <\$> l2). + Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l k : + Forall2 P (f <\$> l) (g <\$> k) → Forall2 (λ x1 x2, P (f x1) (g x2)) l k. + Proof. revert k; induction l; intros [|??]; inversion_clear 1; auto. Qed. + Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l k : + Forall2 (λ x1 x2, P (f x1) (g x2)) l k → Forall2 P (f <\$> l) (g <\$> k). Proof. induction 1; csimpl; auto. Qed. - Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 : - Forall2 P (f <\$> l1) (g <\$> l2) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2. + Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l k : + Forall2 P (f <\$> l) (g <\$> k) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l k. Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed. Lemma list_fmap_bind {C} (g : B → list C) l : (f <\$> l) ≫= g = l ≫= g ∘ f. @@ -3081,7 +3082,7 @@ Section ret_join. Lemma elem_of_list_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y. Proof. apply elem_of_list_singleton. Qed. Lemma elem_of_list_join (x : A) (ls : list (list A)) : - x ∈ mjoin ls ↔ ∃ l, x ∈ l ∧ l ∈ ls. + x ∈ mjoin ls ↔ ∃ l : list A, x ∈ l ∧ l ∈ ls. Proof. by rewrite list_join_bind, elem_of_list_bind. Qed. Lemma join_nil (ls : list (list A)) : mjoin ls = [] ↔ Forall (= []) ls. Proof. diff --git a/theories/listset.v b/theories/listset.v index 4649ede5db3ee1661003324e158d57c2c02ec115..824cbc4513a873ad720018ca11c29baf92cc3f12 100644 --- a/theories/listset.v +++ b/theories/listset.v @@ -12,14 +12,14 @@ Arguments Listset {_} _ : assert. Section listset. Context {A : Type}. -Instance listset_elem_of: ElemOf A (listset A) := λ x l, x ∈ listset_car l. -Instance listset_empty: Empty (listset A) := Listset []. -Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x]. -Instance listset_union: Union (listset A) := λ l k, +Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, x ∈ listset_car l. +Global Instance listset_empty: Empty (listset A) := Listset []. +Global Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x]. +Global Instance listset_union: Union (listset A) := λ l k, let (l') := l in let (k') := k in Listset (l' ++ k'). Global Opaque listset_singleton listset_empty. -Global Instance: SimpleCollection A (listset A). +Global Instance listset_simple_collection : SimpleCollection A (listset A). Proof. split. - by apply not_elem_of_nil. @@ -40,20 +40,21 @@ Defined. Context `{!EqDecision A}. -Instance listset_intersection: Intersection (listset A) := λ l k, +Global Instance listset_intersection: Intersection (listset A) := λ l k, let (l') := l in let (k') := k in Listset (list_intersection l' k'). -Instance listset_difference: Difference (listset A) := λ l k, +Global Instance listset_difference: Difference (listset A) := λ l k, let (l') := l in let (k') := k in Listset (list_difference l' k'). -Instance: Collection A (listset A). +Instance listset_collection: Collection A (listset A). Proof. split. - apply _. - intros [?] [?]. apply elem_of_list_intersection. - intros [?] [?]. apply elem_of_list_difference. Qed. -Instance listset_elems: Elements A (listset A) := remove_dups ∘ listset_car. -Global Instance: FinCollection A (listset A). +Global Instance listset_elements: Elements A (listset A) := + remove_dups ∘ listset_car. +Global Instance listset_fin_collection : FinCollection A (listset A). Proof. split. - apply _. @@ -62,23 +63,6 @@ Proof. Qed. End listset. -(** These instances are declared using [Hint Extern] to avoid too -eager type class search. *) -Hint Extern 1 (ElemOf _ (listset _)) => - eapply @listset_elem_of : typeclass_instances. -Hint Extern 1 (Empty (listset _)) => - eapply @listset_empty : typeclass_instances. -Hint Extern 1 (Singleton _ (listset _)) => - eapply @listset_singleton : typeclass_instances. -Hint Extern 1 (Union (listset _)) => - eapply @listset_union : typeclass_instances. -Hint Extern 1 (Intersection (listset _)) => - eapply @listset_intersection : typeclass_instances. -Hint Extern 1 (Difference (listset _)) => - eapply @listset_difference : typeclass_instances. -Hint Extern 1 (Elements _ (listset _)) => - eapply @listset_elems : typeclass_instances. - Instance listset_ret: MRet listset := λ A x, {[ x ]}. Instance listset_fmap: FMap listset := λ A B f l, let (l') := l in Listset (f <\$> l'). @@ -86,7 +70,7 @@ Instance listset_bind: MBind listset := λ A B f l, let (l') := l in Listset (mbind (listset_car ∘ f) l'). Instance listset_join: MJoin listset := λ A, mbind id. -Instance: CollectionMonad listset. +Instance listset_collection_monad : CollectionMonad listset. Proof. split. - intros. apply _. diff --git a/theories/mapset.v b/theories/mapset.v index bb44b6711ea679d48c9dc2828cb7253a11615167..bb7c479d8678dcdadcadaa54e83f1eafbf133148 100644 --- a/theories/mapset.v +++ b/theories/mapset.v @@ -14,18 +14,18 @@ Arguments mapset_car {_} _ : assert. Section mapset. Context `{FinMap K M}. -Instance mapset_elem_of: ElemOf K (mapset M) := λ x X, +Global 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, +Global Instance mapset_empty: Empty (mapset M) := Mapset ∅. +Global Instance mapset_singleton: Singleton K (mapset M) := λ x, Mapset {[ x := () ]}. -Instance mapset_union: Union (mapset M) := λ X1 X2, +Global Instance mapset_union: Union (mapset M) := λ X1 X2, let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2). -Instance mapset_intersection: Intersection (mapset M) := λ X1 X2, +Global Instance mapset_intersection: Intersection (mapset M) := λ X1 X2, let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2). -Instance mapset_difference: Difference (mapset M) := λ X1 X2, +Global Instance mapset_difference: Difference (mapset M) := λ X1 X2, let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2). -Instance mapset_elems: Elements K (mapset M) := λ X, +Global Instance mapset_elements: Elements K (mapset M) := λ X, let (m) := X in (map_to_list m).*1. Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2. @@ -35,7 +35,7 @@ Proof. f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E. Qed. -Instance: Collection K (mapset M). +Instance mapset_collection: Collection K (mapset M). Proof. split; [split | | ]. - unfold empty, elem_of, mapset_empty, mapset_elem_of. @@ -54,17 +54,17 @@ Proof. intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some. destruct (m2 !! x) as [[]|]; intuition congruence. Qed. -Global Instance: LeibnizEquiv (mapset M). +Global Instance mapset_leibniz : LeibnizEquiv (mapset M). Proof. intros ??. apply mapset_eq. Qed. -Global Instance: FinCollection K (mapset M). +Global Instance mapset_fin_collection : FinCollection K (mapset M). Proof. split. - apply _. - - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of. + - unfold elements, elem_of at 2, mapset_elements, mapset_elem_of. intros [m] x. simpl. rewrite elem_of_list_fmap. split. + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list. + intros. exists (x, ()). by rewrite elem_of_map_to_list. - - unfold elements, mapset_elems. intros [m]. simpl. + - unfold elements, mapset_elements. intros [m]. simpl. apply NoDup_fst_map_to_list. Qed. @@ -127,21 +127,4 @@ Proof. 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. - Arguments mapset_eq_dec : simpl never. diff --git a/theories/option.v b/theories/option.v index 7a2c27f93058fa41508a092202182c643a68b5a6..9f5b7efb4b9bad18636185ae0adc230ec56f82a4 100644 --- a/theories/option.v +++ b/theories/option.v @@ -207,7 +207,7 @@ Proof. by destruct mx. Qed. Lemma option_fmap_ext {A B} (f g : A → B) mx : (∀ x, f x = g x) → f <\$> mx = g <\$> mx. Proof. intros; destruct mx; f_equal/=; auto. Qed. -Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) mx : +Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) (mx : option A) : (∀ x, f x ≡ g x) → f <\$> mx ≡ g <\$> mx. Proof. destruct mx; constructor; auto. Qed. Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx : @@ -306,13 +306,15 @@ Section union_intersection_difference. Proof. by intros [?|]. Qed. Global Instance union_with_right_id : RightId (=) None (union_with f). Proof. by intros [?|]. Qed. - Global Instance union_with_comm : Comm (=) f → Comm (=) (union_with f). + Global Instance union_with_comm : + Comm (=) f → Comm (=) (union_with (M:=option A) f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. - Global Instance difference_with_comm : Comm (=) f → Comm (=) (intersection_with f). + Global Instance difference_with_comm : + Comm (=) f → Comm (=) (intersection_with (M:=option A) f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. Global Instance difference_with_right_id : RightId (=) None (difference_with f). Proof. by intros [?|]. Qed. diff --git a/theories/set.v b/theories/set.v index 80f060ec6b7cda4b28cdb1cec45bc5202a6d8c00..9da4261094bb5cfa4d82e6bb0e0ca3f1a711a029 100644 --- a/theories/set.v +++ b/theories/set.v @@ -24,7 +24,7 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2, Instance set_collection : Collection A (set A). Proof. split; [split | |]; by repeat intro. Qed. -Lemma elem_of_top {A} (x : A) : x ∈ ⊤ ↔ True. +Lemma elem_of_top {A} (x : A) : x ∈ (⊤ : set A) ↔ True. Proof. done. Qed. Lemma elem_of_mkSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x. Proof. done. Qed. @@ -40,7 +40,7 @@ Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A), Instance set_fmap : FMap set := λ A B (f : A → B) (X : set A), {[ b | ∃ a, b = f a ∧ a ∈ X ]}. Instance set_join : MJoin set := λ A (XX : set (set A)), - {[ a | ∃ X, a ∈ X ∧ X ∈ XX ]}. + {[ a | ∃ X : set A, a ∈ X ∧ X ∈ XX ]}. Instance set_collection_monad : CollectionMonad set. Proof. by split; try apply _. Qed.