Require Export Sierpinski.Cardinality.

Require Import Coq.Logic.Classical.

Require Import Coq.Program.Program.
Require Import Coq.Setoids.Setoid.

Definition Less {A} {R : relation A} `{StrictOrder A R} a1 a2 :=
  R a1 a2.
Definition Greater {A} {R : relation A} `{StrictOrder A R} a1 a2 :=
  R a2 a1.
Notation "x < y" := (Less x y).
Notation "x > y" := (Greater x y).

Definition reflexive_closure {A} (R : relation A) : relation A :=
  fun a1 a2 => R a1 a2 \/ a1 = a2.

Instance reflexive_closure_is_pre_order
         {A} (R : relation A) `{StrictOrder A R} :
  PreOrder (reflexive_closure R).
Proof.
  unfold reflexive_closure.
  constructor.
  - intros a. tauto.
  - intros x y z [xy | <-] [yz | <-].
    + left. transitivity y; assumption.
    + left. assumption.
    + left. assumption.
    + right. reflexivity.
Qed.

Instance reflexive_closure_is_partial_order
         {A} (R : relation A) `{StrictOrder A R} :
  PartialOrder eq (reflexive_closure R).
Proof.
  constructor.
  - cbn; unfold flip.
    intros <-. split; reflexivity.
  - cbn; unfold flip. unfold reflexive_closure.
    intros [[xy | xy] [yx | yx]]; try congruence.
    exfalso. apply (asymmetry xy yx).
Qed.

Definition Is_Trichotomous {A} (R : relation A) :=
  forall a1 a2, R a1 a2 \/ a1 = a2 \/ R a2 a1.
Existing Class Is_Trichotomous.

Lemma linearity {A} (R : relation A) `{Is_Trichotomous A R} :
  Is_Trichotomous R.
Proof. assumption. Qed.

Class Strict_Well_Order_On (A : Type) :=
  build_strict_well_order {
      strict_well_order_relation : relation A;
      strict_well_order_is_transitive : Transitive strict_well_order_relation;
      strict_well_order_is_trichotomous :> Is_Trichotomous strict_well_order_relation;
      strict_well_order_is_terminating :> Is_Terminating strict_well_order_relation;
    }.
Arguments build_strict_well_order {_} _ _ _ _.
Arguments strict_well_order_relation {_} _.
Arguments strict_well_order_is_transitive {_} _.
Arguments strict_well_order_is_trichotomous {_} _.
Arguments strict_well_order_is_terminating {_} _.

Coercion strict_well_order_relation : Strict_Well_Order_On >-> relation.

Definition strict_well_order_as_function {A} (R : Strict_Well_Order_On A) :
  A -> A -> Prop :=
  strict_well_order_relation R.
Coercion strict_well_order_as_function : Strict_Well_Order_On >-> Funclass.

Instance strict_well_order_is_strict_order {A} (R : Strict_Well_Order_On A) :
  StrictOrder R.
Proof.
  constructor.
  - intros x x_less_x.
    induction (strict_well_order_is_terminating R x) as [x _ IHx].
    apply (IHx x); assumption.
  - apply strict_well_order_is_transitive.
Qed.

Lemma not_gt_implies_leq {A} (R : Strict_Well_Order_On A) (a1 a2 : A) :
  ~ a1 > a2 -> a1 <= a2.
Proof.
  unfold Greater, Less_Or_Equal, reflexive_closure.
  destruct (linearity R a1 a2); tauto.
Qed.

Lemma strict_well_order_has_least_elements' {A} (R : Strict_Well_Order_On A) :
  forall P : A -> Prop, (exists x, P x) -> exists x, P x /\ forall y, P y -> x <= y.
Proof.
  intros P [x0 Px0]. revert Px0.
  refine (well_founded_induction
            R
            (fun x0 => P x0 -> exists x, P x /\ forall y, P y -> x <= y)
            _
            x0).
  intros x IH Px.
  destruct (classic (exists y, P y /\ y < x)) as [(y & Py & y_x) | H].
  - apply (IH y). exact y_x. exact Py.
  - exists x. split; [exact Px |]. intros y Py. apply not_gt_implies_leq.
    revert Py. apply or_to_imply. apply not_and_or. revert y.
    apply not_ex_all_not. exact H.
Qed.

Lemma strict_well_order_has_least_elements {A : S} (R : Strict_Well_Order_On A) :
  forall A' : 𝒫 A, inhabited A' -> exists a : A', forall a' : A', element a <= element a'.
Proof.
  intros A' [a0].
  assert (a0_in_A' : a0 ∈ A') by exact _.
  revert a0_in_A'.
  refine (well_founded_induction
            R
            (fun a : A => a ∈ A' -> exists a : A', forall a' : A', element a <= element a')
            _
            (element a0)).
  intros a IH a_in_A'.
  destruct (classic (exists a' : A', element a' < a)) as [[a' a'_lt_a] | H].
  - apply (IH (element a')). exact a'_lt_a. exact _.
  - exists (element a). cbn. rewrite strip_element.
    intros a'. apply not_gt_implies_leq.
    apply (not_ex_all_not _ _ H).
Qed.

Definition least_element {A : S} {R : Strict_Well_Order_On A} (A' : 𝒫 A) :
  inhabited A' ->
  A'.
Proof.
  intros H.
  refine (δ a : A', forall a' : A', (element a : A) <= element a').
  destruct (strict_well_order_has_least_elements R A' H) as [a Ha]; cbn in *.
  exists a. split.
  - exact Ha.
  - intros a' Ha'.
    pose (antisymmetry (Ha a') (Ha' a)) as e.
    apply element_equality in e. apply element_equality.
    exact e.
Qed.

Program Definition restrict_well_order {A : Class} (R : Strict_Well_Order_On A)
           (B : Class) `{B ⊆ A} :
  Strict_Well_Order_On B :=
  {| strict_well_order_relation := fun x y : B => R (element x) (element y) |}.
Next Obligation. apply H. exact _. Defined.
Next Obligation. apply H. exact _. Defined.
Next Obligation.
  intros x y z H1 H2. cbn.
  exact (strict_well_order_is_transitive R _ _ _ H1 H2).
Qed.
Next Obligation.
  intros x y.
  epose (strict_well_order_is_trichotomous R (element x) (element y)) as H'.
  rewrite <- element_equality in H'. rewrite <- element_equality. exact H'.
Qed.
Next Obligation.
  intros x.
  assert (H1 : x ∈ A) by (apply H; exact _).
  set (a := element x : A). assert (H2 : a ∈ B) by exact _.
  replace x with (element a). {
    generalize a H2. clear x H1 a H2.
    refine (well_founded_induction R _ _). intros a IH H1.
    apply is_accessible_intro. intros a' a'a.
    cbn in a'a. rewrite strip_element in a'a.
    specialize (IH _ a'a _). cbn in IH. rewrite strip_element in IH.
    exact IH.
  }
  apply element_equality. reflexivity.
Qed.

Definition Preserves_Relation
           {A : Class} (R : relation A)
           {B : Class} (R' : relation B)
           (f : Bijection A B) :=
  forall x y : A, R x y <-> R' (f x) (f y).

Definition Isomorphism
           {A : Class} (R : relation A)
           {B : Class} (R' : relation B) :=
  { f : Bijection A B | Preserves_Relation R R' f }.

Coercion isomorphism_to_bijection
         {A : Class} {R : relation A}
         {B : Class} {R' : relation B}
         (f : Isomorphism R R') : Bijection A B :=
  proj1_sig f.

Lemma isomorphism_preserves_relation
      {A : Class} {R : relation A}
      {B : Class} {R' : relation B}
      (f : Isomorphism R R') (a1 a2 : A) :
  R a1 a2 <-> R' (f a1) (f a2).
Proof.
  destruct f as [f preserving]; cbn.
  apply preserving.
Qed.

Program Definition isomorphism_inverse
        {A : Class} {R : relation A}
        {B : Class} {R' : relation B}
        (f : Isomorphism R R') :
  Isomorphism R' R :=
  f⁻¹.
Next Obligation.
  hnf. intros x y.
  transitivity (R' (f (f⁻¹ x)) (f (f⁻¹ y))). {
    simplify. reflexivity.
  }
  symmetry.
  apply (isomorphism_preserves_relation f (f⁻¹ x) (f⁻¹ y)).
Qed.

Program Definition compose_isos {A B C : Class}
        {R__A : relation A} {R__B : relation B} {R__C : relation C}
        (f1 : Isomorphism R__B R__C) (f2 : Isomorphism R__A R__B) :
  Isomorphism R__A R__C :=
  compose_bijections f1 f2.
Next Obligation.
  unfold Preserves_Relation. cbn.
  intros x y.
  transitivity (R__B (f2 x) (f2 y)).
  apply isomorphism_preserves_relation.
  transitivity (R__C (f1 (f2 x)) (f1 (f2 y))).
  apply isomorphism_preserves_relation.
  reflexivity.
Qed.

Definition isomorphism_relation
           {A : Class} (R : relation A)
           {B : Class} (R' : relation B) :=
  inhabited (Isomorphism R R').
Notation "R ≃ S" := (isomorphism_relation R S) (at level 70).

Lemma isomorphism_relation_reflexivity {A : Class} (R : relation A) :
  R ≃ R.
Proof.
  refine (inhabits (exist _ (id_bijection A) _)).
  intros x y. cbn.
  reflexivity.
Qed.

Lemma isomorphism_relation_transitivity
      {A : Class} (R__A : relation A)
      {B : Class} (R__B : relation B)
      {C : Class} (R__C : relation C) :
  R__A ≃ R__B ->
  R__B ≃ R__C ->
  R__A ≃ R__C.
Proof.
  intros [AB] [BC].
  exact (inhabits (compose_isos BC AB)).
Qed.

Lemma isomorphism_relation_symmetry
      {A : Class} (R__A : relation A)
      {B : Class} (R__B : relation B) :
  R__A ≃ R__B ->
  R__B ≃ R__A.
Proof.
  intros [f].
  exact (inhabits (isomorphism_inverse f)).
Qed.

Definition Is_Transitive_Set (A : S) :=
  forall x y, x ∈ A -> y ∈ x -> y ∈ A.

Inductive Is_Ordinal (α : S) : Prop :=
  transitive_set_of_ordinals_is_ordinal :
    Is_Transitive_Set α ->
    (forall x : α, Is_Ordinal x) ->
    Is_Ordinal α.

Definition O : Class :=
  {| element_predicate := Is_Ordinal |}.

Lemma ordinal_is_transitive (α : O) : Is_Transitive_Set α.
Proof. destruct α as [? [is_transitive ?]]; cbn. exact is_transitive. Qed.

Instance element_of_ordinal_is_ordinal
         {α : S} {H : α ∈ O} (x : S) `{x ∈ α} : x ∈ O.
Proof. destruct H as [_ H]. exact (H (element x)). Qed.

Instance element_relation_on_O_is_well_founded :
  Is_Terminating (fun α β : O => α ∈ β).
Proof.
  intros [x x_in_O]. induction (sets_are_well_founded x) as [x _ IHx].
  apply is_accessible_intro. intros [y y_in_O] y_in_x.
  exact (IHx y y_in_x y_in_O).
Qed.

Program Instance strict_well_order_on_O : Strict_Well_Order_On O :=
  {| strict_well_order_relation := fun x y => x ∈ y |}.
Next Obligation.
  intros α β γ. intros α_in_β β_in_γ.
  apply (ordinal_is_transitive γ β α); assumption.
Qed.
Next Obligation.
  unfold Is_Trichotomous.
  intros α. induction (foundation (fun x y : O => x ∈ y) α) as [α _ IHα].
  intros β. induction (foundation (fun x y : O => x ∈ y) β) as [β _ IHβ].

  assert (α = β \/ α ⊈ β \/ β ⊈ α)
         as [-> | [H | H]]. {
    classical_right. apply not_and_or.
    intros [α_sub_β β_sub_α]. apply H.
    apply element_equality. apply extensionality. automation.
  }

  - tauto.

  - right; right.
    assert (exists ξ : S, ξ ∈ α /\ ξ ∉ β)
      as (ξ & ? & ξ_β). {
      unfold Is_Subclass_Of in H.
      apply not_all_ex_not in H as [ξ H]. exists ξ.
      apply imply_to_and. exact H.
    }
    assert (ξ ∈ β \/ element ξ = β \/ β ∈ ξ)
      as [? | [<- | ?]]
by refine (IHα _ _ _).
    + contradiction ξ_β.
    + exact _.
    + apply (ordinal_is_transitive _ ξ); exact _.

  - left.
    assert (exists ξ : S, ξ ∈ β /\ ξ ∉ α)
      as (ξ & ? & ξ_α). {
      unfold Is_Subclass_Of in H.
      apply not_all_ex_not in H as [ξ H]. exists ξ.
      apply imply_to_and. exact H.
    }
    assert (α ∈ ξ \/ α = element ξ \/ ξ ∈ α)
      as [? | [-> | H']]
by refine (IHβ _ _).
    + apply (ordinal_is_transitive _ ξ); exact _.
    + exact _.
    + contradiction ξ_α.
Qed.

Program Instance strict_well_order_on_ordinal (α : O) : Strict_Well_Order_On α :=
  restrict_well_order strict_well_order_on_O α.
Next Obligation. intros x. apply element_of_ordinal_is_ordinal. Qed.

Definition Has_Least_Elements {A} (R : relation A) : Prop
  := forall P : A -> Prop, (exists a, P a) -> exists a, P a /\ forall a', P a' -> R a a' \/ a = a'.

(* First-order characterisation of strict well-orders *)
Definition Is_Strict_Well_Order' {A} (R : relation A) :=
  Transitive R /\
  Is_Trichotomous R /\
  Has_Least_Elements R.

Lemma strict_well_order_is_strict_well_order' {A} (R : Strict_Well_Order_On A) :
  Is_Strict_Well_Order' R.
Proof.
  split.
  - apply strict_well_order_is_transitive.
  - split.
    + apply strict_well_order_is_trichotomous.
    + intros P.
      apply (strict_well_order_has_least_elements' R).
Qed.

Lemma ordinal_characterisation (A : S) :
  Is_Ordinal A <->
  Is_Transitive_Set A /\
  Is_Strict_Well_Order' (fun x y : A => x ∈ y).
Proof.
  split.
  - intros H. change (A ∈ O) in H. split.
    + exact (ordinal_is_transitive (element A)).
    + change (fun x y : A => x ∈ y)
        with (strict_well_order_on_ordinal (element A) : relation A).
      apply strict_well_order_is_strict_well_order'.
  - intros [transitive_A [transitive_in [trichotomy least_elements]]].
    constructor.
    + exact transitive_A.
    + intros [x0 x0_A]. revert x0_A.
      induction (foundation In_Set x0) as [x _ IH]. intros x_A.
      constructor.
      * intros y z y_x z_y.
        assert (y ∈ A). {
          apply (transitive_A x); exact _.
        }
        assert (z ∈ A). {
          apply (transitive_A y); exact _.
        }
        apply (transitive_in (element z) (element y) (element x)); assumption.
      * intros [y y_x].
        assert (y ∈ A). {
          apply (transitive_A x); exact _.
        }
        exact (IH y y_x _).
Qed.

Instance ordinal_is_transitive' (α : O) : forall (x : α) y, y ∈ x -> y ∈ α.
Proof. intros x y H. apply (ordinal_is_transitive α x); exact _. Qed.

Definition restrict_ordinal_isomorphism {α β : O}
           (f : Isomorphism (fun x y : α => x ∈ y)
                            (fun x y : β => x ∈ y))
           (ξ : α) :
  Isomorphism (fun x y : ξ => x ∈ y)
              (fun x y : f ξ => x ∈ y).
Proof.
  assert (forall x : α, x ∈ ξ -> f x ∈ f ξ)
    by (intros x; apply (isomorphism_preserves_relation f)).
  assert (forall y : β, y ∈ f ξ -> f⁻¹ y ∈ ξ). {
    intros y.
    rewrite (isomorphism_preserves_relation f).
    rewrite cancel_inverse_right. tauto.
  }
  unshelve eexists.
  + refine {| bijection_to_right := fun x : ξ => element (f (element x))
            ; bijection_to_left := fun y : f ξ => element (f⁻¹ (element y))
            |}.
    * cbn. intros x. apply element_equality; cbn.
      rewrite strip_element. rewrite cancel_inverse_left. reflexivity.
    * cbn. intros y. apply element_equality; cbn.
      rewrite strip_element. rewrite cancel_inverse_right. reflexivity.
  + intros x y. cbn.
    exact (isomorphism_preserves_relation f (element x) (element y)).
Qed.

Lemma isomorphic_ordinals_are_equal (α β : O) :
  (fun x y : α => x ∈ y) ≃ (fun x y : β => x ∈ y) ->
  α = β.
Proof.
  intros [f]. apply element_equality.
  revert β f. induction (element_relation_on_O_is_well_founded α) as [α _ IHα].
  intros β. revert α IHα.
  induction (element_relation_on_O_is_well_founded β) as [β _ IHβ].
  intros α IHα f. apply extensionality; intros ξ. split.
  - intros ?.
    rewrite (IHα (element ξ) _ (element (f (element ξ)))).
    + exact _.
    + exact (restrict_ordinal_isomorphism f (element ξ)).
  - intros ξ_in_β.
    set (g := isomorphism_inverse f).
    rewrite <- (IHβ (element ξ) _ (element (g (element ξ)))).
    + exact _.
    + intros α' ? β' f'. apply IHα.
      * exact _.
      * exact f'.
    + exact (isomorphism_inverse (restrict_ordinal_isomorphism g (element ξ))).
Qed.

Notation "A ⊊ B" := (A ⊆ B /\ A <> B) (at level 70).
Lemma ordinal_is_element_iff_strict_sub (α β : O) :
  α ∈ β <-> α ⊊ β.
Proof.
  split.
  - intros α_in_β. split.
    + intros x Hx.
      apply (ordinal_is_transitive β α); assumption.
    + intros.
      intros <-.
      apply (irreflexivity (R := strict_well_order_on_O)) in α_in_β.
      assumption.
  - intros [α_sub_β α_neq_β].
    apply NNPP. intros α_not_in_β.
    destruct (strict_well_order_is_trichotomous strict_well_order_on_O α β) as [H | [<- | H]];
      cbn in *.
    + tauto.
    + tauto.
    + apply α_sub_β in H. apply (irreflexivity (R := strict_well_order_on_O)) in H.
      assumption.
Qed.

Instance empty_set_is_ordinal :
  ∅ ∈ O.
Proof.
  apply transitive_set_of_ordinals_is_ordinal.
  - unfold Is_Transitive_Set. automation.
  - automation.
Qed.

Definition zero_ordinal : O :=
  element ∅.

Instance successor_is_ordinal (α : S) :
  α ∈ O ->
  σ α ∈ O.
Proof.
  intros H.
  apply transitive_set_of_ordinals_is_ordinal.
  - intros x y x_in_succ y_in_x.
    autorewrite with sets in x_in_succ. destruct x_in_succ as [-> | x_in_α].
    + automation.
    + autorewrite with sets. right.
      apply (ordinal_is_transitive (element α) x); assumption.
  - intros [x x_in_succ]; cbn.
    autorewrite with sets in x_in_succ. destruct x_in_succ as [-> | x_in_α].
    + exact H.
    + apply element_of_ordinal_is_ordinal. exact x_in_α.
Qed.

Definition successor_ordinal (α : O) : O :=
  element (σ α).

Instance union_is_ordinal (I : S) (F : I -> S) :
  (forall i, F i ∈ O) ->
  (⋃ i ∈ I, F i) ∈ O.
Proof.
  intros H.
  apply transitive_set_of_ordinals_is_ordinal.
  - intros x y x_in_union y_in_x.
    autorewrite with sets in *.
    destruct x_in_union as [i x_in_F_i].
    exists i. apply (ordinal_is_transitive (element (F i)) x); assumption.
  - intros [x x_in_union]; cbn. autorewrite with sets in x_in_union.
    destruct x_in_union as [i x_in_F_i].
    apply element_of_ordinal_is_ordinal. exact x_in_F_i.
Qed.

Definition ordinal_upper_bound {I : S} (F : I -> O) : O :=
  element (⋃ i ∈ I, F i).

Definition Is_Limit (α : O) :=
  α <> zero_ordinal /\
  ~ exists β, α = successor_ordinal β.

Lemma ordinal_induction (P : O -> Prop) :
  P zero_ordinal ->
  (forall α, P α -> P (successor_ordinal α)) ->
  (forall λ, Is_Limit λ -> (forall α : O, α ∈ λ -> P α) -> P λ) ->
  forall α, P α.
Proof.
  intros zero_case successor_case limit_case α.
  induction (strict_well_order_is_terminating _ α) as [α _ IH]; cbn in IH.
  destruct (classic (Is_Limit α)) as [H | H].
  - apply limit_case.
    + exact H.
    + intros β β_in_α. apply IH. exact β_in_α.
  - unfold Is_Limit in H. apply not_and_or in H. destruct H as [H | H].
    + apply NNPP in H. subst α. apply zero_case.
    + apply NNPP in H. destruct H as [β ->]. apply successor_case.
      apply IH. cbn. autorewrite with sets. left. reflexivity.
Qed.

Definition encodings (A : S) :=
  𝒫 A × 𝒫 (A × A).

Program Definition encode {A} {A' : 𝒫 A} (R : relation A') : encodings A :=
  `(A', element `{ z in A' × A' | R (π1 z) (π2 z) }).
Next Obligation.
  rewrite in_power_set_iff. intros z.
  rewrite in_comprehension_iff. intros [H _].
  change z with (element z : S). rewrite <- (cartesian_product_eta (element z)).
  change (`(π1 (element z), π2 (element z)) : S) with
      (`(element (π1 (element z)) : A, element (π2 (element z)) : A) : S).
  exact _.
Qed.

Definition decode {A} (R : encodings A) : relation (π1 R) :=
  fun x y => `(x, y) ∈ π2 R.
Arguments decode : simpl never.

Lemma decode_encode {A} {A' : 𝒫 A} (R : relation A') :
  decode (encode R) ≃ R.
Proof.
  unfold encode, decode. simplify.
  apply inhabits. exists (id_bijection A').
  intros a1 a2. simplify. reflexivity.
Qed.

Definition transport_relation {A B} (f : Bijection A B) (R : relation A) :
  relation B :=
  fun b1 b2 => R (f⁻¹ b1) (f⁻¹ b2).

Lemma transported_relation_is_isomorphic {A B : Class} (f : Bijection A B) R :
  R ≃ transport_relation f R.
Proof.
  apply inhabits.
  exists f.
  unfold Preserves_Relation, transport_relation.
  setoid_rewrite cancel_inverse_left.
  tauto.
Qed.

Definition transport_strict_well_order
           {A B} (f : Bijection A B) (R : Strict_Well_Order_On A) :
  Strict_Well_Order_On B.
Proof.
  refine (build_strict_well_order (transport_relation f R) _ _ _);
    unfold transport_relation.
  - intros x y z. apply transitivity.
  - intros x y.
    destruct (linearity R (f⁻¹ x) (f⁻¹ y)) as [less | [equal | greater]].
    + tauto.
    + right; left. exact (bijection_is_injective _ _ _ equal).
    + tauto.
  - intros x.
    rewrite <- (cancel_inverse_right f). generalize (f⁻¹ x). clear x.
    refine (well_founded_induction _ _ _). intros a IH.
    apply is_accessible_intro. intros b H.
    rewrite <- (cancel_inverse_right f). apply IH.
    rewrite cancel_inverse_left in H. exact H.
Qed.