From 596a0a2c136a7e7bfe5c107272d6c569846acc73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 13:32:50 +0200
Subject: [PATCH] =?UTF-8?q?Use=20=E2=8A=86=20type=20class=20for=20set-like?=
 =?UTF-8?q?=20inclusion=20of=20lists.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This also solves a name clash with the extension order of CMRAs.
---
 theories/collections.v | 4 ++--
 theories/fin_maps.v    | 8 ++++----
 theories/list.v        | 9 ++++-----
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/theories/collections.v b/theories/collections.v
index 3a49b8de..cf898767 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 fc89ab4e..9abe5b0e 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 c968df49..bcd3c29a 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 *)
-- 
GitLab