Browse the main library: A B C D E F G or go to appendix or return to overview.

Library a_sets

This formalisation is part of Dominik Kirst's Bachelor Thesis, submitted Sep 2014. It was implemented at the Programming Systems Lab in Saarbruecken, headed by Prof. Gert Smolka. We present the development of a ZF set theory, introduce the notions of orderings, functions and ordinals and conclude the equivalence of Well-Ordering Theorem and Axiom of Choice. We do not provide excessive commentary in the source files and refer to the explanations given in the thesis.

import of necessary libraries

Require Export Coq.Logic.Classical_Prop.
Require Export Coq.Setoids.Setoid.

Classical Meta-Theory

Lemma cp (A B: Prop): A -> B <-> ~ B -> ~ A.

Lemma notex2all (X: Type) (P :X -> Prop): (~ exists x, P x) -> forall x, ~ P x.

Lemma notall2ex (X: Type) (P: X -> Prop): (~ forall x, P x) -> exists x, ~ P x.

Lemma imp_neg (X: Type) (P Q: X -> Prop) (x: X): ~ (P x -> Q x) -> P x /\ ~ Q x.

Basic Framework with Element- and Subset-Relation

Parameter set: Type.
Parameter el: set -> set -> Prop.

Notation "x '<e' y" := (el x y) (at level 70).
Notation "x '/<e' y" := (~(el x y)) (at level 70).

Definition subs: set -> set -> Prop :=
fun X Y => forall x : set, x <e X -> x <e Y.

Notation "X 'c=' Y" := (subs X Y) (at level 70).
Notation "X '/c=' Y" := (~(subs X Y)) (at level 70).

Description

Parameter desc: (set -> Prop) -> set.
Axiom Desc: forall P, (exists! x, P x) -> P (desc P).

Lemma desc_unique P A: (exists! x, P x) -> P A -> A = desc P.

Lemma desc_P P x: (exists! x, P x) -> x = desc P -> P x.

The Axioms of ZF

Axiom Extensionality:
  forall A B, A c= B -> B c= A -> A = B.

Axiom ZF_Existence:
  exists! empty, forall x, x /<e empty.

Axiom ZF_Specification:
  forall A P, exists! specification, forall x, x <e specification <-> x <e A /\ P x.

Axiom ZF_Pair:
  forall A B, exists! pair, forall x, x <e pair <-> x = A \/ x = B.

Axiom ZF_Union:
  forall S, exists! union, forall x, x <e union <-> exists A, x <e A /\ A <e S.

Axiom ZF_Power:
  forall S, exists! power, forall X, X <e power <-> X c= S.

Axiom ZF_Replacement:
  forall A R, exists! replacement, forall y, y <e replacement <-> exists x, x <e A /\ y = R x.

Simplification of the Axioms via Description

Definition empty :=
  desc (fun empty => forall x, x /<e empty).

Definition specification A P :=
  desc (fun specification => forall x, x <e specification <-> x <e A /\ P x).

Definition pair A B :=
  desc (fun pair => forall x, x <e pair <-> x = A \/ x = B).

Definition union S :=
  desc (fun union => forall x, x <e union <-> exists A, x <e A /\ A <e S).

Definition power S :=
  desc (fun power => forall X, X <e power <-> X c= S).

Definition replacement A R :=
  desc (fun replacement => forall y, y <e replacement <-> exists x, x <e A /\ y = R x).

Lemma Existence:
  forall x, x /<e empty.

Lemma Specification:
  forall A P x, x <e (specification A P) <-> x <e A /\ P x.

Lemma Pair:
  forall A B x, x <e (pair A B) <-> x = A \/ x = B.

Lemma Union:
  forall S x, x <e (union S) <-> exists A, x <e A /\ A <e S.

Lemma Power:
  forall S X, X <e (power S) <-> X c= S.

Lemma Replacement:
  forall A R y, y <e (replacement A R) <-> exists x, x <e A /\ y = R x.

Regularity and Infinity

Axiom Regularity:
forall A, A <> empty -> exists B, B <e A /\ (forall x, x <e B -> x /<e A).

Axiom Infinity:
exists A, empty <e A /\ (forall x, x <e A -> union (pair x (pair x x)) <e A).

Some General Statements

Lemma subseq A: A c= A.

Lemma subs_trans A B C: A c= B -> B c= C -> A c= C.

Lemma empty_subs A: empty c= A.

Lemma empty_el A: A <> empty <-> exists x, x <e A.

Lemma subs_el A B: A /c= B <-> exists x, x <e A /\ x /<e B.

Lemma extenE A B: A = B -> A c= B /\ B c= A.

Lemma pair1 a b: a <e pair a b.

Lemma pair2 a b: b <e pair a b.

Lemma spec_subs A P: specification A P c= A.

Lemma spec_equal A P: specification A P = A <-> (forall x, x <e A -> P x).

Lemma spec_empty P: specification empty P = empty.

Lemma power_trans A B C: A c= B -> B <e power C -> A <e power C.

Lemma one_cycles A: A /<e A.

Lemma all_set: ~ exists A, forall a, a <e A.

Lemma russell: ~ exists A, forall a, a <e A.

Binary Union, Intersection and Complement Sets

Definition bunion A B := union (pair A B).
Definition inter S := specification (union S) (fun x => forall A, A <e S -> x <e A).
Definition binter A B := inter (pair A B).
Definition comp A B := specification A (fun a => a /<e B).
Notation "A \ B" := (comp A B) (at level 55).

Lemma bunionI1 A B x: x <e A -> x <e bunion A B.

Lemma bunionI2 A B x: x <e B -> x <e bunion A B.

Lemma bunionE A B x: x <e bunion A B -> x <e A \/ x <e B.

Lemma interI S x: (forall A, A <e S -> x <e A) -> S <> empty -> x <e (inter S).

Lemma interE S x: x <e (inter S) -> (forall A, A <e S -> x <e A) /\ S <> empty.

Lemma binterI A B x: x <e A -> x <e B -> x <e (binter A B).

Lemma binterE A B x: x <e (binter A B) -> x <e A /\ x <e B.

Lemma union_empty: union empty = empty.

Lemma inter_empty: inter empty = empty.

Lemma repl_empty R: replacement empty R = empty.

Lemma binter_subs1 A B: binter A B c= A.

Lemma binter_subs2 A B: binter A B c= B.

Lemma binter_eq1 A B: binter A B = A -> A c= B.

Lemma binter_eq2 A B: binter A B = B -> B c= A.

Lemma comp_empty A B: A\B = empty <-> A c= B.

Lemma comp_nempty A B: A <> B -> A c= B -> B\A <> empty.

Lemma subs_comp A B: A /c= B -> exists x, x <e A \ B.

Lemma bunion_subs1 A B C: C c= A -> C c= bunion A B.

Lemma bunion_subs2 A B C: C c= B -> C c= bunion A B.

Singletons and Ordered Pairs, Projection and Cartesian Product

Definition singleton A := pair A A.
Definition opair A B := pair (singleton A) (pair A B).
Notation "( x , y )" := (opair x y) (at level 0).

Definition pi1 p := union (inter p).
Definition pi2 p := union (specification (union p) (fun x => x <e inter p -> union p = inter p)).
Definition product A B := union (replacement A (fun a => replacement B (fun b => opair a b))).

Lemma single_el A B: A = B <-> A <e singleton B.

Lemma single_union a: union (singleton a) = a.

Lemma single_inter a: inter (singleton a) = a.

Lemma opair_single a: (a,a) = singleton(singleton a).

Lemma single_opair a b: singleton a <e (a,b).

Lemma opair_intuni a b: union (a,b) = inter (a,b) <-> a = b.

Lemma opair_nempty a b: (a,b) <> empty.

Lemma pi1_subs1 a b: pi1 (a,b) c= a.

Lemma pi1_subs2 a b: a c= pi1 (a,b).

Lemma pi1_cor a b: pi1 (a,b) = a.

Lemma pi2_subs1 a b: pi2 (a,b) c= b.

Lemma pi2_subs2 a b: b c= pi2 (a,b).

Lemma pi2_cor a b: pi2 (a,b) = b.

Lemma opair_eq a a' b b': (a,b) = (a',b') <-> a = a' /\ b = b'.

Lemma product_empty1 B: product empty B = empty.

Lemma product_empty2 A: product A empty = empty.

Lemma product_el A B p: p <e product A B <-> exists a b, a <e A /\ b <e B /\ p = (a,b).

Lemma opair_pi A B a b p: p <e product A B -> a = pi1 p -> b = pi2 p -> p = (a,b).

Lemma product_opair x y A B: x <e A /\ y <e B <-> (x,y) <e product A B.

Lemma product_pi1 A B p: p <e product A B -> pi1 p <e A.

Lemma product_pi2 A B p: p <e product A B -> pi2 p <e B.

Lemma product_pi A B p: p <e product A B -> pi1 p <e A /\ pi2 p <e B.

Lemma product_p A B p: p <e product A B -> p = (pi1 p, pi2 p).

Lemma product_subs1 A A' B: A' c= A -> product A' B c= product A B.

Lemma product_subs2 A B B': B c= B' -> product A B c= product A B'.

Lemma product_subs A A': A' c= A -> product A' A' c= product A A.

Lemma product_monotone A B C D: A c= C -> B c= D -> product A B c= product C D.