Library schutte.Well_Orders

Add LoadPath "../prelude".
Add LoadPath "../hilbert".
Add LoadPath "../denumerable".

Require Import Relations.
Require Import Classical.
Require Import Classical_sets.
Require Import PartialFun.

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

Set Implicit Arguments.
Hint Unfold In.

Section least_member_def.
  Variables (M:Type)
             (D: Ensemble M)
             (Lt:M->M->Prop).

Definition is_least_member(X:Ensemble M)(a:M) :=
   In D a /\ In X a /\ forall x, In D x -> In X x -> x=a \/ Lt a x.
End least_member_def.

Record WO: Type:= {
 M:Set;  Lt : relation M;
 D : Ensemble M ;
 Lt_inc_D1 : forall x y, Lt x y -> In D x;
 Lt_inc_D2 : forall x y, Lt x y -> In D y;
 Lt_trans : transitive _ Lt;
 Lt_irreflexive : forall a:M, ~ (Lt a a);
 well_order : forall (M0:Ensemble M)(a:M),In D a -> In M0 a ->
                                   exists a0:M, is_least_member D Lt M0 a0
}.

Hint Resolve Lt_inc_D1 Lt_inc_D2.

Section About_WO.

 Variable Wo : WO.

 Let M := M Wo.
 Let Lt := Lt Wo.
 Let D := D Wo.
 Definition Le (a b:M) := (In D a /\ a = b) \/ Lt a b.

 Lemma Lt_connect : forall a b, In D a -> In D b -> Lt a b \/ a = b \/ Lt b a.
 Proof.
  intros. generalize (well_order Wo (fun z => z=a \/ z=b) a H).
  destruct 1.
 red.
 auto.
 case H1.
 destruct 2.
 case H3.
 intro;subst x.
 case (H4 b H0).
 red;auto.
 auto.
 auto.
 intro;subst x.
 case (H4 a H).
 red;auto.
 auto.
 auto.
Qed.

 Lemma Le_refl : forall x, In D x -> Le x x.
 Proof.
  red;unfold Le;auto.
 Qed.

 Lemma Le_antisym : forall a b, Le a b -> Le b a -> a = b.
 Proof.
  intros a b H H'; case H; case H';auto.
  tauto.
 tauto.
 destruct 1;auto.
  intros;case (Lt_irreflexive Wo a).
  eapply (Lt_trans Wo);eauto.
 Qed.

 Lemma Le_trans : transitive _ Le.
 Proof.
  unfold transitive, Le;intros.
  case H;case H0.
  intuition.
  left;intuition.
  transitivity y;auto.
  left;split.
  auto.
 transitivity y;auto.
 left;split.
  auto.
 transitivity y;auto.
  right;apply (Lt_trans Wo) with y;eauto.
  intros H1 (H2,H3).
 right;subst x;auto.
  intros (H1,H2) H3.
 right ; subst y; auto.
  right;apply (Lt_trans Wo) with y;eauto.
Qed.

 Lemma Le_Lt_trans : forall x y z, Le x y -> Lt y z -> Lt x z.
 Proof.
  intros x y z Hxy Hyz.
  case Hxy;intros.
  case H;intros.
  subst y;auto.
  eapply (Lt_trans Wo);eauto.
 Qed.

 Lemma Lt_Le_trans : forall x y z, Lt x y -> Le y z -> Lt x z.
 Proof.
  intros x y z Hxy Hyz.
  case Hyz;intros.
 case H;intros.
  subst y;auto.
  eapply (Lt_trans Wo);eauto.
 Qed.

 Lemma Lt_not_Gt : forall x y, Lt x y -> ~ Lt y x.
 Proof.
  intros x y H H'; case (Lt_irreflexive Wo x).
  eapply (Lt_trans Wo); eauto.
 Qed.

 Lemma least_member_lower_bound : forall X a,
   is_least_member D Lt X a -> forall b, In X b -> In D b -> Le a b.
 Proof.
  intros X a H; case H.
  unfold In; intuition.
  unfold Le; case (H3 _ H4 H1);auto.
 Qed.

 Lemma least_member_glb :
   forall X a,
   is_least_member D Lt X a ->
     forall b, (forall c, In X c -> In D c -> Le b c) ->
               Le b a.
 Proof.
   intros.
   case H;intros H1 (H2,_).
  apply H0; auto.
 Qed.



 Theorem least_member_unicity : forall X a b,
    is_least_member D Lt X a -> is_least_member D Lt X b -> a = b.
 Proof.
  intros.
  case H;case H0;intros.
  apply Le_antisym;auto.
  case H2;intros H5 H6.
  case H4;intros H7 H8.
  unfold Le.
  case (H8 b H1 H5);auto.
  unfold Le.
  case H2;intros H5 H6.
  case H4;intros H7 H8.
  case (H6 a H3 H7);auto.
 Qed.

 Theorem least_member_of_eq : forall (X Y : Ensemble M) a b ,
    Included X Y -> Included Y X ->
      is_least_member D Lt X a -> is_least_member D Lt Y b -> a = b.
 Proof.
  intros.
 case H1;case H2;intros.
  apply Le_antisym;auto.
  case H4;intros H7 H8.
 case H6;intros H9 H10.
 case (H10 b H3).
 auto.
 unfold Le.
 left;split;auto.
 right;auto.
  case H4;intros H7 H8.
 case H6;intros H9 H10.
 case (H8 a H5).
 auto.
 unfold Le;auto.
 right;auto.
Qed.


Section restriction.

 Variable a : M.
 Hypothesis Ha : D a.

 Definition D_a x := In D x /\ Lt x a.
 Definition lt_a := fun x => In D x /\ Lt x a.
 Definition Lt_a := fun x y => Lt x a /\ Lt y a /\ Lt x y.

 Remark Lta_inc_D1 : forall x y, Lt_a x y -> D_a x.
 Proof.
  unfold D_a;intros.
  case H.
  split;auto.
  apply (Lt_inc_D1 Wo _ _ H0);auto.
 Qed.

 Remark Lta_inc_D2 : forall x y, Lt_a x y -> D_a y.
 Proof.
  unfold D_a;intros.
  case H.
  split;try tauto.
  case H1;intros _ H2;apply (Lt_inc_D2 Wo _ _ H2);auto.
 Qed.

 Remark Lta_irr : forall x, ~ Lt_a x x.
 Proof.
  unfold Lt_a; intros x Hx.
  case (Lt_irreflexive Wo x); try tauto.
Qed.

Remark Lta_trans : transitive _ Lt_a.
Proof.
 unfold transitive, Lt_a.
 repeat split; try tauto.
 apply (Lt_trans Wo ) with y;eauto.
 tauto.
 tauto.
Qed.

Remark Lta_connect : forall x y, D_a x -> D_a y ->
                       Lt_a x y \/ x = y \/ Lt_a y x.
Proof.
 intros.
 case H;case H0;intros.
 case (Lt_connect x y H3 H1).
 left;unfold Lt_a;auto.
 destruct 1.
 auto.
 right;right;unfold Lt_a;auto.
Qed.

Remark well_order_a : forall (M0:M->Prop)(m:M),
                        D_a m -> M0 m ->
                        exists a0:M, is_least_member D_a Lt_a M0 a0.
Proof.
 intros.
 case (well_order Wo (fun y => M0 y /\ Lt y a) m).
 case H;auto.
 case H;auto.
 intros.
 case (Lt_connect x a).
 case H1.
 intros.
 auto.
 auto.


 exists x.
 repeat split;auto.
 case H1;auto.
 unfold is_least_member in H1;decompose [and] H1.
 case H5.
 auto.

 destruct 1.
 intro.
 unfold is_least_member in H1;decompose [and] H1.
  clear H1.
 case (H9 x0 H3).
 red.
 split;auto.
 auto.
 right.
 red.
 auto.
 destruct 1.
 subst x.
 unfold is_least_member in H1;decompose [and] H1.
 case (Lt_irreflexive Wo a);auto.
 case (Lt_irreflexive Wo a).
 case H4;auto.
case (Lt_irreflexive Wo a).
 apply Lt_Le_trans with x.
 auto.
unfold is_least_member in H1;decompose [and] H1.
 right.
 case H5;auto.
Qed.

Definition restrict : WO.
 split with (M:=M)(Lt:=Lt_a)(D:=D_a).
 apply Lta_inc_D1.
 apply Lta_inc_D2.
 apply Lta_trans.
 apply Lta_irr.
 apply well_order_a.
Defined.

End restriction.

End About_WO.

Section isotonicity_def.
 Variables M1 M2:WO.

 Section f_fixed.

 Variable f : (M M1) -> (M M2) -> Prop.
 Definition rel_mono := forall a1 b1 a2 b2, D M1 a1 -> D M1 b1 ->
      f a1 a2 -> f b1 b2 -> Lt M1 a1 b1 -> Lt M2 a2 b2.
 Definition rel_isotonic := rel_domain (D M1) f/\
                          rel_functional (D M1) f /\
                          rel_onto (D M1) (D M2) f/\
                          rel_codomain (D M1) (D M2) f /\
                          rel_mono.

 Lemma iso_inj : rel_isotonic -> rel_inj (D M1) f.
  unfold rel_inj, rel_isotonic;intro H;decompose [and] H.
  intros.
  case (Lt_connect M1 a a').
  auto.
  auto.
  intro; case (Lt_irreflexive M2 b).
  apply H5 with (a1:=a)(b1:=a');auto.
  destruct 1;auto.
  case (Lt_irreflexive M2 b).
  apply H5 with (a1:=a')(b1:=a);auto.
 Qed.

End f_fixed.

Definition isotonic := exists f, rel_isotonic f.

End isotonicity_def.

Theorem isotonicity_refl : reflexive _ isotonic.
Proof.
 unfold isotonic, reflexive; intros.
 exists (fun (z z':M x) => z=z').
 unfold rel_isotonic.
 repeat split.
 unfold rel_domain;intros.
 exists a;auto.
 unfold rel_functional;intros.
 subst b;auto.
 unfold rel_onto;intros.
 exists b;auto.
 unfold rel_codomain;intros.
 subst b;auto.
 unfold rel_mono;intros.
 subst a2;subst b2;auto.
Qed.

Theorem isotonicity_sym : symmetric _ isotonic.
Proof.
 unfold isotonic, symmetric; intros.
 case H;intros f Hf.
 exists (fun z z' => D x z' /\ f z' z).
 unfold rel_isotonic in Hf;decompose [and] Hf.
 unfold rel_isotonic.
 repeat split.
 unfold rel_domain;intros.
 case (H1 _ H4).
 intros x0 H';exists x0;auto.
 unfold rel_functional;intros.
 generalize (iso_inj (f:=f)); unfold rel_inj; intro Inj.
 eapply Inj.
 split; auto.
 tauto.
 tauto.
 instantiate (1:=a).
 tauto.
 tauto.
 unfold rel_onto.
 intros.
 case (H0 b).
 auto.
 intro x0;exists x0.
 generalize (H3 b x0).
 tauto.
 unfold rel_codomain;intros.
 tauto.
 unfold rel_mono;intros.
 case (Lt_connect x a2 b2).
 tauto.
 tauto.
 auto.
 destruct 1.
 subst b2.
 replace a1 with b1 in H9.
 case (Lt_irreflexive y b1);auto.
 eapply (H2 a2 b1 a1).
 tauto.
 tauto.
 tauto.
 assert (Lt y b1 a1).
 eapply (H5 b2 a2).
 tauto.
 tauto.
 tauto.
 tauto.
 auto.
 case (Lt_irreflexive y a1).
 eapply (Lt_trans y);eauto.
Qed.


Theorem isotonicity_trans : transitive _ isotonic.
Proof.
 unfold isotonic, transitive; intros.
 case H;intros f Hf.
 case H0;intros f' Hf'.
 exists (fun z z'' => D x z /\ (exists z', f z z' /\ f' z' z'')).
 unfold rel_isotonic in Hf;decompose [and] Hf.
 unfold rel_isotonic in Hf';decompose [and] Hf'.
 unfold rel_isotonic.
 repeat split.
 unfold rel_domain;intros.
 case (H1 _ H10).
 intros x0 H'.
 case (H5 x0).
 apply (H4 a).
 auto.
 auto.
 intros.
 exists x1.
 split.
 auto.
 exists x0;auto.
 unfold rel_functional;intros.
 case H12;intros.
 case H13;intros.
 case H15;intros;case H17;intros.
 assert (x0=x1).
 apply (H3 a x0 x1).
 auto.
 tauto.
 tauto.
 subst x1.
 apply (H8 x0 b b').
 apply (H4 a).
 auto.
 tauto.
 tauto.
 tauto.
 unfold rel_onto.
 intros.
 case (H7 b).
 auto.
 intros x0 (H12,H13).
 case (H2 x0).
 auto.
 intros x1 (H14,H15).
 exists x1.
 repeat split;auto.
 exists x0;auto.
 unfold rel_codomain;intros.
 case H12;intros H13 (z',(H14,H15)).
 apply (H9 z');auto.
 apply (H4 a);auto.
 unfold rel_mono;intros.
 case H13;intros H16 (z',(H17,H18)).
 case H14;intros H19 (z'',(H20,H21)).
 apply (H11 z' z'').
 apply (H4 a1);auto.
 apply (H4 b1);auto.
 auto.
 auto.
 apply (H6 a1 b1);auto.
Qed.

Inductive WO_lt (W W1:WO) : Prop :=
WO_lt_i: forall a (H:D W1 a), isotonic W (restrict W1 a H) ->
  WO_lt W W1.