Library Coq.MSets.MSetWeakList
Finite sets library
Require Import MSetInterface.
Set Implicit Arguments.
Local Ltac Tauto.intuition_solver ::= auto with typeclass_instances.
Functions over lists
The set operations.
Module Ops (X: DecidableType) <: WOps X.
Definition elt := X.t.
Definition t := list elt.
Definition empty : t := nil.
Definition is_empty (l : t) : bool := if l then true else false.
Fixpoint mem (x : elt) (s : t) : bool :=
match s with
| nil => false
| y :: l =>
if X.eq_dec x y then true else mem x l
end.
Fixpoint add (x : elt) (s : t) : t :=
match s with
| nil => x :: nil
| y :: l =>
if X.eq_dec x y then s else y :: add x l
end.
Definition singleton (x : elt) : t := x :: nil.
Fixpoint remove (x : elt) (s : t) : t :=
match s with
| nil => nil
| y :: l =>
if X.eq_dec x y then l else y :: remove x l
end.
Definition fold (B : Type) (f : elt -> B -> B) : t -> B -> B :=
fold_left (flip f).
Definition union (s : t) : t -> t := fold add s.
Definition diff (s s' : t) : t := fold remove s' s.
Definition inter (s s': t) : t :=
fold (fun x s => if mem x s' then add x s else s) s nil.
Definition subset (s s' : t) : bool := is_empty (diff s s').
Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).
Fixpoint filter (f : elt -> bool) (s : t) : t :=
match s with
| nil => nil
| x :: l => if f x then x :: filter f l else filter f l
end.
Fixpoint for_all (f : elt -> bool) (s : t) : bool :=
match s with
| nil => true
| x :: l => if f x then for_all f l else false
end.
Fixpoint exists_ (f : elt -> bool) (s : t) : bool :=
match s with
| nil => false
| x :: l => if f x then true else exists_ f l
end.
Fixpoint partition (f : elt -> bool) (s : t) : t * t :=
match s with
| nil => (nil, nil)
| x :: l =>
let (s1, s2) := partition f l in
if f x then (x :: s1, s2) else (s1, x :: s2)
end.
Definition cardinal (s : t) : nat := length s.
Definition elements (s : t) : list elt := s.
Definition choose (s : t) : option elt :=
match s with
| nil => None
| x::_ => Some x
end.
End Ops.
Module MakeRaw (X:DecidableType) <: WRawSets X.
Include Ops X.
Section ForNotations.
Notation NoDup := (NoDupA X.eq).
Notation In := (InA X.eq).
Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
#[local]
Hint Resolve eqr eqtrans : core.
#[local]
Hint Immediate eqsym : core.
Definition IsOk := NoDup.
Class Ok (s:t) : Prop := ok : NoDup s.
#[local]
Hint Unfold Ok : core.
#[local]
Hint Resolve ok : core.
Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
Ltac inv_ok := match goal with
| H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok
| H:Ok nil |- _ => clear H; inv_ok
| H:NoDup ?l |- _ => change (Ok l) in H; inv_ok
| _ => idtac
end.
Ltac inv := invlist InA; inv_ok.
Ltac constructors := repeat constructor.
Fixpoint isok l := match l with
| nil => true
| a::l => negb (mem a l) && isok l
end.
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
Definition Empty s := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
Lemma In_compat : Proper (X.eq==>eq==>iff) In.
Lemma mem_spec : forall s x `{Ok s},
mem x s = true <-> In x s.
Lemma isok_iff : forall l, Ok l <-> isok l = true.
Global Instance isok_Ok l : isok l = true -> Ok l | 10.
Lemma add_spec :
forall (s : t) (x y : elt) {Hs : Ok s},
In y (add x s) <-> X.eq y x \/ In y s.
Global Instance add_ok s x `(Ok s) : Ok (add x s).
Lemma remove_spec :
forall (s : t) (x y : elt) {Hs : Ok s},
In y (remove x s) <-> In y s /\ ~X.eq y x.
Global Instance remove_ok s x `(Ok s) : Ok (remove x s).
Lemma singleton_ok : forall x : elt, Ok (singleton x).
Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.
Lemma empty_ok : Ok empty.
Lemma empty_spec : Empty empty.
Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.
Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.
Lemma elements_spec2w : forall (s : t) {Hs : Ok s}, NoDup (elements s).
Lemma fold_spec :
forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i.
Global Instance union_ok : forall s s' `(Ok s, Ok s'), Ok (union s s').
Lemma union_spec :
forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
In x (union s s') <-> In x s \/ In x s'.
Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
Lemma inter_spec :
forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
In x (inter s s') <-> In x s /\ In x s'.
Global Instance diff_ok : forall s s' `(Ok s, Ok s'), Ok (diff s s').
Lemma diff_spec :
forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
In x (diff s s') <-> In x s /\ ~In x s'.
Lemma subset_spec :
forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
subset s s' = true <-> Subset s s'.
Lemma equal_spec :
forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
equal s s' = true <-> Equal s s'.
Definition choose_spec1 :
forall (s : t) (x : elt), choose s = Some x -> In x s.
Definition choose_spec2 : forall s : t, choose s = None -> Empty s.
Lemma cardinal_spec :
forall (s : t) {Hs : Ok s}, cardinal s = length (elements s).
Lemma filter_spec' : forall s x f,
In x (filter f s) -> In x s.
Lemma filter_spec :
forall (s : t) (x : elt) (f : elt -> bool),
Proper (X.eq==>eq) f ->
(In x (filter f s) <-> In x s /\ f x = true).
Global Instance filter_ok s f `(Ok s) : Ok (filter f s).
Lemma for_all_spec :
forall (s : t) (f : elt -> bool),
Proper (X.eq==>eq) f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Lemma exists_spec :
forall (s : t) (f : elt -> bool),
Proper (X.eq==>eq) f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).
Lemma partition_spec1 :
forall (s : t) (f : elt -> bool),
Proper (X.eq==>eq) f ->
Equal (fst (partition f s)) (filter f s).
Lemma partition_spec2 :
forall (s : t) (f : elt -> bool),
Proper (X.eq==>eq) f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
Lemma partition_ok1' :
forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
In x (fst (partition f s)) -> In x s.
Lemma partition_ok2' :
forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
In x (snd (partition f s)) -> In x s.
Global Instance partition_ok1 : forall s f `(Ok s), Ok (fst (partition f s)).
Global Instance partition_ok2 : forall s f `(Ok s), Ok (snd (partition f s)).
End ForNotations.
Definition In := InA X.eq.
Definition eq := Equal.
#[global]
Instance eq_equiv : Equivalence eq := _.
End MakeRaw.