Commit 7d7c9871 authored by Robbert Krebbers's avatar Robbert Krebbers

Set Hint Mode for all classes in `base.v`.

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None  m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None  m !! j = None.

That is, we have to specify the type of `m`.
parent 24aef2fe
......@@ -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.
......@@ -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.
......
......@@ -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.