Require Export Prelims Classical.

(* Tactic for proof by contradiction *)

Ltac contra A :=
  match goal with
  |[ |- ?t] => destruct (classic t) as [A|A]; [exact A|exfalso]
  end.

Section Basic.

Context { set : ZFStruct }.
Context { setZF : 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.

Lemma Ext x y :
  x <<= y -> y <<= x -> x = y.
Proof.
  intros H1 H2. now apply ZFExt.
Qed.

Lemma fres_eq F :
  fres equiv F.
Proof.
  now intros x x' -> % ZFExt.
Qed.

Lemma cres_eq P :
  cres equiv P.
Proof.
  now intros x x' -> % ZFExt.
Qed.

Hint Resolve fres_eq cres_eq.
Hint Unfold sub.
Hint Resolve sub_refl.

Lemma WF_sub p :
  p <=p WF.
Proof.
  intros x _. apply AxWF.
Qed.

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.

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.

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.

Lemma pair_el x y z :
  z el upair x y <-> z = x \/ z = y.
Proof.
  rewrite <- !ZFExt. apply Pair.
Qed.

Fact sing_el x y :
  y el sing x <-> y = x.
Proof.
  unfold sing. rewrite pair_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.

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 y z) in H1; auto.
  - intros H y z 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 u (y&H2&H3) % Union H4. apply Union.
  exists y. split. exact H2. now apply (H1 y H2 z).
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.

Lemma sep_el P x z :
  z el sep P x <-> z el x /\ P z.
Proof.
  apply Sep. now intros y y' -> % ZFExt.
Qed.

Lemma frep_el F x z :
  z el frep F x <-> exists y, y el x /\ z = F y.
Proof.
  rewrite Frep.
  - split; intros [y Y]; exists y.
    + now rewrite <- ZFExt.
    + now rewrite ZFExt.
  - now intros y y' -> % ZFExt.
Qed.

Fact sep_sub x p :
  sep p x <<= 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 (sep p x). 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 (sep p x). intros z.
  rewrite sep_el. intuition.
Qed.

Fact subset_outside x :
  exists u, u <<= x /\ u nel x.
Proof.
  pose (u:= sep (fun z => z nel z) x).
  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:= sep (fun z => z nel f z) x).
  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 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 z H1 H2.
  apply Power. apply Power in H1.
  intros u. apply (H z). 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. intros u. now apply H1.
  - intros H1 y H2 H3. now apply Power, H1.
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.

(* Simplification of description axioms *)

Lemma delta_spec (P : set -> Prop) x :
  P x -> unique P -> P (delta P).
Proof.
  intros H1 H2. apply Desc1.
  exists x. intros y. rewrite ZFExt.
  split; intros H.
  - now apply H2.
  - now rewrite H.
Qed.

Fact delta_eq P x :
  unique P -> P x -> delta P = x.
Proof.
  intros H1 H2. apply H1; trivial.
  now apply (delta_spec H2).
Qed.

(* Replacement for relations is defined by separation and functional replacement *)

Definition dom_rep (R : set -> set -> Prop) x :=
  sep (fun a => exists b, R a b) x.

Definition rep R x :=
  frep (fun a => delta (R a)) (dom_rep R x).

Lemma Rep R :
  functional R -> forall x z, z el (rep R x) <-> (exists y, y el x /\ R y z).
Proof.
  intros FR x b. split; intros H.
  - apply frep_el in H as [a[A ->]].
    apply sep_el in A as [A[b B]].
    exists a. split; trivial.
    apply (delta_spec B). firstorder.
  - destruct H as [a[A1 A2]].
    apply frep_el. exists a. split.
    + apply sep_el. split; trivial. now exists b.
    + apply (FR a b (delta (R a)) A2).
      apply (delta_spec A2). firstorder.
Qed.

(* Relational replacement can express unordered pairing *)

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

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 rep_upair x y :
  upair x y = upair' x y.
Proof.
  apply Ext; intros z H.
  - apply upair'_el. now apply pair_el in H.
  - apply Pair. rewrite !ZFExt. now apply upair'_el in H.
Qed.

(* Relational replacement can express separation *)

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

Lemma sep'_el P x z :
  z el sep' P x <-> 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 rep_sep P x :
  sep P x = sep' P x.
Proof.
  apply Ext; intros z H.
  - apply sep'_el. now apply sep_el in H.
  - apply sep_el. now apply sep'_el in H.
Qed.

(* Relational replacement can express functional replacement *)

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

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

Fact rep_frep F x :
  frep F x = frep' F x.
Proof.
  apply Ext; intros z H.
  - apply frep'_el. now apply frep_el in H.
  - apply frep_el. now apply frep'_el in H.
Qed.

(* A transitive class is ZF-closed iff it contains 0 and is closed under union, power and rep *)

Definition closed_rep (U : set -> Prop) :=
  forall R x, functional R -> U x -> rep R x <=c U -> U (rep R x).

Fact Z_rep U :
  closed_Z U -> closed_frep U <-> closed_rep U.
Proof.
  intros UZ. split; intros UR.
  - intros R x FR H1 H2.
    apply UR; trivial.
    apply UZ; trivial.
  - intros F x _ H1 H2. rewrite rep_frep. apply UR; trivial.
    + intros y a b. congruence.
    + intros b [a[A ->]] % frep'_el.
      apply H2. apply frep_el. now exists a.
Qed.

Lemma ZF_rep' U :
  ctrans U /\ U 0 /\ closed_union U /\ closed_power U /\ closed_rep U -> closed_Z U.
Proof.
  intros H. repeat split; try apply H.
  - intros x y X Y. rewrite rep_upair. apply H.
    + apply upair_fun.
    + repeat apply H.
    + now intros z [->| ->] % upair'_el.
  - intros P x _ X. rewrite rep_sep. apply H; trivial.
    + cbv. intuition congruence.
    + intros y [Y _] % sep'_el. now apply H in Y.
Qed.

Fact ZF_rep U :
  closed_ZF U <-> ctrans U /\ U 0 /\ closed_union U /\ closed_power U /\ closed_rep U.
Proof.
  split; intros H.
  - repeat split; try apply H.
    apply Z_rep; apply H.
  - split; try now apply ZF_rep'.
    apply Z_rep; try apply H.
    now apply ZF_rep'.
Qed.

Fact trans_strength n x :
  trans x -> (exists y, y el x /\ strength n y) -> strength n x.
Proof.
  destruct n; cbn; auto.
  intros H1 [y[H2 [u[U1[U2 U3]]]]].
  exists u. split; try now apply (H1 y). now split.
Qed.

Lemma uni_strength u n :
  universe u -> strength n u -> (exists x, x el u /\ strength n x).
Proof.
  intros H1 H2. destruct n.
  - exists 0. split; auto. apply H1.
  - destruct H2 as [u'[U1[U2 U3]]].
    exists (power u'). split; try now apply H1.
    exists u'. split; auto. apply power_eager.
Qed.

Lemma strength_weak n x :
  trans x -> strength (S n) x -> strength n x.
Proof.
  destruct n; cbn; auto.
  intros H [u[U1[U2 [u'[U1' U2']]]]].
  exists u'. split; trivial. now apply (H u).
Qed.

End Basic.

(* Some hints for automation *)

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 Resolve WF_sub.
Hint Resolve fres_eq cres_eq.

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.