Library hydras.OrdinalNotations.ON_O
Ordinal Notation for a segment O alpha Pierre Castéran, Unviv. Bordeaux and LaBRI
From Coq Require Import Arith Relations Lia Logic.Eqdep_dec Ensembles
Wellfounded.Inverse_Image Wellfounded.Inclusion
RelationClasses.
From hydras Require Import ON_Generic.
Coercion is_true: bool >-> Sortclass.
Generalizable Variables A Lt comp.
Section OA_given.
Context {A:Type}
{Lt Le: relation A}
{cmpA: Compare A}
(OA : ON Lt cmpA).
The type of ordinals less than a
Definition t (a:A) := {b:A | compare b a = Datatypes.Lt}.
Definition lt {a:A} : relation (t a) :=
fun alpha beta ⇒ ON_lt (proj1_sig alpha) (proj1_sig beta).
Definition le {a:A} : relation (t a) :=
clos_refl (t a) lt.
#[global]
Instance compare_O {a:A} : Compare (t a) :=
fun (alpha beta : t a) ⇒
compare (proj1_sig alpha) (proj1_sig beta).
Lemma compare_correct {a} (alpha beta : t a) :
CompSpec eq lt alpha beta (compare alpha beta).
Lemma compare_reflect {a:A} (alpha beta : t a) :
match (compare alpha beta)
with
Datatypes.Lt ⇒ lt alpha beta
| Eq ⇒ alpha = beta
| Gt ⇒ lt beta alpha
end.
Lemma lt_wf (a:A) : well_founded (@lt a).
#[global] Instance sto a : StrictOrder (@lt a).
#[global] Instance ON_O_comp (a:A) : Comparable (@lt a) compare .
We have now an ordinal notation