Require Import List.
Finite sets with extensional equality |
Record ExtFset (A : Set) : Type := mkExtFset {
extFset : Set;
In : A -> extFset -> Prop;
In_dec : forall x E, {In x E} + {~ In x E};
eq_carrier_dec : forall (x y : A), {x = y} + {x <> y};
eq_extFset : forall E F, (forall x, In x E <-> In x F) -> E = F;
empty : extFset;
empty_neg_intro : forall x, ~ In x empty;
add : A -> extFset -> extFset;
add_intro_1 : forall x y E, x = y -> In x (add y E);
add_intro_2 : forall x y E, In x E -> In x (add y E);
add_elim : forall x y E, In x (add y E) -> x = y \/ In x E;
union : extFset -> extFset -> extFset;
union_intro_1 : forall x E F, In x E -> In x (union E F);
union_intro_2 : forall x E F, In x F -> In x (union E F);
union_elim : forall x E F, In x (union E F) -> In x E \/ In x F;
intersection : extFset -> extFset -> extFset;
intersection_intro :
forall x E F, In x E -> In x F -> In x (intersection E F);
intersection_elim_1 : forall x E F, In x (intersection E F) -> In x E;
intersection_elim_2 : forall x E F, In x (intersection E F) -> In x F;
diff : extFset -> extFset -> extFset;
diff_intro : forall x E F, In x E -> ~ In x F -> In x (diff E F);
diff_elim_1 : forall x E F, In x (diff E F) -> In x E;
diff_elim_2 : forall x E F, In x (diff E F) -> ~ In x F;
map : (A -> A) -> extFset -> extFset;
map_intro : forall x E f, In x E -> In (f x) (map f E);
map_elim : forall y E f, In y (map f E) -> exists x, In x E /\ y = f x;
elements : extFset -> list A;
elements_spec : forall x E, In x E <-> List.In x (elements E)
}.
Implicit Arguments extFset [A].
Implicit Arguments In [A e].
Implicit Arguments In_dec [A e].
Implicit Arguments eq_carrier_dec [A].
Implicit Arguments empty [A e].
Implicit Arguments empty_neg_intro [A e].
Implicit Arguments add [A e].
Implicit Arguments add_intro_1 [A e].
Implicit Arguments add_intro_2 [A e].
Implicit Arguments add_elim [A e].
Implicit Arguments union [A e].
Implicit Arguments union_intro_1 [A e].
Implicit Arguments union_intro_2 [A e].
Implicit Arguments union_elim [A e].
Implicit Arguments intersection [A e].
Implicit Arguments intersection_intro [A e].
Implicit Arguments intersection_elim_1 [A e].
Implicit Arguments intersection_elim_2 [A e].
Implicit Arguments diff [A e].
Implicit Arguments diff_intro [A e].
Implicit Arguments diff_elim_1 [A e].
Implicit Arguments diff_elim_2 [A e].
Implicit Arguments map [A e].
Implicit Arguments map_intro [A e].
Implicit Arguments map_elim [A e].
Implicit Arguments elements [A e].
Implicit Arguments elements_spec [A e].
Hint Resolve empty_neg_intro : sets.
Hint Resolve add_intro_1 add_intro_2 add_elim : sets.
Hint Resolve union_intro_1 union_intro_2 union_elim : sets.
Hint Resolve intersection_intro intersection_elim_1 intersection_elim_2 : sets.
Hint Resolve diff_intro diff_elim_1 diff_elim_2 : sets.
Hint Resolve map_intro map_elim : sets.
Hint Resolve elements_spec : sets.
Ltac destruct_empty :=
match goal with
| H : In (e:= ?e) _ empty |- _ =>
assert (fresh:= @empty_neg_intro _ e _ H);
contradiction
end.
Ltac destruct_add H :=
match goal with
| _ : In (e:= ?e) _ (add _ _) |- _ =>
let H' := fresh in (
assert (H':= @add_elim _ e _ _ _ H);
clear H;
inversion_clear H' as [H | H]
)
end.
Ltac destruct_union H :=
match goal with
| _ : In (e:= ?e) _ (union _ _) |- _ =>
let H' := fresh in (
assert (H':= @union_elim _ e _ _ _ H);
clear H;
inversion_clear H' as [H | H]
)
end.
Ltac destruct_intersection H H1 H2 :=
match goal with
| _ : In (e:= ?e) _ (intersection _ _) |- _ =>
assert (H1:= @intersection_elim_1 _ e _ _ _ H);
assert (H2:= @intersection_elim_2 _ e _ _ _ H);
clear H
end.
Ltac destruct_diff H H1 H2 :=
match goal with
| _ : In (e:= ?e) _ (diff _ _) |- _ =>
assert (H1:= @diff_elim_1 _ e _ _ _ H);
assert (H2:= @diff_elim_2 _ e _ _ _ H);
clear H
end.
Ltac destruct_map H x H1 H2 :=
match goal with
| _ : In (e:= ?e) _ (map _ _) |- _ =>
case (@map_elim _ _ _ _ _ H); intros x [H1 H2];
clear H
end.
Additional theorems |
Section AdditionalTheorems.
Variable A : Set.
Variable ER : ExtFset A.
| Empty. |
Theorem empty_elim :
forall (x : A) (E : extFset ER), In x (@empty _ ER) -> In x E.
| Add. |
Theorem add_elim_1 :
forall (x y : A) (E : extFset ER), In x (add y E) -> ~ In x E -> x = y.
Theorem add_elim_2 :
forall (x y : A) (E : extFset ER), In x (add y E) -> x <> y -> In x E.
Theorem add_neg_elim_1 :
forall (x y : A) (E : extFset ER), ~ In x (add y E) -> x <> y.
Theorem add_neg_elim_2 :
forall (x y : A) (E : extFset ER), ~ In x (add y E) -> ~ In x E.
Theorem add_neg_intro :
forall (x y : A) (E : extFset ER), x <> y -> ~ In x E -> ~ In x (add y E).
| Union. |
Theorem union_elim_1 :
forall (x : A) (E F : extFset ER), In x (union E F) -> ~ In x F -> In x E.
Theorem union_elim_2 :
forall (x : A) (E F : extFset ER), In x (union E F) -> ~ In x E -> In x F.
Theorem union_neg_elim_1 :
forall (x : A) (E F : extFset ER), ~ In x (union E F) -> ~ In x E.
Theorem union_neg_elim_2 :
forall (x : A) (E F : extFset ER), ~ In x (union E F) -> ~ In x F.
Theorem union_neg_intro :
forall (x : A) (E F : extFset ER),
~ In x E -> ~ In x F -> ~ In x (union E F).
| Intersection. |
Theorem intersection_neg_elim :
forall (x : A) (E F : extFset ER),
~ In x (intersection E F) -> ~ In x E \/ ~ In x F.
Theorem intersection_neg_elim_1 :
forall (x : A) (E F : extFset ER),
~ In x (intersection E F) -> In x F -> ~ In x E.
Theorem intersection_neg_elim_2 :
forall (x : A) (E F : extFset ER),
~ In x (intersection E F) -> In x E -> ~ In x F.
Theorem intersection_neg_intro_1 :
forall (x : A) (E F : extFset ER), ~ In x E -> ~ In x (intersection E F).
Theorem intersection_neg_intro_2 :
forall (x : A) (E F : extFset ER), ~ In x F -> ~ In x (intersection E F).
| Diff. |
Theorem diff_neg_elim :
forall (x : A) (E F : extFset ER), ~ In x (diff E F) -> ~ In x E \/ In x F.
Theorem diff_neg_elim_1 :
forall (x : A) (E F : extFset ER), ~ In x (diff E F) -> ~ In x F -> ~ In x F.
Theorem diff_neg_elim_2 :
forall (x : A) (E F : extFset ER), ~ In x (diff E F) -> In x E -> In x F.
Theorem diff_neg_intro_1 :
forall (x : A) (E F : extFset ER), ~ In x E -> ~ In x (diff E F).
Theorem diff_neg_intro_2 :
forall (x : A) (E F : extFset ER), In x F -> ~ In x (diff E F).
| Map. |
Theorem map_compose :
forall f g (F : extFset ER), map (fun x => f (g x)) F = map f (map g F).
| Elements. |
Theorem elements_empty :
elements (@empty _ ER) = nil.
End AdditionalTheorems.
Implicit Arguments empty_elim [A ER].
Implicit Arguments add_elim_1 [A ER].
Implicit Arguments add_elim_2 [A ER].
Implicit Arguments add_neg_elim_1 [A ER].
Implicit Arguments add_neg_elim_2 [A ER].
Implicit Arguments add_neg_intro [A ER].
Implicit Arguments union_elim_1 [A ER].
Implicit Arguments union_elim_2 [A ER].
Implicit Arguments union_neg_elim_1 [A ER].
Implicit Arguments union_neg_elim_2 [A ER].
Implicit Arguments union_neg_intro [A ER].
Implicit Arguments intersection_neg_elim [A ER].
Implicit Arguments intersection_neg_elim_1 [A ER].
Implicit Arguments intersection_neg_elim_2 [A ER].
Implicit Arguments intersection_neg_intro_1 [A ER].
Implicit Arguments intersection_neg_intro_2 [A ER].
Implicit Arguments diff_neg_elim [A ER].
Implicit Arguments diff_neg_elim_1 [A ER].
Implicit Arguments diff_neg_elim_2 [A ER].
Implicit Arguments diff_neg_intro_1 [A ER].
Implicit Arguments diff_neg_intro_2 [A ER].
Hint Resolve empty_elim : sets.
Hint Immediate add_elim_1 : sets.
Hint Resolve add_elim_2 : sets.
Hint Resolve add_neg_elim_1 add_neg_elim_2 add_neg_intro : sets.
Hint Resolve union_elim_1 union_elim_2 : sets.
Hint Resolve union_neg_elim_1 union_neg_elim_2 union_neg_intro : sets.
Hint Resolve intersection_neg_elim : sets.
Hint Resolve intersection_neg_elim_1 intersection_neg_elim_2 : sets.
Hint Resolve intersection_neg_intro_1 intersection_neg_intro_2 : sets.
Hint Resolve diff_neg_elim diff_neg_elim_1 diff_neg_elim_2 : sets.
Hint Resolve diff_neg_intro_1 diff_neg_intro_2 : sets.
Hint Resolve map_compose : sets.
Hint Resolve elements_empty : sets.
Hint Rewrite elements_empty : sets.
Ltac destruct_neg_add H H1 H2 :=
match goal with
| _ : ~ In (e:= ?e) _ (add _ _) |- _ =>
assert (H1:= @add_neg_elim_1 _ e _ _ _ H);
assert (H2:= @add_neg_elim_2 _ e _ _ _ H);
clear H
end.
Ltac destruct_neg_union H H1 H2 :=
match goal with
| _ : ~ In (e:= ?e) _ (union _ _) |- _ =>
assert (H1:= @union_neg_elim_1 _ e _ _ _ H);
assert (H2:= @union_neg_elim_2 _ e _ _ _ H);
clear H
end.
Ltac destruct_neg_intersection H :=
match goal with
| _ : ~ In (e:= ?e) _ (intersection _ _) |- _ =>
let H' := fresh in (
assert (H':= @intersection_neg_elim _ e _ _ _ H);
clear H;
inversion_clear H' as [H | H]
)
end.
Ltac destruct_neg_diff H :=
match goal with
| _ : ~ In (e:= ?e) _ (diff _ _) |- _ =>
let H' := fresh in (
assert (H':= @diff_neg_elim _ e _ _ _ H);
clear H;
inversion_clear H' as [H | H]
)
end.
Singleton sets |
Section Singleton.
Variable A : Set.
Variable ER : ExtFset A.
Definition singleton (x : A) : extFset ER := add x empty.
Theorem singleton_intro : forall (x y : A), x = y -> In x (singleton y).
Theorem singleton_elim : forall (x y : A), In x (singleton y) -> x = y.
Theorem singleton_neg_elim : forall (x y : A), ~ In x (singleton y) -> x <> y.
Theorem singleton_neg_intro : forall (x y : A), x <> y -> ~ In x (singleton y).
End Singleton.
Implicit Arguments singleton [A ER].
Implicit Arguments singleton_intro [A ER].
Implicit Arguments singleton_elim [A ER].
Implicit Arguments singleton_neg_elim [A ER].
Implicit Arguments singleton_neg_intro [A ER].
Hint Resolve singleton_intro : sets.
Hint Immediate singleton_elim : sets.
Hint Resolve singleton_neg_elim singleton_neg_intro : sets.
Ltac destruct_singleton H :=
match goal with
| _ : In (e:= ?e) _ (singleton _) |- _ =>
let H' := fresh in (
rename H into H';
assert (H:= @singleton_elim _ e _ _ H');
clear H'
)
end.
Ltac destruct_neg_singleton H :=
match goal with
| _ : ~ In (e:= ?e) _ (singleton _) |- _ =>
let H' := fresh in (
rename H into H';
assert (H:= @singleton_neg_elim _ e _ _ H');
clear H'
)
end.
Removing an element from a set |
Section Remove.
Variable A : Set.
Variable ER : ExtFset A.
Definition remove (x : A) (E : extFset ER) : extFset ER :=
diff E (singleton x).
Theorem remove_intro :
forall (x y : A) (E : extFset ER), x <> y -> In x E -> In x (remove y E).
Theorem remove_elim_1 :
forall (x y : A) (E : extFset ER), In x (remove y E) -> x <> y.
Theorem remove_elim_2 :
forall (x y : A) (E : extFset ER), In x (remove y E) -> In x E.
Lemma remove_neg_elim :
forall (x y : A) (E : extFset ER),
~ In x (remove y E) -> x = y \/ ~ In x E.
Lemma remove_neg_elim_strong_1 :
forall (x y : A) (E : extFset ER),
~ In x (remove y E) -> x = y \/ (x <> y /\ ~ In x E).
Lemma remove_neg_elim_strong_2 :
forall (x y : A) (E : extFset ER),
~ In x (remove y E) -> (x = y /\ In x E) \/ ~ In x E.
Theorem remove_neg_intro_1 :
forall (x y : A) (E : extFset ER), x = y -> ~ In x (remove y E).
Theorem remove_neg_intro_2 :
forall (x y : A) (E : extFset ER), ~ In x E -> ~ In x (remove y E).
End Remove.
Implicit Arguments remove [A ER].
Implicit Arguments remove_intro [A ER].
Implicit Arguments remove_elim_1 [A ER].
Implicit Arguments remove_elim_2 [A ER].
Implicit Arguments remove_neg_elim [A ER].
Implicit Arguments remove_neg_elim_strong_1 [A ER].
Implicit Arguments remove_neg_elim_strong_2 [A ER].
Implicit Arguments remove_neg_intro_1 [A ER].
Implicit Arguments remove_neg_intro_2 [A ER].
Hint Resolve remove_intro remove_elim_1 remove_elim_2 : sets.
Hint Resolve remove_neg_elim remove_neg_intro_1 remove_neg_intro_2 : sets.
Hint Resolve remove_neg_elim_strong_1 remove_neg_elim_strong_2 : sets.
Ltac destruct_remove H H1 H2 :=
match goal with
| _ : In (e:= ?e) _ (remove _ _) |- _ =>
assert (H1:= @remove_elim_1 _ e _ _ _ H);
assert (H2:= @remove_elim_2 _ e _ _ _ H);
clear H
end.
Ltac destruct_neg_remove H :=
match goal with
| _ : ~ In (e:= ?e) _ (remove _ _) |- _ =>
let H' := fresh in (
assert (H':= @remove_neg_elim _ e _ _ _ H);
clear H;
inversion_clear H' as [H | H]
)
end.
Equivalence theorems |
Section EquivalenceTheorems.
Variable A : Set.
Variable ER : ExtFset A.
| Add. |
Lemma add_add_incl :
forall (x y z: A) (E : extFset ER),
In x (add y (add z E)) -> In x (add z (add y E)).
Theorem add_add :
forall (x y : A) (E : extFset ER), add x (add y E) = add y (add x E).
Theorem add_union :
forall (x : A) (E F : extFset ER),
add x (union E F) = union (add x E) (add x F).
| Union. |
Theorem union_empty_1 :
forall (E : extFset ER), union empty E = E.
Theorem union_empty_2 :
forall (E : extFset ER), union E empty = E.
Theorem union_commute :
forall (E F : extFset ER), union E F = union F E.
Theorem union_union_distrib :
forall (E F G : extFset ER),
union (union E F) G = union (union E G) (union F G).
| Intersection. |
Theorem intersection_empty_1 :
forall (E : extFset ER), intersection empty E = empty.
Theorem intersection_empty_2 :
forall (E : extFset ER), intersection E empty = empty.
| Diff. |
Theorem diff_empty_1 :
forall (E : extFset ER), diff E empty = E.
Theorem diff_empty_2 :
forall (E : extFset ER), diff empty E = empty.
| Remove. |
Theorem remove_empty :
forall (x : A), remove x (@empty _ ER) = empty.
Theorem remove_union :
forall (x : A) (E F : extFset ER),
remove x (union E F) = union (remove x E) (remove x F).
Theorem remove_singleton_1 :
forall (x y : A), x = y -> remove x (singleton y) = @empty _ ER.
Theorem remove_singleton_2 :
forall (x y : A),
x <> y -> remove (ER:= ER) x (singleton y) = (singleton y).
End EquivalenceTheorems.
Implicit Arguments add_add_incl [A ER].
Implicit Arguments add_add [A ER].
Implicit Arguments add_union [A ER].
Implicit Arguments union_empty_1 [A ER].
Implicit Arguments union_empty_2 [A ER].
Implicit Arguments union_union_distrib [A ER].
Implicit Arguments intersection_empty_1 [A ER].
Implicit Arguments intersection_empty_2 [A ER].
Implicit Arguments diff_empty_1 [A ER].
Implicit Arguments diff_empty_2 [A ER].
Implicit Arguments remove_empty [A ER].
Implicit Arguments remove_union [A ER].
Implicit Arguments remove_singleton_1 [A ER].
Implicit Arguments remove_singleton_2 [A ER].
Hint Immediate add_add_incl : sets.
Hint Resolve add_add add_union : sets.
Hint Resolve union_empty_1 union_empty_2 : sets.
Hint Immediate union_commute : sets.
Hint Resolve union_union_distrib : sets.
Hint Resolve intersection_empty_1 intersection_empty_2 : sets.
Hint Resolve diff_empty_1 diff_empty_2 : sets.
Hint Resolve remove_empty remove_union : sets.
Hint Resolve remove_singleton_1 remove_singleton_2 : sets.
Hint Rewrite add_union : sets.
Hint Rewrite union_empty_1 union_empty_2 : sets.
Hint Rewrite intersection_empty_1 intersection_empty_2 : sets.
Hint Rewrite diff_empty_1 diff_empty_2 : sets.
Hint Rewrite remove_empty remove_union : sets.
Hint Rewrite remove_singleton_1 using (auto; fail) : sets.
Hint Rewrite remove_singleton_2 using (auto; fail) : sets.
Predicates on sets. |
Section Predicates.
Variable A : Set.
Variable ER : ExtFset A.
Definition Subset (E F : extFset ER) := forall x, In x E -> In x F.
Theorem Subset_refl :
forall (E : extFset ER), Subset E E.
Theorem Subset_trans :
forall (E F G : extFset ER),
Subset E F -> Subset F G -> Subset E G.
Theorem Subset_empty :
forall (E : extFset ER), Subset empty E.
Theorem Subset_singleton_l :
forall (E : extFset ER) (x : A), In x E -> Subset (singleton x) E.
Theorem Subset_union_l :
forall (E F G : extFset ER), Subset E G -> Subset F G -> Subset (union E F) G.
Theorem Subset_union_r1 :
forall (E F : extFset ER), Subset E (union E F).
Theorem Subset_union_r2 :
forall (E F : extFset ER), Subset F (union E F).
Theorem Subset_union_union :
forall (A B C D : extFset ER),
Subset A C -> Subset B D -> Subset (union A B) (union C D).
Theorem Subset_add :
forall (E F : extFset ER) (x : A),
Subset E F -> Subset (add x E) (add x F).
Theorem Subset_add_r :
forall (E F G : extFset ER) (x : A),
Subset F G -> Subset E (add x F) -> Subset E (add x G).
Theorem Subset_remove_l_to_add :
forall (E F : extFset ER) (x : A),
Subset (remove x E) F -> Subset E (add x F).
Theorem Subset_add_l_to_remove :
forall (E F : extFset ER) (x : A),
Subset E (add x F) -> Subset (remove x E) F.
End Predicates.
Implicit Arguments Subset [A ER].
Hint Resolve Subset_refl : sets.
Hint Resolve Subset_empty Subset_singleton_l : sets.
Hint Resolve Subset_union_l : sets.
Hint Resolve Subset_union_r1 Subset_union_r2 Subset_union_union : sets.
Hint Resolve Subset_add Subset_add_r : sets.
Hint Resolve Subset_remove_l_to_add Subset_add_l_to_remove : sets.