Library Coq.Lists.ListSet
A Library for finite sets, implemented as lists
List is loaded, but not exported.
This allow to "hide" the definitions, functions and theorems of List
and to see only the ones of ListSet
If a belongs to x, removes a from x. If not, does nothing
returns the set of all els of x that does not belong to y
Fixpoint set_diff (
x y:set) {
struct x} :
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).
Hint Resolve set_add_intro1 set_add_intro2.
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.
Hint Resolve set_add_intro set_add_elim set_add_elim2.
Lemma set_add_not_empty :
forall (
a:A) (
x:set),
set_add a x <>
empty_set.
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).
Hint Resolve set_union_intro2 set_union_intro1.
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_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.
Hint Resolve set_inter_elim1 set_inter_elim2.
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_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_trivial :
forall (
a:A) (
x:set), ~
set_In a (
set_diff x x).
Hint Resolve set_diff_intro set_diff_trivial.
End first_definitions.
Section other_definitions.
Variables A B :
Type.
Definition set_prod :
set A ->
set B ->
set (
A *
B) :=
list_prod (
A:=A) (
B:=B).
B^A, set of applications from A to B