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 *)
Fixpoint set_eq (a : V) (b : V) : Prop :=
  match (a, b) with
      (sup A f, sup B g) =>
      (forall (x:A), exists (y: B), (set_eq (f x) (g y)))
      /\ (forall (y:B), exists (x: A), (set_eq (f x) (g y)))
  end.
Instance equiv_V : Equiv V := set_eq.

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

Lemma eq2 : forall x y, 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,  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 equiv_V := eq1.
Instance set_eq_sym : Symmetric equiv_V := eq2.
Instance set_eq_trans : Transitive equiv_V := eq3.
Instance set_eq_equivalence : Equivalence equiv_V.
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 *)

Lemma test1 (a b c : V) :
  a ≡ b →
  b ≡ c →
  a ≡ c.
Proof.
  intros ? H2.
  rewrite <-H2.
  apply H.
Qed.

Lemma test2 (a b c : V) :
  equiv_V a b →
  equiv_V b c →
  equiv_V a c.
Proof.
  intros ? H2.
  Fail rewrite <-H2.
Abort.

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

Instance elem_of_V_proper : Proper ((≡) ==> (≡) ==> (=)) elem_of_V.
Proof. Admitted.

(* Instance elem_of_V_proper : Proper ((=) ==> (≡) ==> (impl)) elem_of_V. *)
(* Proof. *)
(*   intros a a' Ha b b' Hb. *)
(*   apply propositional_extensionality. split. *)
(*   rewrite <-Ha. *)
(*   { 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. unfold equiv. admit. } *)
(*   { intros [y' Hy']. *)
(*     destruct b as [B g]. *)
(*     destruct b' as [B' g']. *)
(*     simpl in *. *)
(*     destruct Hb as [i1 i2]. *)
(*     destruct (i2 y') as [y Hy]. *)
(*     exists y. simpl. symmetry. *)
(*     unfold equiv. *)
(* admit. } *)
(* Admitted. *)

Instance Acc_elem_of_proper : Proper ((≡) ==> (impl)) (Acc elem_of_V).
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. }
  (* TODO: does not work *)
  (* 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 _).