Library hydras.OrdinalNotations.OmegaOmega
From hydras Require Import T1 E0 Comparable.
From Coq Require Import Arith Logic.Eqdep_dec Peano_dec
List Bool
Recdef Lia Wellfounded.Inverse_Image
Wellfounded.Inclusion RelationClasses .
omega^ i * S n + alpha
Finite ordinals
Notation FS n := (cons 0 n zero: t).
Definition fin (n:nat): t := match n with 0 ⇒ zero | S p ⇒ FS p end.
Coercion fin : nat >-> t.
omega ^i
data refinement
Fixpoint refine (a : t) : T1.T1 :=
match a with
nil ⇒ T1.zero
| cons i n b ⇒ T1.cons (\F i)%t1 n (refine b)
end.
Inductive ap : t → Prop :=
ap_intro : ∀ a, ap (phi0 a).
Successor and limits (syntactic definitions)
Fixpoint succb (a : t) :=
match a with
nil ⇒ false
| cons 0 _ _ ⇒ true
| cons _ _ b ⇒ succb b
end.
Fixpoint limitb (a : t) :=
match a with
nil ⇒ false
| cons 0 _ _ ⇒ false
| cons _ _ nil ⇒ true
| cons _ _ b ⇒ limitb b
end.
Lemma succb_ref (a:t): succb a → T1is_succ (refine a).
Lemma limitb_ref (a:t): limitb a → T1limit (refine a).
#[ global ] Instance compare_oo : Compare t :=
fix cmp (a b : t) :=
match a, b with
| nil, nil ⇒ Eq
| nil, cons a' n' b' ⇒ Datatypes.Lt
| _ , nil ⇒ Gt
| (cons a n b),(cons a' n' b') ⇒
(match Nat.compare a a' with
| Datatypes.Lt ⇒ Datatypes.Lt
| Gt ⇒ Gt
| Eq ⇒ (match Nat.compare n n' with
| Eq ⇒ cmp b b'
| comp ⇒ comp
end)
end)
end.
Lemma compare_ref (a b : t) :
compare a b = compare (refine a) (refine b).
Definition lt (a b : t) : Prop :=
compare a b = Datatypes.Lt.
Lemma compare_rev :
∀ (a b : t),
compare b a = CompOpp (compare a b).
Lemma compare_reflect :
∀ a b,
match compare a b with
| Datatypes.Lt ⇒ lt a b
| Eq ⇒ a = b
| Gt ⇒ lt b a
end.
Lemma compare_correct (a b: t):
CompSpec eq lt a b (compare a b).
Lemma lt_ref (a b : t) :
lt a b ↔ T1.lt (refine a) (refine b).
Lemma eq_ref (a b : t) : a = b ↔ refine a = refine b.
Lemma lt_irrefl (a : t): ¬ lt a a.
Lemma lt_trans (a b c : t): lt a b → lt b c → lt a c.
#[global] Instance lo_strorder: StrictOrder lt.
#[global] Instance lo_comparable : Comparable lt compare.
Fixpoint nf_b (alpha : t) : bool :=
match alpha with
| nil ⇒ true
| cons a n nil ⇒ true
| cons a n ((cons a' n' b') as b) ⇒
(nf_b b && Nat.ltb a' a)%bool
end.
Definition nf alpha :Prop := nf_b alpha.
refinements of T1's lemmas
Lemma zero_nf : nf zero.
Lemma fin_nf (i:nat) : nf (fin i).
Lemma single_nf :
∀ i n, nf (cons i n zero).
Lemma cons_nf :
∀ i n j n' b,
Nat.lt j i →
nf(cons j n' b)→
nf(cons i n (cons j n' b)).
#[local] Hint Resolve zero_nf single_nf cons_nf : core.
Lemma nf_inv2 :
∀ i n b, nf (cons i n b) → nf b.
Lemma nf_inv3 :
∀ i n j n' b',
nf (cons i n (cons j n' b')) → Nat.lt j i.
Lemma nf_ref: ∀ a, T1.nf (refine a) ↔ nf a.
Declare Scope lo_scope.
Delimit Scope lo_scope with lo.
Open Scope lo_scope.
Fixpoint succ (a : t) : t :=
match a with
| nil ⇒ fin 1
| cons 0 n _ ⇒ cons 0 (S n) nil
| cons a n b ⇒ cons a n (succ b)
end.
Fixpoint plus (a b : t) :t :=
match a, b with
| nil, y ⇒ y
| x, nil ⇒ x
| cons a n b, cons a' n' b' ⇒
(match Nat.compare a a' with
| Datatypes.Lt ⇒ cons a' n' b'
| Gt ⇒ (cons a n (plus b (cons a' n' b')))
| Eq ⇒ (cons a (S (n+n')) b')
end)
end
where "a + b" := (plus a b) : lo_scope.
Fixpoint mult (a b : t) : t :=
match a, b with
| nil, _ ⇒ zero
| _, nil ⇒ zero
| cons 0 n _, cons 0 n' b' ⇒
cons 0 (Peano.pred((S n) × (S n'))) b'
| cons a n b, cons 0 n' _ ⇒
cons a (Peano.pred ((S n) × (S n'))) b
| cons a n b, cons a' n' b' ⇒
cons (a + a')%nat n' ((cons a n b) × b')
end
where "a * b" := (mult a b) : lo_scope.
Lemma phi0_ref (i:nat) : refine (phi0 i) = T1.phi0 (\F i).
Lemma phi0_nf (i:nat) : nf (phi0 i).
Lemma succ_ref (alpha : t) :
refine (succ alpha) = T1.succ (refine alpha).
Lemma succ_nf alpha : nf alpha → nf (succ alpha).
Lemma plus_ref : ∀ alpha beta: t,
refine (alpha + beta) = T1.T1add (refine alpha) (refine beta).
Lemma plus_nf alpha beta : nf alpha → nf beta → nf (alpha + beta).
Lemma mult_ref : ∀ alpha beta: t,
refine (alpha × beta) =
T1.T1mul (refine alpha) (refine beta).
Lemma mult_nf alpha beta : nf alpha → nf beta → nf (alpha × beta).
#[global] Instance plus_assoc: Assoc eq plus.
Lemma mult_plus_distr_l (a b c: t) : nf a → nf b → nf c →
a × (b + c) = a × b + a × c.
End LO.
Declare Scope OO_scope.
Delimit Scope OO_scope with oo.
Open Scope OO_scope.
Import LO.
Module OO.
Class OO : Type := mkord {data: LO.t ; data_ok : LO.nf data}.
Arguments data : clear implicits.
#[local] Hint Resolve data_ok : core.
Definition lt (alpha beta: OO) := LO.lt (data alpha) (data beta).
Definition le := leq lt.
#[ global ] Instance compare_OO : Compare OO :=
fun (alpha beta: OO) ⇒ LO.compare_oo (data alpha) (data beta).
#[ global ] Instance Zero : OO := @mkord nil refl_equal.
#[ global ] Instance _Omega : OO.
#[ global ] Instance Fin (i:nat) : OO.
Notation omega := _Omega.
#[ global ] Instance Succ (alpha : OO) : OO.
#[ global ] Instance plus (alpha beta : OO) : OO.
Infix "+" := plus : OO_scope.
#[ global ] Instance mult (alpha beta : OO) : OO.
Infix "×" := mult : OO_scope.
#[ global ] Instance phi0 (i : nat): OO.
Notation "'omega^'" := phi0 (only parsing) : OO_scope.
Infix "×" := mult : OO_scope.
#[ global ] Instance embed (alpha: OO) : E0.E0.
Lemma lt_embed (alpha beta : OO): lt alpha beta →
E0lt (embed alpha) (embed beta).
#[ global ] Instance oo_str : StrictOrder lt.
Qed.
Lemma nf_proof_unicity :
∀ (alpha:t) (H H': nf alpha), H = H'.
Lemma OO_eq_intro : ∀ alpha beta : OO,
data alpha = data beta → alpha = beta.
#[ global ] Instance OO_comp : Comparable lt compare.
Lemma lt_wf : well_founded lt.
Import ON_Generic.
#[ global ] Instance ON_OO : ON lt compare.
End OO.
Import OO.
#[local] Open Scope OO_scope.
Check phi0 7.
#[global] Coercion Fin : nat >-> OO.
Example Ex42: omega + 42 + omega^ 2 = omega^ 2. Qed.