Commit 80b3d10e authored by Robbert Krebbers's avatar Robbert Krebbers

Use `Typeclasses Opaque` for all operational type classes in `base`.

parent 7e77bf8d
......@@ -191,6 +191,7 @@ 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.
Typeclasses Opaque equiv.
(* No Hint Mode set because of Coq bug #5735
Hint Mode Equiv ! : typeclass_instances. *)
......@@ -238,6 +239,8 @@ Ltac unfold_leibniz := repeat
end.
Definition equivL {A} : Equiv A := (=).
Instance equivL_equivalence {A} : Equivalence (@equiv A equivL).
Proof. unfold equiv; apply _. Qed.
(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
......@@ -257,6 +260,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 +280,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})).
......@@ -658,12 +663,14 @@ Section prod_relation.
End prod_relation.
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Instance pair_proper `{Equiv A, Equiv B} :
Proper (() ==> () ==> ()) (@pair A B) := _.
Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B) := _.
Instance fst_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@fst A B) := _.
Instance snd_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@snd A B) := _.
Typeclasses Opaque prod_equiv.
Instance pair_proper `{Equiv A, Equiv B} : Proper (() ==> () ==> ()) (@pair A B).
Proof. apply pair_proper'. Qed.
Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 () () () (@pair A B).
Proof. apply pair_inj'. Qed.
Instance fst_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@fst A B).
Proof. apply fst_proper'. Qed.
Instance snd_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@snd A B).
Proof. apply snd_proper'. Qed.
Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
......@@ -717,11 +724,14 @@ Section sum_relation.
End sum_relation.
Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation () ().
Instance inl_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@inl A B) := _.
Instance inr_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@inr A B) := _.
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inl A B) := _.
Instance inl_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@inl A B).
Proof. apply inl_proper'. Qed.
Instance inr_proper `{Equiv A, Equiv B} : Proper (() ==> ()) (@inr A B).
Proof. apply inr_proper'. Qed.
Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inl A B).
Proof. apply inl_inj'. Qed.
Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj () () (@inr A B) := _.
Typeclasses Opaque sum_equiv.
Proof. apply inr_inj'. Qed.
(** ** Option *)
Instance option_inhabited {A} : Inhabited (option A) := populate None.
......@@ -761,12 +771,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 +792,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 +807,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 +816,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 +831,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 +844,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 +899,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 +918,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 +941,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 +959,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 +982,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 +995,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 +1043,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 +1056,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 +1067,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 +1075,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 +1086,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 +1094,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 +1105,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 +1113,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 +1123,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 +1133,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 +1141,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 +1158,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 +1167,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 +1200,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 +1237,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 +1288,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 +1297,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 +1313,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 +1322,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 +1331,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.
......
......@@ -122,7 +122,7 @@ Section setoids.
Global Instance option_equivalence :
Equivalence (@{A}) Equivalence (@{option A}).
Proof. apply _. Qed.
Proof. apply option_Forall2_equiv. Qed.
Global Instance Some_proper : Proper (() ==> (@{option A})) Some.
Proof. by constructor. Qed.
Global Instance Some_equiv_inj : Inj () (@{option A}) Some.
......
......@@ -40,9 +40,9 @@ Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1
Proof. by constructor. Qed.
Global Instance equal_equivalence : Equivalence (@{stream A}).
Proof.
split.
- now cofix FIX; intros [??]; constructor.
- now cofix FIX; intros ?? [??]; constructor.
unfold equiv, stream_equiv. split.
- cofix FIX; intros [??]; by constructor.
- cofix FIX; intros ?? [??]; by constructor.
- cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
Qed.
Global Instance scons_proper x : Proper (() ==> ()) (scons x).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment