...

Commits (3)
 ... ... @@ -191,6 +191,11 @@ Proof. split; repeat intro; congruence. Qed. "canonical" equivalence for a type. The typeclass is tied to the \equiv symbol. This is based on (Spitters/van der Weegen, 2011). *) Class Equiv A := equiv: relation A. (* No Typeclasses Opaque because we often rely on [≡] being unified with [=] in case of types with Leibniz equality as [≡]. Typeclasses Opaque equiv. *) (* No Hint Mode set because of Coq bug #5735 Hint Mode Equiv ! : typeclass_instances. *) ... ... @@ -257,6 +262,7 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption : core. (** This type class by (Spitters/van der Weegen, 2011) collects decidable propositions. *) Class Decision (P : Prop) := decide : {P} + {¬P}. Typeclasses Opaque decide. Hint Mode Decision ! : typeclass_instances. Arguments decide _ {_} : simpl never, assert. ... ... @@ -276,6 +282,7 @@ an explicit class instead of a notation for two reasons: unnecessary evaluation. *) Class RelDecision {A B} (R : A → B → Prop) := decide_rel x y :> Decision (R x y). Typeclasses Opaque decide_rel. Hint Mode RelDecision ! ! ! : typeclass_instances. Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert. Notation EqDecision A := (RelDecision (=@{A})). ... ... @@ -761,12 +768,14 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *) Class Empty A := empty: A. Hint Mode Empty ! : typeclass_instances. Typeclasses Opaque empty. Notation "∅" := empty (format "∅") : stdpp_scope. Instance empty_inhabited (Empty A) : Inhabited A := populate ∅. Class Union A := union: A → A → A. Hint Mode Union ! : typeclass_instances. Typeclasses Opaque union. Instance: Params (@union) 2 := {}. Infix "∪" := union (at level 50, left associativity) : stdpp_scope. Notation "(∪)" := union (only parsing) : stdpp_scope. ... ... @@ -780,11 +789,13 @@ Infix "∪*∪**" := (zip_with (prod_zip (∪) (∪*))) (at level 50, left associativity) : stdpp_scope. Definition union_list {Empty A} {Union A} : list A → A := fold_right (∪) ∅. Typeclasses Opaque union_list. Arguments union_list _ _ _ !_ / : assert. Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope. Class DisjUnion A := disj_union: A → A → A. Hint Mode DisjUnion ! : typeclass_instances. Typeclasses Opaque disj_union. Instance: Params (@disj_union) 2 := {}. Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope. Notation "(⊎)" := disj_union (only parsing) : stdpp_scope. ... ... @@ -793,6 +804,7 @@ Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope. Class Intersection A := intersection: A → A → A. Hint Mode Intersection ! : typeclass_instances. Typeclasses Opaque intersection. Instance: Params (@intersection) 2 := {}. Infix "∩" := intersection (at level 40) : stdpp_scope. Notation "(∩)" := intersection (only parsing) : stdpp_scope. ... ... @@ -801,6 +813,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope. Class Difference A := difference: A → A → A. Hint Mode Difference ! : typeclass_instances. Typeclasses Opaque difference. Instance: Params (@difference) 2 := {}. Infix "∖" := difference (at level 40, left associativity) : stdpp_scope. Notation "(∖)" := difference (only parsing) : stdpp_scope. ... ... @@ -815,6 +828,7 @@ Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*))) Class Singleton A B := singleton: A → B. Hint Mode Singleton - ! : typeclass_instances. Typeclasses Opaque singleton. Instance: Params (@singleton) 3 := {}. Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope. Notation "{[ x ; y ; .. ; z ]}" := ... ... @@ -827,6 +841,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z)) Class SubsetEq A := subseteq: relation A. Hint Mode SubsetEq ! : typeclass_instances. Typeclasses Opaque subseteq. Instance: Params (@subseteq) 2 := {}. Infix "⊆" := subseteq (at level 70) : stdpp_scope. Notation "(⊆)" := subseteq (only parsing) : stdpp_scope. ... ... @@ -881,9 +896,11 @@ 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. Typeclasses Opaque lexico. Class ElemOf A B := elem_of: A → B → Prop. Hint Mode ElemOf - ! : typeclass_instances. Typeclasses Opaque elem_of. Instance: Params (@elem_of) 3 := {}. Infix "∈" := elem_of (at level 70) : stdpp_scope. Notation "(∈)" := elem_of (only parsing) : stdpp_scope. ... ... @@ -898,7 +915,8 @@ Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope. Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope. Class Disjoint A := disjoint : A → A → Prop. Hint Mode Disjoint ! : typeclass_instances. Hint Mode Disjoint ! : typeclass_instances. Typeclasses Opaque disjoint. Instance: Params (@disjoint) 2 := {}. Infix "##" := disjoint (at level 70) : stdpp_scope. Notation "(##)" := disjoint (only parsing) : stdpp_scope. ... ... @@ -920,6 +938,7 @@ Hint Extern 0 (_ ##* _) => symmetry; eassumption : core. Class DisjointE E A := disjointE : E → A → A → Prop. Hint Mode DisjointE - ! : typeclass_instances. Typeclasses Opaque disjointE. Instance: Params (@disjointE) 4 := {}. Notation "X ##{ Γ } Y" := (disjointE Γ X Y) (at level 70, format "X ##{ Γ } Y") : stdpp_scope. ... ... @@ -937,6 +956,7 @@ Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core. Class DisjointList A := disjoint_list : list A → Prop. Hint Mode DisjointList ! : typeclass_instances. Typeclasses Opaque disjoint_list. Instance: Params (@disjoint_list) 2 := {}. Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope. Notation "##@{ A } Xs" := ... ... @@ -959,9 +979,11 @@ End disjoint_list. Class Filter A B := filter: ∀ (P : A → Prop) {∀ x, Decision (P x)}, B → B. Hint Mode Filter - ! : typeclass_instances. Typeclasses Opaque filter. Class UpClose A B := up_close : A → B. Hint Mode UpClose - ! : typeclass_instances. Typeclasses Opaque up_close. Notation "↑ x" := (up_close x) (at level 20, format "↑ x"). (** * Monadic operations *) ... ... @@ -970,18 +992,27 @@ and fmap. We use these type classes merely for convenient overloading of notations and do not formalize any theory on monads (we do not even define a class with the monad laws). *) Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A. Typeclasses Opaque mret. Arguments mret {_ _ _} _ : assert. Instance: Params (@mret) 3 := {}. Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B. Typeclasses Opaque mbind. Arguments mbind {_ _ _ _} _ !_ / : assert. Instance: Params (@mbind) 4 := {}. Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A. Typeclasses Opaque mjoin. Arguments mjoin {_ _ _} !_ / : assert. Instance: Params (@mjoin) 3 := {}. Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B. Typeclasses Opaque fmap. Arguments fmap {_ _ _ _} _ !_ / : assert. Instance: Params (@fmap) 4 := {}. Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B. Typeclasses Opaque omap. Arguments omap {_ _ _ _} _ !_ / : assert. Instance: Params (@omap) 4 := {}. ... ... @@ -1009,6 +1040,7 @@ Notation "ps .*2" := (fmap (M:=list) snd ps) Class MGuard (M : Type → Type) := mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A. Typeclasses Opaque mguard. Arguments mguard _ _ _ !_ _ _ / : assert. Notation "'guard' P ; z" := (mguard P (λ _, z)) (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. ... ... @@ -1021,6 +1053,7 @@ 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. Typeclasses Opaque lookup. Instance: Params (@lookup) 4 := {}. Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope. Notation "(!!)" := lookup (only parsing) : stdpp_scope. ... ... @@ -1031,6 +1064,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert. (** The singleton map *) Class SingletonM K A M := singletonM: K → A → M. Hint Mode SingletonM - - ! : typeclass_instances. Typeclasses Opaque singletonM. Instance: Params (@singletonM) 5 := {}. Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope. ... ... @@ -1038,6 +1072,7 @@ Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope. value [a] in [m]. *) Class Insert (K A M : Type) := insert: K → A → M → M. Hint Mode Insert - - ! : typeclass_instances. Typeclasses Opaque insert. Instance: Params (@insert) 5 := {}. Notation "<[ k := a ]>" := (insert k a) (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope. ... ... @@ -1048,6 +1083,7 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert. returned. *) Class Delete (K M : Type) := delete: K → M → M. Hint Mode Delete - ! : typeclass_instances. Typeclasses Opaque delete. Instance: Params (@delete) 4 := {}. Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert. ... ... @@ -1055,6 +1091,7 @@ Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert. 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. Typeclasses Opaque alter. Instance: Params (@alter) 5 := {}. Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert. ... ... @@ -1065,6 +1102,7 @@ yields [None]. *) Class PartialAlter (K A M : Type) := partial_alter: (option A → option A) → K → M → M. Hint Mode PartialAlter - - ! : typeclass_instances. Typeclasses Opaque partial_alter. Instance: Params (@partial_alter) 4 := {}. Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert. ... ... @@ -1072,6 +1110,7 @@ Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert. set 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. Typeclasses Opaque dom. Instance: Params (@dom) 3 := {}. Arguments dom : clear implicits. Arguments dom {_} _ {_} !_ / : simpl nomatch, assert. ... ... @@ -1081,6 +1120,7 @@ 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. Typeclasses Opaque merge. Instance: Params (@merge) 4 := {}. Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert. ... ... @@ -1090,6 +1130,7 @@ both [m1] and [m2]. *) Class UnionWith (A M : Type) := union_with: (A → A → option A) → M → M → M. Hint Mode UnionWith - ! : typeclass_instances. Typeclasses Opaque union_with. Instance: Params (@union_with) 3 := {}. Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. ... ... @@ -1097,12 +1138,14 @@ Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. Class IntersectionWith (A M : Type) := intersection_with: (A → A → option A) → M → M → M. Hint Mode IntersectionWith - ! : typeclass_instances. Typeclasses Opaque intersection_with. 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. Typeclasses Opaque difference_with. Instance: Params (@difference_with) 3 := {}. Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. ... ... @@ -1112,6 +1155,7 @@ Arguments intersection_with_list _ _ _ _ _ !_ / : assert. Class LookupE (E K A M : Type) := lookupE: E → K → M → option A. Hint Mode LookupE - - - ! : typeclass_instances. Typeclasses Opaque lookupE. Instance: Params (@lookupE) 6 := {}. Notation "m !!{ Γ } i" := (lookupE Γ i m) (at level 20, format "m !!{ Γ } i") : stdpp_scope. ... ... @@ -1120,6 +1164,7 @@ Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert. Class InsertE (E K A M : Type) := insertE: E → K → A → M → M. Hint Mode InsertE - - - ! : typeclass_instances. Typeclasses Opaque insertE. Instance: Params (@insertE) 6 := {}. Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a) (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : stdpp_scope. ... ... @@ -1152,6 +1197,7 @@ 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. Typeclasses Opaque elements. Instance: Params (@elements) 3 := {}. (** We redefine the standard library's [In] and [NoDup] using type classes. *) ... ... @@ -1188,6 +1234,7 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C, }. Class Size C := size: C → nat. Hint Mode Size ! : typeclass_instances. Typeclasses Opaque size. Arguments size {_ _} !_ / : simpl nomatch, assert. Instance: Params (@size) 2 := {}. ... ... @@ -1238,6 +1285,7 @@ Arguments infinite_fresh : simpl never. (** * Miscellaneous *) Class Half A := half: A → A. Hint Mode Half ! : typeclass_instances. Typeclasses Opaque half. Notation "½" := half (format "½") : stdpp_scope. Notation "½*" := (fmap (M:=list) half) : stdpp_scope. ... ... @@ -1246,6 +1294,7 @@ Notation "½*" := (fmap (M:=list) half) : stdpp_scope. for the \sqsubseteq symbol. *) Class SqSubsetEq A := sqsubseteq: relation A. Hint Mode SqSubsetEq ! : typeclass_instances. Typeclasses Opaque sqsubseteq. Instance: Params (@sqsubseteq) 2 := {}. Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope. Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope. ... ... @@ -1261,6 +1310,7 @@ Hint Extern 0 (_ ⊑ _) => reflexivity : core. Class Meet A := meet: A → A → A. Hint Mode Meet ! : typeclass_instances. Typeclasses Opaque meet. Instance: Params (@meet) 2 := {}. Infix "⊓" := meet (at level 40) : stdpp_scope. Notation "(⊓)" := meet (only parsing) : stdpp_scope. ... ... @@ -1269,6 +1319,7 @@ Notation "(⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope. Class Join A := join: A → A → A. Hint Mode Join ! : typeclass_instances. Typeclasses Opaque join. Instance: Params (@join) 2 := {}. Infix "⊔" := join (at level 50) : stdpp_scope. Notation "(⊔)" := join (only parsing) : stdpp_scope. ... ... @@ -1277,8 +1328,10 @@ Notation "(⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope. Class Top A := top : A. Hint Mode Top ! : typeclass_instances. Typeclasses Opaque top. Notation "⊤" := top (format "⊤") : stdpp_scope. Class Bottom A := bottom : A. Hint Mode Bottom ! : typeclass_instances. Typeclasses Opaque bottom. Notation "⊥" := bottom (format "⊥") : stdpp_scope.
 ... ... @@ -191,7 +191,7 @@ Proof. Qed. Instance coPset_elem_of_dec : RelDecision (∈@{coPset}). Proof. solve_decision. Defined. Proof. unfold elem_of. solve_decision. Defined. Instance coPset_equiv_dec : RelDecision (≡@{coPset}). Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined. Instance mapset_disjoint_dec : RelDecision (##@{coPset}). ... ...
 ... ... @@ -233,7 +233,7 @@ Proof. Qed. Global Instance map_subseteq_po : PartialOrder (⊆@{M A}). Proof. split; [apply _|]. split; [apply map_included_preorder, _|]. intros m1 m2; rewrite !map_subseteq_spec. intros; apply map_eq; intros i; apply option_eq; naive_solver. Qed. ... ... @@ -1534,8 +1534,10 @@ Qed. End union_with. (** ** Properties of the [union] operation *) Global Instance: LeftId (=@{M A}) ∅ (∪) := _. Global Instance: RightId (=@{M A}) ∅ (∪) := _. Global Instance: LeftId (=@{M A}) ∅ (∪). Proof. unfold union; apply _. Qed. Global Instance: RightId (=@{M A}) ∅ (∪). Proof. unfold union; apply _. Qed. Global Instance: Assoc (=@{M A}) (∪). Proof. intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with. ... ...
 ... ... @@ -130,8 +130,4 @@ Proof. Qed. End mapset. (** [mapset_elem_of] internally contains an equality; make sure that tactics do not unfold it and try to unify [∈] against goals with [=]. *) Opaque mapset_elem_of. Arguments mapset_eq_dec : simpl never.