Library hydras.Schutte.Well_Orders

From Coq Require Import Relations Classical Classical_sets RelationClasses
     Wf_nat.

From hydras Require Import PartialFun.
Import MoreEpsilonIota.

Arguments In [U].
Arguments Included [U].

Set Implicit Arguments.
#[global] Hint Unfold In : core.

Section the_context.

  Variables (M:Type)
            (Lt : relation M).

  Definition Le (a b:M) := a = b ∨ Lt a b.

  Definition least_member (X:Ensemble M) (a:M) :=
    In X a ∧ ∀ x, In X x → Le a x.

  Definition least_fixpoint (f : M → M) (x:M) :=
    f x = x ∧ ∀ y: M, f y = y → Le x y.

  Class WO : Type:=
    {
    Lt_trans : Transitive Lt;
    Lt_irreflexive : ∀ a:M, ¬ Lt a a;
    well_order : ∀ (X:Ensemble M)(a:M),
        In X a →
        ∃ a0:M, least_member X a0
    }.


  Section About_WO.
    Context (Wo : WO).

    Lemma Lt_connect : ∀ a b, Lt a b ∨ a = b ∨ Lt b a.

    Lemma Le_refl : ∀ x:M, Le x x.

    Lemma Le_antisym : ∀ a b, Le a b → Le b a → a = b.

    #[global] Instance Le_trans : Transitive Le.

    Lemma Le_Lt_trans : ∀ x y z, Le x y → Lt y z → Lt x z.

    Lemma Lt_Le_trans : ∀ x y z, Lt x y → Le y z → Lt x z.

    Lemma Lt_not_Gt : ∀ x y, Lt x y → ¬ Lt y x.

    Lemma least_member_lower_bound : ∀ X a,
        least_member X a → ∀ b, In X b → Le a b.

    Lemma least_member_glb :
      ∀ X a,
        least_member X a →
        ∀ b, (∀ c, In X c → Le b c) →
                  Le b a.

    Theorem least_member_unicity : ∀ X a b,
        least_member X a → least_member X b → a = b.

    Theorem least_member_ex_unique :
      ∀ X x
               (inhX: In X x),
      ∃! a, least_member X a.

    Theorem least_member_of_eq : ∀ (X Y : Ensemble M) a b ,
        Included X Y → Included Y X →
        least_member X a →
        least_member Y b →
        a = b.

  End About_WO.

End the_context.


Definition the_least {M: Type} {Lt}
           {inh : InH M} {WO: WO Lt} (X: Ensemble M) : M :=
  the (least_member Lt X ).


Lemma the_least_unicity {M: Type} {Lt}
       {inh : InH M} {WO: WO Lt} (X: Ensemble M)
       (HX: Inhabited X)
  : ∃! l , least_member Lt X l.

#[ global ] Instance WO_nat : WO Peano.lt.
Qed.