Library Coq.Lists.ListSet


A library for finite sets, implemented as lists
This is a light implementation of finite sets as lists; for a more extensive library, you might rather consider MSetWeakList.v. In addition, if your domain is totally ordered, you might also consider implementations of finite sets with access in logarithmic time (e.g. MSetRBT.v which is based on red-black trees).

Require Import List.

Set Implicit Arguments.

Section first_definitions.

  Variable A : Type.
  Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.

  Definition set := list A.

  Definition empty_set : set := nil.

  Fixpoint set_add (a:A) (x:set) : set :=
    match x with
    | nil => a :: nil
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => a1 :: x1
        | right _ => a1 :: set_add a x1
        end
    end.

  Fixpoint set_mem (a:A) (x:set) : bool :=
    match x with
    | nil => false
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => true
        | right _ => set_mem a x1
        end
    end.

If a belongs to x, removes a from x. If not, does nothing. Invariant: any element should occur at most once in x, see for instance set_add. We hence remove here only the first occurrence of a in x.

  Fixpoint set_remove (a:A) (x:set) : set :=
    match x with
    | nil => empty_set
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => x1
        | right _ => a1 :: set_remove a x1
        end
    end.

  Fixpoint set_inter (x:set) : set -> set :=
    match x with
    | nil => fun y => nil
    | a1 :: x1 =>
        fun y =>
          if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
    end.

  Fixpoint set_union (x y:set) : set :=
    match y with
    | nil => x
    | a1 :: y1 => set_add a1 (set_union x y1)
    end.

returns the set of all els of x that does not belong to y
  Fixpoint set_diff (x y:set) : set :=
    match x with
    | nil => nil
    | a1 :: x1 =>
        if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
    end.

  Definition set_In : A -> set -> Prop := In (A:=A).

  Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.

  Lemma set_mem_ind :
   forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
     (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).

  Lemma set_mem_ind2 :
   forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
     (set_In a x -> P y) ->
     (~ set_In a x -> P z) -> P (if set_mem a x then y else z).

  Lemma set_mem_correct1 :
   forall (a:A) (x:set), set_mem a x = true -> set_In a x.

  Lemma set_mem_correct2 :
   forall (a:A) (x:set), set_In a x -> set_mem a x = true.

  Lemma set_mem_complete1 :
   forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.

  Lemma set_mem_complete2 :
   forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.

  Lemma set_add_intro1 :
   forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).

  Lemma set_add_intro2 :
   forall (a b:A) (x:set), a = b -> set_In a (set_add b x).

  #[local]
  Hint Resolve set_add_intro1 set_add_intro2 : core.

  Lemma set_add_intro :
   forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).

  Lemma set_add_elim :
   forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.

  Lemma set_add_elim2 :
   forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.

  #[local]
  Hint Resolve set_add_intro set_add_elim set_add_elim2 : core.

  Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.

  Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l.

  Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l).

  Lemma set_remove_1 (a b : A) (l : set) :
    In a (set_remove b l) -> In a l.

  Lemma set_remove_2 (a b:A) (l : set) :
    NoDup l -> In a (set_remove b l) -> a <> b.

  Lemma set_remove_3 (a b : A) (l : set) :
    In a l -> a <> b -> In a (set_remove b l).

  Lemma set_remove_iff (a b : A) (l : set) :
   NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b).

  Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l).

  Lemma set_union_intro1 :
   forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).

  Lemma set_union_intro2 :
   forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).

  #[local]
  Hint Resolve set_union_intro2 set_union_intro1 : core.

  Lemma set_union_intro :
   forall (a:A) (x y:set),
     set_In a x \/ set_In a y -> set_In a (set_union x y).

  Lemma set_union_elim :
   forall (a:A) (x y:set),
     set_In a (set_union x y) -> set_In a x \/ set_In a y.

  Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'.

  Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l').

  Lemma set_union_emptyL :
   forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.

  Lemma set_union_emptyR :
   forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.

  Lemma set_inter_intro :
   forall (a:A) (x y:set),
     set_In a x -> set_In a y -> set_In a (set_inter x y).

  Lemma set_inter_elim1 :
   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.

  Lemma set_inter_elim2 :
   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.

  #[local]
  Hint Resolve set_inter_elim1 set_inter_elim2 : core.

  Lemma set_inter_elim :
   forall (a:A) (x y:set),
     set_In a (set_inter x y) -> set_In a x /\ set_In a y.

  Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'.

  Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l').

  Lemma set_diff_intro :
   forall (a:A) (x y:set),
     set_In a x -> ~ set_In a y -> set_In a (set_diff x y).

  Lemma set_diff_elim1 :
   forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.

  Lemma set_diff_elim2 :
   forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.

  Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'.

  Lemma set_diff_nodup l l' : NoDup l -> NoDup (set_diff l l').

  Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).

#[local]
Hint Resolve set_diff_intro set_diff_trivial : core.

End first_definitions.

Section other_definitions.

  Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) :=
    list_prod.

B^A, set of applications from A to B
  Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) :=
    list_power.

  Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B :=
    fold_left (A:=B) (B:=A).

  Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A)
    (b:B) : B := fold_right f b x.

  Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y})
    (f : A -> B) (x : set A) : set B :=
    set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B).

End other_definitions.

Unset Implicit Arguments.