Library hydras.OrdinalNotations.ON_plus

From Coq Require Import Arith Compare_dec Lia
     Relation_Operators RelationClasses Disjoint_Union.
From hydras Require Import ON_Generic MoreOrders.

Import Relations.
Generalizable All Variables.
Coercion is_true: bool >-> Sortclass.

Section Defs.

  Context `(ltA: relation A)
          (cmpA : Compare A)
          (NA: ON ltA cmpA).
  Context `(ltB: relation B)
          (cmpB : Compare B)
          (NB: ON ltB cmpB).

  Definition t := (A + B)%type.
  Arguments inl {A B} _.
  Arguments inr {A B} _.

  Definition lt : relation t := le_AsB _ _ ltA ltB.

#[global] Instance compare_plus : Compare t :=
fun (alpha beta: t) ⇒
   match alpha, beta with
     inl _, inr _ ⇒ Lt
   | inl a, inl a' ⇒ compare a a'
   | inr b, inr b' ⇒ compare b b'
   | inr _, inl _ ⇒ Gt
  end.

Definition le := clos_refl _ lt.

#[local] Hint Unfold lt le : core.
#[local] Hint Constructors le_AsB: core.

Instance lt_strorder : StrictOrder lt.

Lemma compare_reflect alpha beta :
  match (compare alpha beta)
  with
    Lt ⇒ lt alpha beta
  | Eq ⇒ alpha = beta
  | Gt ⇒ lt beta alpha
  end.


Lemma compare_correct alpha beta :
    CompSpec eq lt alpha beta (compare alpha beta).

#[global] Instance plus_comp : Comparable lt compare_plus.



Lemma lt_wf : well_founded lt.





#[global] Instance ON_plus : ON lt compare_plus.



Lemma lt_eq_lt_dec alpha beta :
  {lt alpha beta} + {alpha = beta} + {lt beta alpha}.

End Defs.

Arguments lt_eq_lt_dec {A ltA cmpA} _ {B ltB cmpB} _.
Arguments ON_plus {A ltA cmpA} _ {B ltB cmpB}.