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.
  contradiction (Eset H1).
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).