Commit c1f41d83 authored by Robbert Krebbers's avatar Robbert Krebbers

List inclusion in terms of list membership.

parent 56c307ff
......@@ -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 *)
......
......@@ -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 *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment