Basic set theory formalized in Coq (last modified 2019-08-12 06:15)

set-theory.v

(** Originally written when I was in high school so many things are not ideal here **)
Section Sets.
Variable set : Type.
Variable element : set -> set -> Prop.

Definition subset (x:set) (y:set) :=
  forall z:set, element z x -> element z y.

Axiom equality : forall x y:set, x = y <-> forall z:set, element z x <-> element z y.

Definition empty (x : set) : Prop := forall a, ~(element a x).

Definition proper_subset (x:set) (y:set) :=
  subset x y /\ (not (x = y)) /\ (not (empty x)).


Definition intersect (x:set) (y:set) (z:set) := 
 forall a:set, element a x /\ element a y <-> element a z.

Definition union (x:set) (y:set) (z:set) :=
  forall a:set, element a x \/ element a y <-> element a z.

Definition powerset (x:set) (px:set) :=
  forall y:set, element y px -> subset y x.

Definition universal (q:set) :=
  forall x:set, element x q.

Definition disjoint (x:set) (y:set) :=
  forall z:set, (intersect x y z) -> empty z.

Definition complement (x:set) (x_prime:set) :=
  forall y:set, element y x -> ~(element y x_prime).

Definition partition (x:set) (y:set) (z:set) :=
  disjoint x y /\ union x y z.
(* 
Theorem demorgan1 :
  forall a b ca cb uab cuab ap bp right_hand:set,
    union a b uab /\ complement a ca /\ complement b ca /\
    complement uab cuab /\ intersect ca cb right_hand -> cuab = right_hand.
Proof.
  intros.
  destruct H.
  destruct H0.
  destruct H1.
  unfold complement in *.
  unfold intersect.
  unfold not in *.
  destruct H2.
  intros.
  unfold intersect in H3.
  apply equality.
  split.
  intros.
  apply H3.
  left. *)



Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.
Proof.
  firstorder using equality.
Qed.

Theorem sym_subset_is_antisymmetric :
  forall x y: set, subset x y /\ subset y x -> x = y.
Proof.
  firstorder using equality.
  Show Proof.
Qed.

Theorem subset_is_transitive :
  forall x y z: set, subset x y /\ subset y z -> subset x z.
Proof.
  firstorder.
Qed.

Theorem exercise_4 : forall a b:set, subset a b <-> intersect a b a.
Proof.
  split; firstorder.
Qed.

Theorem union_sym : forall a b c:set, union a b c <-> union b a c.
Proof.
  firstorder using equality.
Qed.

Theorem example_6 : 
  forall a b: set, subset b a <-> union a b a.
Proof.
  firstorder using equality.
  first
Qed.

(* Theorem union_associative : *)
(*   forall a b c d e:set, (union a b d) /\ (union d c e) <-> *)
(*                         (union b c d) /\ (union d a e). *)
(* Proof. *)
(*   firstorder using equality. *)