From stdpp Require Import base.
From Coq Require Import Logic.PropExtensionality.

(** * 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.

(** * 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 *)
Instance empty_V : Empty V :=
  sup Empty_set (Empty_set_rect _).