Library hydras.OrdinalNotations.ON_Omega_plus_omega

From Coq Require Import Arith Compare_dec Lia.
From hydras Require Import Comparable Simple_LexProd ON_Generic
        ON_plus ON_Omega Compat815.

Import Relations.
Declare Scope opo_scope.
Delimit Scope opo_scope with opo.
Open Scope ON_scope.
Open Scope opo_scope.


#[global] Instance compare_nat_nat : Compare t :=
 compare_plus compare_nat compare_nat.

#[global] Instance Omega_plus_Omega: ON _ compare_nat_nat :=
 ON_plus Omega Omega.

Definition t := ON_t.


Example ex1 : inl 7 o< inr 8.


Open Scope opo_scope.

Definition fin (i:nat) : t := inl i.
Coercion fin : nat >-> t.

Notation omega := (inr 0:ON_t).


Example ex2 : inl 7 o< omega.

Lemma omega_is_limit : Limit omega.

Lemma limit_is_omega alpha : Limit alpha → alpha = omega.


Lemma limit_iff (alpha : t) : Limit alpha ↔ alpha = omega.
Lemma Successor_inv1 : ∀ i j, Successor (inl j) (inl i) → j = S i.

Lemma Successor_inv2 : ∀ i j, Successor (inr j) (inr i) → j = S i.

Lemma Successor_inv3 : ∀ i j, ¬ Successor (inr j) (inl i).

Lemma Successor_inv4 : ∀ i j, ¬ Successor (inl j) (inr i).


Definition succ (alpha : t) :=
  match alpha with
    inl n ⇒ inl (S n)
  | inr n ⇒ inr (S n)
  end.


Lemma Successor_succ alpha : Successor (succ alpha) alpha.


Lemma succ_correct alpha beta :
  Successor beta alpha ↔ beta = succ alpha.


Definition succb (alpha: t) : bool
  := match alpha with
     | inr (S _) | inl (S _) ⇒ true
     | _ ⇒ false
     end.

Lemma succb_correct (alpha: t) :
  succb alpha ↔ ∃ beta: t, alpha = succ beta.

Lemma omega_not_succ : ∀ alpha, ¬ Successor omega alpha.

Lemma Least_is_0 (alpha:t) : Least alpha ↔ alpha = 0.

Lemma ZLS_dec (alpha : t) :
  {alpha = 0} +
  {Limit alpha} +
  {beta : t | Successor alpha beta}.


Definition Zero_limit_succ_dec : ON_Generic.ZeroLimitSucc_dec.

Definition limitb (alpha: t) := match ON_compare alpha omega
                                with Eq ⇒ true | _ ⇒ false end.

Lemma eq_dec (alpha beta: t) : {alpha = beta} + {alpha ≠ beta}.

Lemma le_introl :
  ∀ i j :nat, (i≤ j)%nat → inl i o≤ inl j.

Lemma le_intror :
  ∀ i j :nat, (i≤ j)%nat → inr i o≤ inr j.

Lemma le_0 : ∀ p: t, fin 0 o≤ p.

Lemma le_lt_trans : ∀ p q r, p o≤ q → q o< r → p o< r.

Lemma lt_le_trans : ∀ p q r, p o< q → q o≤ r → p o< r.

Lemma lt_succ_le alpha beta : alpha o< beta ↔ succ alpha o≤ beta.

Lemma lt_succ alpha : alpha o< succ alpha.

Lemma lt_omega alpha :
  alpha o< omega ↔ ∃ n:nat, alpha = fin n.

Lemma Omega_as_lub :
   ∀ alpha,
     (∀ i, fin i o< alpha) ↔ omega o≤ alpha.


 #[global] Instance Incl : SubON Omega Omega_plus_Omega omega fin.

Section NotIncl.
  Context (i : nat)
          (f : t → nat)
          (Hyp : SubON Omega_plus_Omega Omega i f).

  Remark R1: ∀ n: nat, ¬ Limit n.

Lemma ExNotIncl: False.

End NotIncl.