From c1f41d83370d2b2639dbaebc95919b94b16fca9d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Mar 2016 15:00:30 +0100
Subject: [PATCH] List inclusion in terms of list membership.

---
 prelude/collections.v | 4 ++++
 prelude/list.v        | 9 +++++++++
 2 files changed, 13 insertions(+)

diff --git a/prelude/collections.v b/prelude/collections.v
index 6591108dc..cf4669c0a 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -324,6 +324,10 @@ Section list_unfold.
     intros ??; constructor.
     by rewrite elem_of_app, (set_unfold (x ∈ l) P), (set_unfold (x ∈ k) Q).
   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.
 End list_unfold.
 
 (** * Guard *)
diff --git a/prelude/list.v b/prelude/list.v
index f7527b30c..735949853 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -282,6 +282,9 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
      P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k').
 
 (** Set operations on lists *)
+Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2.
+Infix "`included`" := included (at level 70) : C_scope.
+
 Section list_set.
   Context {A} {dec : ∀ x y : A, Decision (x = y)}.
   Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)}
@@ -2017,6 +2020,12 @@ Section contains_dec.
     abstract (rewrite Permutation_alt; tauto).
   Defined.
 End contains_dec.
+
+(** ** Properties of [included] *)
+Global Instance included_preorder : PreOrder (@included A).
+Proof. split; firstorder. Qed.
+Lemma included_nil l : [] `included` l.
+Proof. intros x. by rewrite elem_of_nil. Qed.
 End more_general_properties.
 
 (** ** Properties of the [Forall] and [Exists] predicate *)
-- 
GitLab