Library hydras.Epsilon0.E0

Class of ordinals less than epsilon0

E0 is a class type for ordinal terms proved to be in normal form.

From Coq Require Import Arith Max Bool Lia Compare_dec Relations Ensembles
ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec.

From hydras Require Import Prelude.More_Arith Prelude.Restriction
Prelude.DecPreOrder ON_Generic OrdNotations.

From hydras.Epsilon0 Require Export T1 Hessenberg.

Set Implicit Arguments.

Create HintDb E0.
Create HintDb E0_rw.

Declare Scope E0_scope.
Delimit Scope E0_scope with e0.
Open Scope E0_scope.

Declare Scope E0_scope.

Class E0 : Type := mkord {cnf : T1; cnf_ok : nf cnf}.

Arguments cnf : clear implicits.

#[export] Hint Resolve cnf_ok : E0.

Lifting functions from T1 to E0

Definition E0lt (alpha beta : E0) := T1.LT (@cnf alpha) (@cnf beta).
Definition E0le := leq E0lt.

Infix "o<" := E0lt : E0_scope.
Infix "o<=" := E0le : E0_scope.

#[export] Instance E0zero : E0 := @mkord zero refl_equal.

#[export] Instance E0_omega : E0 := @mkord T1omega refl_equal.

#[deprecated(note="use E0zero")]
Notation Zero := E0zero (only parsing).

#[deprecated(note="use E0_omega")]
Notation _Omega := E0_omega (only parsing).

#[global, program] Instance E0_succ (alpha : E0) : E0 :=
@mkord (T1.succ (@cnf alpha)) _.

#[deprecated(note="use E0_succ")]
Notation Succ := E0_succ (only parsing).

Definition E0limit (alpha : E0) : bool := T1limit (@cnf alpha).

#[deprecated(note="use E0limit")]
Notation Limitb := E0limit (only parsing).

Definition E0is_succ (alpha : E0) : bool :=
  T1is_succ (@cnf alpha).

#[deprecated(note="use E0is_succ")]
Notation E0succb := E0is_succ (only parsing).

#[global, program] Instance E0one : E0:= @mkord (T1.succ zero) _.

#[global, program] Instance E0add (alpha beta : E0) : E0 :=
  @mkord (T1add (@cnf alpha) (@cnf beta))_ .

Infix "+" := E0add : E0_scope.

#[deprecated(note="use E0add")]
Notation Plus := E0add (only parsing).

Check E0_omega + E0_omega.

#[global, program] Instance E0_phi0 (alpha: E0) : E0 :=
@mkord (T1.phi0 (cnf alpha)) _.

Notation "'E0_omega^'" := E0_phi0 (only parsing) : E0_scope.

#[global, program] Instance Omega_term (alpha: E0) (n: nat) : E0 :=
   @mkord (cons (cnf alpha) n zero) _.

#[global] Instance Cons (alpha : E0) (n: nat) (beta: E0) : E0
  := (Omega_term alpha n + beta)%e0.

#[global, program] Instance E0finS (i:nat) : E0:= @mkord (FS i)%t1 _.

#[global, program] Instance E0fin (i:nat) : E0:=
  match i with
    0 ⇒ E0zero
  | S i ⇒ E0finS i
  end.

#[deprecated(note="use E0fin")]
Notation Fin := E0fin (only parsing).

Coercion E0fin : nat >-> E0.

#[global, program] Instance E0mul (alpha beta : E0) : E0 :=
  @mkord (cnf alpha × cnf beta)%t1 _.

#[deprecated(note="use E0mul")]
Notation Mult := E0mul (only parsing).

Infix "×" := E0mul : E0_scope.

#[global, program] Instance Mult_i (alpha: E0) (n: nat) : E0 :=
  @mkord (cnf alpha × n)%t1 _.

Lemmas

On equality on type E0

Lemma nf_proof_unicity :
  ∀ (alpha:T1) (H H': nf alpha), H = H'.

Lemma E0_eq_intro : ∀ alpha beta : E0,
    cnf alpha = cnf beta → alpha = beta.

Corollary E0_eq_iff (alpha beta: E0) :
  alpha = beta ↔ cnf alpha = cnf beta.

Remark Le_iff : ∀ alpha beta,
    E0le alpha beta ↔ T1.LE (@cnf alpha) (@cnf beta).

Lemma Succb_Succ alpha : E0is_succ alpha → {beta : E0 | alpha = E0_succ beta }.

#[export] Hint Resolve E0_eq_intro : E0.

Ltac orefl := (apply E0_eq_intro; try reflexivity).

Ltac ochange alpha beta := (replace alpha with beta; [| orefl]).

Lemma E0_eq_dec : ∀ alpha beta: E0,
    {alpha = beta }+{alpha ≠ beta }.

Adaptation to E0 of lemmas about T1

Lemma alpha_plus_zero alpha : alpha + E0zero = alpha.

#[export] Hint Rewrite alpha_plus_zero : E0_rw.

Lemma cnf_phi0 (alpha : E0) :
  cnf (E0_phi0 alpha) = T1.phi0 (cnf alpha).

Lemma cnf_Succ (alpha : E0) :
  cnf (E0_succ alpha) = succ (cnf alpha).

Lemma cnf_Omega_term (alpha: E0) (n: nat) :
  cnf (Omega_term alpha n) = omega_term (cnf alpha) n.

Lemma T1limit_Omega_term alpha i : alpha ≠ E0zero →
                                  E0limit (Omega_term alpha i).

Lemma T1limit_phi0 alpha : alpha ≠ E0zero →
                           E0limit (E0_phi0 alpha).

#[export] Hint Resolve T1limit_phi0 : E0.

Definition Zero_Limit_Succ_dec (alpha : E0) :
  {alpha = E0zero } + {E0limit alpha = true } +
  {beta : E0 | alpha = E0_succ beta }.
Defined.

Definition E0_pred (alpha: E0) : E0 :=
  match Zero_Limit_Succ_dec alpha with
      inl _ ⇒ alpha
    | inr (exist _ beta _) ⇒ beta
  end.

Tactic Notation "mko" constr(alpha) := refine (@mkord alpha eq_refl).

#[global] Instance Two : E0 := ltac:(mko (\F 2)).

#[global] Instance Omega_2 : E0 :=ltac:(mko (T1omega × T1omega)%t1).

#[global] Instance E0_sto : StrictOrder E0lt.

#[ global ] Instance compare_E0 : Compare E0 :=
fun (alpha beta:E0) ⇒ compare (cnf alpha) (cnf beta).

Lemma compare_correct (alpha beta : E0) :
  CompSpec eq E0lt alpha beta (compare alpha beta).

Lemma E0lt_wf : well_founded E0lt.

#[export] Hint Resolve E0lt_wf : E0.

Lemma Lt_Succ_Le (alpha beta: E0): beta o < alpha → E0_succ beta o ≤ alpha.

Lemma E0_pred_of_Succ (alpha:E0) : E0_pred (E0_succ alpha) = alpha.

#[export] Hint Rewrite E0_pred_of_Succ: E0_rw.

Lemma Succ_inj alpha beta : E0_succ alpha = E0_succ beta → alpha = beta.

Lemma E0_pred_Lt (alpha : E0) : alpha ≠ E0zero → E0limit alpha = false →
                       E0_pred alpha o < alpha.

#[export] Hint Resolve E0_pred_Lt : E0.

Lemma Succ_Succb (alpha : E0) : E0is_succ (E0_succ alpha).

#[export] Hint Resolve Succ_Succb : E0.

Ltac ord_eq alpha beta := assert (alpha = beta);
      [apply E0_eq_intro ; try reflexivity|].

Lemma FinS_eq i : E0finS i = E0fin (S i).

Lemma mult_fin_rw alpha (i:nat) : alpha × i = Mult_i alpha i.

Lemma FinS_Succ_eq : ∀ i, E0finS i = E0_succ (E0fin i).

#[export] Hint Rewrite FinS_Succ_eq : E0_rw.

Lemma Limit_not_Zero alpha : E0limit alpha → alpha ≠ E0zero.

Lemma Succ_not_Zero alpha: E0is_succ alpha → alpha ≠ E0zero.

Lemma Lt_Succ : ∀ alpha, E0lt alpha (E0_succ alpha).

Lemma Succ_not_T1limit alpha : E0is_succ alpha → ¬ E0limit alpha .

#[export]
  Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_T1limit : E0.

Lemma lt_Succ_inv : ∀ alpha beta, beta o < alpha ↔
                                       E0_succ beta o ≤ alpha.

Lemma lt_Succ_le_2 (alpha beta: E0):
    alpha o < E0_succ beta → alpha o ≤ beta.

Lemma Succ_lt_T1limit alpha beta:
    E0limit alpha → beta o < alpha → E0_succ beta o < alpha.

Lemma le_lt_eq_dec : ∀ alpha beta, alpha o ≤ beta →
                                        {alpha o < beta } + {alpha = beta }.

#[global] Instance E0_comp: Comparable E0lt compare.

#[global] Instance Epsilon0 : ON E0lt compare.

Definition Zero_limit_succ_dec : ZeroLimitSucc_dec .

Qed.

Rewriting lemmas

Lemma Succ_rw : ∀ alpha, cnf (E0_succ alpha) = T1.succ (cnf alpha).

Lemma Plus_rw : ∀ alpha beta, cnf (alpha + beta) =
                                   (cnf alpha + cnf beta)%t1.

Lemma Lt_trans alpha beta gamma :
  alpha o < beta → beta o < gamma → alpha o < gamma.

Lemma Le_trans alpha beta gamma :
  alpha o ≤ beta → beta o ≤ gamma → alpha o ≤ gamma.

Lemma Omega_term_plus alpha beta i :
  alpha ≠ E0zero → (beta o < E0_phi0 alpha)%e0 →
  cnf (Omega_term alpha i + beta)%e0 = cons (cnf alpha) i (cnf beta).

Lemma cnf_Cons (alpha beta: E0) n : alpha ≠ E0zero → beta o < E0_phi0 alpha →
                                     cnf (Cons alpha n beta) =
                                     cons (cnf alpha) n (cnf beta).

Lemma T1limit_plus alpha beta i:
  (beta o < E0_phi0 alpha)%e0 → E0limit beta →
  E0limit (Omega_term alpha i + beta)%e0.

Lemma Succ_of_cons alpha gamma i : alpha ≠ E0zero → gamma o < E0_phi0 alpha →
                                cnf (E0_succ (Omega_term alpha i + gamma)%e0) =
                                cnf (Omega_term alpha i + E0_succ gamma)%e0.

#[global, program] Instance Oplus (alpha beta : E0) : E0 :=
@mkord (oplus (cnf alpha) (cnf beta)) _.

Infix "O+" := Oplus (at level 50, left associativity): E0_scope.

#[global] Instance Oplus_assoc : Assoc eq Oplus.

Lemma oPlus_rw (alpha beta : E0) :
  cnf (alpha O + beta)%e0 = (cnf alpha o + cnf beta)%t1.

Example L_3_plus_omega : 3 + E0_omega = E0_omega.

Lemma succ_correct alpha beta : cnf beta = succ (cnf alpha) ↔
                                Successor beta alpha.

Lemma Le_refl alpha : alpha o ≤ alpha.

Lemma Lt_Le_incl alpha beta : alpha o < beta → alpha o ≤ beta.

Lemma E0_Lt_irrefl (alpha : E0) : ¬ alpha o < alpha.

Lemma E0_Lt_Succ_inv (alpha beta: E0):
  alpha o < E0_succ beta → alpha o < beta ∨ alpha = beta.

Lemma E0_not_Lt_zero alpha : ¬ alpha o < E0zero.

Lemma lt_omega_inv: ∀ alpha:E0, alpha o < E0_omega →
                                      ∃ (i:nat ), alpha = E0fin i.

Lemma E0_lt_eq_lt alpha beta : alpha o < beta ∨ alpha = beta ∨ beta o < alpha.

Lemma E0_lt_ge alpha beta : alpha o < beta ∨ beta o ≤ alpha.

Lemma Limit_gt_Zero (alpha: E0) : E0limit alpha → E0zero o < alpha.

Lemma phi0_mono alpha beta : alpha o < beta → E0_phi0 alpha o < E0_phi0 beta.

#[global] Instance plus_assoc : Assoc eq E0add .

Theorem mult_plus_distr_l (alpha beta gamma: E0) :
  alpha × (beta + gamma ) = alpha × beta + alpha × gamma.

Example Ex42: E0_omega + 42 + E0_omega ^2 = E0_omega ^2.