...
 
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.