From Coq Require Import Relations Classical Classical_sets.
From ZornsLemma Require Import CountableTypes.
From hydras Require Import Well_Orders Lub Countable.

Import Compare_dec Coq.Sets.Image PartialFun MoreEpsilonIota.

Declare Scope schutte_scope.

Set Implicit Arguments.

#[global] Hint Unfold In : schutte.

Delimit Scope schutte_scope with sch.
Open Scope schutte_scope.

Parameter Ord : Type.
Parameter lt : relation Ord.
Infix "<" := lt : schutte_scope.

Notation ordinal := (@Full_set Ord).
Definition big0 alpha : Ensemble Ord := fun beta ⇒ beta < alpha.



#[global] Hint Resolve ordinal_ok : schutte.

Axiom AX1 : WO lt.

#[global] Hint Resolve AX1 : schutte.

#[global] Instance WO_ord : WO lt := AX1.

Axiom inh_Ord : inhabited Ord.

#[ global ] Instance InH_Ord : InH Ord.
#[ global ] Instance Inh_OSets : InH (Ensemble Ord).

#[ global ] Instance Inh_Ord_Ord : InH (Ord → Ord).

#[global] Hint Resolve AX1 Inh_Ord_Ord Inh_OSets inh_Ord : schutte.

Definition le := Le lt.

Infix "≤" := le : schutte_scope.

Axiom AX2 :
  ∀ X: Ensemble Ord,
    (∃ a, (∀ y, In X y → y < a)) →
    Countable X.

Axiom AX3 :
  ∀ X : Ensemble Ord,
    Countable X →
    ∃ a, ∀ y, In X y → y < a.

Definition ge alpha : Ensemble Ord := fun beta ⇒ alpha ≤ beta.

Definition Unbounded (X : Ensemble Ord) :=
  ∀ x: Ord, ∃ y, In X y ∧ x < y.


Definition zero := the_least ordinal.


Definition succ (alpha : Ord)
  := the_least (fun beta ⇒ alpha < beta).

Fixpoint finite (i:nat) : Ord :=
  match i with 0 ⇒ zero
            | S i ⇒ succ (finite i)
  end.

Notation F i := (finite i).

Coercion finite : nat >-> Ord.


Definition is_finite := seq_range finite.

Definition sup_spec X lambda := is_lub ordinal lt X lambda.

Definition sup (X: Ensemble Ord) : Ord := the (sup_spec X).

Notation "'|_|' X" := (sup X) (at level 29) : schutte_scope.

Definition omega_limit (s:nat→Ord) : Ord
  := |_| (seq_range s).

Definition _omega := omega_limit finite.

Notation omega := (_omega).

Definition is_succ (alpha:Ord)
  := ∃ beta, alpha = succ beta.

Definition is_limit (alpha:Ord)
  := alpha ≠ zero ∧ ¬ is_succ alpha.

Definition members (a:Ord) := (fun b ⇒ b < a).

Definition set_eq (X Y: Ord → Prop) := ∀ a, (X a ↔ Y a).

Definition progressive (P : Ord → Prop) : Prop :=
  ∀ a, (∀ b, b < a → P b) → P a.


Definition Closed (B : Ensemble Ord) : Prop :=
  ∀ M, Included M B → Inhabited M → Countable M →
                            In B (|_| M).


Definition continuous (f:Ord→Ord)(A B : Ensemble Ord) : Prop :=
  fun_codomain A B f ∧
  Closed A ∧
  (∀ U, Included U A → Inhabited U →
             Countable U → |_| (image U f) = f (|_| U)).

Lemma Unbounded_not_countable (X: Ensemble Ord) :
    Unbounded X → not (Countable X).

Lemma countable_not_Unbounded : ∀ X,
    Countable X → not (Unbounded X).

Lemma Progressive_Acc: progressive (Acc lt).

Theorem transfinite_induction (P: Ord→Prop) : progressive P →
                                 ∀ a, P a.

Lemma le_refl : ∀ alpha, alpha ≤ alpha.

#[global] Hint Resolve le_refl : schutte.

Lemma eq_le : ∀ a b : Ord, a = b → a ≤ b.

Lemma lt_le : ∀ a b: Ord, a < b → a ≤ b.

Lemma lt_trans : ∀ a b c : Ord, a < b → b < c → a < c.

Lemma le_lt_trans : ∀ a b c, a ≤ b → b < c → a < c.

Lemma lt_le_trans : ∀ a b c, a < b → b ≤ c → a < c.

Lemma le_trans : ∀ a b c, a ≤ b → b ≤ c → a ≤ c.

Lemma lt_irrefl : ∀ a, ¬ (a < a).

Lemma le_antisym : ∀ a b, a ≤ b → b ≤ a → a = b.

Lemma le_eq_or_lt : ∀ a b, a ≤ b → a = b ∨ a < b.

Lemma le_not_gt : ∀ a b, a ≤ b → ¬ b < a.

#[global] Hint Resolve eq_le lt_le lt_trans le_trans le_lt_trans
     lt_le_trans lt_irrefl le_not_gt:
  schutte.

Lemma le_disj : ∀ alpha beta, alpha ≤ beta →
                                   alpha = beta ∨ alpha < beta.

Lemma all_ord_acc : ∀ alpha : Ord, Acc lt alpha.

Lemma trichotomy : ∀ a b : Ord ,
                               a < b ∨ a = b ∨ b < a.


Lemma lt_or_ge : ∀ a b: Ord, a < b ∨ b ≤ a.

Lemma not_gt_le : ∀ a b, ¬ b < a → a ≤ b.

#[global] Hint Unfold Included : schutte.

Theorem Non_denum : ¬ Countable ordinal.

Lemma Inh_ord : Inhabited ordinal.

Theorem unbounded : ∀ alpha, ∃ beta, alpha < beta.

Lemma the_least_ok : ∀ X : Ensemble Ord,
    Inhabited X → ∀ a, In X a → the_least X ≤ a.

Lemma zero_le (alpha : Ord) : zero ≤ alpha.

Lemma not_lt_zero : ∀ alpha, ¬ alpha < zero.

Lemma zero_or_greater : ∀ alpha : Ord,
    alpha = zero ∨ ∃ beta, beta < alpha.

Lemma zero_or_positive : ∀ alpha, alpha = zero ∨ zero < alpha.

Definition succ_spec (alpha:Ord) :=
  least_member lt (fun z ⇒ alpha < z).


Lemma succ_ok :
  ∀ alpha, succ_spec alpha (succ alpha).


Lemma lt_succ (alpha : Ord): alpha < succ alpha.

#[global] Hint Resolve lt_succ : schutte.
Lemma lt_succ_le (alpha beta : Ord):
  alpha < beta → succ alpha ≤ beta.

Lemma lt_succ_le_2 (alpha beta : Ord):
  alpha < succ beta → alpha ≤ beta.
Lemma succ_mono (alpha beta : Ord):
  alpha < beta → succ alpha < succ beta.
Arguments succ_mono [ alpha beta].

Lemma succ_monoR (alpha beta : Ord) :
 succ alpha < succ beta → alpha < beta.
Lemma succ_injection (alpha beta : Ord) :
  succ alpha = succ beta → alpha = beta.
Lemma succ_zero_diff (alpha : Ord): succ alpha ≠ zero.
Lemma zero_lt_succ : ∀ alpha, zero < succ alpha.
Lemma lt_succ_lt (alpha beta : Ord) :
  is_limit beta → alpha < beta → succ alpha < beta.

#[global] Hint Resolve zero_lt_succ zero_le : schutte.

Lemma finite_lt_inv : ∀ i o,
    o < F i →
    ∃ j:nat , (j<i)%nat ∧ o = F j.

Lemma finite_mono : ∀ i j, (i<j)%nat → F i < F j.

#[global] Hint Resolve finite_mono : schutte.

Lemma finite_inj : ∀ i j, F i = F j → i = j.

Lemma sup_exists : ∀ X, Countable X →
                             ex (sup_spec X).

Lemma sup_unicity : ∀ X l l',
                      (Countable X ∧ ∀ x, X x → ordinal x) →
                      sup_spec X l → sup_spec X l' → l = l'.

Lemma sup_spec_unicity (X:Ensemble Ord) (HX : Countable X) :
  ∃! u, sup_spec X u.

Lemma sup_ok1 (X: Ensemble Ord)(HX : Countable X) :
  sup_spec X (sup X).

Lemma sup_upper_bound (X : Ensemble Ord) (alpha : Ord):
  Countable X → In X alpha → alpha ≤ |_| X.

Lemma sup_least_upper_bound (X : Ensemble Ord) (alpha : Ord) :
  Countable X → (∀ y, In X y → y ≤ alpha) → sup X ≤ alpha.

Lemma sup_of_leq (alpha : Ord) :
    alpha = |_| (fun x : Ord ⇒ x ≤ alpha).

Lemma sup_mono (X Y : Ensemble Ord) :
    Countable X →
    Countable Y →
    (∀ x, In X x → ∃ y, In Y y ∧ x ≤ y) →
|_| X ≤ |_| Y.

Lemma sup_eq_intro (X Y : Ensemble Ord):
  Countable X → Countable Y →
  Included X Y → Included Y X →
|_| X = |_| Y.

Lemma lt_sup_exists_leq (X: Ensemble Ord) :
  Countable X →
  ∀ y, y < sup X →
            ∃ x, In X x ∧ y ≤ x.

Lemma lt_sup_exists_lt (X : Ensemble Ord) :
  Countable X →
  ∀ y, y < sup X → ∃ x, In X x ∧ y < x.

Lemma members_eq (alpha beta : Ord) :
  members alpha = members beta → alpha = beta.

Lemma sup_members_succ (alpha : Ord) :
  sup (members alpha) < alpha → alpha = succ (|_| (members alpha)).

Lemma sup_members_not_succ (alpha beta : Ord) :
  alpha = sup (members alpha) → alpha ≠ succ beta.

Definition seq_mono (s:nat → Ord) :=
  ∀ i j, (i < j)%nat → s i < s j.

Lemma seq_mono_intro (s: nat → Ord) :
  (∀ i, s i < s (S i)) → seq_mono s.

Lemma seq_mono_inj (s : nat → Ord) :
  seq_mono s → injective s.

#[global] Hint Resolve Countable.seq_range_countable seq_mono_intro : schutte.

#[global] Hint Constructors Full_set: core.

Lemma lt_omega_limit (s : nat → Ord) :
  seq_mono s → ∀ i, s i < omega_limit s.

Lemma omega_limit_least (s : nat → Ord) :
    seq_mono s →
    ∀ y : Ord,
      (∀ i, s i < y) →
      omega_limit s ≤ y.

Lemma lt_omega_limit_lt_exists_lt (alpha : Ord) (s : nat → Ord) :
  (∀ i, s i < s (S i)) →
  alpha < omega_limit s →
  ∃ j, alpha < s j.

Lemma omega_limit_least_gt (alpha : Ord) (s : nat → Ord)
      (Hmono : ∀ i, s i < s (S i))
      (H : alpha < omega_limit s) :
  ∃ i, least_member Peano.lt (fun j ⇒ alpha < s j) i.

Lemma finite_lt_omega (i : nat) : i < omega.

Lemma zero_lt_omega : zero < omega.

Lemma lt_omega_finite (alpha : Ord) :
  alpha < omega → ∃ i:nat, alpha = i.

Lemma is_limit_omega : is_limit omega.

Lemma not_is_succ_zero : ¬ is_succ zero.

Lemma not_is_limit_zero : ¬ is_limit zero.

Lemma not_is_limit_succ (alpha : Ord) : is_succ alpha → ¬ is_limit alpha.

Lemma not_is_succ_limit (alpha : Ord) : is_limit alpha → ¬ is_succ alpha.

Lemma countable_members (alpha : Ord): Countable (members alpha).

#[global] Hint Resolve countable_members : schutte.

Lemma le_sup_members (alpha : Ord) : |_| (members alpha) ≤ alpha.

Lemma is_limit_sup_members (alpha : Ord) :
  is_limit alpha → alpha = |_| (members alpha).

Lemma sup_members_disj (alpha : Ord) :
  alpha = sup (members alpha) →
  alpha = zero ∨ is_limit alpha.

Theorem classification (alpha : Ord) :
  alpha = zero ∨ is_succ alpha ∨ is_limit alpha.

Lemma members_omega : Same_set (members omega) is_finite.

Lemma Not_Unbounded_bounded (X: Ensemble Ord):
   ¬ Unbounded X →
   ∃ beta : Ord, ∀ x, In X x → x < beta.

Lemma Not_Unbounded_countable (X : Ensemble Ord) :
  ¬ Unbounded X → Countable X.

Lemma not_countable_unbounded (X : Ensemble Ord):
    ¬ Countable X → Unbounded X.

Lemma le_alpha_zero (alpha : Ord) :
  alpha ≤ zero → alpha = zero.

Lemma finite_not_limit (i: nat): ¬ is_limit i.


Definition zero: Ord := iota inh_Ord (least_member lt ordinal).

Lemma zero_le (alpha : Ord) : zero ≤ alpha.

Module Bad.

  Definition bottom := the_least Empty_set.

  Lemma le_zero_bottom : zero ≤ bottom.

  Lemma bottom_eq : bottom = bottom.

  Lemma le_bottom_zero : bottom ≤ zero.
End Bad.

End iota_demo.