From 186da990ebce236a402421c6cfce17af37cf1c72 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.
---
 heap_lang/lang.v      | 4 ++--
 prelude/collections.v | 4 ++--
 prelude/fin_maps.v    | 8 ++++----
 prelude/list.v        | 9 ++++-----
 4 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 6a0f8af99..6436b4217 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -318,11 +318,11 @@ Lemma alloc_fresh e v σ :
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
 (** Closed expressions *)
-Lemma is_closed_weaken X Y e : is_closed X e → X `included` Y → is_closed Y e.
+Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
 Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
 
 Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
-Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
+Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
 
 Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
 Proof.
diff --git a/prelude/collections.v b/prelude/collections.v
index ef7383d52..39eb6f103 100644
--- a/prelude/collections.v
+++ b/prelude/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/prelude/fin_maps.v b/prelude/fin_maps.v
index 2f75f6b98..69c1f1c80 100644
--- a/prelude/fin_maps.v
+++ b/prelude/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/prelude/list.v b/prelude/list.v
index c5f4ee34c..b96edfdc9 100644
--- a/prelude/list.v
+++ b/prelude/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