Require Export Continuum.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_Linear_Relation {A} (R : relation A) :=
  ∀ a1 a2, R a1 a2 ∨ a1 = a2 ∨ R a2 a1.
Existing Class Is_Linear_Relation.

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

Class Well_Order_On (A : Type) :=
  build_well_order {
      well_order_relation : relation A;
      well_order_is_transitive : Transitive well_order_relation;
      well_order_is_irreflexive : Irreflexive well_order_relation;
      well_order_is_linear :> Is_Linear_Relation well_order_relation;
      well_order_is_well_founded :> Is_Well_Founded well_order_relation;
    }.
Arguments build_well_order {_} _ _ _ _ _.
Arguments well_order_relation {_} _.
Arguments well_order_is_transitive {_} _.
Arguments well_order_is_irreflexive {_} _.
Arguments well_order_is_linear {_} _.
Arguments well_order_is_well_founded {_} _.

Coercion well_order_relation : Well_Order_On >-> relation.

Instance well_order_is_strict_order {A} (R : Well_Order_On A) :
  StrictOrder R.
Proof.
  constructor.
  - apply well_order_is_irreflexive.
  - apply well_order_is_transitive.
Qed.

Lemma not_gt_implies_leq {A} (R : 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 well_order_has_least_elements {A : S} (R : Well_Order_On A) :
  ∀ A' : 𝒫 A, inhabited A' → ∃ a : A', ∀ 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' → ∃ a : A', ∀ a' : A', element a ≤ element a')
            _
            (element a0)).
  intros a IH a_in_A'.
  destruct (classic (∃ a' : A', element a' < a)) as [[a' a'_lt_a] | H].
  - apply (IH (element a')). exact a'_lt_a. exact _.
  - ∃ (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 : Well_Order_On A} (A' : 𝒫 A) :
  inhabited A' →
  A'.
Proof.
  intros H.
  refine (δ a : A', ∀ a' : A', (element a : A) ≤ element a').
  destruct (well_order_has_least_elements R A' H) as [a Ha]; cbn in ×.
  ∃ 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.

Definition restrict_well_order {A : S} (R : Well_Order_On A) (A' : 𝒫 A) :
  Well_Order_On A'.
Proof.
  set (R' (x y : A') := (element x : A) < element y).
  simple refine (build_well_order R' _ _ _ _).
  - intros x y z. apply well_order_is_transitive.
  - intros x. apply well_order_is_irreflexive.
  - intros x y. pose (well_order_is_linear R (element x) (element y)) as H.
    rewrite <- element_equality in H. rewrite <- element_equality.
    exact H.
  - intros x.
    set (a := element x : A). assert (H : a ∈ A') by exact _.
    replace x with (element a). {
      generalize a H. clear x a H.
      refine (well_founded_induction R _ _). intros a IH H.
      apply is_accessible_intro. intros a' a'a.
      unfold R' in 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) :=
  ∀ 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.

Lemma in_successor_iff x y :
  x ∈ σ y ↔ x = y ∨ x ∈ y.
Proof. automation. Qed.
Hint Rewrite in_successor_iff.

Inductive Is_Ordinal : S → Prop :=
| successor_is_ordinal x :
    Is_Ordinal x → Is_Ordinal (σ x)
| big_union_is_ordinal (x : S) :
    (∀ y : x, Is_Ordinal y) → Is_Ordinal (big_union x).
Existing Class Is_Ordinal.
Existing Instances successor_is_ordinal big_union_is_ordinal.

Definition Ordinal :=
  {| element_predicate := Is_Ordinal |}.
Instance ordinal_is_ordinal (O : Ordinal) : Is_Ordinal O.
Proof. change (O ∈ Ordinal). exact _. Qed.
Instance ordinal_is_in_Ordinal (x : S) : Is_Ordinal x → x ∈ Ordinal.
Proof. intros H. exact H. Qed.

Notation ordinal_order_relation O :=
  (fun x y : (O : Ordinal) ⇒ x ∈ y)
    (only parsing).

Lemma ordinal_order_irreflexivity O :
  Irreflexive (ordinal_order_relation O).
Proof.
  change (∀ x : O, x ∉ x).
  intros x. apply no_set_contains_itself.
Qed.

Lemma element_of_ordinal_is_subset (x y : S) :
  Is_Ordinal x →
  y ∈ x →
  y ⊆ x.
Proof.
  intros x_is_ordinal. induction x_is_ordinal.
  - rewrite in_successor_iff.
    intros [-> | y_in_x].
    + intros z. automation.
    + specialize (IHx_is_ordinal _).
      intros z z_in_y.
      rewrite in_successor_iff.
      right.
      apply IHx_is_ordinal.
      exact _.
  - rewrite in_big_union_iff.
    intros [z y_in_z].
    specialize (H0 z _).
    intros u u_in_y.
    rewrite in_big_union_iff.
    ∃ z.
    apply H0.
    exact _.
Qed.

Instance element_of_ordinal_is_ordinal (x y : S) :
  Is_Ordinal x →
  y ∈ x →
  Is_Ordinal y.
Proof.
  intros x_is_ordinal. induction x_is_ordinal.
  - rewrite in_successor_iff.
    intros [-> | ?].
    + assumption.
    + apply IHx_is_ordinal.
      assumption.
  - rewrite in_big_union_iff.
    intros [z y_in_z].
    exact (H0 z _).
Qed.

Lemma ordinal_order_transitivity O :
  Transitive (ordinal_order_relation O).
Proof.
  change (∀ x y z : O, x ∈ y → y ∈ z → x ∈ z).
  intros x y z x_in_y y_in_z.
  assert (y ⊆ z). {
    apply element_of_ordinal_is_subset.
    - apply (element_of_ordinal_is_ordinal O); exact _.
    - exact _.
  }
  apply H.
  exact _.
Qed.

Lemma double_induction (R : S → S → Prop) :
  (∀ x y, R x y → R y x → R (σ x) y) →
  (∀ x y : S, (∀ z : x, R z y) → R (big_union x) y) →
  ∀ (x y : Ordinal), R x y.
Proof.
  intros succ_step union_step [x x_ord]. cbn.
  induction x_ord as [x x_ord IHx | x x_elems_ord IHx].
  - intros [y y_ord].
    apply succ_step.
    + apply IHx.
    + cbn.
      induction y_ord as [y y_ord IHy | y y_elems_ord IHy ].
      × apply succ_step.
        -- exact IHy.
        -- change (y ∈ Ordinal) in y_ord.
           apply (IHx (element y)).
      × apply union_step.
        apply IHy.
  - intros [y y_ord].
    apply union_step. intros z.
    apply IHx; exact _.
Qed.

Lemma successor_linearity (x y : Ordinal) :
  x ⊆ y ∨ σ y ⊆ x.
Proof.
  pattern (element_value x), (element_value y).
  apply double_induction; try exact _; clear.
  - intros x y [x_sub_y | succ_y_sub_x] [y_sub_x | succ_x_sub_y].
    + right.
      assert (x = y). {
        apply extensionality; automation.
      }
      automation.
    + left. automation.
    + right. intros z z_in_succ_y. rewrite in_successor_iff.
      right. apply succ_y_sub_x. assumption.
    + left. automation.
  - intros x y IH.
    destruct (classic (∀ z : x, z ⊆ y)) as [H | H].
    + left. intros z z_in_union.
      autorewrite with sets in z_in_union. destruct z_in_union as [u z_in_u].
      apply (H u). assumption.
    + right.
      apply not_all_ex_not in H as [z H].
      destruct (IH z) as [z_sub_y | succ_y_sub_z].
      × contradiction.
      × assert (z ∈ x) by exact _.
        assert (z ⊆ big_union x). {
          intros u u_in_z. rewrite in_big_union_iff. ∃ z. exact u_in_z.
        }
        automation.
Qed.

Lemma ordinal_linearity (x y : Ordinal) :
  x ∈ y ∨ x = y ∨ y ∈ x.
Proof.
  assert (cases : σ x ⊆ y ∨ (x ⊆ y ∧ y ⊆ x) ∨ σ y ⊆ x). {
    pose (successor_linearity x y).
    pose (successor_linearity y x).
    intuition.
  }
  destruct cases as [ | [ | ]].
  - left. apply H. automation.
  - right. left. destruct H. apply element_equality.
    apply extensionality. automation.
  - right. right. apply H. auto.
Qed.

Definition ordinal_order (O : Ordinal) : Well_Order_On O.
Proof.
  simple refine (build_well_order (ordinal_order_relation O) _ _ _ _).
  - apply ordinal_order_transitivity.
  - apply ordinal_order_irreflexivity.
  - intros x y.
    pose (ordinal_linearity (element x) (element y)) as H.
    rewrite <- element_equality in H; cbn in H.
    rewrite <- element_equality.
    exact H.
  - intros [x Hx]. revert x Hx.
    refine (well_founded_induction In_Set _ _).
    intros x IH Hx. apply is_accessible_intro; intros [y Hy] y_in_x.
    cbn in y_in_x. apply IH. exact y_in_x.
Defined.

Lemma isomorphism_from_ordinal_to_element_is_non_decreasing
      (A : Ordinal) (B : A)
      (f : Isomorphism (ordinal_order A)
                       (ordinal_order (element B))) :
  ∀ x : A, f x ∉ x.
Proof.
  intros [u u_in_x]; cbn.
  induction (sets_are_well_founded u) as [u _ IH].
  intros H.
  simple refine (IH (f (element u)) _ _ _).
  - exact _.
  - change (f (element u) ∈ u). exact _.
  - apply (element_of_ordinal_is_subset _ u); exact _.
  - apply (isomorphism_preserves_relation f).
    change (f (element u) ∈ u). exact _.
Qed.


Lemma ordinal_is_not_isomorphic_to_element
      (A B : Ordinal) :
  ordinal_order A ≃ ordinal_order B → B ∉ A.
Proof.
  intros [f] B_in_A.
  assert (f (element B) ∉ B). {
    apply (isomorphism_from_ordinal_to_element_is_non_decreasing
             A (element B) f (element B)).
  }
  apply H. exact _.
Qed.

Lemma isomorphic_ordinals_are_equal (x y : Ordinal) :
  ordinal_order x ≃ ordinal_order y →
  x = y.
Proof.
  intros [f].

  assert (x ∈ y ∨ x = y ∨ y ∈ x)
    by apply (ordinal_linearity x y).

  assert (y ∉ x). {
    apply (ordinal_is_not_isomorphic_to_element x y).
    exact (inhabits f).
  }

  assert (x ∉ y). {
    apply (ordinal_is_not_isomorphic_to_element y x).
    exact (inhabits (isomorphism_inverse f)).
  }

  tauto.
Qed.

Definition Is_Transitive_Set (A : Class) :=
  ∀ x : A, ∀ y : x, y ∈ A.

Lemma transitive_set_of_ordinals_is_ordinal (A : S) :
  (∀ x : A, Is_Ordinal x) →
  Is_Transitive_Set A →
  Is_Ordinal A.
Proof.
  intros elements_are_ordinals transitive.
  replace A with (big_union `{σ x | x in A}). {
    apply big_union_is_ordinal.
    intros [y Hy]; cbn.
    rewrite in_fun_replacement_iff in Hy. destruct Hy as [x ->].
    apply successor_is_ordinal. apply elements_are_ordinals.
  }
  apply extensionality; intros y.
    split.
  - rewrite in_big_union_iff.
    intros [x H].
    assert (Hx : x ∈ `{ σ x | x in A }) by exact _.
    rewrite in_fun_replacement_iff in Hx. destruct Hx as [a Hx].
    rewrite Hx in H.
    rewrite in_successor_iff in H. destruct H as [-> | H].
    + exact _.
    + exact (transitive a (element y)).
  - intros y_in_A.
    rewrite in_big_union_iff.
    assert (σ y ∈ `{ σ x | x in A}). {
      rewrite in_fun_replacement_iff.
      ∃ (element y).
      reflexivity.
    }
    ∃ (element (σ y)). automation.
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. ∃ (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.
  ∃ f.
  unfold Preserves_Relation, transport_relation.
  setoid_rewrite cancel_inverse_left.
  tauto.
Qed.

Definition transport_well_order
           {A B} (f : Bijection A B) (R : Well_Order_On A) :
  Well_Order_On B.
Proof.
  refine (build_well_order (transport_relation f R) _ _ _ _);
    unfold transport_relation.
  - intros x y z. apply transitivity.
  - intros x. unfold complement. apply irreflexivity.
  - 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.