Library gaia_hydras.onType
Ordinal Notations (Experimental !!!!) Warning: This file is a draft !!! We try to adapt to Gaia the ON class of ordinal notations
(defined as a naïve (pre Stdpp) type class).
An Ordinal Notation is just a well-founded ordered type, with
a trichotomic comparison
Notions of ordinal arithmetics should be defined in substructures
From mathcomp Require Import all_ssreflect zify.
From mathcomp Require Import fintype.
From Coq Require Import Logic.Eqdep_dec.
From Coq Require Import Wellfounded.Inclusion Wf_nat Inverse_Image.
Set Implicit Arguments.
Section MoreOrderType.
Variable disp: unit.
Variable T: orderType disp.
Definition limit_v2 (f: nat → T)(x: T) :=
(∀ (n:nat), (f n < x)%O) ∧
(∀ y : T, (y < x)%O → ∃ n : nat, (y ≤ f n)%O).
Definition limit_of (f: nat → T) x :=
(∀ n m : nat, (n < m)%nat → (f n < f m)%O) ∧ limit_v2 f x.
Definition is_successor_of (x y: T):=
(x < y)%O ∧ ∀ z, (x < z)%O → ~~ (z < y)%O.
Section Succ_no_limit.
Variables (x y: T) (s: nat → T).
Hypothesis Hsucc : is_successor_of x y.
Hypothesis Hlim : limit_of s y.
Remark R0: ∃ (n:nat), (x ≤ (s n))%O.
Remark R1: ∃ z, (x < z < y)%O.
Lemma F: False.
End Succ_no_limit.
End MoreOrderType.
Type for ordinal notations
Module ONDef.
Record mixin_of disp (T: orderType disp) :=
Mixin {
_ : @well_founded T <%O;
}.
Section Packing.
Variable disp: unit.
Structure pack_type : Type :=
Pack{ type: orderType disp; _ : mixin_of type}.
Variable cT: pack_type.
Definition on_struct: mixin_of cT :=
let: Pack _ c := cT return mixin_of cT in c.
End Packing.
Module Exports.
Notation on := (pack_type ).
Notation ONMixin := Mixin.
Notation ON T m := (@Pack T m).
Coercion type : pack_type >-> orderType.
Section Lemmas.
Variable disp: unit.
Variable U: @on disp.
Definition tricho (a b: U) := if (a == b)%O then Eq
else if (a < b)%O then Lt
else Gt.
Lemma trichoP (a b: U) :
CompareSpec (a == b) (a < b)%O (b < a)%O (tricho a b).
Lemma wf : @well_founded U <%O.
End Lemmas.
End Exports.
End ONDef.
Export ONDef.Exports.
Lemma wf_ltn: well_founded (fun n ⇒ [eta ltn n]).
Section onFiniteDef.
Variable i: nat.
Lemma I_i_wf: @well_founded 'I_i (<%O).
Definition onFiniteMixin := ONMixin I_i_wf.
Canonical onFiniteType := ON _ _ onFiniteMixin.
End onFiniteDef.
Tests
Definition O12_33: onFiniteType 33.
by exists 12.
Defined.
Compute tricho O12_33 O12_33.
Goal (O12_33 <= O12_33)
An ordinal notation for omega
Section onOmegaDef.
Lemma omega_lt_wf : @well_founded Order.NatOrder.orderType <%O.
Definition onOmegaMixin := ONMixin omega_lt_wf.
Canonical onOmegaType := ON _ _ onOmegaMixin.
End onOmegaDef.
Example om12 : onOmegaType := 12.
Example om67 : onOmegaType := 67.
To do : Notation for epsilon0