Require Export ST.

(* An inner model is a class of sets satisfying the axioms of set theory *)

Section Sub.

  Variable set : SetStruct.
  Variable p : set -> Prop.

  Structure ZF_closed :=
    {
      p_trans : forall x y, y el x -> p x -> p y;
      p_eset : p 0;
      p_union : forall x, p x -> p (union x);
      p_power : forall x, p x -> p (power x);
      p_rep : forall R x, functional R ->
                (forall y z, R y z -> y el x -> p z) ->
                      p x -> p (rep R x);
    }.

  Variable set_ZF : ZF set.
  Variable PC : ZF_closed.

  (* We define the substructure corresponding to p and show that it is a model *)

  Definition P :=
    { x | p x }.

  Fact PI x :
    forall (PX PX' : p x), PX = PX'.
  Proof.
    apply proof_irrelevance.
  Qed.

  Definition embed R x y :=
    exists (PX : p x) (PY : p y), R (exist p x PX) (exist p y PY).

  Definition res (R : set -> set -> Prop) (X Y : P) :=
    R (proj1_sig X) (proj1_sig Y).

  Fact embed_fun R :
    functional R -> functional (embed R).
  Proof.
    intros H x y y' [H1[H2 H3]] [I1[I2 I3]]. rewrite (PI H1 I1) in *.
    specialize (H (exist p x I1) (exist p y H2) (exist p y' I2) H3 I3).
    now apply EqdepFacts.eq_sig_fst in H.
  Qed.

  Fact res_fun R :
    functional R -> functional (res R).
  Proof.
    intros FR [x PX] [y PY] [z PZ] H1 H2.
    unfold res in *; simpl in *.
    specialize (FR x y z H1 H2); subst.
    now rewrite (PI PY PZ).
  Qed.

  Definition pseudo_rep R x :=
    union (sing (rep (embed R) x) ! (fun _ => functional R)).

  Fact pseudo_rep_fun R x :
    functional R -> pseudo_rep R x = rep (embed R) x.
  Proof.
    intros H. unfold pseudo_rep.
    now rewrite sep_true, sing_union.
  Qed.

  Fact pseudo_rep_neg R x :
    ~ functional R -> pseudo_rep R x = 0.
  Proof.
    intros H. unfold pseudo_rep.
    now rewrite sep_false, union_eset.
  Qed.

  Definition IM : SetStruct.
    apply (Build_SetStruct) with (set:=P).
    - intros [x _] [y _]. exact (x el y).
    - exists 0. now apply p_eset.
    - intros [x XP]. exists (union x). now apply p_union.
    - intros [x XP]. exists (power x). now apply p_power.
    - intros R [x XP]. exists (pseudo_rep R x).
      destruct (classic (functional R)).
      + rewrite pseudo_rep_fun; trivial.
        apply p_rep; trivial; try now apply embed_fun.
        now intros y z [_[PZ _]].
      + rewrite pseudo_rep_neg; trivial.
        now apply p_eset.
  Defined.

  Lemma IM_ZF :
    ZF IM.
  Proof.
    split.
    - intros [x PX] [y PY] H1 H2.
      assert (H : x = y).
      + apply Ext; intros z H3.
        * apply (H1 (exist p z (p_trans PC H3 PX)) H3).
        * apply (H2 (exist p z (p_trans PC H3 PY)) H3).
      + subst y. rewrite (PI PY PX). reflexivity.
    - intros [x PX] H. apply (Eset (z:=x)), H.
    - intros [x PX] [y PY]. split; intros H.
      + apply (Union x y) in H as [z[Z1 Z2]].
        now exists (exist p z (p_trans PC Z1 PX)).
      + apply (Union x y). destruct H as [[z PZ] Z]. now exists z.
    - intros [x PX] [y PY]. split; intros H.
      + apply (Power x y) in H. intros [z PZ] Z. apply H, Z.
      + apply (Power x y). intros z Z.
        apply (H (exist p z (p_trans PC Z PY)) Z).
    - intros R FR [x PX] [y PY]. split; intros H.
      + apply Union in H. rewrite sep_true in H; trivial.
        apply Union in H. rewrite sing_union in H.
        apply Rep in H as [z[Z[H1[H2 H3]]]]; try now apply embed_fun.
        exists (exist p z (p_trans PC Z PX)).
        rewrite (PI (p_trans PC Z PX) H1), (PI PY H2). now split.
      + apply Union. rewrite sep_true; trivial.
        apply Union. rewrite sing_union.
        destruct H as [[z PZ][Z1 Z2]].
        apply Rep; try now apply embed_fun. exists z.
        split; trivial. now exists PZ, PY.
    - intros [x PX]. induction (AxWF x) as [x _ IH].
      constructor. intros [y PY] Y. now apply IH.
  Qed.

End Sub.