Sets over types with decidable equality(** version 1.0 |
Usage example for a set of naturals
Require Esets. Module NatEq <: Esets.EQ. Definition dom := nat. Definition dom_eq_dec := eq_nat_dec. End NatEq. Module NatSet := Esets.MakeSet(NatEq). |
Require Import List Elists.
Set Implicit Arguments.
| A signature for a data type with decidable equality |
Module Type EQ.
Parameter dom : Set.
Parameter dom_eq_dec : forall (x y : dom), {x = y} + {x <> y}.
End EQ.
Module MakeSet (Param : EQ) .
Import Param.
Definition set := list dom.
| The empty set |
Definition empty : set := nil.
| Membership |
Fixpoint In (x: dom) (l:set) {struct l} : bool :=
match l with
| nil => false
| b :: m => if dom_eq_dec x b then
true
else In x m
end.
Fixpoint incl (s1 s2 : set) { struct s1} : bool :=
match s1 with
nil => true
| x :: s11 =>
match In x s2 with
true => incl s11 s2
| _ => false
end
end.
| Set equality |
Definition seq (s1 s2: set) : bool :=
match incl s1 s2, incl s2 s1 with
true, true => true
| _, _ => false
end.
Hint Unfold seq.
| Add an element to a set |
Fixpoint add (v: dom) (s : set) { struct s } : set :=
match s with
| nil => v :: nil
| v' :: t => if dom_eq_dec v v' then s else v' :: add v t
end.
| Remove an element from a set |
Fixpoint remove (s : set) (v : dom) {struct s} : set :=
match s with
| nil => nil
| v' :: s' =>
if dom_eq_dec v v'
then s'
else v' :: remove s' v
end.
| Set union |
Fixpoint union (s1 s2 : set) {struct s1} : set :=
match s1 with
| nil => s2
| v :: s1' => add v (union s1' s2)
end.
Fixpoint intersect (s1 s2 : set) {struct s1} : set :=
match s1 with
| nil => nil
| v :: s1' =>
if In v s2
then v :: intersect s1' s2
else intersect s1' s2
end.
| A fold operation |
Definition fold (A: Type) (f: A -> dom -> A) (s: set) (start: A) : A
:= Elists.fold f s start.
| forall operation |
Fixpoint setall (f: dom -> bool) (s: set) { struct s } : bool :=
match s with
nil => true
| h::t => if f h then setall f t else false
end.
| exists operation |
Fixpoint setexists (f: dom -> bool) (s: set) { struct s } : bool :=
match s with
nil => false
| h::t => if f h then true else setexists f t
end.
| The elements of a set, as a list |
Definition elems (s : set) : list dom := s.
Theorems about sets |
Ltac setSimpl :=
repeat match goal with
| [ |- context[if dom_eq_dec ?V1 ?V2 then _ else _] ] =>
destruct (dom_eq_dec V1 V2); try subst; simpl; intuition
| [ H : context[if dom_eq_dec ?V1 ?V2 then _ else _] |- _ ] =>
destruct (dom_eq_dec V1 V2); try subst; simpl; intuition
| [ H : context[nil] |- _ ] => progress simpl in H
| [ H : context[_ :: _] |- _ ] => progress simpl in H
| [ |- context[nil] ] => progress simpl
| [ |- context[_ :: _] ] => progress simpl
end.
Theorem In_dec: forall v s,
{In v s = true} + {In v s = false}.
Theorem In_add : forall v v' s,
In v (add v' s) = true -> v = v' \/ In v s = true.
Theorem In_add_eq : forall v s, In v (add v s) = true.
Hint Resolve In_add_eq.
Theorem In_add_already: forall v v' s,
In v s = true -> In v (add v' s) = true.
Hint Resolve In_add_already.
Theorem In_add_neq : forall s v v',
v <> v' -> In v' (add v s) = In v' s.
Hint Resolve In_add_neq.
Lemma In_eq : forall a t,
In a (a :: t) = true.
Hint Resolve In_eq.
Theorems about
|
Theorem incl_empty : forall s, incl empty s = true.
Hint Resolve incl_empty.
Theorem incl_empty_empty: forall s, incl s empty = true -> s = empty.
Theorem incl_ok : forall s1 s2,
incl s1 s2 = true <-> (forall x, In x s1 = true -> In x s2 = true).
Theorem incl_refl : forall s,
incl s s = true.
Hint Resolve incl_refl.
Theorem incl_false : forall s1 s2,
incl s1 s2 = false
-> exists x, In x s1 = true /\ In x s2 = false.
Theorem incl_trans : forall s1 s2,
incl s1 s2 = true
-> forall s3, incl s2 s3 = true -> incl s1 s3 = true.
Theorem incl_In : forall s1 s2,
incl s1 s2 = true -> forall x, In x s1 = true -> In x s2 = true.
Theorem incl_add : forall s v,
incl s (add v s) = true.
Hint Resolve incl_add.
Theorem incl_union_left : forall s1 s1' s2,
incl s1 s1' = true -> incl s1 (union s1' s2) = true.
Hint Resolve incl_union_left.
Theorem incl_union_right : forall s1 s2 s2',
incl s2 s2' = true -> incl s2 (union s1 s2') = true.
Hint Resolve incl_union_right.
Theorems about
|
Theorem seq_refl : forall s : set, seq s s = true.
Hint Resolve seq_refl.
Theorem seq_trans : forall x y z:set, seq x y = true ->
seq y z = true ->
seq x z = true.
Theorem seq_sym : forall x y:set, seq x y = true -> seq y x = true.
Theorems about
|
Theorem union_empty_left : forall s : set, seq (union empty s) s = true.
Hint Resolve union_empty_left.
Theorem union_empty_right : forall s:set, seq s (union s empty) = true.
Hint Resolve union_empty_right.
Theorem union_comm : forall s1 s2:set, seq (union s1 s2) (union s2 s1) = true.
Hint Resolve union_comm.
Theorem union_ass :
forall s1 s2 s3:set,
seq (union (union s1 s2) s3) (union s1 (union s2 s3)) = true.
Hint Resolve union_ass.
Theorem seq_union_left : forall s1 s2 s:set,
seq s1 s2 = true ->
seq (union s1 s) (union s2 s) = true.
Hint Resolve seq_union_left.
Lemma seq_union_right : forall s1 s2 s:set,
seq s1 s2 = true ->
seq (union s s1) (union s s2) = true.
Hint Resolve seq_union_right.
Theorem union_congr : forall s1 s1' s2 s2' : set,
seq s1 s1' = true ->
seq s2 s2' = true ->
seq (union s1 s2) (union s1' s2') = true.
Theorem In_union_left : forall v s1 s2,
In v s1 = true -> In v (union s1 s2) = true.
Hint Resolve In_union_left.
Theorem In_union_right : forall v s1 s2,
In v s2 = true -> In v (union s1 s2) = true.
Hint Resolve In_union_right.
Theorem In_union : forall v s1 s2,
In v (union s1 s2) = true -> In v s1 = true \/ In v s2 = true.
Lemma union_idempotent' : forall s s',
incl s s' = true -> union s s' = s'.
Theorem union_idempotent : forall s,
union s s = s.
Hint Resolve union_idempotent.
Theorems about
|
Theorem In_intersect : forall v s' s,
In v (intersect s s') = true
-> In v s = true /\ In v s' = true.
Theorem In_intersect' : forall v s' s,
In v (intersect s s') = false
-> In v s = false \/ In v s' = false.
Theorem elems_ok : forall s x,
List.In x (elems s) <-> In x s = true.
Theorem elems_remove : forall s x ls,
elems s = x :: ls
-> elems (remove s x) = ls.
Theorems about
|
Theorem In_remove : forall x x' s,
In x s = true
-> x <> x'
-> In x (remove s x') = true.
Theorems about
|
| Fold transitions from property P0 to property P1, if P0 holds initially P1 is established at some element, and both are preserved. Must invoke with a specific P0. Use fold_monotone_1 if P0 = P1 and fold_monotone_2 if P0 = True |
Theorem fold_monotone_gen: forall (Acc:Type)
(P0: Acc -> Prop)
(s: set)
(start: Acc)
(f: Acc -> dom -> Acc)
(P1: Acc -> Prop),
P0 start ->
(forall x acc, In x s = true -> P0 acc -> P0 (f acc x)) ->
(exists x: dom, In x s = true /\
forall acc, P0 acc -> P1 (f acc x)) ->
(forall x acc, In x s = true -> P1 acc -> P1 (f acc x)) ->
P1 (fold f s start).
| Fold for a monotonic function is monotonic |
Theorem fold_monotone_1: forall (Acc:Type)
(s: set)
(start: Acc)
(f: Acc -> dom -> Acc)
(P: Acc -> Prop),
P start -> (forall x acc, In x s = true -> P acc -> P (f acc x)) ->
P (fold f s start).
| Fold for a monotonic function establishes a property, if the property is established by some element in the list and the folded function is monotone. |
Theorem fold_monotone_2: forall (Acc:Type)
(s: set)
(start: Acc)
(f: Acc -> dom -> Acc)
(P: Acc -> Prop),
(exists x: dom, In x s = true /\ forall acc, P (f acc x)) ->
(forall x acc, In x s = true -> P acc -> P (f acc x)) ->
P (fold f s start).
Definition dom := dom.
End MakeSet.
History |
|