Commit 210bf091 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation `∈@{A}`.

parent 6aba4a3f
...@@ -856,6 +856,9 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope. ...@@ -856,6 +856,9 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope.
Notation "( x ∉)" := (λ X, x X) (only parsing) : stdpp_scope. Notation "( x ∉)" := (λ X, x X) (only parsing) : stdpp_scope.
Notation "(∉ X )" := (λ x, x X) (only parsing) : stdpp_scope. Notation "(∉ X )" := (λ x, x X) (only parsing) : stdpp_scope.
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. Class Disjoint A := disjoint : A A Prop.
Hint Mode Disjoint ! : typeclass_instances. Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2. Instance: Params (@disjoint) 2.
......
...@@ -29,7 +29,7 @@ Proof. ...@@ -29,7 +29,7 @@ Proof.
- intros X Y x; unfold elem_of, bset_elem_of; simpl. - intros X Y x; unfold elem_of, bset_elem_of; simpl.
destruct (bset_car X x), (bset_car Y x); simpl; tauto. destruct (bset_car X x), (bset_car Y x); simpl; tauto.
Qed. Qed.
Instance bset_elem_of_dec {A} : RelDecision (@elem_of _ (bset A) _). Instance bset_elem_of_dec {A} : RelDecision (@{bset A}).
Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined. Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
Typeclasses Opaque bset_elem_of. Typeclasses Opaque bset_elem_of.
......
...@@ -190,7 +190,7 @@ Proof. ...@@ -190,7 +190,7 @@ Proof.
intros p; apply eq_bool_prop_intro, (HXY p). intros p; apply eq_bool_prop_intro, (HXY p).
Qed. Qed.
Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _). Instance coPset_elem_of_dec : RelDecision (@{coPset}).
Proof. solve_decision. Defined. Proof. 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.
......
...@@ -28,8 +28,7 @@ Section setoids_simple. ...@@ -28,8 +28,7 @@ Section setoids_simple.
Qed. Qed.
Global Instance singleton_proper : Proper ((=) ==> (@{C})) singleton. Global Instance singleton_proper : Proper ((=) ==> (@{C})) singleton.
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance elem_of_proper : Global Instance elem_of_proper : Proper ((=) ==> () ==> iff) (@{C}) | 5.
Proper ((=) ==> () ==> iff) (@elem_of A C _) | 5.
Proof. by intros x ? <- X Y. Qed. Proof. by intros x ? <- X Y. Qed.
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _). Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _).
Proof. Proof.
...@@ -695,7 +694,7 @@ Section collection. ...@@ -695,7 +694,7 @@ Section collection.
End leibniz. End leibniz.
Section dec. Section dec.
Context `{!RelDecision (@elem_of A C _)}. Context `{!RelDecision (@{C})}.
Lemma not_elem_of_intersection x X Y : x X Y x X x Y. Lemma not_elem_of_intersection x X Y : x X Y x X x Y.
Proof. rewrite elem_of_intersection. destruct (decide (x X)); tauto. Qed. Proof. rewrite elem_of_intersection. destruct (decide (x X)); tauto. Qed.
Lemma not_elem_of_difference x X Y : x X Y x X x Y. Lemma not_elem_of_difference x X Y : x X Y x X x Y.
......
...@@ -23,7 +23,7 @@ Implicit Types X Y : C. ...@@ -23,7 +23,7 @@ Implicit Types X Y : C.
Lemma fin_collection_finite X : set_finite X. Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
Instance elem_of_dec_slow : RelDecision (@elem_of A C _) | 100. Instance elem_of_dec_slow : RelDecision (@{C}) | 100.
Proof. Proof.
refine (λ x X, cast_if (decide_rel () x (elements X))); refine (λ x X, cast_if (decide_rel () x (elements X)));
by rewrite <-(elem_of_elements _). by rewrite <-(elem_of_elements _).
......
...@@ -98,7 +98,7 @@ Proof. ...@@ -98,7 +98,7 @@ Proof.
by split; auto with lia. by split; auto with lia.
- intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega. - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega.
Qed. Qed.
Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _). Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined. Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
(* Algebraic laws *) (* Algebraic laws *)
......
...@@ -26,7 +26,7 @@ Qed. ...@@ -26,7 +26,7 @@ Qed.
(** * Fresh elements *) (** * Fresh elements *)
Section Fresh. Section Fresh.
Context `{FinCollection A C, Infinite A, !RelDecision (@elem_of A C _)}. Context `{FinCollection A C, Infinite A, !RelDecision (@{C})}.
Definition fresh_generic_body (s : C) (rec : s', s' s nat A) (n : nat) : A := Definition fresh_generic_body (s : C) (rec : s', s' s nat A) (n : nat) : A :=
let cand := inject n in let cand := inject n in
......
...@@ -311,7 +311,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → ...@@ -311,7 +311,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 →
Section list_set. Section list_set.
Context `{dec : EqDecision A}. Context `{dec : EqDecision A}.
Global Instance elem_of_list_dec : RelDecision (@elem_of A (list A) _). Global Instance elem_of_list_dec : RelDecision (@{list A}).
Proof. Proof.
refine ( refine (
fix go x l := fix go x l :=
......
...@@ -78,7 +78,7 @@ Section deciders. ...@@ -78,7 +78,7 @@ Section deciders.
Defined. Defined.
Global Instance mapset_equiv_dec : RelDecision (@{mapset M}) | 1. Global Instance mapset_equiv_dec : RelDecision (@{mapset M}) | 1.
Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined. Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
Global Instance mapset_elem_of_dec : RelDecision (@elem_of _ (mapset M) _) | 1. Global Instance mapset_elem_of_dec : RelDecision (@{mapset M}) | 1.
Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined. Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _). Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _).
Proof. Proof.
......
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