Library hydras.OrdinalNotations.ON_Finite

From Coq Require Import Arith Relations Lia Logic.Eqdep_dec Ensembles
        Wellfounded.Inverse_Image Wellfounded.Inclusion
        RelationClasses.
From hydras Require Import ON_Generic.

From Coq Require Wf_nat.

Coercion is_true: bool >-> Sortclass.


Definition t (n:nat) := {i:nat | Nat.ltb i n}.

Definition lt {n:nat} : relation (t n) :=
  fun alpha beta ⇒ Nat.ltb (proj1_sig alpha) (proj1_sig beta).


Open Scope ON_scope.


Lemma t0_empty (alpha: t 0): False.


Definition bad : t 10. Abort.


#[global] Instance compare_fin {n:nat} : Compare (t n) :=
  fun (alpha beta : t n) ⇒ Nat.compare (proj1_sig alpha) (proj1_sig beta).

Lemma compare_correct {n} (alpha beta : t n) :
  CompSpec eq lt alpha beta (compare alpha beta).

Lemma compare_reflect {n:nat} (alpha beta : t n) :
  match (compare alpha beta)
  with
    Lt ⇒ lt alpha beta
  | Eq ⇒ alpha = beta
  | Gt ⇒ lt beta alpha
  end.


Lemma lt_wf (n:nat) : well_founded (@lt n).

#[global] Instance sto n : StrictOrder (@lt n).

#[global] Instance comp n: Comparable (@lt n) compare.
#[global] Instance FinOrd n : ON (@lt n) compare.

Definition Zero_limit_succ_dec (n:nat) : ZeroLimitSucc_dec (on := FinOrd n).

Lemma sig_eq_intro {n:nat} (x y : t n) :
  proj1_sig x = proj1_sig y → x = y.


Section Inclusion_ij.

  Variables i j : nat.
  Hypothesis Hij : i < j.

  Remark Ltb_ij : Nat.ltb i j.


  #[program] Definition iota_ij (alpha: t i) : t j := alpha.


   Let b : t j := exist _ i Ltb_ij.

  #[global]
   Instance F_incl_ij: SubON (FinOrd i) (FinOrd j) b iota_ij.

  Lemma iota_compare_commute alpha beta:
    compare alpha beta =
    compare (iota_ij alpha) (iota_ij beta).

  Lemma iota_mono : ∀ alpha beta,
      lt alpha beta ↔
      lt (iota_ij alpha) (iota_ij beta).

End Inclusion_ij.

Arguments iota_ij {i j}.


Program Example alpha1 : t 7 := 2.

Program Example beta1 : t 7 := 5.

Example i1 : lt alpha1 beta1.


Program Example gamma1 : t 8 := 7.



Example i2 : lt (iota_ij (le_n 8) alpha1) gamma1.

Example Ex1 : In (bigO beta1) alpha1.