# Basic Library for ZF

Require Export Model.

Section Basic.

## We assume a model of ZF

Context { set : SetStruct }.
Context { ZFS : ZF set }.

Implicit Types x y z a b c u v : set.
Implicit Types p q : set -> Prop.

Fact class_not_sub p q :
~ p <=p q -> exists x, p x /\ ~ q x.
Proof.
intros H1. contra H2. apply H1.
intros x X. contra H3. apply H2. now exists x.
Qed.

Fact set_not_sub x y :
~ x <<= y -> exists z, z el x /\ z nel y.
Proof.
intros H1. contra H2. apply H1.
intros z Z. contra H3. apply H2. now exists z.
Qed.

Lemma sub_refl x :
x <<= x.
Proof.
unfold sub. auto.
Qed.

Lemma sub_trans x y z :
x <<= y -> y <<= z -> x <<= z.
Proof.
unfold sub. auto.
Qed.

Hint Unfold sub.
Hint Resolve sub_refl.

## Well-founded sets

Lemma WF_no_loop x :
x el x -> False.
Proof.
induction (AxWF x) as [x _ IH]. eauto.
Qed.

Lemma WF_no_loop2 x y :
y el x -> x el y -> False.
Proof.
revert y. induction (AxWF x) as [x _ IH]. eauto.
Qed.

Lemma WF_no_loop3 x y z :
z el y -> y el x -> x el z -> False.
Proof.
revert y z. induction (AxWF x) as [x _ IH]. eauto.
Qed.

## Least sets

Definition least p x := p x /\ forall y, p y -> x <<= y.
Definition unique p := forall x y, p x -> p y -> x = y.

Fact least_unique p :
unique (least p).
Proof.
intros x y [H1 H2] [H3 H4]. apply Ext; firstorder.
Qed.

Fact agree_unique p :
unique (agree p).
Proof.
intros a b H1 H2. apply Ext; intros x.
- intros H3 % H1 % H2. exact H3.
- intros H3 % H2 % H1. exact H3.
Qed.

## Empty set

Lemma eset_sub x :
0 <<= x.
Proof.
intros z H. exfalso. eapply Eset, H.
Qed.

Lemma eset_unique x :
(forall z, z nel x) -> x = 0.
Proof.
intros H. apply Ext.
- intros z H1. contradiction (H z H1).
- apply eset_sub.
Qed.

Lemma sub_eset x :
x <<= 0 -> x = 0.
Proof.
intros H. apply eset_unique. intros z H1 % H.
Qed.

Hint Resolve eset_sub sub_eset.

Hint Extern 4 =>
match goal with
| [ H : _ el 0 |- _ ] => exfalso; apply (Eset H)
end.

Lemma inhab_not x :
~ inhab x <-> x = 0.
Proof.
split.
- intros H. apply eset_unique. intros z H1. firstorder.
- intros -> [z H]. eauto.
Qed.

Lemma inhab_neq x :
inhab x -> x <> 0.
Proof.
intros [z H] ->. eauto.
Qed.

Hint Resolve inhab_neq.

Hint Extern 4 =>
match goal with
| [ H : inhab 0 |- _ ] => exfalso; now apply (inhab_neq H)
end.

## Unordered Pair

Definition upair x y :=
rep (fun a b => (a = 0 /\ b = x) \/ (a = power 0 /\ b = y)) (power (power (0))).

Definition sing x :=
upair x x.

Lemma upair_fun x y :
functional (fun a b : set => a = 0 /\ b = x \/ a = power 0 /\ b = y).
Proof.
intros a b c [[H1 H2]|[H1 H2]] [[I1 I2]|[I1 I2]]; subst; auto.
- symmetry in I1. apply inhab_not in I1. contradict I1.
exists 0. now apply Power.
- apply inhab_not in I1. contradict I1.
exists 0. now apply Power.
Qed.

Lemma upair_el x y z :
z el upair x y <-> z = x \/ z = y.
Proof with eauto using upair_fun.
split; intros H.
- apply Rep in H as [a [_ [[_ A]|[_ A]]]]...
- apply Rep... destruct H as [<-|<-].
+ exists 0. split... apply Power...
+ exists (power 0). split... apply Power...
Qed.

Fact sing_el x y :
y el sing x <-> y = x.
Proof.
unfold sing. rewrite upair_el. tauto.
Qed.

Fact sing_union x :
union (sing x) = x.
Proof.
apply Ext; intros y Y.
- now apply Union in Y as [z[<- % sing_el H]].
- apply Union. exists x. split; trivial.
now apply sing_el.
Qed.

## Union

Fact union_el_sub x y :
x el y -> x <<= union y.
Proof.
intros H z H1. apply Union. eauto.
Qed.

Lemma union_sub x u :
upbnd x u -> union x <<= u.
Proof.
intros H z [y [H1 H2]] % Union.
now apply (H y).
Qed.

Hint Resolve union_el_sub union_sub.

Fact union_trans_sub x :
trans x <-> union x <<= x.
Proof.
split.
- intros H z (y&H1&H2) % Union. apply H in H1. auto.
- intros H y H1 % union_el_sub. auto.
Qed.

Lemma union_mono x y :
x <<= y -> union x <<= union y.
Proof.
auto.
Qed.

Lemma union_lub u x :
union x = u <-> upbnd x u /\ forall v, upbnd x v -> u <<= v.
Proof.
split.
- intros <-. split.
+ intros z. apply union_el_sub.
+ apply union_sub.
- intros [H1 H2]. apply Ext.
+ apply union_sub, H1.
+ apply H2. intros z. apply union_el_sub.
Qed.

Fact union_gel x :
union x el x -> gel x (union x).
Proof.
auto.
Qed.

Fact union_gel_eq x u :
gel x u -> union x = u.
Proof.
intros [H1 H2]. apply union_lub; auto.
Qed.

Lemma union_eset :
union 0 = 0.
Proof.
apply union_lub. auto.
Qed.

Fact union_trans x :
x <=c trans -> trans (union x).
Proof.
intros H1 z (y&H2&H3) % Union u H4. apply Union.
exists y. split. exact H2. revert u H4. apply (H1 y H2), H3.
Qed.

Lemma union_sub_el_sub x y z :
x <<= y -> y el z -> x <<= union z.
Proof.
intros H I a A. apply Union. exists y. split; auto.
Qed.

## Replacement and Separation

Definition frep f x := rep (fun a b => f a = b) x.

Lemma frep_el f x z :
z el frep f x <-> exists y, y el x /\ f y = z.
Proof.
unfold frep. rewrite Rep. reflexivity.
clear x z. intros x a b. congruence.
Qed.

Definition sep x p :=
rep (fun z y => p z /\ z = y) x.

Notation "x ! p" := (sep x p) (at level 59, left associativity).

Lemma sep_el x p z :
z el x!p <-> z el x /\ p z.
Proof.
unfold sep. rewrite Rep.
- split.
+ intros (y&H1&H2&<-). auto.
+ intros (H1&H2); eauto.
- cbv. intuition congruence.
Qed.

Fact sep_sub x p :
x!p <<= x.
Proof.
intros y (H&_) % sep_el. exact H.
Qed.

Fact small_red p q :
p <=p q -> small q -> small p.
Proof.
intros H [x H1]. exists (x!p). intros z.
rewrite sep_el. split. tauto.
intros H2. split. apply H1, H, H2. exact H2.
Qed.

Fact bounded_small p x :
p <=s x -> small p.
Proof.
intros H. exists (x ! p). intros z.
rewrite sep_el. intuition.
Qed.

Fact subset_outside x :
exists u, u <<= x /\ u nel x.
Proof.
pose (u:= x ! (fun z => z nel z)).
assert (u <<= x) as H by apply sep_sub.
exists u. split. exact H. intros H1.
enough (u el u <-> u nel u) by tauto.
split.
+ intros H2 % sep_el. tauto.
+ intros H2. apply sep_el. auto.
Qed.

Fact Cantor f x :
exists u, u <<= x /\ u nel frep f x.
Proof.
pose (u:= x ! (fun z => z nel f z)).
exists u. split. now apply sep_sub.
intros (y&H1&H2) % frep_el.
enough (y el u <-> y nel u) by tauto.
split.
- intros [H3 H4] % sep_el. congruence.
- intros H3. apply sep_el.
split. exact H1. congruence.
Qed.

Fact sep_true x p :
(forall x, p x) -> x ! p = x.
Proof.
intros H. apply Ext; try apply sep_sub.
intros y Y. apply sep_el. split; auto.
Qed.

Fact sep_false x p :
(forall x, ~ p x) -> x ! p = 0.
Proof.
intros H. apply eset_unique.
intros y [_ Y] % sep_el. apply (H y Y).
Qed.

## Description

Definition delta p := union (rep (fun x y => p y) (upair 0 0)).

Fact delta_eq p x :
unique p -> p x -> delta p = x.
Proof.
intros H1 H2. apply union_lub. split.
- intros y (z&H3&H4) % Rep.
+ rewrite (H1 y x); auto.
+ intros z. exact H1.
- intros u H3. apply H3. apply Rep.
+ hnf. eauto.
+ exists 0. split; trivial. apply upair_el; auto.
Qed.

Fact delta_spec x (p : set -> Prop) :
p x -> unique p -> p (delta p).
Proof.
intros H I. now rewrite (delta_eq I H).
Qed.

## Power

Fact power_eager x :
x el power x.
Proof.
apply Power; auto.
Qed.

Fact power_trans x :
trans x -> trans (power x).
Proof.
intros H y H1 z H2.
apply Power. rewrite Power in H1.
apply H. auto.
Qed.

Fact power_WF x :
WF x -> WF (power x).
Proof.
intros [H]. constructor. intros y H1.
rewrite Power in H1.
constructor. auto.
Qed.

Fact power_mono x y :
x <<= y -> power x <<= power y.
Proof.
intros H1 z H2 % Power. apply Power. auto.
Qed.

Fact union_power_eq x :
union (power x) = x.
Proof.
apply union_lub. split.
- intros y H % Power. exact H.
- intros y H. apply H, power_eager.
Qed.

Fact power_inj x y :
power x = power y -> x = y.
Proof.
intros H.
rewrite <- (union_power_eq x), H.
apply union_power_eq.
Qed.

Fact trans_power x :
trans x <-> x <<= power x.
Proof.
split.
- intros H1 y H2. apply Power, H1, H2.
- intros H1 y H2. apply Power. auto.
Qed.

Fact power_above x :
~ power x <<= x.
Proof.
intros H.
destruct (subset_outside x) as (u&H1&H2).
apply H2, H. apply Power, H1.
Qed.

End Basic.

Hint Unfold sub.
Hint Resolve sub_refl.
Hint Resolve eset_sub sub_eset.
Hint Resolve inhab_neq.
Hint Resolve union_el_sub union_sub.

Hint Extern 4 =>
match goal with
| [ H : _ el 0 |- _ ] => exfalso; apply (Eset H)
end.

Hint Extern 4 =>
match goal with
| [ H : inhab 0 |- _ ] => exfalso; now apply (inhab_neq H)
end.

Notation "x ! p" := (sep x p) (at level 59, left associativity).