### Remove some generic decision procedures for sets.

```These just make things more complicated, it would be more useful to
declare (efficient) decision procedures for each instance, so that
we can properly predict which instance we will get.```
parent 38417bec
 ... ... @@ -115,15 +115,6 @@ Section simple_collection. Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅. Proof. unfold_leibniz. apply non_empty_singleton. Qed. End leibniz. Section dec. Context `{∀ X Y : C, Decision (X ⊆ Y)}. Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Proof. refine (cast_if (decide_rel (⊆) {[ x ]} X)); by rewrite elem_of_subseteq_singleton. Defined. End dec. End simple_collection. (** * Tactics *) ... ...
 ... ... @@ -101,24 +101,12 @@ Proof. intros x; rewrite !elem_of_elements; set_solver. - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. Qed. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Proof. refine (cast_if (decide_rel (∈) x (elements X))); by rewrite <-(elem_of_elements _). Defined. Global Program Instance collection_subseteq_dec_slow (X Y : C) : Decision (X ⊆ Y) | 100 := match decide_rel (=) (size (X ∖ Y)) 0 return _ with | left _ => left _ | right _ => right _ end. Next Obligation. intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)). apply (size_empty_inv _ E1). by rewrite elem_of_difference. Qed. Next Obligation. intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x. rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3. Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). Proof. rewrite <-size_union by set_solver. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!