From stdpp Require Import base.

(** * Cumulative hierarchy *)
Inductive V : Type :=
  sup : forall (A : Set) (f : A -> V), V.

Definition ind (a : V) : Set :=
  match a with
  | sup A f => A
  end.
Definition branch (a : V) : ind a -> V :=
  match a with
  | sup A f => f
  end.

(** * Equality *)
Instance set_eq : Equiv V :=
  fix go a b : Prop :=
  let _ : Equiv V := @go in
  match a, b with
  | sup A f, sup B g =>
     (∀ x:A, ∃ y: B, f x ≡ g y) ∧ (∀ y:B, ∃ x: A, f x ≡ g y)
  end.

Lemma eq1 : forall (x : V), x ≡ x.
Proof.
  intros. induction x.
  split; intros; [exists x | exists y]; apply H.
Qed.

Lemma eq2 : forall (x y : V), x ≡ y -> y ≡ x.
Proof.
  intro x. induction x as [A f IHx].
  intro y. destruct y as [B g].
  intros [F1 F2].
  split; intros.
  (* Case 1 *)
    destruct (F2 x) as [x0 ?].
    exists x0. apply (IHx x0 (g x)). assumption.
  (* Case 2 *)
    destruct (F1 y) as [y0 ?].
    exists y0. apply (IHx y (g y0)). assumption.
Qed.

Lemma eq3 : forall (x y z : V),  x≡y -> y≡z -> x≡z.
Proof.
  intro. induction x as [A f X].
  intro. destruct y as [B g].
  intro. destruct z as [C h].
  intros [P0 P1] [Q0 Q1].
  split; intro.
  - (* Case 1 *)
    destruct (P0 x) as [y L0].
    destruct (Q0 y) as [z L1].
    exists z. apply (X x (g y) (h z)); assumption.
  - (* Case 2 *)
    destruct (Q1 y) as [y0 L0].
    destruct (P1 y0) as [z L1].
    exists z. apply (X z (g y0) (h y)); assumption.
Qed.

Instance set_eq_refl : Reflexive set_eq := eq1.
Instance set_eq_sym : Symmetric set_eq := eq2.
Instance set_eq_trans : Transitive set_eq := eq3.
Instance set_eq_equivalence : Equivalence set_eq.
Proof. split; apply _. Qed.

Lemma set_eq_unfold a b :
  (a ≡ b) =
  ((forall (x:ind a), exists (y: ind b), ((branch a x) ≡ (branch b y)))
/\ (forall (y:ind b), exists (x: ind a), ((branch a x) ≡ (branch b y)))).
Proof.
  destruct a, b; reflexivity.
Qed.

Instance sup_proper A : Proper (((=) ==> (≡)) ==> (≡)) (sup A).
Proof. intros f f' Hf. split; eauto. Qed.

(** * Membership *)
Instance elem_of_V : ElemOf V V := λ (a b : V),
    exists (y : ind b), a ≡ (branch b y).

Instance elem_of_V_proper : Proper ((≡) ==> (≡) ==> (impl)) elem_of_V.
Proof.
  intros a a' Ha b b' Hb.
  intros [y Hy].
  destruct b as [B g].
  destruct b' as [B' g'].
  simpl in *.
  destruct Hb as [i1 i2].
  destruct (i1 y) as [y' Hy'].
  exists y'. simpl. rewrite <- Hy'.
  rewrite <- Ha. apply Hy.
Qed.

(* Here we have to use `elem_of` instead of `elem_of_V` *)
Instance Acc_elem_of_proper : Proper ((≡) ==> (impl)) (Acc (elem_of : V -> V -> Prop)).
Proof.
  intros a a' Ha.
  intros acc.
  revert a' Ha.
  induction acc as [a acc IH].
  intros a' Ha.
  rewrite set_eq_unfold in Ha.
  destruct Ha as [i1 i2].
  constructor. intros x' [y' Hx'].
  eapply IH. 2:{ reflexivity. }
  rewrite Hx'.
  (* erewrite (elem_of_V_proper x' (branch a' y')); eauto. *)
  destruct (i2 y') as [y Hy].
  exists y. symmetry. apply Hy.
Qed.

(** The cumulative hierarchy is well-founded *)
Lemma V_wf : well_founded elem_of_V.
Proof.
  unfold well_founded.
  induction a as [A f IH].
  constructor. intros y [a Hy]. cbn in Hy.
  rewrite Hy.
  apply IH.
Qed.

(** * Set formers *)

(** *** Empty set *)
Instance empty_V : Empty V :=
  sup Empty_set (Empty_set_rect _).

(** *** Singleton *)
Instance singleton_V : Singleton V V := λ x,
  sup unit (λ _, x).

Instance singleton_proper : Proper ((≡) ==> (≡)) (singleton : V → V).
Proof.
  intros x x' Hx.
  unfold singleton, singleton_V. f_equiv.
  intros ??. eauto.
Qed.

(** *** Union *)
Instance union_V : Union V := λ a b,
    match (a, b) with
    | (sup A f, sup B g) =>
      sup (A + B) (λ x, match x with
                        | inl a => f a
                        | inr b => g b
                        end)
    end.

Instance union_proper : Proper ((≡) ==> (≡) ==> (≡)) (union : V → V → V).
Proof.
  intros [A f] [A' f'] [i1 i2] [B g] [B' g'] [j1 j2].
  cbn. split.
  - intros [a|b].
    + destruct (i1 a) as [a' Ha].
      exists (inl a'). assumption.
    + destruct (j1 b) as [b' Hb].
      exists (inr b'). assumption.
  - intros [a|b].
    + destruct (i2 a) as [a' Ha].
      exists (inl a'). assumption.
    + destruct (j2 b) as [b' Hb].
      exists (inr b'). assumption.
Qed.

(** *** Natural numbers *)
Fixpoint delta (n:nat) : V :=
  match n with
    | O => ∅
    | S x => (delta x) ∪ {[ delta x ]}
  end.
Definition NN : V := sup nat delta.

(** * Extensionality *)
Instance subseteq_V : SubsetEq V := λ a b,
  forall x, x ∈ a → x ∈ b.

Instance subseteq_proper : Proper ((≡) ==> (≡) ==> impl) (subseteq : relation V).
Proof.
  intros a a' Ha b b' Hb.
  unfold subseteq, subseteq_V. intros Hs x.
  rewrite <- Ha. rewrite <- Hb. apply Hs.
Qed.

Instance subseteq_reflexive : Reflexive (subseteq : relation V).
Proof. intros ?. unfold subseteq, subseteq_V. auto. Qed.

Instance subseteq_transitive : Transitive (subseteq : relation V).
Proof. intros ???. unfold subseteq, subseteq_V. auto. Qed.

Lemma V_ext (a b : V) :
  a ⊆ b → b ⊆ a → a ≡ b.
Proof.
  destruct a as [A f]. destruct b as [B g].
  intros HAB HBA. split.
  - intros x. apply HAB.
    exists x. reflexivity.
  - intros y.
    assert (g y ∈ sup B g) as Hgy. { exists y. reflexivity. }
    destruct (HBA (g y) Hgy) as [x Hx].
    exists x. symmetry. apply Hx.
Qed.

(** * Axioms *)

(** First, we define a class of set predicates: predicates that respect the equality on V *)
Class SetPredicate (ϕ : V → Prop) :=
  pred_proper :> Proper ((≡) ==> impl) ϕ.

(** Extensionality *)
Theorem CZF_extensionality (a b : V) :
  a ⊆ b ∧ b ⊆ a ↔ a ≡ b.
Proof.
  split.
  - intros [? ?]. apply V_ext; auto.
  - intros ->. split; auto.
Qed.

(** Paring *)
Theorem CZF_pairing (x y : V) :
  forall (w : V), w ∈ ({[x; y]} : V)
                ↔ w ≡ x ∨ w ≡ y.
Proof.
  intros w. split.
  - intros [[?|?] ?]; eauto.
  - intros [Hw|Hw].
    + exists (inl ()). eauto.
    + exists (inr ()). eauto.
Qed.

(** Union *)
(* TODO: need big union operation *)

(** Empty set *)
Theorem CZF_empty :
  forall y, ¬ (y ∈ (∅ : V)).
Proof. intros ? [[] ?]. Qed.

(** Set Induction *)
Theorem CZF_induction ϕ `{SetPredicate ϕ} :
  (forall x, (forall y, y ∈ x → ϕ y) → ϕ x) → (forall x, ϕ x).
Proof.
  intros Hϕ x.
  induction x as [A f IH].
  apply Hϕ.
  intros y [a ->]. apply IH.
Qed.

(** Infinity *)
Definition suc (x : V) := x ∪ {[x]}.
Theorem CZF_infinity :
  ∅ ∈ NN ∧ (forall y, y ∈ NN → suc y ∈ NN).
Proof.
  split.
  - exists 0. reflexivity.
  - intros y [n Hn]. exists (S n).
    unfold suc. rewrite Hn.
    reflexivity.
Qed.

(** Separation *)
Definition sep (a : V) (ϕ : V → Prop) : V.
Proof.
  destruct a as [A f].
  refine (sup (sigT (λ (x:A), ϕ (f x))) _).
  intros [x ?]. exact (f x).
Defined.

(* Note that we have non-restricted separation *)
Theorem CZF_separation a ϕ `{SetPredicate ϕ} :
  forall y, (y ∈ sep a ϕ ↔ y ∈ a ∧ ϕ y).
Proof.
  intros y. destruct a as [A f]. split.
  - intros [[x Hϕ] Hx]. simpl in *.
    rewrite Hx. split; [exists x|]; eauto.
  - intros [[x Hx] Hϕ]. simpl in *.
    rewrite Hx in Hϕ.
    exists (existT x Hϕ). assumption.
Qed.

(** Collection *)
(** Collection holds only if we use types-as-proposition
interpretation, by using Σ-types (landing in Type) instead of ∃
(landing in Prop). Curiously, the predicate ϕ doesn't have to be
proper. *)
Definition coll (a : V) (ϕ : V → V → Prop) :
  (forall (x : V), x ∈ a → { y | ϕ x y }) →
  V.
Proof.
  intros Hϕ.
  destruct a as [A f].
  refine (sup A _).
  intros x.
  assert (f x ∈ sup A f) as Hfx. { exists x; reflexivity. }
  exact (proj1_sig (Hϕ (f x) Hfx)).
Defined.

(* ∀a[∀x∈a ∃y φ(x,y) → ∃b∀x∈a ∃y∈b φ(x,y)]  *)
Theorem CZF_collection (a : V) (ϕ : V → V → Prop)
        `{Proper _ ((≡) ==> (≡) ==> (impl)) ϕ} :
  (forall (x : V), x ∈ a → { y | ϕ x y }) →
  exists (b : V), (forall (x : V), x ∈ a → exists y, y ∈ b ∧ ϕ x y ).
Proof.
  intros Hϕ.
  exists (coll a ϕ Hϕ). intros xx Hxx.
  destruct a as [A f].
  destruct Hxx as [x Hx]. simpl in *.
  set (Hϕ':=Hϕ (f x) (ex_intro (λ y, f x ≡ f y) x (reflexivity _))).
  exists (proj1_sig Hϕ'). split.
  2: { rewrite Hx. apply (proj2_sig Hϕ'). }
  exists x. cbn. reflexivity.
Qed.

Theorem CZF_collection_stong (a : V) (ϕ : V → V → Prop)
        `{Proper _ ((≡) ==> (≡) ==> (impl)) ϕ} :
  (forall (x : V), x ∈ a → { y | ϕ x y }) →
  exists (b : V), (forall (y : V), y ∈ b → exists x, x ∈ a ∧ ϕ x y ).
Proof.
  intros Hϕ.
  exists (coll a ϕ Hϕ). intros yy Hyy.
  destruct a as [A f].
  destruct Hyy as [y Hy]. simpl in *.
  exists (f y). split.
  { exists y. reflexivity. }
  rewrite Hy.
  set (Hϕ':=Hϕ (f y) (ex_intro (λ z, f y ≡ f z) y (reflexivity _))).
  apply (proj2_sig Hϕ').
Qed.