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