Library hydras.OrdinalNotations.ON_Generic
Pierre Castéran, Univ. Bordeaux and LaBRI
This module defines a type class of ordinal notations, i.e._, data types
with a well-founded strict order and a compare function
From Coq Require Import RelationClasses Relation_Operators Ensembles.
From hydras Require Import OrdNotations Schutte_basics.
From Coq Require Export Wellfounded.Inverse_Image Wellfounded.Inclusion.
Import Relation_Definitions.
From hydras Require Export MoreOrders.
From hydras Require Export Comparable.
Generalizable All Variables.
Declare Scope ON_scope.
Delimit Scope ON_scope with on.
#[local] Open Scope ON_scope.
Ordinal notation system on type A :
Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
{
ON_comp :> Comparable lt cmp;
ON_wf : well_founded lt;
}.
#[global] Existing Instance ON_comp.
Coercion ON_wf : ON >-> well_founded.
Definition rep {A:Type} {lt: relation A} {cmp: Compare A}
(on : ON lt cmp) := A.
#[global] Coercion rep : ON >-> Sortclass.
Section Definitions.
Context {A:Type} {lt : relation A} {cmp : Compare A} {on: ON lt cmp}.
#[using="All"] Definition ON_t := A.
#[using="All"] Definition ON_compare : A → A → comparison := compare.
#[using="All"] Definition ON_lt := lt.
#[using="All"] Definition ON_le: relation A := leq lt.
#[using="All"]
Definition measure_lt {B : Type} (m : B → A) : relation B :=
fun x y ⇒ ON_lt (m x) (m y).
#[using="All"]
Lemma wf_measure {B : Type} (m : B → A) :
well_founded (measure_lt m).
#[using="All"]
Definition ZeroLimitSucc_dec :=
∀ alpha,
{Least alpha} +
{Limit alpha} +
{beta: A | Successor alpha beta}.
The segment called O alpha in Schutte's book
#[using="All"]
Definition bigO (a: A) : Ensemble A := fun x: A ⇒ lt x a.
End Definitions.
Infix "o<" := ON_lt : ON_scope.
Infix "o<=" := ON_le : ON_scope.
Infix "o?=" := ON_compare (at level 70) : ON_scope.
#[global] Hint Resolve wf_measure : core.
The segment associated with nA is isomorphic to
the segment of ordinals strictly less than b
Class SubON
`(OA: @ON A ltA compareA)
`(OB: @ON B ltB compareB)
(alpha: B) (iota: A → B):=
{
SubON_compare: ∀ x y : A,
compareB (iota x) (iota y) = compareA x y;
SubON_incl : ∀ x, ltB (iota x) alpha;
SubON_onto : ∀ y, ltB y alpha → ∃ x:A, iota x = y}.
OA and OB are order-isomporphic
Class ON_Iso
`(OA : @ON A ltA compareA)
`(OB : @ON B ltB compareB)
(f : A → B) (g : B → A):=
{
iso_compare :∀ x y : A,
compareB (f x) (f y) = compareA x y;
iso_inv1 : ∀ a, g (f a)= a;
iso_inv2 : ∀ b, f (g b) = b
}.
OA is an ordinal notation for alpha (in Schutte's model)
Class ON_correct `(alpha : Ord)
`(OA : @ON A ltA compareA)
(iota : A → Ord) :=
{ ON_correct_inj : ∀ a, lt (iota a) alpha;
ON_correct_onto : ∀ beta, lt beta alpha →
∃ b, iota b = beta;
On_compare_spec : ∀ a b:A,
match compareA a b with
| Datatypes.Lt ⇒ lt (iota a) (iota b)
| Datatypes.Eq ⇒ iota a = iota b
| Datatypes.Gt ⇒ lt (iota b) (iota a)
end
}.
Definition SubON_same_cst `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{iota : A → B}
{alpha: B}
{_ : SubON OA OB alpha iota}
(a : A)
(b : B)
:= iota a = b.
Definition SubON_same_fun `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{iota : A → B}
{alpha: B}
{_ : SubON OA OB alpha iota}
(f : A → A)
(g : B → B)
:= ∀ x, iota (f x) = g (iota x).
Definition SubON_same_op `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{iota : A → B} {alpha: B}
{_ : SubON OA OB alpha iota}
(f : A → A → A)
(g : B → B → B)
:= ∀ x y, iota (f x y) = g (iota x) (iota y).
Correctness w.r.t. Schutte's model
Definition ON_cst_ok {alpha: Ord} `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{iota : A → Ord}
{_ : ON_correct alpha OA iota}
(a: A)
(b: Ord)
:= iota a = b.
Definition ON_fun_ok {alpha: Ord} `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{iota : A → Ord}
{_ : ON_correct alpha OA iota}
(f : A → A)
(g : Ord → Ord)
:=
∀ x, iota (f x) = g (iota x).
Definition ON_op_ok {alpha: Ord} `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{iota : A → Ord}
{_ : ON_correct alpha OA iota}
(f : A → A → A)
(g : Ord → Ord → Ord)
:=
∀ x y, iota (f x y) = g (iota x) (iota y).
Definition Iso_same_cst `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{f : A → B} {g : B → A}
{_ : ON_Iso OA OB f g}
(a : A)
(b : B)
:= f a = b.
Definition Iso_same_fun `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{f : A → B} {g : B → A}
{_ : ON_Iso OA OB f g}
(fA : A → A)
(fB : B → B)
:=
∀ x, f (fA x) = fB (f x).
Definition Iso_same_op `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
{f : A → B} {g : B → A}
{_ : ON_Iso OA OB f g}
(opA : A → A → A)
(opB : B → B → B)
:=
∀ x y, f (opA x y) = opB (f x) (f y).
Section SubON_properties.
Context `{OA : @ON A ltA compareA}
`{OB : @ON B ltB compareB}
(f : A → B)
(alpha : B)
(Su : SubON OA OB alpha f).
Lemma SubON_mono a b : ltA a b ↔ ltB (f a) (f b).
Lemma SubON_inj : ∀ a b, f a = f b → a = b.
Lemma SubON_successor : ∀ a b, Successor a b ↔ Successor (f a) (f b).
Lemma SubON_limit : ∀ a , Limit a ↔ Limit (f a).
Lemma SubON_least : ∀ a , Least a ↔ Least (f a).
End SubON_properties.