diff --git a/theories/collections.v b/theories/collections.v index 3a49b8deb7e39928a11456bf7098b49468c1c2e0..cf898767d00da9410bb3cd05161a0cc96b9ad773 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -711,8 +711,8 @@ Section list_unfold. Qed. Global Instance set_unfold_included l k (P Q : A → Prop) : (∀ x, SetUnfold (x ∈ l) (P x)) → (∀ x, SetUnfold (x ∈ k) (Q x)) → - SetUnfold (l `included` k) (∀ x, P x → Q x). - Proof. by constructor; unfold included; set_unfold. Qed. + SetUnfold (l ⊆ k) (∀ x, P x → Q x). + Proof. by constructor; unfold subseteq, list_subseteq; set_unfold. Qed. End list_unfold. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index fc89ab4e266d3320bb7e479af62745852c8daa2e..9abe5b0e4f0f2e18e11f83e98b6818ce84e53ed3 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1225,14 +1225,14 @@ Qed. Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) : m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2. Proof. - intros. apply (anti_symm (⊆)); - apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=(⊆))). + intros. apply (anti_symm (⊆)); apply map_union_reflecting_l with m3; + auto using (reflexive_eq (R:=@subseteq (M A) _)). Qed. Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) : m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2. Proof. - intros. apply (anti_symm (⊆)); - apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=(⊆))). + intros. apply (anti_symm (⊆)); apply map_union_reflecting_r with m3; + auto using (reflexive_eq (R:=@subseteq (M A) _)). Qed. Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) : m1 ∪ m2 ⊥ₘ m3 ↔ m1 ⊥ₘ m3 ∧ m2 ⊥ₘ m3. diff --git a/theories/list.v b/theories/list.v index c968df49941f4bc9b7f231289eca4ecd8eb7b988..bcd3c29a73f6c7edc5200fb5f5b254b640b7c87a 100644 --- a/theories/list.v +++ b/theories/list.v @@ -303,9 +303,8 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) : | Forall3_cons x y z l k k' : P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k'). -(** Set operations Decisionon lists *) -Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2. -Infix "`included`" := included (at level 70) : C_scope. +(** Set operations on lists *) +Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → x ∈ l2. Section list_set. Context `{dec : EqDecision A}. @@ -2046,9 +2045,9 @@ Section contains_dec. End contains_dec. (** ** Properties of [included] *) -Global Instance included_preorder : PreOrder (@included A). +Global Instance list_subseteq_po : PreOrder (@subseteq (list A) _). Proof. split; firstorder. Qed. -Lemma included_nil l : [] `included` l. +Lemma list_subseteq_nil l : [] ⊆ l. Proof. intros x. by rewrite elem_of_nil. Qed. (** ** Properties of the [Forall] and [Exists] predicate *)