Library hydras.OrdinalNotations.ON_Omega2

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

Import Relations ON_Generic.

Open Scope ON_scope.


#[ global ] Instance compare_omega2 : Compare ON_mult.t :=
 compare_mult compare_nat compare_nat.

#[ global ] Instance Omega2: ON _ compare_omega2 := ON_mult Omega Omega.

Definition t := ON_t.

Open Scope ON_scope.


Notation omega := (1,0).
Definition zero: t := (0,0).

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


Example ex1 : (5,8) o< (5,10).



Lemma omega_is_limit : Limit omega.


Definition succ (alpha : t) := (fst alpha, S (snd alpha)).


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

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

Lemma le_0 : ∀ p: t, (0,0) o≤ p.


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

Lemma lt_succ alpha : alpha o< succ alpha.



#[global] Hint Constructors clos_refl lexico : O2.
#[global] Hint Unfold lt le : O2.

Lemma compare_reflect alpha beta :
  match (ON_compare alpha beta)
  with
    Lt ⇒ alpha o< beta
  | Eq ⇒ alpha = beta
  | Gt ⇒ beta o< alpha
  end.

Lemma compare_correct alpha beta :
    CompSpec eq ON_lt alpha beta (ON_compare alpha beta).

Lemma zero_le alpha : zero o≤ alpha.

Lemma Least_zero alpha : Least alpha ↔ alpha = zero.

Definition Zero_limit_succ_dec : ZeroLimitSucc_dec.
Defined.

Lemma lt_eq_lt_dec alpha beta :
  {alpha o< beta} + {alpha = beta} + {beta o< alpha}.

Lemma Successor_inv : ∀ i j k l : nat, Successor (k, l) (i, j) →
                                            i = k ∧ l = S j.

Corollary Successor_not (i j k : nat) : ¬ Successor (k,0) (i,j).

Lemma Successor_succ : ∀ alpha, Successor (succ alpha) alpha.


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

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

Definition limitb (alpha : t): bool :=
  match alpha with
    (S _, 0) ⇒ true
  | _ ⇒ false
  end.

Lemma Omega_limit_limitb alpha s : Omega_limit s alpha →
                                   limitb alpha.

Definition canon alpha i :=
  match alpha with
    (0,0) ⇒ (0,0)
  | (_, S p) ⇒ (0,p)
  | (S n, 0) ⇒ (n, i)
  end.

Lemma limitb_limit alpha :
  limitb alpha → Omega_limit (canon alpha) alpha.

 Example Ex1 : limitb omega.


Lemma limit_is_lub_0 : ∀ i alpha, (∀ j, (i,j) o< alpha) ↔
                                 (S i, 0) o≤ alpha.

Lemma limit_is_lub beta :
  limitb beta → ∀ alpha,
    (∀ i, canon beta i o< alpha) ↔ beta o≤ alpha.

 Definition zero_limit_succ_dec :
  ∀ alpha,
                ({alpha = zero} + {limitb alpha }) +
                {beta : t | alpha = succ beta} .

Definition plus (alpha beta : t) : t :=
  match alpha,beta with
  | (0, b), (0, b') ⇒ (0, b + b')
  | (0,0), y ⇒ y
  | x, (0,0) ⇒ x
  | (0, _b), (S n', b') ⇒ (S n', b')
  | (S n, b), (S n', b') ⇒ (S n + S n', b')
  | (S n, b), (0, b') ⇒ (S n, b + b')
   end.

Infix "+" := plus : ON_scope.

Lemma plus_compat (n p: nat) :
  fin (n + p )%nat = fin n + fin p.




Example non_commutativity_of_plus: omega + 3 ≠ 3 + omega.

Definition mult_fin_r (alpha : t) (p : nat): t :=
  match alpha, p with
  | (0,0), _ ⇒ zero
  | _, 0 ⇒ zero
  | (0, n), p ⇒ (0, n × p)
  | (n, b), n' ⇒ ( n × n', b)
  end.
Infix "×" := mult_fin_r : ON_scope.

Definition mult_fin_l (n:nat)(alpha : t) : t :=
  match n, alpha with
  | 0, _ ⇒ zero
  | _, (0,0) ⇒ zero
  | n , (0,n') ⇒ (0, (n×n')%nat)
  | n, (n',p') ⇒ (n', (n × p')%nat)
  end.



Example e1 : (omega × 7 + 15) × 3 = omega × 21 + 15.

Example e2 : mult_fin_l 3 (omega × 7 + 15) = omega × 7 + 45.


#[global] Instance plus_assoc: Assoc eq plus.

Lemma succ_is_plus_1 alpha : alpha + 1 = succ alpha.

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

Lemma decompose (i j : nat): (i,j) = omega × i + j.


Lemma unique_decomposition (alpha: t) :
  ∃! i j: nat, alpha = omega × i + j.

Definition ap (alpha : t) :=
  alpha ≠ zero ∧
  (∀ beta gamma, beta o< alpha → gamma o< alpha →
                       beta + gamma o< alpha).

Lemma omega_ap : ap omega.

Lemma ap_cases alpha : ap alpha → alpha = 1 ∨ alpha = omega.






Open Scope ON_scope.

Example L_3_plus_omega : 3 + omega = omega.


From Equations Require Import Equations.
Section A_def.

Let m (x : nat × nat): t := omega × fst x + snd x.

#[ local ] Instance WF : WellFounded (measure_lt m):=
  wf_measure m.

Equations A (p : nat × nat) : nat by wf p (measure_lt m):=
    A (0, j) := S j;
    A (S i, 0) := A(i, 1);
    A (S i, S j) := A(i, A(S i, j)).


End A_def.