Require Import HFS.Ordinals.

Section Equipotence.
  Variable X : HF.
  Implicit Types x y z a b c alpha beta : X.

  Inductive epot : X -> X -> Prop :=
  | epot0 : epot 0 0
  | epotA a x b y : a nel x -> b nel y -> epot x y -> epot (a@x) (b@y).

  Notation "x == y" := (epot x y) (at level 70). (* x ≈ y *)

  Lemma epot_empty x:
    x == 0 <-> x = 0.
  Proof.
    split.
    - intros A. inv A; hfs.
    - intros ->. constructor.
  Qed.

  Inductive card: X -> X -> Prop :=
  |card0: card 0 0
  |cardA a x alpha: a nel x -> card x alpha -> card (a@x) (alpha @ alpha).

  Fact card_epot x y :
    card x y -> x == y.
  Proof.
    induction 1; eauto using epot, el_irrefl.
  Qed.

  Fact card_total x :
    Sigma alpha, card x alpha.
  Proof.
    hf_induction x.
    - exists 0. constructor.
    - intros a x _ (alpha&IH).
      decide (a el x) as [-> |A]; eauto using card.
  Qed.

  Fact card_empty alpha :
    card 0 alpha -> alpha = 0.
  Proof.
    intros A. inv A; hfs.
  Qed.

  Fact card_empty' x :
    card x 0 -> x = 0.
  Proof.
    intros A. inv A; hfs.
  Qed.

  Lemma card_adj x alpha :
    card x (alpha @ alpha) -> exists a x', x = a@x' /\ a nel x' /\ card x' alpha.
  Proof.
    intros A. remember (alpha @ alpha) as gamma eqn:E.
    destruct A as [|a x' alpha' B A].
    - hfs.
    - exists a, x'. apply succ_inj in E as ->. auto.
  Qed.

  Fact card_inj x y alpha :
    card x alpha -> card y alpha -> x == y.
  Proof.
    intros A. revert y. induction A as [|a x' alpha A B IH].
    - intros y -> % card_empty'. constructor.
    - intros y C.
      apply card_adj in C as (y'&b&->&D&E);
        eauto using epot.
  Qed.

  Lemma card_wo_inv x a alpha :
    card x alpha -> a el x -> exists beta, alpha = beta @ beta /\ card (x\\a) beta.
  Proof.
    intros A. revert a. induction A as [|a' x' alpha A B IH B].
    - hfs.
    - intros a C.
      enough (card ((a'@x') \\ a) alpha) by eauto.
      apply adj_el_strong in C as [-> |[C D]].
      + now rewrite withoutA_eq, without_nin.
      + rewrite (withoutA_neq _ C). destruct (IH a D) as (beta&->&E).
        constructor.
        * contradict B. rewrite without_el in B. hfs.
        * assumption.
  Qed.

  Fact card_inv x a alpha :
    a nel x -> card (a@x) alpha -> exists beta, alpha = beta @ beta /\ card x beta.
  Proof.
    intros A B.
    assert (a el a@x) as C by hfs.
    destruct (card_wo_inv B C) as (beta&->&D).
    exists beta. rewrite withoutA_eq, without_nin in D; auto.
  Qed.

  Fact card_fun x alpha beta:
    card x alpha -> card x beta -> alpha = beta.
  Proof.
    intros A. revert beta.
    induction A as [|a' x alpha A B IH].
    - now intros alpha -> % card_empty.
    - intros beta C. apply (card_inv A) in C as (gamma&->&C).
      now rewrite (IH _ C).
  Qed.

  Fact card_invariance x y alpha:
    x == y -> card x alpha -> card y alpha.
  Proof.
    intros A. revert alpha.
    induction A as [|a' x alpha y B IH].
    - auto.
    - intros beta C.
      apply card_inv in C as [alpha' [-> C2]]; eauto using card.
  Qed.

  Fact card_ord x y :
    card x y -> ord y.
  Proof.
    induction 1; eauto using ord.
  Qed.

  Fact card_ord_normal alpha :
    ord alpha -> card alpha alpha.
  Proof.
    induction 1; eauto using card, el_irrefl.
  Qed.

  Fact ord_canonical alpha beta:
    ord alpha -> ord beta -> alpha == beta -> alpha = beta.
  Proof.
    intros A B C.
    apply card_fun with (x := beta).
    - apply card_invariance with (x := alpha). exact C.
      now apply card_ord_normal.
    - now apply card_ord_normal.
  Qed.

  Definition Gamma x : X := projT1 (card_total x).

  Fact Gamma_card x :
    card x (Gamma x).
  Proof.
    unfold Gamma. now destruct (card_total x).
  Qed.

  Fact Gamma_ord x:
    ord (Gamma x).
  Proof.
    eapply card_ord, Gamma_card.
  Qed.

  Fact Gamma_coincidence x y :
    x == y <-> Gamma x = Gamma y.
  Proof.
    split.
    - intros A. apply card_fun with (x := y).
      + apply (card_invariance A), Gamma_card.
      + apply Gamma_card.
    - intros A. apply card_inj with (alpha := Gamma x).
      + apply Gamma_card.
      + rewrite A; apply Gamma_card.
  Qed.

  Global Instance epot_Equivalence :
    Equivalence epot.
  Proof.
    split.
    - intros x. now apply Gamma_coincidence.
    - intros x y. rewrite !Gamma_coincidence. congruence.
    - intros x y z. rewrite !Gamma_coincidence. congruence.
  Qed.

  Fact epot_dec x y :
    dec (x == y).
  Proof.
    apply (dec_trans (Gamma x = Gamma y)).
     - now rewrite Gamma_coincidence.
    - auto.
 Qed.

  Fact Gamma_idempotent x :
    Gamma (Gamma x) = Gamma x.
  Proof.
    symmetry. apply Gamma_coincidence.
    apply card_epot, Gamma_card.
  Qed.

  Fact Gamma_equipotence x :
    Gamma x == x.
  Proof.
    apply Gamma_coincidence, Gamma_idempotent.
  Qed.

  Fact Gamma_fixed_point x :
    ord x <-> Gamma x = x.
  Proof.
    split.
    - intros A. apply card_fun with (x := x).
      + apply Gamma_card.
      + apply card_ord_normal, A.
    - intros <-. apply Gamma_ord.
  Qed.

  Corollary ord_dec x :
    dec (ord x).
  Proof.
     apply (dec_trans (Gamma x = x)).
     - now rewrite Gamma_fixed_point.
    - auto.
 Qed.

  Corollary Gamma_range x :
    ord x <-> exists y, Gamma y = x.
  Proof.
    split.
    - intros <- % Gamma_fixed_point. now eexists.
    - intros (y&<-). apply Gamma_ord.
  Qed.

  Corollary Gamma_ord_equiv alpha x:
    ord alpha -> x == alpha <-> Gamma x = alpha.
  Proof.
    rewrite Gamma_coincidence, Gamma_fixed_point.
    intuition congruence.
  Qed.

  Fact Gamma0_eq :
    Gamma 0 = 0.
  Proof.
    apply card_empty, Gamma_card.
  Qed.

  Fact Gamma0_eq' x:
    Gamma x = 0 -> x = 0.
  Proof.
    intros A. apply card_empty'. rewrite <- A. apply Gamma_card.
  Qed.

  Fact GammaS_eq' a x :
    a nel x -> Gamma (a@x) = Gamma x @ Gamma x.
  Proof.
    intros A. eapply card_fun.
    - apply Gamma_card.
    - constructor; auto using Gamma_card.
  Qed.

  Fact GammaS_eq x :
    Gamma (x@x) = Gamma x @ Gamma x.
  Proof.
    apply GammaS_eq'. apply el_irrefl.
  Qed.

  Fact Gamma_strict_incl x y :
    x <<= y -> x <> y -> Gamma x el Gamma y.
  Proof.
    revert y. hf_induction x.
    - intros y _ A. rewrite Gamma0_eq.
      apply ord_eset'. now apply Gamma_ord.
      contradict A. now apply Gamma0_eq' in A.
    - intros a x _ IH y A B.
      decide (a el x) as [C|C].
      + rewrite C in *. now apply IH.
      + apply adj_incl in A as (A&A').
        apply part in A as (y'&-> &A).
        rewrite (GammaS_eq' C), (GammaS_eq' A).
        apply ord_mono. now apply Gamma_ord.
        apply IH; hfs.
  Qed.

  Theorem Gamma_induction (p : X -> Type) :
    (forall x, (forall y, Gamma y el Gamma x -> p y) -> p x) -> forall x, p x.
  Proof.
    intros A x. apply A. revert x.
    enough (forall alpha x, ord alpha -> Gamma x el alpha -> p x) by eauto using Gamma_ord.
    intros alpha. epsilon_induction alpha. intros alpha IH x B C.
    apply A. intros y D. apply (IH (Gamma x)); auto using Gamma_ord.
  Qed.

  Corollary subset_induction (p : X -> Type) :
    (forall x, (forall y, y <<= x -> y <>x -> p y) -> p x) -> forall x, p x.
  Proof.
    intros A. apply Gamma_induction. intros x IH.
    apply A. intros y B C. apply IH.
    now apply Gamma_strict_incl.
  Qed.

End Equipotence.