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.